PRISM
PRISM
Description: PRISM is a probabilistic model checker, a tool for formal modeling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others.
PRISM can build and analyse several types of probabilistic models:
- discrete-time Markov chains (DTMCs)
- continuous-time Markov chains (CTMCs)
- Markov decision processes (MDPs)
- probabilistic automata (PAs)
- probabilistic timed automata (PTAs)
plus extensions of these models with costs and rewards.
VO Integration: No
Active: No
Available Benchmarks: Case studies can be found here.
Website: http://www.prismmodelchecker.org/
Download: Link
Documentation: Links to documentation, manual, and a tutorial.
Contact: Link to list of contributors.
Excerpt and graphics from: http://www.prismmodelchecker.org/
Backlinks:
- Validation and Verification
- Tool
- Free
- Own interface
- Own language
- Linux
- Mac OS X
- Windows
- Continuous-time Markov chains
- Discrete-time Markov chains
- Discrete/continuous and deterministic/nondeterministic probabilistic models
- Markov decision processes
- Probabilistic automata
- Probabilistic timed automata
- Quantitative abstraction refinement
- Guaranteed to terminate
- Probabilistic model checking