GradedCTL NuSMV
Home Page
GradedCTL NuSMV is an integration of the NuSMV tool that
allows to model check formulas expressed in gradedCTL, as defined
in the paper CTL ModelChecking with Graded Quantifiers
[FNP08].
To integrate our symbolic gradedCTL modelchecking algorithm into NuSMV, we had to modify some parts of the original packages and insert a new package for the symbolic algorithm for the gradedCTL model checking.

Modifications: We have modified the NuSMV parser to recognize specifications in
gradedCTL by adding the token GRADCTLSPEC and a syntax to specify gradedCTL formulas.
The syntax used in the tool to express gradedCTL formulas is shown in the following
table:
GradedCTL Formula GradedCTL NuSMV Syntax E>k X ψ1 EX k ψ1 E>k ψ1 U ψ2 E k ψ1 U ψ2 E>k G ψ1 EG k ψ1 E>k F ψ1 EF k ψ1 GradedCTL Formula GradedCTL NuSMV Syntax A≤k X ψ1 AX k ψ1 A≤k ψ1 U ψ2 A k ψ1 U ψ2 A≤k G ψ1 AX k ψ1 A≤k F ψ1 AF k ψ1

New Packages: We have introduced a new package called Graded where we have implemented our algorithms and utility
functions that we use in the implementation of the model checking algorithm. You can find the details about this package
here