PV3 PRISMmodel checker for probabilistic timed automata

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

Application domain/field

Type of tool

Probabilistic model checker

Expected input

Format:

PRISM language

Internals

PRISM can be used to analyse many different types of probabilistic models, including: 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:

Comments

Along with the tool, there also exists a PRISM language.
Automaton Model checking Probabilistic

Links

Related papers

Related tools

PRISM-PSY, PRISM-games

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.