Thesis: Automatic Verification and Strategy Synthesis for Zero-sum and Equilibria Properties of Concurrent Stochastic Games

Case Studies

Thesis: "Automatic Verification and Strategy Synthesis for Zero-sum and Equilibria Properties of Concurrent Stochastic Games"
Author: Gabriel Santos

Included below are the models and properties used to generate experimental results for the case studies in the thesis. The models follow the syntax of CSG models for the PRISM-games tool. More details about the case studies can be found here.

Case Studies

• Robot Coordination []
  
  
  • Model: .prism
  • Parameters:
    • ? (?)
    Other constants (fixed):
    • ? (?)
    • ? (?)
  
  
• Secret Sharing []
  
  
  • Model: .prism
  • Parameters:
    • ? (?)
  
  
• Future Market Investors [MM07, KNPS18]
  
  
  • Model: .prism
  • Parameters:
    • ? (?)
  
  
• Trust Models for User-centric Networks [KNPS13, KNPS18]
  
  
  • Model: .prism
  • Parameters:
    • ? (?)
  
  
• Aloha Protocol []
  
  
  • Model: .prism
  • Properties: .props
  • Parameters:
    • ? (?)
    • ? (?)
  
  
• Public Good []
  
  
  • Model: .prism
  • Properties: .props
  • Parameters:
    • ? (?)
    • ? (?)

• Medium Access Control []
  
  
  • Model: .prism (?)
  • Model: .prism (?)
  • Properties: .props
  
  
• Power Control []
  
  
  • Model: .prism
  • Properties: .props
  • Parameters:
    • ? (?)
    • ? (?)
  
  
• Intrusion Detection Policies []
  
  
  • Model: .prism
  • Properties: .props
  • Parameters:
    • ? (?)
  
  
• Jamming Multi-channel Radio Systems []
  
  
  • Model: .prism
  • Model: .prism
  • Properties: .props
  • Parameters:
    • ? (?)