Reachability in timed automata with diagonal constraints

06/28/2018
by   Paul Gastin, et al.
0

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 the form of a data structure called "zones". Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test "is-Z-simulated-by-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. In this paper, we propose a simulation relation LU-d for timed automata with diagonal constraints. On the negative side, we show that deciding Z-is-not-LU-d-simulated-by-Z' is NP-complete. On the positive side, we identify a witness for non-simulation 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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset