Sciweavers

Share
ICFEM
2009
Springer

Graded-CTL: Satisfiability and Symbolic Model Checking

8 years 6 months ago
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 theoretica...
Alessandro Ferrante, Margherita Napoli, Mimmo Pare
Added 19 Feb 2011
Updated 19 Feb 2011
Type Journal
Year 2009
Where ICFEM
Authors Alessandro Ferrante, Margherita Napoli, Mimmo Parente
Comments (0)
books