2026-07-22T18:45:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7801 2024-03-06T10:41:11Z ddc:004 open_access

Towards an Efficient Tree Automata Based Technique for Timed Systems Akshay, S. Gastin, Paul Krishna, Shankara Narayanan Sarkar, Ilias Timed automata tree automata pushdown systems tree-width The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion. Schloss Dagstuhl – Leibniz-Zentrum für Informatik S. Akshay and Paul Gastin and Shankara Narayanan Krishna and Ilias Sarkar 2017 Is Part Of LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2017.39 urn:nbn:de:0030-drops-78017 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.39 eng https://creativecommons.org/licenses/by/3.0/legalcode