LIPIcs.TIME.2021.12.pdf
- Filesize: 0.72 MB
- 14 pages
Document
Model Checking Timed Recursive CTL
Authors
-
Part of:
Volume:
28th International Symposium on Temporal Representation and Reasoning (TIME 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Temporal Representation and Reasoning (TIME) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-09-16
File
Document Identifiers
Acknowledgements
The open access publication of this article was supported by the Alpen-Adria-Universität Klagenfurt, Austria.
Cite AsGet 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
https://doi.org/10.4230/LIPIcs.TIME.2021.12
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.
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)
0PDF Downloads
References
- 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.
- 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.
- 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.
-
A. Arnold and D. Niwiński. Rudiments of μ-calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2001.
- 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.
-
C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008.
-
H. Bekić. Programming Languages and Their Definition, Selected Papers, volume 177 of LNCS. Springer, 1984.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.