"Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games" - Supporting Material

Paper: "Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games"
Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos

Models and Properties

Included below are the models and properties for the examples and case studies included in the submission. The models are concurrent stochastic games (CSGs) and the properties are rPTAL Nash formulae. A copy of this prototype is available below.

• Robot coordination
  
  
  • Model: robot_coordination.prism
  • Properties: robot_coordination.props
  • Parameters: l (grid size), q (probability robot moves in the wrong direction) and k (step bound)
  
  
• Aloha
  
  
  • Models: aloha_backoff3.prism (three players) and aloha_backoff2.prism (two players)
  • Properties: aloha_backoff3.props (three players) and aloha_backoff2.props (two players)
  • Parameters: bcmax (bound on backoff counter), q (probability of single user failing to transmit) and D (deadline)
  
  
• Medium access control
  
  
  • Models: medium_access_example2.prism, medium_access.prism and medium_access_count.prism
  • Properties: medium_access.props and medium_access_count.props
  • Parameters: emax (maximum energy), q1 (probability of a successful transmission for single user), q2 (probability of a successful transmission for two users), smax (number of messages to send) and k (step bound)
  
  
• Power Control
  
  
  • Model: power_control.prism
  • Properties: power_control.props
  • Parameters: powmax (maximum power level), emax (maximum energy), fail (failure probability) and k (step bound)
  
  

The Tool

A source code release of our prototype tool is available here: https://gitlab.com/prismmodelchecker/prism-games-csg.

This can be built in exactly the same way as normal versions of PRISM. See the installation instructions.

The case studies above can be found in the examples-csg/nash/ directory. The directory has an auto.sh script, showing how the examples run.

Here is an example of how to build the distribution and run an example:

git clone https://gitlab.com/prismmodelchecker/prism-games-csg
cd prism-games-csg/prism
make
bin/prism examples-csg/nash/robot_coordination.prism examples-csg/nash/robot_coordination.props -prop 2 -const q=0.1,l=4,k=3

Note: the syntax of the model language for CSGs and the model checking implementation have been updated in the prototype from that used in the case studies and experimental results section of the paper. This version of the prototype, including the model and property files and a logs directory containing the experiments from the paper (Table 1), is available from here.