Other Tools for Probabilistic Model Checking

Below is a brief summary of other available tools for probabilistic model checking. If we have omitted your tool or the description is incorrect, please contact us.

• LiQuor - explicit-state model checking of MDPs, expressed in Probmela (a probabilistic extension of SPIN's Promela language), against LTL. See [CB06b].
  
  
• RAPTURE - implementation of the MDP-based abstraction-refinement technique described in [DJJL01]. See [JDL02]
  
  
• ProbDiVinE - parallel and/or distributed LTL model checking of MDPs. See [BBC+08]

• MRMC (formerly ETMCC) - explicit-state (and approximate) model checking for DTMCs, CTMCs and CTMDPs (with rewards) against PC(R)TL and CS(R)L. Also support for bisimulation. See [KHH+09].
  
  
• The PEPA Eclipse Plug-in project - CSL model checking (plus steady-state/ODE analysis and abstraction techniques) for the stochastic process algebra PEPA. See [Tri07].
  
  
• CASPA - symbolic (MTBDD-based) model checking of (extended) stochastic labelled transition systems against Stochastic Propositional Dynamic Logic (SPDL). See [RSS08].

• APMC - distributed approximate model checking for DTMCs and CTMCs. See [GHLP05].
  
  
• Ymer (formerly ProVer) - approximate probabilistic model checking of generalized semi-Markov processes (GSMPs) and CTMCs against transient properties expressed in CSL. See [You05].
  
  
• VESTA - approximate model checking of PCTL/CSL (and more) for probabilistic systems. See [SVA05].

• CADP
  
  
• Möbius

• MOTOR - tool environment for the MODEST language. See [BHK07].
  
  
• SMART - explicit-state/symbolic numerical solution (and CTL model checking) of Markov chains. See [CJMS06].
  
  
• APNN-Toolbox - a Petri Net tool-set, that includes support for CTMCs and CSL model checking. See [BK99].
  
  
• GreatSPN analysis of Generalized Stochastic Petri Nets (GSPNs) and extensions.
  
  
• GRIP - language-level symmetry reduction for PRISM models.
  
  
• ipc/DNAmaca