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;

Internals

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*.