论文标题
参数定时自动机中的区域外推
Zone extrapolations in parametric timed automata
论文作者
论文摘要
定时自动机（TAS）是一种有效的形式主义，可以建模和验证艰苦的时序限制和并发的系统。尽管TA具有无限精度的确切定时常数，但参数TA（PTA）利用了这一限制并以不可证明的成本来提高其表现力。 TAS效率的一个实际解释是区域外推，其中的时钟估值超过给定常数。由于参数可以无限制，因此无法轻易扩展到PTA。在这项工作中，我们提出了基于M驱除的PTA外推的几个定义，并研究了它们的正确性。我们的实验显示了计算时间的总体减少，最重要的是，允许终止一些以前无法解决的基准。
Timed automata (TAs) are an efficient formalism to model and verify systems with hard timing constraints, and concurrency. While TAs assume exact timing constants with infinite precision, parametric TAs (PTAs) leverage this limitation and increase their expressiveness, at the cost of undecidability. A practical explanation for the efficiency of TAs is zone extrapolation, where clock valuations beyond a given constant are considered equivalent. This concept cannot be easily extended to PTAs, due to the fact that parameters can be unbounded. In this work, we propose several definitions of extrapolation for PTAs based on the M-extrapolation, and we study their correctness. Our experiments show an overall decrease of the computation time and, most importantly, allow termination of some previously unsolvable benchmarks.
