PV3 ⊧ PRISMmodel checker for probabilistic timed automata

Probabilistic model checker, specifically for quantitative verification of (priced) probabilistic timed automata

Application domain/field

• Model checking
• Probabilistic model checking
• Symbolic model checking
• Probabilistic timed automata

Type of tool

Probabilistic model checker

Expected input

• Model (e.g. a probabilistic automata)
• Property to check (e.g. "what is the probability of a failure causing the system to shut down within 4 hours?")

Format:

PRISM language

Internals

PRISM can be used to analyse many different types of probabilistic models, including:

• Discrete-time Markov chains (DTMCs)
• Continuous-time Markov chain (CTMCs)
• Markov decision processes (MDPs)
• Probabilistic automata (PAs)
• Probabilistic timed automata (PTAs)
• Partially observable Markov decision processes (POMDPs)
• Partially observable probabilistic timed automata (POPTAs)

Such models can be used to analyse systems from domains such as communication protocols, randomised distributed algorithms, security protocols and biological systems. It includes several different techniques that can be used to analyse systems, including:

• Approximate/statistical model checking
• Quantitative abstraction refinement
• Symmetry reduction

Comments

Along with the tool, there also exists a PRISM language.