PV3 PRISM-gameschecks user-specified properties for stochastic multi-player games models

Probabilistic model checker for stochastic multi-player games

Application domain/field

Type of tool

Model checker

Expected input


Own format which is an extension of the PRISM format.


Extension of PRISM. PRISM-games supports several stochastic multi-player game models, including:
Model checking Probabilistic


Related papers

PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time

Last publication date

14 July 2020

ProVerB specific

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