Sciweavers

CAV
2010
Springer

A NuSMV Extension for Graded-CTL Model Checking

13 years 7 months ago
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...
Alessandro Ferrante, Maurizio Memoli, Margherita N
Added 17 Aug 2010
Updated 17 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Alessandro Ferrante, Maurizio Memoli, Margherita Napoli, Mimmo Parente, Francesco Sorrentino 0002
Comments (0)