3 papers
cs.FL2026
TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)
Andrea Manini, Matteo Rossi, Pierluigi San Pietro
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 abstractio…
cs.FL2025
Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation
Andrea Manini, Matteo Rossi, Pierluigi San Pietro
A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult…
cs.FL2025
On Decidability Timed Automata with 2 Parametric Clocks
Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
In this paper, we introduce a restriction of Timed Automata (TA), called non-resetting test Timed Automata (nrtTA). An nrtTA does not allow to test and reset the same clock on the…