TACAS'14 Case Studies

Paper: "Permissive Controller Synthesis for Probabilistic Systems"
by Klaus Draeger, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma.

Included below are all models and properties used to generate experimental results in the paper. The models are in the format for the PRISM-games tool. Generation of multi-strategies for the properties given below, as discussed in the paper, currently requires an extension of PRISM-games, which will be made publicly available in due course.

• cloud: Cloud service deployment ([CKJ12])
  
  
  • Model: cloud_steering_vm_5.prism (2 servers, 5 virtual machines)
  • Model: cloud_steering_vm_6.prism (2 servers, 6 virtual machines)
  • Properties: cloud.props
  
  
• android: Android stock monitoring examples
  
  
  • Model: android_3.prism
  • Properties: android.props
  • Parameters:
    • r (number of retries)
    • s (stock to query)
  
  
• mdsm: Microgrid Demand-Side Management ([CFK+12])
  
  
  • Model: mdsm3304.prism
  • Properties: mdsm3304.props
  • Parameters:
    • N (number of households: 3)
  
  
• 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-form-offline-fc-3.prism
  • Model: team-form-offline-fc-4.prism
  • Properties: team-form.props
  • Parameters:
    • N (number of agents: 3, 4, 5)
  
  
• cdmsn: Collective Decision Making for Sensor Networks [SS11]
  
  
  • Model: cdm3032.prism
  • Properties: cdmsn3032-runtime.props
  • Parameters:
    • N (number of sensors: 3, 4, 5)