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.12
URN: urn:nbn:de:0030-drops-170756
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17075/
Go to the corresponding LIPIcs Volume Portal

Herbreteau, Frédéric ; Srivathsan, B. ; Walukiewicz, Igor

Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics

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

Abstract

We study the Büchi non-emptiness problem for networks of timed automata. Standard solutions consider the network as a monolithic timed automaton obtained as a synchronized product and build its zone graph on-the-fly under the classical global-time semantics. In the global-time semantics, all processes are assumed to have a common global timeline.
Bengtsson et al. in 1998 have proposed a local-time semantics where each process in the network moves independently according to a local timeline, and processes synchronize their timelines when they do a common action. It has been shown that the local-time semantics is equivalent to the global-time semantics for finite runs, and hence can be used for checking reachability. The local-time semantics allows computation of a local zone graph which has good independence properties and is amenable to partial-order methods. Hence local zone graphs are able to better tackle the state-space explosion due to concurrency.
In this work, we extend the results to the Büchi setting. We propose a local zone graph computation that can be coupled with a partial-order method, to solve the Büchi non-emptiness problem in timed networks. In the process, we develop a theory of regions for the local-time semantics.

BibTeX - Entry

@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2022.12,
  author =	{Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Walukiewicz, Igor},
  title =	{{Checking Timed B\"{u}chi Automata Emptiness Using the Local-Time Semantics}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{12:1--12:24},
  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/17075},
  URN =		{urn:nbn:de:0030-drops-170756},
  doi =		{10.4230/LIPIcs.CONCUR.2022.12},
  annote =	{Keywords: Timed B\"{u}chi automata, local-time semantics, zones, abstraction, partial-order reduction}
}

Keywords: Timed Büchi automata, local-time semantics, zones, abstraction, partial-order reduction
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