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

Probabilistic model checker for stochastic multi-player games

Application domain/field

• Model checking
• Symbolic model checking
• Probabilistic model checking
• Stochastic systems

Type of tool

Model checker

Expected input

• Model
• Property/properties to check

Format:

Own format which is an extension of the PRISM format.

Internals

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

• Turn-based stochastic multi-player games (SMGs or TSGs)
• Concurrent stochastic multi-player games (CSGs)
• (Turn-based) probabilistic timed games (TPTGs)