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.

Other Probabilistic Model Checkers

General-purpose probilistic model checkers:
  • STORM - model checking for DTMCs, CTMCs, MDPs and Markov automata. See [DJKV17].
  • MRMC (formerly ETMCC) - explicit-state (and approximate) model checking for DTMCs, CTMCs and CTMDPs (with rewards) against PC(R)TL and CS(R)L. See [KZH+11].
  • The Modest Toolset - a collection of tools for modelling and analysis of hybrid, real-time, distributed and stochastic systems. See [HHHK13].
Specialist model checkers for particular models or techniques:
  • PARAM - parametric probabilistic model checking of DTMCs. See [HHWZ10].
  • INFAMY - model checking of infinite-state CTMCs. See [HHWZ09b].
  • ProbDiVinE - parallel and/or distributed LTL model checking of MDPs. See [BBC+08].
  • PASS - abstraction refinement of probabilistic models. See [HHWZ10b].
  • 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].
  • COMICS - model checking and generation of counterexamples for DTMCs. See [JAV+12].
  • PROPhESY - a tool for analyzing parametric Markov chains.
Approximate (statistical) probabilistic model checkers:
  • Ymer - approximate probabilistic model checking of generalized semi-Markov processes (GSMPs) and CTMCs against transient properties expressed in CSL. See [You05].
  • VESTA / PVeStA - 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].
Other tools with support for probabilistic model checking:
  • 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].
  • 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.
  • Marcie - tool for analyis of Generalised Stochastic Petri Nets (GSPNs) with extended arcs.
  • SMART - explicit-state/symbolic numerical solution (and CTL model checking) of Markov chains. See [CJMS06].
  • PAT - a model checking framework which includes support for probabilistic models. See [SLDP09].

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.