Parameterized Verification of Disjunctive Timed Networks
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909059374907392 |
|---|---|
| author | André, Étienne Eichler, Paul Jacobs, Swen Karra, Shyam Lal |
| author_facet | André, Étienne Eichler, Paul Jacobs, Swen Karra, Shyam Lal |
| contents | We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if there is another process in a given location. This computational model has been considered in the literature before, example applications are gossiping clock synchronization protocols or planning problems. We address the minimum-time reachability problem (Minreach) in DTNs, and show how to efficiently solve it based on a novel zone graph algorithm. We further show that solving Minreach allows us to construct a summary TA capturing exactly the possible behaviors of a single TA within a DTN of arbitrary size. The combination of these two results enables the parameterized verification of DTNs, while avoiding the construction of an exponential-size cutoff system required by existing results. Additionally, we develop sufficient conditions for solving Minreach and parameterized verification problems even in certain cases where locations that appear in location guards can have clock invariants, a case that has usually been excluded in the literature. Our techniques are also implemented, and experiments show their practicality. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2305_07295 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Parameterized Verification of Disjunctive Timed Networks André, Étienne Eichler, Paul Jacobs, Swen Karra, Shyam Lal Logic in Computer Science Formal Languages and Automata Theory D.2.4; F.1.2 We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if there is another process in a given location. This computational model has been considered in the literature before, example applications are gossiping clock synchronization protocols or planning problems. We address the minimum-time reachability problem (Minreach) in DTNs, and show how to efficiently solve it based on a novel zone graph algorithm. We further show that solving Minreach allows us to construct a summary TA capturing exactly the possible behaviors of a single TA within a DTN of arbitrary size. The combination of these two results enables the parameterized verification of DTNs, while avoiding the construction of an exponential-size cutoff system required by existing results. Additionally, we develop sufficient conditions for solving Minreach and parameterized verification problems even in certain cases where locations that appear in location guards can have clock invariants, a case that has usually been excluded in the literature. Our techniques are also implemented, and experiments show their practicality. |
| title | Parameterized Verification of Disjunctive Timed Networks |
| topic | Logic in Computer Science Formal Languages and Automata Theory D.2.4; F.1.2 |
| url | https://arxiv.org/abs/2305.07295 |