A NuSMV Extension for Graded-CTL Model Checking

Graded-CTL is an extension of CTL with graded quantifiers which allow to reason about either at least or all but any number of possible futures. In this paper we show an extension of the NuSMV model-checker implementing symbolic algorithms for graded-CTL model checking. The implementation is based on the CUDD library, for BDDs and ADDs manipulation, and includes also an efficient algorithm for multiple counterexamples generation. 1 Description and Architecture In this paper we introduce a new model-checker which is an extension of NuSMV [CCG+ 02], an efficient and easy to extend re-implementation and integration of the SMV model-checker [McM93, CMCH96]. Our tool implements symbolic algorithms for graded-CTL model checking1 . Graded-CTL [FNP08, FNP09a] is an extension of CTL with graded quantifiers that allow to reason about either at least or all but any number of possible futures. For example, the formula E>k F(critic1 ∧ critic2) expresses that there are more than k possibiliti...

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Alessandro Ferrante, Maurizio Memoli, Margherita Napoli, Mimmo Parente, Francesco Sorrentino 0002
• Keywords: CAV 2010, Graded-CTL Model, Graded-CTL Model Checking, Hardware, Symbolic Algorithms