Document Open Access Logo

Temporal Logics with Local Constraints (Invited Talk)

Authors Claudia Carapelle, Markus Lohrey

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.2.pdf
  • Filesize: 499 kB
  • 12 pages

Document Identifiers

Author Details

Claudia Carapelle
Markus Lohrey

Cite As Get BibTex

Claudia Carapelle and Markus Lohrey. Temporal Logics with Local Constraints (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 2-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.2

Abstract

Recent decidability results on the satisfiability problem for temporal logics, in particular LTL, CTL* and ECTL*, with constraints over external structures like the integers with the order or infinite trees are surveyed in this paper.

Subject Classification

Keywords
  • Temporal logics with constraints
  • concrete domains
  • LTL
  • CTL*
  • ECTL*

Metrics

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

References

  1. Rajeev Alur and Thomas A. Henzinger. A really temporal logic. In Proceedings of the 30th Annual Symposium on Foundations of Computer Science (FOCS 1989), pages 164-169. IEEE Computer Society Press, 1989. Google Scholar
  2. Rajeev Alur and Thomas A. Henzinger. Real-time logics: complexity and expressiveness. Information and Computation, 104:390-401, 1993. Google Scholar
  3. Franz Baader and Philipp Hanschke. A scheme for integrating concrete domains into concept languages. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI 1991), volume 1, pages 452-457. Morgan Kaufmann, 1991. Google Scholar
  4. Philippe Balbiani and Jean-François Condotta. Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In Proceedings of the 4th International Workshop on Frontiers of Combining Systems (FroCos 2002), volume 2309 of Lecture Notes in Computer Science, pages 162-176. Springer, 2002. Google Scholar
  5. M. Bojańczyk and S. Toruńczyk. Weak MSO+U over infinite trees. In Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012), volume 14 of Leibniz International Proceedings in Informatics (LIPIcs), pages 648-660. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  6. Laura Bozzelli and Régis Gascon. Branching-time temporal logic extended with qualitative presburger constraints. In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), volume 4246 of Lecture Notes in Computer Science, pages 197-211. Springer, 2006. Google Scholar
  7. Laura Bozzelli and Sophie Pinchinat. Verification of gap-order constraint abstractions of counter systems. Theoretical Computer Science, 523:1-36, 2014. Google Scholar
  8. Claudia Carapelle. On the Satisfiability of Temporal Logics with Concrete Domains. PhD thesis, University of Leipzig, 2015. submitted. Google Scholar
  9. Claudia Carapelle, Shiguang Feng, Oliver Fernández Gil, and Karin Quaas. Satisfiability for MTL and TPTL over Non-monotonic Data Words. In Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA 2014), volume 8370 of Lecture Notes in Computer Science. Springer, 2014. Google Scholar
  10. Claudia Carapelle, Shiguang Feng, Alexander Kartzow, and Markus Lohrey. Satisfiability of ECTL* with Tree Constraints. In Proceedings of the 10th International Computer Science Symposium in Russia (CSR 2015), volume 9139 of Lecture Notes in Computer Science, pages 94-108. Springer, 2015. Google Scholar
  11. Claudia Carapelle, Alexander Kartzow, and Markus Lohrey. Satisfiability of CTL* with Constraints. In Proceedings of the 24th International Conference on Concurrency Theory (CONCUR 2013), volume 8052 of Lecture Notes in Computer Science, pages 455-469. Springer, 2013. Google Scholar
  12. Claudia Carapelle, Alexander Kartzow, and Markus Lohrey. Satisfiability of ECTL* with Constraints, 2015. submitted for publication, URL: http://www.eti.uni-siegen.de/ti/veroeffentlichungen/ectl-with-constraints.pdf.
  13. Karlis Cerans. Deciding properties of integral relational automata. In Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP 1994), volume 820 of Lecture Notes in Computer Science, pages 35-46. Springer-Verlag, 1994. Google Scholar
  14. Stéphane Demri and Morgan Deters. Temporal logics on strings with prefix relation. Journal of Logic and Computation, 2015. to appear. Google Scholar
  15. Stéphane Demri and Deepak D'Souza. An automata-theoretic approach to constraint LTL. Information and Computation, 205(3):380-415, 2007. Google Scholar
  16. Stéphane Demri and Régis Gascon. Verification of qualitative Z constraints. Theoretical Computer Science, 409(1):24-40, 2008. Google Scholar
  17. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic, 10(3):16:1-16:30, 2009. Google Scholar
  18. E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs. SIAM Journal on Computing, 29(1):132-158, 1999. Google Scholar
  19. Shigunag Feng, Markus Lohrey, and Karin Quaas. Path-checking for MTL and TPTL over data words. In Proceedings of the 19th International Conference on Developments in Language Theory (DL 2015), 2015. to appear. Google Scholar
  20. Régis Gascon. An automata-based approach for CTL* with constraints. Electronic Notes in Theoretical Computer Science, 239:193-211, 2009. Google Scholar
  21. Alexander Kartzow and Thomas Weidner. Model checking constraint LTL over trees. Technical report, arxiv.org, 2015. URL: http://arxiv.org/abs/1504.06105.
  22. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990. Google Scholar
  23. Carsten Lutz. Description logics with concrete domains - a survey. In Advances in Modal Logic 4, pages 265-296. King’s College Publications, 2003. Google Scholar
  24. Carsten Lutz. Combining interval-based temporal reasoning with general TBoxes. Artificial Intelligence, 152(2):235-274, 2004. Google Scholar
  25. Carsten Lutz. NEXP TIME-complete description logics with concrete domains. ACM Transactions on Computational Logic, 5(4):669-705, 2004. Google Scholar
  26. Carsten Lutz and Maja Milicic. A tableau algorithm for description logics with concrete domains and general TBoxes. Journal of Automated Reasoning, 38(1-3):227-259, 2007. Google Scholar
  27. Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), pages 46-57. IEEE Computer Society, 1977. Google Scholar
  28. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. Google Scholar
  29. Wolfgang Thomas. Computation tree logic and regular omega-languages. In REX Workshop, pages 690-713, 1988. Google Scholar
  30. Moshe Y. Vardi and Larry J. Stockmeyer. Improved upper and lower bounds for modal logics of programs: Preliminary report. In Proceedings of the 17th Annual ACM Symposium on Theory of Computing, STOC 1985, pages 240-251. ACM, 1985. Google Scholar
  31. Moshe Y. Vardi and Pierre Wolper. Yet another process logic (preliminary version). In Logic of Programs, pages 501-512, 1983. Google Scholar
  32. Frank Wolter and Michael Zakharyaschev. Spatio-temporal representation and reasoning based on RCC-8. In Proceedings of the 7th Conference on Principles of Knowledge Representation and Reasoning (KR2000), pages 3-14. Morgan Kaufmann, 2000. 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