Paper:
"Verification and Control of Turn-Based Probabilistic Real-Time Games"
Marta Kwiatkowska, Gethin Norman and David Parker
Included below are the models and properties for the case studies included in the submission. We include PRISM models representing the turn-based probabilistic real-time games (TPTGs), the corresponding digital clocks models both when represented as as a turn-based stochastic game (TSG) and as a Markov decision process (MDP), as well as the corresponding properties. That digital clocks MDP models are constructed automatically by PRISM (using the exportdigital switch by specifying the TPTG models to be PTAs) and the TSG models are then constructed by editing the MDP models. For deadline properties an extra clock and module is added to the model and the property is modified. For PTAs this is automated in PRISM, here we follow this construct.
The TSG models require PRISM-games an extension of PRISM for the verification of probabilistic systems that can incorporate competitive or collaborative behaviour, modelled as (turn-based) stochastic multi-player games.