2026-07-22T22:17:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9566 2024-03-06T10:44:44Z ddc:004 open_access

Reachability in Timed Automata with Diagonal Constraints Gastin, Paul Mukherjee, Sayan Srivathsan, B. Timed Automata Reachability Zones Diagonal constraints We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called "zones". Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Paul Gastin and Sayan Mukherjee and B. Srivathsan 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.28 urn:nbn:de:0030-drops-95660 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.28 eng https://creativecommons.org/licenses/by/3.0/legalcode