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...

• Type: Journal
• Year: 2009
• Where: ICFEM
• Authors: Alessandro Ferrante, Margherita Napoli, Mimmo Parente
• Keywords: Algorithms, ICFEM 2009, Software Engineering, Specifications, Symbolic Algorithms