Deriving Parameter Conditions for Periodic Timed Automata Satisfying Real-Time Temporal Logic Formulas
Deriving Parameter Conditions for Periodic Timed Automata Satisfying Real-Time Temporal Logic Formulas
复制标题
推导满足实时时序逻辑公式的周期性定时自动机的参数条件
DOI：
10.1007/0-306-47003-9_10
复制
发表时间：
2001
影响因子：
1.5
通讯作者：
T. Higashino
中科院分区：
文献类型：
--
作者：
A. Nakata;T. Higashino
提出了一种参数周期时间自动机的符号模型检验方法。该方法象征性地推导出参数的最弱条件，使得周期时间自动机的指定控制状态满足某些时间性质。与现有的几种参数化符号模型检测方法不同，所提出的方法是“即时”的-它不需要检查所有的状态。相反，它会遍历计算树的某些必要部分，以导出最弱的条件。我们表明，如果我们限制一个时间自动机是周期性的，即如果我们迫使一个时间自动机定期返回到其初始状态在指定的恒定时间，我们只需要遍历最多的前3个周期的无限计算树。在所提出的方法中，我们可以避免一个昂贵的（和一般不可判定的）密集时域状态集的不动点计算，并推导出最弱的条件，时间自动机的参数，以满足给定的时间属性写在一个实时的时间逻辑公式。
A symbolic model checking method for parametric periodic timed automata is proposed. The method derives symbolically the weakest condition for parameters such that the specified control state of a periodic timed automaton satisfies some temporal properties. Unlike several existing parametric symbolic model checking methods, the proposed method is ‘on-the-fly’ — it does not unnecessarily check all the states. Instead, it traverses some necessary part of the computation tree to derive the weakest condition. We show that if we constrain a timed automaton to be periodic, i.e. if we force a timed automaton to return to its initial state periodically at the specified constant time, we have only to traverse at most the first 3 periods in the infinite computation tree. In the proposed method, we can avoid a costly (and generally undecidable) fixpoint-calculation for dense-time-domain state sets, and derive the weakest condition for parameters of a timed automaton to satisfy given temporal properties written in a real-time temporal logic formula.