Document Open Access Logo

Higher-Order Timed Automata and Tail Recursion

Author Florian Bruse

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2025.5.pdf
  • Filesize: 1.05 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Tree languages
  • Theory of computation → Automata over infinite objects
Keywords
  • Timed Automata
  • Higher-Order Recursion Schemes
  • Tree Automata
  • Tail Recursion

Metrics

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

Abstract

Timed Automata (TA) are a popular formalism to model systems in dense linear time. However, due to their finite state-space, they can only model systems with a finitary logical behavior. There are extensions to e.g., timed pushdown systems and timed recursive state machines. Higher-Order Recursion Schemes (HORS) are another popular model for infinite-state, non-regular systems, naturally stratified by their type-theoretic order. We recently introduced Real-Time Recursion schemes as an approximation of HORS to real-time systems.
This paper updates Real-Time Recursion Schemes into Higher-Order Timed Automata, a formalism that defines a tree-shaped timed automaton, which is more suitable to model actual systems. We show that the model-checking problem against the timed version of the modal mu-calculus exhibits the expected complexity bounds, i.e., an increase by one exponential towards the untimed version. We also show that, in the presence of tail recursion, half an exponential can be recovered, mirroring similar gains in the untimed setting. We also give a matching lower bound for the special case of order-1 HORTA. We conjecture that this can be generalized for all orders.

Cite As Get BibTex

Florian Bruse. Higher-Order Timed Automata and Tail Recursion. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TIME.2025.5

Author Details

Florian Bruse
  • TUM School of Computation, Information and Technology, Technical University of Munich, Munich, Germany

References

  1. Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler. Scheduling with timed automata. Theor. Comput. Sci., 354(2):272-300, 2006. URL: https://doi.org/10.1016/J.TCS.2005.11.018.
  2. Luca Aceto and François 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. URL: https://doi.org/10.1016/S1567-8326(02)00022-X.
  3. Eric Alsmann and Florian Bruse. Real-time higher-order recursion schemes. In Pietro Sala, Michael Sioutis, and Fusheng Wang, editors, 31st International Symposium on Temporal Representation and Reasoning, TIME 2024, October 28-30, 2024, Montpellier, France, volume 318 of LIPIcs, pages 16:1-16:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.TIME.2024.16.
  4. Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2-34, 1993. URL: https://doi.org/10.1006/inco.1993.1024.
  5. Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In Mike Paterson, editor, Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, UK, July 16-20, 1990, Proceedings, volume 443 of Lecture Notes in Computer Science, pages 322-335. Springer, 1990. URL: https://doi.org/10.1007/BFB0032042.
  6. C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  7. Massimo Benerecetti, Stefano Minopoli, and Adriano Peron. Analysis of timed recursive state machines. In 2010 17th International Symposium on Temporal Representation and Reasoning, pages 61-68, 2010. URL: https://doi.org/10.1109/TIME.2010.10.
  8. Ahmed Bouajjani, Rachid Echahed, and Riadh Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Hybrid Systems II, pages 64-85, Berlin, Heidelberg, 1995. Springer-Verlag. Google Scholar
  9. Florian Bruse. Space-efficient model-checking of higher-order recursion schemes. In Shankaranarayanan Krishna, Sriram Sankaranarayanan, and Ashutosh Trivedi, editors, Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part I, volume 15529 of Lecture Notes in Computer Science, pages 29-51. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-82700-6_2.
  10. Florian Bruse, Oliver Friedmann, and Martin Lange. On guarded transformation in the modal μ-calculus. Log. J. IGPL, 23(2):194-216, 2015. URL: https://doi.org/10.1093/JIGPAL/JZU030.
  11. Florian Bruse and Martin Lange. The tail-recursive fragment of timed recursive CTL. Inf. Comput., 294:105084, 2023. URL: https://doi.org/10.1016/J.IC.2023.105084.
  12. Florian Bruse, Martin Lange, and Étienne Lozes. Space-efficient fragments of higher-order fixpoint logic. In Matthew Hague and Igor Potapov, editors, Reachability Problems - 11th International Workshop, RP 2017, London, UK, September 7-9, 2017, Proceedings, volume 10506 of Lecture Notes in Computer Science, pages 26-41. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67089-8_3.
  13. Lorenzo Clemente and Slawomir Lasota. Timed pushdown automata revisited. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 738-749. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.73.
  14. Werner Damm. The IO- and oi-hierarchies. Theor. Comput. Sci., 20:95-207, 1982. URL: https://doi.org/10.1016/0304-3975(82)90009-3.
  15. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781139236119.
  16. Martijn Hendriks and Marcel Verhoef. Timed automata based analysis of embedded system architectures. In Proceedings 20th IEEE International Parallel & Distributed Processing Symposium, pages 8-pp. IEEE, 2006. Google Scholar
  17. Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Inf. Comput., 111(2):193-244, 1994. URL: https://doi.org/10.1006/INCO.1994.1045.
  18. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_15.
  19. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179-188. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.29.
  20. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  21. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Information and Compututation, 239:340-355, 2014. URL: https://doi.org/10.1016/J.IC.2014.07.012.
  22. Ashutosh Trivedi and Dominik Wojtczak. Recursive timed automata. In Ahmed Bouajjani and Wei-Ngan Chin, editors, Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, volume 6252 of Lecture Notes in Computer Science, pages 306-324. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15643-4_23.
  23. P. van Emde Boas. The convenience of tilings. In A. Sorbi, editor, Complexity, Logic, and Recursion Theory, volume 187 of Lecture notes in pure and applied mathematics, pages 331-363. Marcel Dekker, Inc., 1997. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact