Model-checking real-time systems: revisiting the alternating automaton route
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914235508850688 |
|---|---|
| author | Bouyer, Patricia Srivathsan, B Vishwanath, Vaishnavi |
| author_facet | Bouyer, Patricia Srivathsan, B Vishwanath, Vaishnavi |
| contents | Alternating timed automata (ATA) are an extension of timed automata, that are closed under complementation and hence amenable to logic-to-automata translations. Several timed logics, including Metric Temporal Logic (MTL), can be converted to equivalent 1-clock ATAs (1-ATAs). Satisfiability of an MTL formula reduces to checking emptiness of a 1-ATA. A straightforward modification of the 1-ATA emptiness algorithm can be applied for model-checking timed automata models against 1-ATA specifications. However, existing emptiness algorithms for 1-ATA proceed by an extended region construction, and are not suitable for implementations. Our goal in this work is to initiate the study of zone-based methods directly for 1-ATAs. We first introduce a deactivation operation on the 1-ATA syntax to allow an explicit deactivation of the clock in transitions. Using the deactivation operation, we improve the existing MTL-to-1-ATA conversion and present a fragment of MTL for which the equivalent 1-ATA generate a bounded number of variables. Secondly, we develop the idea of zones for 1-ATA and present an emptiness algorithm which explores a corresponding zone graph. For termination, a special entailment check between zones is necessary. Our main technical contributions are: (1) an algorithm for the entailment check using simple zone operations and (2) an NP-hardness for the entailment check in the general case. Finally, we adapt our methods to the problem of model-checking timed automata models against 1-ATA specifications. We observe that when the timed automaton is strongly non-Zeno or when the 1-ATA generates a bounded number of variables, a modified entailment check with quadratic complexity can be applied. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_17576 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Model-checking real-time systems: revisiting the alternating automaton route Bouyer, Patricia Srivathsan, B Vishwanath, Vaishnavi Logic in Computer Science Formal Languages and Automata Theory 68N30 Alternating timed automata (ATA) are an extension of timed automata, that are closed under complementation and hence amenable to logic-to-automata translations. Several timed logics, including Metric Temporal Logic (MTL), can be converted to equivalent 1-clock ATAs (1-ATAs). Satisfiability of an MTL formula reduces to checking emptiness of a 1-ATA. A straightforward modification of the 1-ATA emptiness algorithm can be applied for model-checking timed automata models against 1-ATA specifications. However, existing emptiness algorithms for 1-ATA proceed by an extended region construction, and are not suitable for implementations. Our goal in this work is to initiate the study of zone-based methods directly for 1-ATAs. We first introduce a deactivation operation on the 1-ATA syntax to allow an explicit deactivation of the clock in transitions. Using the deactivation operation, we improve the existing MTL-to-1-ATA conversion and present a fragment of MTL for which the equivalent 1-ATA generate a bounded number of variables. Secondly, we develop the idea of zones for 1-ATA and present an emptiness algorithm which explores a corresponding zone graph. For termination, a special entailment check between zones is necessary. Our main technical contributions are: (1) an algorithm for the entailment check using simple zone operations and (2) an NP-hardness for the entailment check in the general case. Finally, we adapt our methods to the problem of model-checking timed automata models against 1-ATA specifications. We observe that when the timed automaton is strongly non-Zeno or when the 1-ATA generates a bounded number of variables, a modified entailment check with quadratic complexity can be applied. |
| title | Model-checking real-time systems: revisiting the alternating automaton route |
| topic | Logic in Computer Science Formal Languages and Automata Theory 68N30 |
| url | https://arxiv.org/abs/2501.17576 |