CTL with Finitely Bounded Semantics

Authors Valentin Goranko, Antti Kuusisto, Raine Rönnholm



PDF
Thumbnail PDF

File

LIPIcs.TIME.2017.14.pdf
  • Filesize: 0.64 MB
  • 19 pages

Document Identifiers

Author Details

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

Cite AsGet BibTex

Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. CTL with Finitely Bounded Semantics. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.TIME.2017.14

Abstract

We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property. We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.
Keywords
  • CTL
  • finitely bounded semantics
  • tableaux
  • decidability

Metrics

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

References

  1. R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. Google Scholar
  2. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Proc. of TACAS'99, pages 193-207, 1999. Google Scholar
  3. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. CUP, 2001. Google Scholar
  4. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronisation skeletons using branching time temporal logic. In Logics of Programs, pages 52-71. Springer, 1981. Google Scholar
  5. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science. Cambridge University Press, 2016. Google Scholar
  6. Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. Game-theoretic semantics for alternating-time temporal logic. In Proc. of AAMAS 2016, pages 671-679, 2016. Google Scholar
  7. Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. Game-theoretic semantics for alternating-time temporal logic. arXiv:1602.07667 [math.LO], submitted, 2017. Google Scholar
  8. Wojciech Penczek, Bozena Wozna, and Andrzej Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundam. Inform., 51(1-2):135-156, 2002. Google Scholar
  9. Bozena Wozna. ACTLS properties and bounded model checking. Fundam. Inform., 63(1):65-87, 2004. Google Scholar
  10. Wenhui Zhang. Bounded semantics. Theor. Comput. Sci., 564:1-29, 2015. 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