Probabilistic Model Checking of Disaster Resource Distribution Strategies

Disasters are unexpected, and capable of severely impacting an urban region. A key challenge for disaster managers is to distribute resources to meet evolving demand. This paper presents a work in progress framework to verify provably correct team strategies to safely carry out resource distribution. Uncertainties from infrastructure damage and team fatigue are modelled using Markov Decision Processes, and verified against temporal logic properties to support disaster managers resourcing decisions. We implement the framework with PRISM and test its effectiveness across a range of resourcing scenarios.