Document Open Access Logo

A One-Pass Tree-Shaped Tableau for Defeasible LTL

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

PDF
Thumbnail PDF

File

LIPIcs.TIME.2021.16.pdf
  • Filesize: 0.73 MB
  • 18 pages

Document Identifiers

Author Details

Anasse Chafik
  • CRIL, University of Artois & CNRS, Arras, France
Fahima Cheikh-Alili
  • CRIL, University of Artois & CNRS, Arras, France
Jean-François Condotta
  • CRIL, University of Artois & CNRS, Arras, France
Ivan Varzinczak
  • CRIL, University of Artois & CNRS, Arras, France

Acknowledgements

The open access publication of this article was supported by the Alpen-Adria-Universität Klagenfurt, Austria.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.TIME.2021.16

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Temporal logic
  • Non-monotonic reasoning
  • Tableau Calculi

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Ben-Ari. Mathematical Logic for Computer Science, third edition. Springer, 2012. Google Scholar
  2. K. Britz, T. Meyer, and I. Varzinczak. Preferential reasoning for modal logics. Electronic Notes in Theoretical Computer Science, 278:55-69, 2011. URL: https://doi.org/10.1016/j.entcs.2011.10.006.
  3. K. Britz, T. Meyer, and I. Varzinczak. Semantic foundation for preferential description logics. In AI 2011: Advances in Artificial Intelligence, pages 491-500, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  4. K. Britz and I. Varzinczak. From KLM-style conditionals to defeasible modalities, and back. Journal of Applied Non-Classical Logics, 28(1):92-121, 2018. URL: https://doi.org/10.1080/11663081.2017.1397325.
  5. K. Britz and I. Varzinczak. Preferential tableaux for contextual defeasible ALC. In Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), number 11714 in LNCS, pages 39-57, 2019. Google Scholar
  6. A. Chafik, F. Cheikh Alili, J.-F. Condotta, and I. Varzinczak. On the decidability of a fragment of preferential LTL. In 27th International Symposium on Temporal Representation and Reasoning, TIME 2020, volume 178 of LIPIcs, pages 19:1-19:19, 2020. URL: https://doi.org/10.4230/LIPIcs.TIME.2020.19.
  7. D. M. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings, volume 398 of Lecture Notes in Computer Science, pages 409-448. Springer, 1987. URL: https://doi.org/10.1007/3-540-51803-7_36.
  8. L. Giordano, V. Gliozzi, N. Olivetti, and G.L. Pozzato. Preferential description logics. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), number 4790 in LNAI, pages 257-272. Springer, 2007. Google Scholar
  9. L. Giordano, V. Gliozzi, N. Olivetti, and G.L. Pozzato. Analytic tableaux calculi for KLM logics of nonmonotonic reasoning. ACM Transactions on Computational Logic, 10(3):18:1-18:47, 2009. Google Scholar
  10. Y. Kesten, Z. Manna, H. Mcguire, and A. Pnueli. A decision algorithm for full propositional temporal logic. LNCS, 697, April 1999. Google Scholar
  11. S. Kraus, D. Lehmann, and M. Magidor. Nonmonotonic reasoning, preferential models and cumulative logics. Artificial Intelligence, 44:167-207, 1990. Google Scholar
  12. Z. Manna and A. Pnueli. Temporal verification of reactive systems - safety. Springer, 1995. Google Scholar
  13. A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pages 46-57, October 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  14. M. Reynolds. A new rule for LTL tableaux. Electronic Proceedings in Theoretical Computer Science, 226:287–301, September 2016. URL: https://doi.org/10.4204/eptcs.226.20.
  15. M. Reynolds. A traditional tree-style tableau for LTL, 2016. URL: http://arxiv.org/abs/1604.03962.
  16. K. Y. Rozier and M. Y. Vardi. LTL satisfiability checking. In Model Checking Software, pages 149-167, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  17. S. Schwendimann. A new one-pass tableau calculus for PLTL. In Automated Reasoning with Analytic Tableaux and Related Methods, pages 277-291. Springer Berlin Heidelberg, 1998. Google Scholar
  18. Y. Shoham. A Semantical Approach to Nonmonotonic Logics, page 227–250. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1987. Google Scholar
  19. Y. Shoham. Reasoning about Change: Time and Causation from the Standpoint of Artificial Intelligence. MIT Press, 1988. Google Scholar
  20. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  21. P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
  22. P. Wolper. The tableau method for temporal logic. Logique Et Analyse, 28:110-111, January 1985. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact