On Model Checking Durational Kripke Structures
On Model Checking Durational Kripke Structures
复制标题
持续 Kripke 结构的模型检验
DOI：
10.1007/3-540-45931-6_19
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
P. Schnoebelen
中科院分区：
文献类型：
--
作者：
F. Laroussinie;N. Markey;P. Schnoebelen
我们考虑了持续Kripke结构的定量模型检验（Kripke结构的过渡有整数持续时间）与时间的时间逻辑，其中下标把定量约束的时间之前，一个属性得到满足.我们调查的条件，允许多项式时间的模型检查算法的时间版本的CTL和表现出一个重要的差距逻辑，其中下标的形式“= c”（确切的持续时间）是允许的，更简单的逻辑，只允许形式的下标“？c”还是“？C”（有限持续时间）。这项研究的一个令人惊讶的结果是，它提供了第二个例子？P2-完全模型检验问题
We consider quantitative model checking in durational Kripke structures (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied.We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "? c" or "? c" (bounded duration).A surprising outcome of this study is that it provides the second example of a ?p2-complete model checking problem.