"Distributional Probabilistic Model Checking" - Supporting Files

Paper: "Distributional Probabilistic Model Checking" by Ingy ElSayed-Aly, David Parker and Lu Feng

Code: Full source code, instructions and all other files are on GitHub:

• https://github.com/davexparker/prism/blob/ingy/INSTRUCTIONS.md

Benchmarks: Included below are the PRISM models and properties files for the benchmarks featured in the paper.

MDP benchmarks:

• Betting Game: Betting game example (adapted from [RDLH22])
  
  
  • Model: betting_game.prism
  • Properties: betting_game.props
  
  
• DS Treasure: Deep sea treasure example (adapted from [RDLH22])
  
  
  • Model: ds_treasure.prism
  • Properties: ds_treasure.props
  
  
• Obstacle: Gridworld navigation examples from a source to a target (adapted from [CTMP15])
  
  
  • Base Model: gridmap_10_10.prism
  • Properties: gridmap_10_10.props
  • Larger Model (Obstacle 150): gridmap_150_3918.prism
  • Properties: gridmap_150_3918.props
  
  
• Energy: Unmanned drone scenario while managing a battery resource
  
  
  • Base Model: drones.prism
  • Larger Model (Energy 15): drones_15.prism
  • Properties: drones.props
  
  
• uav: Unmanned aerial vehicle (adapted from [FWHT16])
  
  
  • Model: uav_var.prism
  • Properties: uav_var.props

DTMC benchmarks: (from the PRISM Benchmark Suite)

• EGL:
  
  
  • Model: egl.pm models
  • Properties: messagesA.props
  
  
• Leader:
  
  
  • Models: leader_sync8_5.pm leader_sync10_4.pm leader_sync6_8.pm
  • Properties: time.props
  
  
• Herman:
  
  
  • Model: herman13.pm herman15.pm herman17.pm
  • Properties: steps.props