Probabilistic Model Checking: Advances and Applications - Supporting Material

Book chapter: "Probabilistic Model Checking: Advances and Applications"
Marta Kwiatkowska, Gethin Norman and David Parker

Models and Properties

Included below are the models and properties for the examples and case studies included in this book chapter.

• Running example: Robot
  
  
  • DTMC model robot_dtmc.prism and properties robot_dtmc.props
  • MDP model robot_mdp.prism and properties robot_mdp.props (including multi-objective query)
  • PTA model robot_pta.prism and properties robot_pta.props
  • PDTMC model robot_pdtmc.prism and properties robot_pdtmc.props
  
  
• NAND Multiplexing (DTMC and PDTMC case studies)
  
  
  • (P)DTMC model: nand.prism
  • (P)DTMC model with modelling error: nand_error.prism
  • Properties (both versions): nand.props
  
  
• Processor Task Scheduling (PTA case study)
  
  
  • Basic model: scheduler.prism
  • Model extended with random processor execution times: scheduler_prob.prism
  • Model extended with a third faulty processor: scheduler_failure.prism
  • Properties (all versions): scheduler.props
  • Commands for visualising optimal schedulers: commands.txt