"Automatic Verification of Concurrent Stochastic Systems" - Supporting Material

Paper: "Automatic Verification of Concurrent Stochastic Systems"
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. The PRISM-games website has details on the modelling language for CSGs, specification language and how to install the tool. More details on the case studies can be found here.

• Robot coordination
  
  
  • Model: robot_coordination2.prism
  • Properties: robot_coordination2.props
  • Parameters: l (grid size), q (probability robot moves in the wrong direction) and k1,k2 (step bounds)
  
  
• Future markets investors
  
  
  • Models (CSGs): two_investors_csg.prism and two_investors_nash.prism
  • Models (TSGs): two_investors_tsg.prism
  • Properties: two_investors.props and two_investors_nash.props
  • Parameters: months (number of months)
  
  
• User-centric networks
  
  
  • Models: user-centric.prism
  • Properties: user-centric.props
  • Parameters: k (number of services) and td (trust model)
  
  
• 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_access2.prism (two players), medium_access_count2.prism (two players), medium_access3.prism (three players) and medium_access_count3.prism (three players)
  • Properties: medium_access2.props (two players), medium_access_count2.props (two players), medium_access3.props (three players) and medium_access_count3.props (three players)
  • Parameters: emax (maximum energy), q1 (probability of a successful transmission for single user), q2 (probability of a successful transmission for two users), q3 (probability of a successful transmission for three users), smax (number of messages to send) and k1,k2 (step bounds)
  
  
• Power control
  
  
  • Model: power_control.prism
  • Properties: power_control.props
  • Parameters: powmax (maximum power level), emax (maximum energy), fail (failure probability) and k1,k2 (step bounds)
  
  
• Intrusion detection system
  
  
  • Models: ids_scenarios.prism
  • Properties: ids.props
  • Parameters: scenario (which scenario to model), rounds (total number of rounds) and K (specific round)
  
  
• Jamming radio systems
  
  
  • Model: jamming.prism
  • Property: jamming.props
  • Parameters: slots (number of time slots)
  
  

A tar.gz archive of the log files from the experiments are available from here and an archive of the bimatrix games used in Section 6.2 of the paper (together with the log files) from here.