Document Open Access Logo

Real-Time Higher-Order Recursion Schemes

Authors Eric Alsmann , Florian Bruse

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2024.16.pdf
  • Filesize: 0.82 MB
  • 20 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

Metrics

Abstract

Higher-Order Recursion Schemes (HORS) have long been studied as a tool to model functional programs. Model-checking the tree generated by a HORS of order k against a parity automaton is known to be k-EXPTIME-complete. This paper introduces timed HORS, a real-time version of HORS in the sense of Alur/Dill'90, to be model-checked against a pair of a parity automaton and a timed automaton. We show that adding dense linear time to the notion of recursion schemes adds one exponential to the cost of model-checking, i.e., model-checking a timed HORS of order k can be done in (k+1)-EXPTIME. This is shown by an adaption of the region-graph construction known from the model-checking of timed CTL. We also obtain a hardness result for k = 1, but we strongly conjecture that it holds for all k. This result is obtained by encoding runs of 2-EXPTIME Turing machines into the trees generated by timed HORS.

Cite As Get BibTex

Eric Alsmann and Florian Bruse. Real-Time Higher-Order Recursion Schemes. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.TIME.2024.16

Author Details

Eric Alsmann
  • University of Kassel, Germany
Florian Bruse
  • University of Kassel, Germany

References

  1. 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.
  2. 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.
  3. Rajeev Alur and P. Madhusudan. Decision problems for timed automata: A survey. In Marco Bernardo and Flavio Corradini, editors, Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures, volume 3185 of Lecture Notes in Computer Science, pages 1-24. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30080-9_1.
  4. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  5. Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, and Olivier Serre. C-shore: a collapsible approach to higher-order verification. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 13-24. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500589.
  6. Christopher H. Broadbent and Naoki Kobayashi. Saturation-based model checking of higher-order recursion schemes. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 129-148. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPICS.CSL.2013.129.
  7. Florian Bruse. Space-efficient model-checking of higher-order recursion schemes. manuscript submitted. Google Scholar
  8. Florian Bruse and Martin Lange. Temporal logic with recursion. Inf. Comput., 281:104804, 2021. URL: https://doi.org/10.1016/J.IC.2021.104804.
  9. 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.
  10. Florian Bruse and Martin Lange. Model checking timed recursive CTL. Inf. Comput., 298:105168, 2024. URL: https://doi.org/10.1016/J.IC.2024.105168.
  11. 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.
  12. Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  13. 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.
  14. Gérard Huet. Résolution d'Équations dans des Langages d'Order 1, 2., ω. PhD thesis, Universite de Paris VII, 1976. Google Scholar
  15. Marcin Jurdzinski. Small progress measures for solving parity games. In Horst Reichel and Sophie Tison, editors, STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings, volume 1770 of Lecture Notes in Computer Science, pages 290-301. Springer, 2000. URL: https://doi.org/10.1007/3-540-46541-3_24.
  16. 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.
  17. Naoki Kobayashi. Model checking higher-order programs. J. ACM, 60(3):20:1-20:62, 2013. URL: https://doi.org/10.1145/2487241.2487246.
  18. Naoki Kobayashi, Étienne Lozes, and Florian Bruse. On the relationship between higher-order recursion schemes and higher-order fixpoint logic. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 246-259. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009854.
  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.
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