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

被引:0
|
作者
Cicirelli, Franco [1 ]
Nigro, Libero [2 ]
机构
[1] CNR Natl Res Council Italy, ICAR, I-87036 Arcavacata Di Rende, Italy
[2] Univ Calabria, DIMES, I-87036 Arcavacata Di Rende, Italy
关键词
Disaster Management; Methodological Approach; Time Constraints; Stochastic Reward Nets; Model Checking; UPPAAL; LOCATION;
D O I
10.1109/ICT-DM58371.2023.10286950
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
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.
引用
收藏
页码:181 / 186
页数:6
相关论文
共 50 条
  • [1] TCTL Model Checking of Time Petri Nets
    Boucheneb, Hanifa
    Gardey, Guillaume
    Roux, Olivier H.
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2009, 19 (06) : 1509 - 1540
  • [2] CTL* model checking for time Petri nets
    Boucheneb, H
    Hadjidj, R
    [J]. THEORETICAL COMPUTER SCIENCE, 2006, 353 (1-3) : 208 - 227
  • [3] CTL model checking of time Petri nets using geometric regions
    Yoneda, T
    Ryuba, H
    [J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1998, E81D (03) : 297 - 306
  • [4] Bounded model checking of Time Petri Nets using SAT solver
    Yokogawa, Tomoyuki
    Kondo, Masafumi
    Miyazaki, Hisashi
    Amasaki, Sousuke
    Sato, Yoichiro
    Arimoto, Kazutami
    [J]. IEICE ELECTRONICS EXPRESS, 2015, 12 (02):
  • [5] Towards TCTLhΔ model checking of Time Petri Nets
    Chtourou, Ameni
    Sbai, Zohra
    [J]. 2016 INTERNATIONAL CONFERENCE ON CONTROL, DECISION AND INFORMATION TECHNOLOGIES (CODIT), 2016, : 563 - 568
  • [6] Model checking Bounded Prioritized Time Petri Nets
    Berthomieu, Bernard
    Peres, Florent
    Vernadat, Francois
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 523 - +
  • [7] Model checking of time Petri nets using the state class timed automaton
    Lime, Didier
    Roux, Olivier H.
    [J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2006, 16 (02): : 179 - 205
  • [8] Model Checking of Time Petri Nets Using the State Class Timed Automaton
    Didier Lime
    Olivier H. Roux
    [J]. Discrete Event Dynamic Systems, 2006, 16 : 179 - 205
  • [9] On-the-fly TCTL model checking for time Petri nets
    Hadjidj, Rachid
    Boucheneb, Hanifa
    [J]. THEORETICAL COMPUTER SCIENCE, 2009, 410 (42) : 4241 - 4261
  • [10] Interpolation Based Unbounded Model Checking for Time Petri Nets
    Igawa, Nao
    Yokogawa, Tomoyuki
    Amasaki, Sousuke
    Komoku, Kiyotaka
    Sato, Yoichiro
    Arimoto, Kazutami
    [J]. 2018 IEEE 7TH GLOBAL CONFERENCE ON CONSUMER ELECTRONICS (GCCE 2018), 2018, : 619 - 623