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.
@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/entities/document/10.4230/LIPIcs.CONCUR.2022.12}, 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} }
Feedback for Dagstuhl Publishing