PV3 ⊧ Stormcomputes how a given property is related to a given specification

Application domain/field

• Probabilistic model checking
• Model checking

Type of tool

Probabilistic model checker

Expected input

• Input model:
• DTMCs (discrete time Markov chains)
• CTMCs (continuous time Markov chains)
• MDPs (Markov decision processes)
• GSPN (generalised stochastic Petri nets)
• DFTs (dynamic fault trees)
• cpGCL (conditional probabilistic guarded command language) program
• Explicit model

• Quantitative specification:
• PCTL (probabilistic computation tree logic, for discrete-time models)
• CSL (continuous stochastic logic, for continuous-time models)
• Extensions of the abovementioned logics: Expected rewards, long-run average rewards, conditional probabilities and multi-objective model checking

Format:

Storm supports many different input formats:

• Input model:
• PRISM for DTMCs, CTMCs and MDPs
• JANI for DTMCs, CTMCs and MDPs
• PNML or GreatSPN for GSPNs
• Galileo format for DFTs
• cpGCL
• Explicit format
• Specification:
• "Extended subset" of the PRISM property language
• Embedded in the JANI model

Expected output

Depends on the property. It can give the probability of a certain outcome, but also whether a property is true or false. It will also give information about the model such as the number of states and transitions.

Internals

It uses the following solvers: Eigen, gmm++, CUDD, Sylvan, Gurobi, GLPK, Z3, MathSAT, SMT-LIB

Comments

There is also a fuzzer that is called STORM.