Assessing Time Behaviour in Disaster Management by Using Petri Nets and Model Checking

Disaster Management (DM) involves a range of procedures and best practices aimed at minimising the impact of natural or human-made disasters on people, infrastructure, and the environment. Time is a critical factor in DM. An effective and timely response can save lives, prevent further damage to infrastructure and the environment, and facilitate the recovery process. Assessing time behaviour in a DM scenario is a complex task because it depends on many factors like the kind of disaster, resource availability and the situation's complexity. This paper proposes an approach for assessing system behaviour in DM based on an extended version of the Stochastic Reward Nets (SRNs), named SRNs*, as modeling language and the Uppaal Model Checker as a formal analysis tool. The approach is demonstrated through modeling and analysis of a DM scenario tied to emergency response and specifically on the problem of deploying medical resources to provide adequate hospital care.