ATVA'12 Case Studies

Paper: "Pareto Curves for Probabilistic Model Checking"
by Vojtěch Forejt, Marta Kwiatkowska and David Parker.

Included below are all models and properties used to generate experimental results in the paper. Models are in standard PRISM format and can be analysed with the default version of PRISM. Properties currently require the "prism-multi" extension of PRISM (which will be made publicly available in due course) and are provided for information only.

• Randomised consensus protocol (algorithm from [AH90])
  
  
  • 2 processes, model (R=3), model (R=4), model (R=5) and properties
  • 3 processes, model (R=3), model (R=4), model (R=5) and properties
  
  
• Zeroconf network configuration protocol (protocol from [CAG02], original PRISM model from [KNPS06])

  K is the number of probe messages sent by the protocol.

  • model (K=2), model (K=4), model (K=6), model (K=8), and properties
  
  
• Zeroconf protocol with time-based assumption (original PRISM model from [KNPS06])

  K is the number of probe messages sent by the protocol, T is the time bound encoded into the assumption.

  • model (K=2), model (K=4) and properties

• Team formation protocol (PRISM model from [CKPS11])

  N is the number of agents (sensors) involved in team formation.

  • model (N=2), model (N=5) and properties
  
  
• Task-graph scheduling problem (PRISM model from [NPS12])

  K measures the granularity of the timer, i.e. the number of ticks per time unit.

  • model and properties
  
  
• Dynamic power management (DPM) controller (PRISM model from [FKN+11, NPK+05])

  k is the time-bounded used in the property.

  • model and properties