A Catalog of Tools for the Quantitative Zoo
A Catalog of Tools for the Quantitative Zoo


1. Motivation

This page is intended to scientists interested in complex systems, the behaviour of which combines discrete aspects (namely, states and transitions) and continuous features (e.g., time, delays, probabilities, continuous laws, etc.).

A number of models, logics, and tools have been developed for modelling and verifying such systems. The expression "quantitative zoo" was coined by Hartmanns and Hermanns [1] to characterize the abundance and diversity of probabilistic, stochastic, timed, and hybrid models found in the scientific literature. This page tries to give an overview of software tools for the zoo.

2. List of Tools

The color codes of the status column have the following meaning:

If not empty, the "supported logics" column means that a tool has model-checking capabilities and can evaluate formulas written in the corresponding logic(s).

# tool and university version and status supported models supported logics
1 APAC - Rennes 2011 - not available - follow-up version implemented in the ECDAR tool constraint MC, abstract PA  
2 APHzip - Saarbrücken 2008-2015 CTMC (acyclic phase-type distributions)  
3 APMC, APMC-CA - Paris version 3.0 (APMC: 2006 APMC-CA: 2008) - not available    
4 APNN - Dortmund 2001 - not available CTMC CTL, LTL
5 Bluemoon - Cordoba (Argentina) version 1.0 (2015) - module for the PRISM tool CTMC, DTMC CSL, PCTL
6 CADP - Grenoble version 2017-f (2017) CTMC, DTMC, deterministic IMC, LTS, PTS modal mu-calculus, MCL
7 CASPA - Munich 2009    
8 COMICS - Aachen version 1.0.0 (2010) DTMC PCTL
9 Cosmos - Cachan, Paris, Nancy version 1.0 (2011) HA HASL
10 DDP - Austin (Texas) 2011 - based on Excel spreadsheets CMRM, CTMC, DMRM, DTMC CSL, CSRL, PCTL, PRCTL
11 DiPro - Konstanz version 1.0.0 (2008, 2011) - relies on PRISM 3.3.1 or MRMC 1.4.1 CTMC, DTMC, MDP CSL, PCTL
12 DNAmaca/Hydra - Edinburgh, London 2005 HMM, MC, MDP, SMC, SMDP Conditions specified in the model file
13 DTMCPack version 0.1-2 (2013) - provided as an R package finite DTMC  
14 ECDAR - Aalborg, Copenhagen, Rennes version 0.10 (2013) - follow-up version implemented in the PyECDAR and UPPAAL-TIGA tools TA  
15 EMPEPA - Toulouse version 0.9.3 (2006) - not maintained PEPA  
16 ETMCC - Erlangen, Twente version 1.4 (2003) - not available - follow-up version implemented in the MRMC tool CTMC ACSL, CSL, (PCTL)
17 FACT - York version 1910 (2016) - requires PRISM and Matlab with the YALMIP toolbox IDTMC, IMDP, MC, pMC, UMC PCTL
18 FHP-Murphi - Rome version 5.4.9.1 (2003-2012) - not maintained - now included in CMurphi, relies on Murphi infinite-state DTMC reachability and safety properties
19 FIG - Cordoba (Argentina) version 1.1 (2017) CTMC, IOSTA, (DTMC available soon) CTL subsets (available soon)
20 FlowSim - Saarbrücken 2008-2009 - not maintained MC, PA  
21 Fortuna - Nijmegen version 0.2 (2009) - not maintained PPTA, PTA  
22 GPAnalyser - London version 0.9.1 (2011) - not maintained GPEPA  
23 GreatSPN - Torino, Alessandria version 2.0.2 (1995) GSPN  
24 GRIP - Glasgow version 1.0.0 (2014) - a companion tool for PRISM symmetric PRISM model: CMRM, DTMC, CTMC, CTMDP, DMRM, MDP symmetric properties in CSL, LTL, PCTL, PCTL*
25 HSolver - Prague, Saarbrücken version 3.5a (2005-2014) - constraint solver RSOLVER HA  
26 HTK - Cambridge version 3.4.1 stable or 3.5 beta (2000-2016) HMM  
27 HyTech - Berkeley (California) version 1.04f (1996-2003) - not maintained linear HA  
28 IMCA - Aachen version 1.6 beta (2010-2014) CTMDP, IMC, IPC  
29 Imperial PEPA Compiler - London, Edinburgh version 0.99 (2007) - not maintained - can be used with DNAmaca MC, PEPA, SMC  
30 INFAMY - Saarbrücken version 1.0 (2009) - not maintained CTMC  
31 IscasMC - Beijing version alpha (2014-2017) CTMC, DTMC, MC, MDP PCTL, PCTL*, PLTL
32 Kronos - Grenoble version 2.5i (2002) - not maintained TA TCTL
33 LiQUOR - Bonn 2006 - not available MDP (specified in Probmela) PLTL
34 MAMA - Twente 2013 - web tool based on IMCA and SCOOP DTMC, GSPN, MA, MAPA, PA  
35 MAMOT - Lausanne version 1.0.0 (2008) - not maintained HMM  
36 MARCA - Raleigh (North Carolina) version 3.0.0 (1996) - not available CTMC, DTMC  
37 markovchain version 0.6.9.6 (2017) - provided as an R package DTMC  
38 MC4CSLTA - Torino version 3.0 (2014) - uses GreatSPN CTMC, DTA, GSPN CSLTA
39 Modest - Saarbrücken version 3.0 beta 1 (2014) CTMC, DTMC, IMC, LTS, MA, MDP, PA, PTA, SHA, STA, TA PCTL, CSL
40 Moebius - Urbana-Champaign (Illinois) version 2.5 (2014) MP, PEPA, SPN, SPA, SAN  
41 MoToR - Twente 2007 - not available - follow-up version implemented in the Moebius and Modest tools    
42 MRMC - Aachen version 1.5 (2011) - follow-up version implemented in the Storm tool CMRM, CTMC, CTMDP, DMRM, DTMC, MRM CSL, CSRL, PCTL, PRCTL
43 MRM Solve - Budapest version 2 release 0.91 (2006) - not maintained CTMC  
44 PARAM - Saarbrücken version 2.3 (2010) - not maintained - follow-up version implemented in the PROPhESY, PRISM, and IscasMC tools DTMC, MDP  
45 PASS - Saarbrücken, Oxford version 1.0.0 (2010) - not maintained MDP PCTL
46 PAT - Singapore version 3.5.1 (2007-2014) LTS, MDP, PTA assertions (Spec# and Code Contracts), LTL
47 PEPA Eclipse Plug-in - Edinburgh version v25 (2014) PEPA CSL
48 PHAVer - Grenoble version 0.38 (2007) HA  
49 Plasma-Lab - Rennes version 1.4.0 (2016) CTMC, DTMC, MDP, SMC BLTL
50 PMaude - Urbana-Champaign (Illinois) 2006 - Maude probabilistic actors QUATEX
51 PRINSYS - Aachen 2012-2014 pMDP, MA  
52 PRISM - Glasgow, Oxford version 4.8.1 (2024) CTMC, DTMC, MDP, PA, PEPA, PPTA, PTA CSL, LTL, PCTL, PCTL*
53 ProbDIVINE - Brno 2009 - not maintained    
54 ProbVerus - Belo Horizonte, Pittsburg 1999 - not available Verus language PCTL
55 ProHVer - Saarbrücken 2010 - not maintained - relies on PHAVer HA, PHA assertions
56 PROPhESY - Aachen 2015 - relies on PRISM pMC, DTMC, CTMC, MDP, PA PTA PCTL, PCTL*
57 ProVer - Urbana-Champaign (Illinois) version 1.1 (2002) - not maintained - follow-up version implemented in the Ymer tool GSMP (in SPDL language) CSL
58 PVeStA - Urbana-Champaign (Illinois) 2011 CTMC, DTMC CSL, PCTL, QUATEX
59 PyECDAR - Rennes version 2.1 (2013) - follow-up version implemented in the ECDAR and UPPAAL-TIGA tools TA  
60 Rapture - Rennes, Cordoba (Argentina), Aalborg version 2.0.0 (2010) - not maintained MDP subset of PCTL
61 SCOOP - Twente 2013 - relies on LTSmin, connected to IMCA CTMC, DTMC, IMC, MA, MDP, PA  
62 Sharpe - Durham (North Carolina) 2011-2017 GSPN, MC, SMC  
63 SiSAT - Oldenburg 2011 - not available    
64 SmArT - Ames (Iowa) version 1.1 (2009) - not available SPN, queuing networks  
65 STAMINA - Logan (Utah) version 1.0.0 (2019) CTMC CSL
66 Storm - Aachen version 1.8.0 (2023) cpCGL, CTMC, DFT, DTMC, GSPN, LTS, MA, MDP, pDTMC, pMDP, SPN CSL, PCTL
67 TIMES - Uppsala version 1.3 beta (build 2461) (2003-2008) - not maintained - uses UPPAAL TA extended with tasks subset of TCTL
68 TIPPtool - Erlangen-Nuremberg, Twente version 2.3 (2000) - not available    
69 TwoTowers - Urbino version 5.1 (2006) - not maintained - relies on nuSMV 2.2.5 MC, SPA (in Aemilia language) LTL
70 UPPAAL - Aalborg, Uppsala version 4.0.13 (2010) TA subset of TCTL
71 UPPAAL-PRO - Aalborg 1994-2000 - not available PTA  
72 UPPAAL Tiga - Aalborg version 0.18 (2014) - not maintained    
73 Verus - Pittsburg version 0.9 (1997) - not maintained Verus language CTL, RTCTL
74 VeStA - Urbana-Champaign (Illinois) version 2 (2005) - not available - follow-up version implemented in the PVeStA tool CTMC, DTMC  
75 Ymer - Pittsburgh (Pennsylvania) version 4.2.1 (2002-2016) - relies on Cudd and PRISM hybrid engine CTMC, DTMC, time-homogeneous GSMP CSL, PCTL

3. List of Models

4. List of Logics

5. Credits - History of Versions

Version 1.1 of this page (July 2017) has been prepared by Jean-Philippe Gros, Julie Parreaux, and Hubert Garavel. Its contents have been partly derived from [2] and [3].

Version 1.2 of this page (August 2017) was enhanced by Hubert Garavel based upon the feedback provided by Holger Hermanns.

Version 1.3 of this page (February 2019) was enriched with the STAMINA tool entry communicated by Zhen Zhang.

6. Updates - Future Enhancements

We do not claim that the above lists are exhaustive. The page is primarily oriented toward academic tools rather than commercial ones. Tools dealing with fault-tree models are not well covered, and tools dealing with Bayesian networks are purposely left out.

Additions, corrections, and updates are welcome. Please, send them to hubert.garavel@inria.fr.

The HTML tables of this page have been generated automatically from various ad hoc databases. So, do not try to patch the HTML code itself, but rather describe changes that should be brought to the contents of this page.

It is feasible to attach more information to each tool. This can be done by adding extra attributes in the tool data base, resulting in extra columns in the tool HTML table. Examples of useful attributes would be: the meaning of the tool name if it is an acronym, the complete list of authors, their exact affiliations, the reference scientific papers, the supported hardware/software platforms, the kind of software license, the core functionalities beyond model checking (e.g., steady-state/transient analyzes, simulation, etc.), the possibility of having concurrency and/or variables in the input models, the supported input and output formats, the existence of a graphical user-interface, the known limitations of the tool, etc.

The same idea also applies to the models and logics. For instance, one could associate to each model or logic, the reference scientific papers where this model or logic was defined.

If you are willing to contribute to this page (this could take the form of bibliographic survey projects assigned to students), please contact hubert.garavel@inria.fr.

References

[1] Arnd Hartmanns and Holger Hermanns. In the Quantitative Automata Zoo. Science of Computer Programming, vol. 112, pp. 3-23, 2015.

[2] Jean-Philippe Gros. A unifying framework for comparing and implementing probabilistic models. Master thesis, Univ. Grenoble Alpes (MOSIG), June 2017.

[3] Julie Parreaux. Panorama des modèles et outils de vérification pour les systèmes probabilistes. Bachelor thesis, Univ. Rennes I and ENS Rennes, prepared at INRIA Grenoble, July 2017.

Version 1.4 last updated on 2024/07/22 15:31:13

Back to the CADP Home Page