Document Open Access Logo

Model Checking Timed Recursive CTL

Authors Florian Bruse, Martin Lange

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2021.12.pdf
  • Filesize: 0.72 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Program specifications
Keywords
  • formal specification
  • temporal logic
  • real-time systems

Metrics

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

Abstract

We introduce Timed Recursive CTL, a merger of two extensions of the well-known branching-time logic CTL: Timed CTL is interpreted over real-time systems like timed automata; Recursive CTL introduces a powerful recursion operator which takes the expressiveness of this logic CTL well beyond that of regular properties. The result is an expressive logic for real-time properties. We show that its model checking problem is decidable over timed automata, namely 2-EXPTIME-complete.

Cite As Get BibTex

Florian Bruse and Martin Lange. Model Checking Timed Recursive CTL. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 12:1-12:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.TIME.2021.12

Author Details

Florian Bruse
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany
Martin Lange
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany

Acknowledgements

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

References

  1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th Ann. IEEE Symp. on Logic in Computer Science, LICS'90, pages 414-427. IEEE Computer Society Press, 1990. URL: https://doi.org/10.1109/LICS.1990.113766.
  2. R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Inform. and Comp., 104(1):2-34, 1993. URL: https://doi.org/10.1006/inco.1993.1024.
  3. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  4. A. Arnold and D. Niwiński. Rudiments of μ-calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2001. Google Scholar
  5. R. Axelsson, M. Lange, and R. Somla. The complexity of model checking higher-order fixpoint logic. Logical Methods in Computer Science, 3:1-33, 2007. URL: https://doi.org/10.2168/LMCS-3(2:7)2007.
  6. C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  7. H. Bekić. Programming Languages and Their Definition, Selected Papers, volume 177 of LNCS. Springer, 1984. Google Scholar
  8. P. Bouyer, F. Laroussinie, N. Markey, J. Ouaknine, and J. Worrell. Timed temporal logics. In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, volume 10460 of LNCS, pages 211-230. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63121-9_11.
  9. F. Bruse, J. Kreiker, M. Lange, and M. Sälzer. Local higher-order fixpoint iteration. In Proc. 11th Int. Symp. on Games, Automata, Logics, and Formal Verification, GandALF'20, volume 326 of EPTCS, pages 97-113, 2020. URL: https://doi.org/10.4204/EPTCS.326.7.
  10. F. Bruse and M. Lange. Temporal logic with recursion. In Proc. 27th Int. Symp. on Temporal Representation and Reasoning, TIME'20, volume 178 of LIPIcs, pages 6:1-6:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TIME.2020.6.
  11. A. K. Chandra, D. Kozen, and L. J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  12. E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982. URL: https://doi.org/10.1016/0167-6423(83)90017-5.
  13. D. Harel, A. Pnueli, and J. Stavi. Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences, 26(2):222-243, 1983. URL: https://doi.org/10.1016/0022-0000(83)90014-4.
  14. Y. Hosoi, N. Kobayashi, and T. Tsukada. A type-based HFL model checking algorithm. In Proc. 17th Asian Symp. on Programming Languages and Systems, APLAS'19, volume 11893 of NCS, pages 136-155. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_8.
  15. M. Lange. Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39-49, 2005. URL: https://doi.org/10.1016/j.jal.2005.08.002.
  16. M. Lange and C. Stirling. Model checking fixed point logic with chop. In Proc. 5th Conf. on Foundations of Software Science and Computation Structures, FOSSACS'02, volume 2303 of LNCS, pages 250-263. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_18.
  17. F. Laroussinie, N. Markey, and P. Schnoebelen. Model checking timed automata with one or two clocks. In Proc. 15th Int. Conf. on Concurrency Theory, CONCUR'04, volume 3170 of LNCS, pages 387-401. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_25.
  18. M. Müller-Olm. A modal fixpoint logic with chop. In Proc. 16th Symp. on Theoretical Aspects of Computer Science, STACS'99, volume 1563 of LNCS, pages 510-520. Springer, 1999. URL: https://doi.org/10.1007/3-540-49116-3_48.
  19. A. Pnueli. The temporal logic of programs. In Proc. 18th Symp. on Foundations of Computer Science, FOCS'77, pages 46-57, Providence, RI, USA, 1977. IEEE. URL: https://doi.org/10.1109/SFCS.1977.32.
  20. A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 5:285-309, 1955. URL: https://doi.org/10.2140/pjm.1955.5.285.
  21. M. Viswanathan and R. Viswanathan. A higher order modal fixed point logic. In CONCUR'04, volume 3170 of LNCS, pages 512-528. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_33.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact