PCTL Model Checking

Model Checking can be performed on non-parametric models with respect to the given PCTL formula expressing a property regarding the probability of an event to occur. The tool allows checking whether a given probability threshold is satisfied or find the probability of satisfaction for the given path formula. The Model Checking procedure is performed using an external tool called Storm. 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 stored in a .storm.check file. The text contains some details about Storm model checker performance. Finally, the boolean or numerical result can be found as Result (for initial states). Additionally, any errors Storm encountered are also shown in this file.

---

Command line arguments

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

Model checking

required arguments:
  --transition_file TRANSITION_FILE
  --output OUTPUT
  --formula FORMULA

optional arguments:
  --local_storm