Reachability in timed automata with diagonal constraints

Conference Paper

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.

Full Text

Duke Authors

Cited Authors

  • Gastin, P; Mukherjee, S; Srivathsan, B

Published Date

  • August 1, 2018

Published In

Volume / Issue

  • 118 /

International Standard Serial Number (ISSN)

  • 1868-8969

International Standard Book Number 13 (ISBN-13)

  • 9783959770873

Digital Object Identifier (DOI)

  • 10.4230/LIPIcs.CONCUR.2018.28

Citation Source

  • Scopus