Durations and parametric model-checking in timed automata
Durations and parametric model-checking in timed automata
复制标题
定时自动机中的持续时间和参数模型检查
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
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 Presburger arithmetic (when the time domain is discrete) or in a real arithmetic (when the time domain is dense). Using this logical definition, we show that the parametric model-checking problem for the logic TCTL can be solved algorithmically; the proof of this result is simple. More generally, we are able to effectively characterize the values of the parameters that satisfy the parametric TCTL formula with respect to the given timed automaton.