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 in [FNP08]. 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 the computation of `distinct` counterexamples has inherently high complexity when the model is represented symbolically (consider for example the implementation of a symbolic DFS), we have designed them to make the generation of multiple counterexamples as easy and quick as possible. The symbolic algorithms have also been implemented using BDD data structures, and have been integrated into the well known NuSMV model checker, that has also been modified to accept specifications expressed in graded-CTL. The test results we have reported are very comfortable in the sense that both the running time and the sizes of the BDD produced are comparable to those obtained with specifications expressed in classical CTL.
Graded-CTL: Satisfiability and Symbolic Model Checking
Ferrante, Alessandro;
2009-01-01
Abstract
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 in [FNP08]. 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 the computation of `distinct` counterexamples has inherently high complexity when the model is represented symbolically (consider for example the implementation of a symbolic DFS), we have designed them to make the generation of multiple counterexamples as easy and quick as possible. The symbolic algorithms have also been implemented using BDD data structures, and have been integrated into the well known NuSMV model checker, that has also been modified to accept specifications expressed in graded-CTL. The test results we have reported are very comfortable in the sense that both the running time and the sizes of the BDD produced are comparable to those obtained with specifications expressed in classical CTL.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
