摘要：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.
