Skip to content

CTL Model Checking

Jump to bottom
Matej Troják edited this page Mar 24, 2022 · 2 revisions

CTL model Checking can be performed on \emph{non}-parametric models with respect to the given CTL formula. The Model Checking procedure is performed using a package called pyModelChecking. A step by step Galaxy tour showing how to use the tool can be found here.

Input specification

  • TS file: Generated transition system for the desired model (computed using Transition System generator)

  • PCTL formula: Given formula expressing property to be checked on the transition system of the given model.

Output specification

The textual result is stored in a .ctl.check file. The text contains number of states satisfying the formula and the boolean value for the initial state.

Command line arguments

usage: CTLModelChecking.py [-h] --transition_file TRANSITION_FILE 
                                 --output OUTPUT 
                                 --formula FORMULA 

Model checking

required arguments:
  --transition_file TRANSITION_FILE
  --output OUTPUT 
  --formula FORMULA
Clone this wiki locally