DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2021.16

A One-Pass Tree-Shaped Tableau for Defeasible LTL

Authors: Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

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.

Cite as

Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak. A One-Pass Tree-Shaped Tableau for Defeasible LTL. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.TIME.2021.16},
  URN =		{urn:nbn:de:0030-drops-147924},
  doi =		{10.4230/LIPIcs.TIME.2021.16},
  annote =	{Keywords: Temporal logic, Non-monotonic reasoning, Tableau Calculi}
}

Document

DOI: 10.4230/LIPIcs.TIME.2020.19

On the Decidability of a Fragment of preferential LTL

Authors: Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)

Abstract

Linear Temporal Logic (LTL) has found extensive applications in Computer Science and Artificial Intelligence, notably as a formal framework for representing and verifying computer systems that vary over time. Non-monotonic reasoning, on the other hand, allows us to formalize and reason with exceptions and the dynamics of information. The goal of this paper is therefore to enrich temporal formalisms with non-monotonic reasoning features. We do so by investigating a preferential semantics for defeasible LTL along the lines of that extensively studied by Kraus et al. in the propositional case and recently extended to modal and description logics. The main contribution of the paper is a decidability result for a meaningful fragment of preferential LTL that can serve as the basis for further exploration of defeasibility in temporal formalisms.

Cite as

Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak. On the Decidability of a Fragment of preferential LTL. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chafik_et_al:LIPIcs.TIME.2020.19,
  author =	{Chafik, Anasse and Cheikh-Alili, Fahima and Condotta, Jean-Fran\c{c}ois and Varzinczak, Ivan},
  title =	{{On the Decidability of a Fragment of preferential LTL}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.19},
  URN =		{urn:nbn:de:0030-drops-129871},
  doi =		{10.4230/LIPIcs.TIME.2020.19},
  annote =	{Keywords: Knowledge Representation, non-monotonic reasoning, temporal logic}
}

Search Results

Documents authored by Chafik, Anasse

A One-Pass Tree-Shaped Tableau for Defeasible LTL

Abstract

Cite as

On the Decidability of a Fragment of preferential LTL

Abstract

Cite as

Thanks for your feedback!

Could not send message