"Optimization-Based Robust Permissive Synthesis for Interval MDPs" - Supporting Files

Paper: "Optimization-Based Robust Permissive Synthesis for Interval MDPs"
by Khang Vo Huynh, David Parker, Lu Feng

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

• aca: Aircraft Collision Avoidance (adapted from [TACAS25])
  
  
  • Models: aca_10.prism, aca_12.prism, aca_14.prism
  • Encodings (ASP / LP): aca_encoder_zip
  
  
• obs: Obstacle Avoidance inspired by Frozen Lake (adapted from [OpenAI_Gym])
  
  
  • Models: obs_5.prism, obs_6.prism
  • Encodings (ASP / LP): obs_encoder_zip
  
  
• sav: Semi-autonomous Vehicle Navigation (adapted from [TACAS16])
  
  
  • Model: sav.prism
  • Encodings (ASP / LP): sav_encoder_zip
  
  
• wh: Warehouse Navigation (adapted from [ICCPS22])
  
  
  • Model: wh.prism
  • Encodings (ASP / LP): wh_encoder_zip
  
  
• PRISM properties used for experiments
  
  
  • Properties: experiment.props