Document Open Access Logo

The Tail-Recursive Fragment of Timed Recursive CTL

Authors Florian Bruse, Martin Lange, Etienne Lozes

PDF
Thumbnail PDF

File

LIPIcs.TIME.2022.5.pdf
  • Filesize: 0.75 MB
  • 16 pages

Document Identifiers

Author Details

Florian Bruse
  • School of Electrical Engineering and Computer Science, Universität Kassel, Germany
Martin Lange
  • School of Electrical Engineering and Computer Science, Universität Kassel, Germany
Etienne Lozes
  • Laboratoire d’Informatique, Signaux et Systèmes de Sophia-Antipolis, Université Côte d'Azur, France

Cite As Get BibTex

Florian Bruse, Martin Lange, and Etienne Lozes. The Tail-Recursive Fragment of Timed Recursive CTL. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.TIME.2022.5

Abstract

Timed Recursive CTL (TRCTL) was recently proposed as a merger of two extensions of the well-known branching-time logic CTL: Timed CTL on one hand is interpreted over real-time systems like timed automata, and Recursive CTL (RecCTL) on the other hand obtains high expressiveness through the introduction of a recursion operator. Model checking for the resulting logic is known to be 2-EXPTIME-complete. 
The aim of this paper is to investigate the possibility to obtain a fragment of lower complexity without losing too much expressive power. It is obtained by a syntactic property called "tail-recursiveness" that restricts the way that recursive formulas can be built. This restriction is known to decrease the complexity of model checking by half an exponential in the untimed setting. We show that this also works in the real-time world: model checking for the tail-recursive fragment of TRCTL is EXPSPACE-complete. The upper bound is obtained by a standard untiming construction via region graphs, and rests on the known complexity of tail-recursive fragments of higher-order modal logics. The lower bound is established by a reduction from a suitable tiling problem.

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

References

  1. L. Aceto and F. Laroussinie. Is your model checker on time? On the complexity of model checking for timed modal logics. J. Log. Algebraic Methods Program, 52-53:7-51, 2002. Google Scholar
  2. 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.
  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. R. Alur and P. Madhusudan. Decision problems for timed automata: A survey. In Formal Methods for the Design of Real-Time Systems: Revised Lectures of the International School on Formal Methods for the Design of Computer, Communication, and Software Systems, pages 1-24. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30080-9_1.
  5. R. Axelsson, M. Lange, and R. Somla. The complexity of model checking higher-order fixpoint logic. Log. Meth. in Comp. Sci., 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. P. Bouyer. Timed automata. In Handbook of Automata Theory, pages 1261-1294. European Mathematical Society Publishing House, 2021. URL: https://doi.org/10.4171/Automata-2/12.
  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. Model checking timed recursive CTL. Submitted to Inf. and Comp. Google Scholar
  11. 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.
  12. F. Bruse and M. Lange. Model checking timed recursive CTL. In Proc. 28th Int. Symp. on Temporal Representation and Reasoning, TIME'21, volume 206 of LIPIcs, pages 12:1-12:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  13. F. Bruse, M. Lange, and E. Lozes. Space-efficient fragments of higher-order fixpoint logic. In M. Hague and I. Potapov, editors, Proc. 11th Int. Workshop on Reachability Problems, 2017, London, UK, volume 10506 of LNCS, pages 26-41. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67089-8_3.
  14. S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781139236119.
  15. 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.
  16. T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, 1994. Google Scholar
  17. D. Kozen. Results on the propositional μ-calculus. TCS, 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  18. M. Lange. Specifying program properties using modal fixpoint logics: A survey of results. In Proc. 8th Indian Conf. on Logic and Its Applications, ICLA'19, volume 11600 of LNCS, pages 42-51. Springer, 2019. Google Scholar
  19. 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.
  20. W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4:177-192, 1970. Google Scholar
  21. A. P. Sistla, E. M. Clarke, N. Francez, and A. R. Meyer. Can message buffers be axiomatized in linear temporal logic? Information and Control, 63(1/2):88-112, 1984. Google Scholar
  22. P. van Emde Boas. The convenience of tilings. In Complexity, Logic, and Recursion Theory, volume 187 of Lecture notes in pure and applied mathematics, pages 331-363. Marcel Dekker, Inc., 1997. Google Scholar
  23. M. Y. Vardi. From Church and Prior to PSL. In 25 Years of Model Checking - History, Achievements, Perspectives, volume 5000 of LNCS, pages 150-171. Springer, 2008. Google Scholar
  24. M. Viswanathan and R. Viswanathan. A higher order modal fixed point logic. In Proc. 15th Int. Conf. on Concurrency Theory, 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact