"Correlated Equilibria and Fairness in Concurrent Stochastic Games" - Supporting Material

Paper: "Correlated Equilibria and Fairness in 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 nonzero-sum formulae.

The log files from the experiments in the paper (Tables 1 and 2) are available from here.

• Aloha
  
  
  • Models: aloha_backoff5.prism (five players), aloha_backoff4.prism (four players),aloha_backoff3.prism (three players) and aloha_backoff2.prism (two players)
  • Properties: aloha5.props (four players), aloha4.props (four players), aloha3.props (three players) and aloha2.props (two players)
  • Parameters: bcmax (bound on backoff counter), q (probability of single user failing to transmit) and D (deadline)
  
  
• Power Control
  
  
  • Model: power_control3.prism (three players) and power_control2.prism (two players)
  • Properties: power_control3.props (three players) and power_control2.props (three players)
  • Parameters: powmax (maximum power level), emax (maximum energy), fail (failure probability) and k (step bound)
  
  
• Public Good Game
  
  
  • Models: public_good_game3.prism (three players), public_good_game4.prism (four players) and public_good_game5.prism (five players)
  • Properties: public_good_game3.props (three players), public_good_game4.props (four players) and public_good_game5.props (five players)
  • Parameters: kmax (number of rounds)
  
  
• Future markets investors
  
  
  • Models: three_investors.prism and two_investors.prism
  • Properties: three_investors.props and two_investors.props
  • Parameters: months (number of months)