www.prismmodelchecker.org

Other Tools

Below is a brief summary of some other available tools with support for probabilistic model checking, including those that connect to or integrate PRISM. If we have omitted your tool or the description is incorrect, please contact us.

Probabilistic Model Checkers

Model checkers for discrete-/continuous-time Markov chains (DTMCs/CTMCs) and extensions of:
  • 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 [KZH+11].
  • 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].
  • PARAM - parametric probabilistic model checking of DTMCs. See [HHWZ10].
  • INFAMY - model checking of infinite-state CTMCs. See [HHWZ09b].
  • CASPA - symbolic (MTBDD-based) model checking of (extended) stochastic labelled transition systems against Stochastic Propositional Dynamic Logic (SPDL). See [RSS08].
Model checkers for Markov decision processes (MDPs):
  • LiQuor - explicit-state model checking of MDPs, expressed in Probmela (a probabilistic extension of SPIN's Promela language), against LTL. See [CB06b].
  • ProbDiVinE - parallel and/or distributed LTL model checking of MDPs. See [BBC+08].
  • PASS - abstraction refinement of probabilistic models. See [HHWZ10b].
  • RAPTURE - implementation of the MDP-based abstraction-refinement technique described in [DJJL01]. See [JDL02].
Model checkers for probabilistic timed automata (PTAs):
  • mcpta - supports a subset of the modelling language Modest via translation to PRISM. See [HH09].
  • Fortuna - computes maximum probabilistic reachability properties for PTAs and reward-bounds properties for (linearly) priced PTAs. See [BJV10].
  • UPPAAL-PRO - computes maximum probabilistic reachability properties for PTAs.
Approximate (statistical) probabilistic model checkers:
  • 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].
  • PRISM-U2B - extension of PRISM for approximate model checking of unbounded properties. See [BGH09].
  • COSMOS - statistical model checking for HASL (Hybrid Automata Stochastic Logic) on discrete event stochastic processes (DESPs). See [BDD+11].
  • PLASMA - is a statistical model checking platform for a range of stochastic models. See [JLS12].

Tools Connecting to or Integrating PRISM

  • Infobiotics Workbench - tool for computational systems and synthetic biology. Integrates PRISM.
  • kamiframework - run-time modelling and anlaysis of software designs. Integrates PRISM.
  • Snoopy - Petri net-based tool for analysis of biomolecular networks. Exports to PRISM. See [RMH10].
  • Henshin Statespace Explorer - part of the Eclipse Modeling Framework Project.
  • PSPWizard - generates temporal logic properties from patterns for several tools, including PRISM. See [LMG11].

See also the connections listed here.

Other related tools

  • APNN-Toolbox - a Petri Net tool-set, that includes support for CTMCs and CSL model checking. See [BK99].
  • CADP - "Construction and Analysis of Distributed Processes" toolset, with some support for probabilistic models.
  • GreatSPN analysis of Generalised Stochastic Petri Nets (GSPNs) and extensions.
  • GRIP - language-level symmetry reduction for PRISM models.
  • ipc/DNAmaca - tool extending PEPA's modelling capability with additional performability measures.
  • Marcie - tool for analyis of Generalised Stochastic Petri Nets (GSPNs) with extended arcs.
  • Möbius - multi-formalism modelling and analysis toolset for stochastic systems.
  • MOTOR - tool environment for the MODEST language. See [BHK07].
  • SMART - explicit-state/symbolic numerical solution (and CTL model checking) of Markov chains. See [CJMS06].
  • COMICS - model checking and generation of counterexamples for DTMCs. See [JAV+12].
  • DiPro - a directed probabilistic counterexample generation tool. See [ALLS11].
  • PAT - a model checking framework which includes support for probabilistic models. See [SLDP09].

About PRISM