PRISM language

a simple state-based language to write models to be checked by PRISM; also used by other tools
[action] guard -> prob_1 : update_1 + ... + prob_n : update_n;


based on the Reactive Modules formalism of Alur and Henzinger from 1999 Its property specification language which subsumes several probabilistic temporal logics including PCTL, CSL, probabilistic LTL and PCTL*.
Specification format


ProVerB specific

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