License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2022.13
URN: urn:nbn:de:0030-drops-170766
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17076/
Go to the corresponding LIPIcs Volume Portal

Akshay, S. ; Gastin, Paul ; Govind, R. ; Srivathsan, B.

Simulations for Event-Clock Automata

pdf-format:
LIPIcs-CONCUR-2022-13.pdf (0.8 MB)

Abstract

Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations.
In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the ?-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.

BibTeX - Entry

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2022.13,
  author =	{Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
  title =	{{Simulations for Event-Clock Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/17076},
  URN =		{urn:nbn:de:0030-drops-170766},
  doi =		{10.4230/LIPIcs.CONCUR.2022.13},
  annote =	{Keywords: Event-clock automata, verification, zones, simulations, reachability}
}

Keywords: Event-clock automata, verification, zones, simulations, reachability
Collection: 33rd International Conference on Concurrency Theory (CONCUR 2022)
Issue Date: 2022
Date of publication: 06.09.2022

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