Graded-CTL: Satisfiability and Symbolic Model Checking
Graded-CTL: Satisfiability and Symbolic Model Checking
复制标题
Graded-CTL：可满足性和符号模型检查
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Mimmo Parente
中科院分区：
文献类型：
--
作者：
Alessandro Ferrante;M. Napoli;Mimmo Parente
在本文中，我们继续研究的严格扩展的计算树逻辑，称为分级CTL，最近推出的相同的作者。这种新的逻辑用分级模态扩充了标准量词，从而能够表达“至少存在k“或“除了k之外的所有“未来，对于某个常数k。因此，人们可以描述在系统设计中有用的属性，这些属性不能用CTL表示，就像一种冗余的活性属性，询问是否有多于一条路径满足“最终会发生好的事情”，从而使系统对可能的故障更宽容。分级CTL公式也可以用来确定系统的坏行为是否超过给定数量：在模型检查框架中，这意味着可以在模型检查器的唯一运行中验证给定规范的用户定义数量的反例的存在并生成它们。
在这里，我们展示了理论和应用的贡献。在理论方面，我们给出了一个简单的算法来判定这个逻辑，并且证明了当量词的常数用一元表示时，可满足性问题是ExpTime -完全的。在应用方面，我们提出了符号算法来解决模型检测问题。这些算法的主要特点之一是，虽然“不同”的反例的计算具有固有的高复杂性时，模型表示符号，我们已经设计了它们，使多个反例的生成尽可能容易和快速。符号算法已实现使用BDD数据结构，并已被集成到众所周知的NuSMV模型检查器，已被修改为接受规格表示分级CTL。我们报告的测试结果是非常舒适的，在这个意义上，无论是运行时间和大小的BDD生产的是与经典CTL中表示的规格所获得的。
In this paper we continue the study of a strict extension of the Computation Tree Logic, called graded-CTL , recently introduced by the same authors. This new logic augments the standard quantifiers with graded modalities, being able thus to express "There exist at least k " or "For all but k " futures, for some constant k . One can thus describe properties useful in system design, which cannot be expressed with CTL, like a sort of redundant liveness property asking whether there is more than one path satisfying that "something good eventually happens", making thus the system more tolerant to possible faults. Graded-CTL formulas can also be used to determine whether there are more than a given number of bad behaviors of a system: this, in the model-checking framework, means that one can verify the existence of a user-defined number of counterexamples for a given specification and generate them, in a unique run of the model-checker.
Here we show both theoretical and applicative contributions. On the theoretical side we give a simple algorithm to decide this logic, and we prove that the satisfiability problem is ExpTime -complete when the constants of the quantifiers are represented in unary. On the applicative side we propose symbolic algorithms to solve the model checking problem. One of the main characteristics of these algorithms is that, though the computation of "distinct" counterexamples has inherently high complexity when the model is represented symbolically, we have designed them to make the generation of multiple counterexamples as easy and quick as possible. The symbolic algorithms have been implemented using BDD data structures, and have been integrated into the well known NuSMV model checker, that has been modified to accept specifications expressed in graded-CTL. The test results we report are very comfortable in the sense that both the running time and the size of the BDDs produced are comparable to those obtained with specifications expressed in classical CTL.