License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2021.16
URN: urn:nbn:de:0030-drops-147924
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14792/
Go to the corresponding LIPIcs Volume Portal

Chafik, Anasse ; Cheikh-Alili, Fahima ; Condotta, Jean-François ; Varzinczak, Ivan

A One-Pass Tree-Shaped Tableau for Defeasible LTL

pdf-format:
LIPIcs-TIME-2021-16.pdf (0.7 MB)

Abstract

Defeasible Linear Temporal Logic is a defeasible temporal formalism for representing and verifying exception-tolerant systems. It is based on Linear Temporal Logic (LTL) and builds on the preferential approach of Kraus et al. for non-monotonic reasoning, which allows us to formalize and reason with exceptions. In this paper, we tackle the satisfiability checking problem for defeasible LTL. One of the methods for satisfiability checking in LTL is the one-pass tree shaped analytic tableau proposed by Reynolds. We adapt his tableau to defeasible LTL by integrating the preferential semantics to the method. The novelty of this work is in showing how the preferential semantics works in a tableau method for defeasible linear temporal logic. We introduce a sound and complete tableau method for a fragment that can serve as the basis for further exploring tableau methods for this logic.

BibTeX - Entry

@InProceedings{chafik_et_al:LIPIcs.TIME.2021.16,
  author =	{Chafik, Anasse and Cheikh-Alili, Fahima and Condotta, Jean-Fran\c{c}ois and Varzinczak, Ivan},
  title =	{{A One-Pass Tree-Shaped Tableau for Defeasible LTL}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14792},
  URN =		{urn:nbn:de:0030-drops-147924},
  doi =		{10.4230/LIPIcs.TIME.2021.16},
  annote =	{Keywords: Temporal logic, Non-monotonic reasoning, Tableau Calculi}
}

Keywords: Temporal logic, Non-monotonic reasoning, Tableau Calculi
Collection: 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)
Issue Date: 2021
Date of publication: 16.09.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI