"Automated Verification of Concurrent Stochastic Games" - Supporting Material

Paper: "Automated Verification of 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 paper. The models are concurrent stochastic games (CSGs), for which we have developed an extension of the probabilistic model checker PRISM-games for turn-based stochastic games (TSGs). A copy of this prototype is available below.

• Rock-paper-scissors example
  
  
  • Model: rps.prism
  • Properties: rps.props
  • Parameters: K (number of rounds)
  
  
• Future markets investors
  
  
  • Models (CSGs): investor_csg.prism and two_investors_csg.prism
  • Models (TSGs): investor_tsg.prism and two_investors_tsg.prism
  • Properties: investor.props and two_investors.props
  • Parameters: months (number of months)
  
  
• User-centric networks
  
  
  • Models: trust_csg.prism and trust_tsg.prism
  • Properties: trust_csg.props and trust_tsg.props
  • Parameters: k (number of services) and td (trust model)
  
  
• Intrusion detection system
  
  
  • Models: ids_scenario1.prism and ids_scenario2.prism
  • Properties: ids.props
  • Parameters: rounds (total number of rounds) and K (specific round)
  
  
• Jamming radio systems
  
  
  • Model: jamming.prism
  • Property: jamming.props
  • Parameters: slots (number of time slots)
  
  

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 examples above can be found in the examples-csg directory. Each directory also 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/rps/rps.prism examples-csg/rps/rps.props -const K=2