"Multi-player Equilibria Verification for Concurrent Stochastic Gamess" - Supporting Material

Paper: "Multi-player Equilibria Verification for Concurrent Stochastic Games"
Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos

Models and Properties

Included below are the models and properties for case studies included in the paper. The models are concurrent stochastic games (CSGs) and the properties are rPTAL Nash formulae.

Unfortunately we cannot distribute the tool as it uses the COIN-OR Interior Point Optimizer IPOPT software package in combination with other third-party libraries including the HSL Mathematical Software Library which do not allow redistribution. We are at working on a solution to this issue and aim to incorporate the implementation into the next release of PRISM-games.

The log files from the experiments from the paper (Table 3) are available from here.

• Secret Sharing Protocol
  
  
  • Models: secret_sharing_aaa.prism (three altruistic agents), secret_sharing_raa.prism (one rational and two altruistic agents), secret_sharing_rba.prism (one rational, one byzantine and one altruistic agent), secret_sharing_rra.prism (two rational and one altruistic agent) and secret_sharing_rrr.prism (three rational)
  • Properties: secret_sharing.props
  • Parameters: alpha (coin bias), rmax (round counter)
  
  
• 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)
• Aloha
  
  
  • Models: aloha_backoff3.prism (three players), aloha_backoff4.prism (four players) and aloha_backoff5.prism (five players)
  • Properties: aloha_backoff3.props (three players), aloha_backoff4.props (four players) and aloha_backoff5.props (five players)
  • Parameters: bcmax (bound on backoff counter), q (probability of single user failing to transmit) and D (deadline)
  
  
• Medium Access Control
  
  
  • Models: medium_access3.prism (three player) and medium_access4.prism (four player)
  • Properties: medium_access3.props (three player) and medium_access4.props (four player)
  • Parameters: emax (maximum energy), q1 (probability of a successful transmission for a single user) and k (step bound)