Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic
Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic
复制标题
使用 Presburger 算法在定时自动机中进行持续时间、参数模型检查
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Jean
中科院分区：
文献类型：
--
作者：
V. Bruyère;E. Dall'Olio;Jean
我们考虑模型检查逻辑 TCTL 在时间自动机上的参数扩展的问题，并建立其可判定性。给定一个定时自动机，我们证明从一个区域开始到另一个区域结束的运行持续时间集合可以在 Presburger 算术（当时域离散时）或实数理论（当时域密集时）中定义。通过这个逻辑定义，我们表明可以轻松解决逻辑 TCTL 的参数模型检查问题。更一般地说，我们能够有效地表征满足参数化 TCTL 公式的参数值。
We consider the problem of model-checking a parametric extension of the logic TCTL over timed automata and establish its decidability. Given a timed automaton, we show that the set of durations of runs starting from a region and ending in another region is definable in the arithmetic of Presburger (when the time domain is discrete) or in the theory of the reals (when the time domain is dense). With this logical definition, we show that the parametric model-checking problem for the logic TCTL can easily be solved. More generally, we are able to effectively characterize the values of the parameters that satisfy the parametric TCTL formula.