TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)
Andrea Manini, Matteo Rossi, Pierluigi San Pietro

TL;DR
TARZAN is a new C++ library that uses a region-based approach for verifying Timed Automata, offering advantages over zone-based methods especially for certain subclasses and backward reachability tasks.
Contribution
Introduces TARZAN, a region-based verification library for Timed Automata that employs a novel region abstraction to improve backward reachability analysis.
Findings
TARZAN outperforms zone-based tools on closed TA and punctual guards.
Zones are more efficient with large constants and strict guards.
Backward algorithms in TARZAN are effective for Timed Games.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Security and Verification in Computing · Embedded Systems Design Techniques
