TACAS'12 Paper - Models and Properties

Paper: "Automatic Verification of Competitive Stochastic Systems"
by Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis

Included below are the models and properties for the four case studies mentioned in the paper. The models are stochastic multi-player games, for which we have developed PRISM-games, an extension of the probabilistic model checker PRISM.

• mdsm: Microgrid Demand-Side Management [HS11]
  
  
  • Sample model: mdsm7304.prism
  • Sample properties: mdsm.props
  • Zip of all files: mdsm.tar.gz
  • Parameters:
    • N (number of households: 2, 3, ..., 7)
  
  
• cdmsn: Collective Decision Making for Sensor Networks [SS11]
  
  
  • Sample model: cdm5032.prism
  • Sample properties: cdm.props
  • Zip of all files: cdm.tar.gz
  • Parameters:
    • N (number of sensors: 3, 4, 5)
  
  
• investor: Future Markets Investor [MM07]
  
  
  • Model: investor.prism
  • Properties: investor.props
  • Parameters:
    • vmax (maximum share value: 10, 100, 200)
    • vinit (initial share value: fixed at 5)
  
  
• team-form: Team Formation Protocol [CKPS11, GdJ05]
  
  
  • Model: team_formation.prism
  • Properties: team_formation.props
  • Parameters:
    • N (number of agents: 3, 4, 5)