Graded-CTL NuSMV

Graded-CTL NuSMV is an integration of the NuSMV tool that allows to model check formulas expressed in graded-CTL, as defined in the paper CTL Model-Checking with Graded Quantifiers [FNP08].

To integrate our symbolic graded-CTL model-checking algorithm into NuSMV, we had to modify some parts of the original packages and insert a new package for the symbolic algorithm for the graded-CTL model checking.

1. Modifications: We have modified the NuSMV parser to recognize specifications in graded-CTL by adding the token GRADCTLSPEC and a syntax to specify graded-CTL formulas. The syntax used in the tool to express graded-CTL formulas is shown in the following table:
   
   

   Graded-CTL Formula Graded-CTL 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	Graded-CTL Formula Graded-CTL 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

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