Parameterized Verification of Timed Networks with Clock Invariants
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909834347020288 |
|---|---|
| author | André, Étienne Jacobs, Swen Karra, Shyam Lal Sankur, Ocan |
| author_facet | André, Étienne Jacobs, Swen Karra, Shyam Lal Sankur, Ocan |
| contents | We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed networks (DTNs), i.e., networks of TAs that communicate via location guards that enable a transition only if there is another process in a certain location. We solve for the first time the case with unrestricted clock invariants, and establish that the parameterized model checking problem (PMCP) over finite local traces can be reduced to the corresponding model checking problem on a single TA. Moreover, we prove that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs. Finally, we show that for networks with k-wise synchronization, and therefore also for timed Petri nets, location reachability can be reduced to location reachability in DTNs. As a consequence we can answer positively the open problem from Abdulla et al.(2018) whether the universal safety problem for timed Petri nets with multiple clocks is decidable. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_05190 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Parameterized Verification of Timed Networks with Clock Invariants André, Étienne Jacobs, Swen Karra, Shyam Lal Sankur, Ocan Formal Languages and Automata Theory D.2.4; F.1.2 We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed networks (DTNs), i.e., networks of TAs that communicate via location guards that enable a transition only if there is another process in a certain location. We solve for the first time the case with unrestricted clock invariants, and establish that the parameterized model checking problem (PMCP) over finite local traces can be reduced to the corresponding model checking problem on a single TA. Moreover, we prove that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs. Finally, we show that for networks with k-wise synchronization, and therefore also for timed Petri nets, location reachability can be reduced to location reachability in DTNs. As a consequence we can answer positively the open problem from Abdulla et al.(2018) whether the universal safety problem for timed Petri nets with multiple clocks is decidable. |
| title | Parameterized Verification of Timed Networks with Clock Invariants |
| topic | Formal Languages and Automata Theory D.2.4; F.1.2 |
| url | https://arxiv.org/abs/2408.05190 |