Graded-CTL: Satisfiability and Symbolic Model Checking

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