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.
@InProceedings{alsmann_et_al:LIPIcs.TIME.2024.16, author = {Alsmann, Eric and Bruse, Florian}, title = {{Real-Time Higher-Order Recursion Schemes}}, booktitle = {31st International Symposium on Temporal Representation and Reasoning (TIME 2024)}, pages = {16:1--16:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-349-2}, ISSN = {1868-8969}, year = {2024}, volume = {318}, editor = {Sala, Pietro and Sioutis, Michael and Wang, Fusheng}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.16}, URN = {urn:nbn:de:0030-drops-212236}, doi = {10.4230/LIPIcs.TIME.2024.16}, annote = {Keywords: Timed Automata, Higher-Order Recursion Schemes, Tree Automata} }
Feedback for Dagstuhl Publishing