TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917277857742848 |
|---|---|
| author | Manini, Andrea Rossi, Matteo Pietro, Pierluigi San |
| author_facet | Manini, Andrea Rossi, Matteo Pietro, Pierluigi San |
| contents | The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractions have been shown to outperform zones in specific subclasses of TA. To complement and support mature zone-based tools, we introduce TARZAN, a C++ region-based verification library for TA. The algorithms implemented in TARZAN use a novel region abstraction that tracks the order in which clocks become unbounded. This additional ordering induces a finer partitioning of the state space, enabling backward algorithms to avoid the combinatorial explosion associated with enumerating all ordered partitions of unbounded clocks, when computing immediate delay predecessor regions. We validate TARZAN by comparing forward reachability results against the state-of-the-art tools Uppaal and TChecker. The experiments confirm that zones excel when TA have large constants and strict guards. In contrast, TARZAN exhibits superior performance on closed TA and TA with punctual guards. Finally, we demonstrate the efficacy of our backward algorithms, establishing a foundation for region-based analysis in domains like Timed Games, where backward exploration is essential. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_15435 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version) Manini, Andrea Rossi, Matteo Pietro, Pierluigi San Formal Languages and Automata Theory The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractions have been shown to outperform zones in specific subclasses of TA. To complement and support mature zone-based tools, we introduce TARZAN, a C++ region-based verification library for TA. The algorithms implemented in TARZAN use a novel region abstraction that tracks the order in which clocks become unbounded. This additional ordering induces a finer partitioning of the state space, enabling backward algorithms to avoid the combinatorial explosion associated with enumerating all ordered partitions of unbounded clocks, when computing immediate delay predecessor regions. We validate TARZAN by comparing forward reachability results against the state-of-the-art tools Uppaal and TChecker. The experiments confirm that zones excel when TA have large constants and strict guards. In contrast, TARZAN exhibits superior performance on closed TA and TA with punctual guards. Finally, we demonstrate the efficacy of our backward algorithms, establishing a foundation for region-based analysis in domains like Timed Games, where backward exploration is essential. |
| title | TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version) |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2602.15435 |