2026-07-24T19:05:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:21223 2024-10-22T05:39:58Z ddc:004 open_access

Real-Time Higher-Order Recursion Schemes Alsmann, Eric Bruse, Florian Timed Automata Higher-Order Recursion Schemes Tree Automata 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eric Alsmann and Florian Bruse 2024 Is Part Of LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2024.16 urn:nbn:de:0030-drops-212236 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.16 eng https://creativecommons.org/licenses/by/4.0/legalcode