论文标题
可更新定时自动机的可及性使得更快，更有效
Reachability for Updatable Timed Automata made faster and more effective
论文作者
论文摘要
可更新的定时自动机（UTA）是经典定时自动机的扩展，允许对时钟变量进行特殊更新，例如x：= x -1，x：= y + 2等。一般来说，UTA的可及性是不可决定的。已经研究了各种具有可确定可及性的子类。 UTA可及性的一种通用方法包括两个阶段：首先，对自动机进行静态分析以计算每个状态下的一组时钟约束；在第二阶段中，列举了可及的配置集，称为区域。在这项工作中，我们改进了静态分析的算法。与现有算法相比，我们的方法计算较小的约束集并确保终止更多UTA，从而更快，更有效。作为主要应用程序，我们获得了可确定性的替代证明，并且具有有限减法的定时自动机（一种更有效的算法），这是一类广泛用于建模调度问题的UTA类。我们已经在工具Tchecker中实施了程序，并进行了实验以验证我们方法的好处。
Updatable timed automata (UTA) are extensions of classic timed automata that allow special updates to clock variables, like x:= x - 1, x := y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysis. Compared to the existing algorithm, our method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective. As the main application, we get an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modelling scheduling problems. We have implemented our procedure in the tool TChecker and conducted experiments that validate the benefits of our approach.
