License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2018.28
URN: urn:nbn:de:0030-drops-95660
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9566/
Go to the corresponding LIPIcs Volume Portal

Gastin, Paul ; Mukherjee, Sayan ; Srivathsan, B.

Reachability in Timed Automata with Diagonal Constraints

pdf-format:
LIPIcs-CONCUR-2018-28.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{gastin_et_al:LIPIcs:2018:9566,
  author =	{Paul Gastin and Sayan Mukherjee and B. Srivathsan},
  title =	{{Reachability in Timed Automata with Diagonal Constraints}},
  booktitle =	{29th International Conference on Concurrency Theory  (CONCUR 2018)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Sven Schewe and Lijun Zhang},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9566},
  URN =		{urn:nbn:de:0030-drops-95660},
  doi =		{10.4230/LIPIcs.CONCUR.2018.28},
  annote =	{Keywords: Timed Automata, Reachability, Zones, Diagonal constraints}
}

Keywords: Timed Automata, Reachability, Zones, Diagonal constraints
Collection: 29th International Conference on Concurrency Theory (CONCUR 2018)
Issue Date: 2018
Date of publication: 31.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI