2026-07-26T03:05:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17075 2024-03-06T10:58:41Z ddc:004 open_access

Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics Herbreteau, Frédéric Srivathsan, B. Walukiewicz, Igor Timed Büchi automata local-time semantics zones abstraction partial-order reduction 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Frédéric Herbreteau and B. Srivathsan and Igor Walukiewicz 2022 Is Part Of LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2022.12 urn:nbn:de:0030-drops-170756 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.12 eng https://creativecommons.org/licenses/by/4.0/legalcode