Selected publications at LSV

Abstract:
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.

@inproceedings{GMS-concur18,
   address = {Beijing, China},
   author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan},
   booktitle = {{P}roceedings of the 29th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'18)},
   DOI = {10.4230/LIPIcs.CONCUR.2018.28},
   editor = {Schewe, Sven and Zhang, Lijun},
   month = sep,
   pages = {28:1-28:17},
   publisher = {Leibniz-Zentrum f{\"u}r Informatik},
   series = {Leibniz International Proceedings in Informatics},
   title = {Reachability in timed automata with diagonal constraints},
   url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9566},
   volume = {118},
   year = {2018},
}

About LSV

Select by Year