Skip to main content

Reachability in timed automata with diagonal constraints

Publication ,  Conference
Gastin, P; Mukherjee, S; Srivathsan, B
Published in: Leibniz International Proceedings in Informatics, LIPIcs
August 1, 2018

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 e ciency. 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 e ective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation dLU for timed automata with diagonal constraints. On the negative side, we show that deciding Z dLU Z is NP-complete. On the positive side, we identify a witness for Z dLU 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 e cient in practice.

Duke Scholars

Published In

Leibniz International Proceedings in Informatics, LIPIcs

DOI

ISSN

1868-8969

ISBN

9783959770873

Publication Date

August 1, 2018

Volume

118
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Gastin, P., Mukherjee, S., & Srivathsan, B. (2018). Reachability in timed automata with diagonal constraints. In Leibniz International Proceedings in Informatics, LIPIcs (Vol. 118). https://doi.org/10.4230/LIPIcs.CONCUR.2018.28
Gastin, P., S. Mukherjee, and B. Srivathsan. “Reachability in timed automata with diagonal constraints.” In Leibniz International Proceedings in Informatics, LIPIcs, Vol. 118, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.28.
Gastin P, Mukherjee S, Srivathsan B. Reachability in timed automata with diagonal constraints. In: Leibniz International Proceedings in Informatics, LIPIcs. 2018.
Gastin, P., et al. “Reachability in timed automata with diagonal constraints.” Leibniz International Proceedings in Informatics, LIPIcs, vol. 118, 2018. Scopus, doi:10.4230/LIPIcs.CONCUR.2018.28.
Gastin P, Mukherjee S, Srivathsan B. Reachability in timed automata with diagonal constraints. Leibniz International Proceedings in Informatics, LIPIcs. 2018.

Published In

Leibniz International Proceedings in Informatics, LIPIcs

DOI

ISSN

1868-8969

ISBN

9783959770873

Publication Date

August 1, 2018

Volume

118