Parametric disjunctive timed networks
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911302217105408 |
|---|---|
| author | André, Étienne Jacobs, Swen Lefaucheux, Engel |
| author_facet | André, Étienne Jacobs, Swen Lefaucheux, Engel |
| contents | We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e. unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which
1) a given location is reachable for at least one process (local property), and
2) a global state is reachable where all processes are in a given location (global property).
Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters -- a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_04991 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Parametric disjunctive timed networks André, Étienne Jacobs, Swen Lefaucheux, Engel Logic in Computer Science We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e. unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which 1) a given location is reachable for at least one process (local property), and 2) a global state is reachable where all processes are in a given location (global property). Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters -- a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants. |
| title | Parametric disjunctive timed networks |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2512.04991 |