Statistical Model Checking of Relief Supply Location and Distribution in Natural Disaster Management

Abstract

Examining the e cacy of natural disaster management readiness and response activities is challenging due to the randomized behaviors and uncertainties of natural disaster. These uncertainties are captured by stochastic models quite well and thus have been widely used in disaster response activities for evacuation operations, coordinating logistics support and accurate relief shelter planning. The analysis of these stochastic models is carried out using Monte Carlo simulations to judge the e ectiveness of natural disaster management solutions. However, this approach uses the static estimators, which generally rely on sampled number of events taken from the random space. The safety-critical nature of such domain requires a more quanti able analysis. In order to overcome this challenge, we propose to use statistical model checking. The paper presents a framework for the formal statistical analysis of relief supply location and distribution of natural disaster management in PRISM. In PRISM model checker, we model and analyze a real-world natural disaster management plan incorporating key factors i.e. demand of medical supplies at hospitals, predestined routes from warehouses to hospitals, capacity of warehouses and transportation plans ensuring successful delivery of medical supplies to the hospitals.