TARZAN：面向有时自动机正向与反向可达性的区域基库
形式语言与自动机理论
2026-02-18 v1
摘要
zone抽象技术因其显著的实际效率而广泛采用，是有时自动机验证的事实标准。然而，区域基抽象在特定子类中显示出优于区域的性能。为补充和支持成熟的基于区域工具，我们引入TARZAN，一个C++区域基验证库，用于有时自动机。TARZAN中实现的算法使用一种新颖的区域抽象，跟踪时钟何时变得无穷大的顺序。这种额外的排序导致更细致的状态空间分区，使反向算法能够避免在计算immediate delay前驱区域时枚举所有无穷大时钟有序分区的组合爆炸。我们通过将正向可达性结果与最先进的工具Uppaal和TChecker进行比较来验证TARZAN。实验表明，当等时自动机拥有大型常数和严格守卫时，区域性能最佳。相比之下，TARZAN在封闭等时自动机和带有 punctual守卫的等时自动机方面表现出优越性能。最后，我们展示了反向算法的有效性，为像有时游戏这样的领域中的区域基分析奠定了基础。
引用
@article{arxiv.2602.15435,
title = {TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)},
author = {Andrea Manini and Matteo Rossi and Pierluigi San Pietro},
journal= {arXiv preprint arXiv:2602.15435},
year = {2026}
}