Fluid Model-Checking in UPPAAL for Covid-19

Fluid Model-Checking in UPPAAL for Covid-19, Peter G. Jensen, Kenneth Y. Jørgensen, Kim G. Larsen, Marius Mikučionis, Marco Muñiz, and Danny B. Poulsen. Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2020), October 2020. Springer-Verlag Berlin Heidelberg. [doi] [bib] [pre-print]

Abstract

During the spring of 2020, the BEOCOVID project has been funded to investigate the use of stochastic hybrid models, statistical model checking and machine learning to anlyse, predict and control the rapid spreading of Covid-19. In this paper we focus on the SEIHR epidemiological model instance of Covid-19 pandemics and show how the risk of viral exposure, the impact of super-spreader events as well as other scenarios can be modelled, estimated and controlled using the tool Uppaal SMC.

Early SIR models with work and shopping:

• covid19-ctmc.xml hand-crafted CTMC version.
• covid19-ode.xml generated ODE version.

Models for the SEIHR diagram:

• seihr-ode.xml ODE approach to SEIRH model with population of 10000 (Fig.2).
• seihr-ctmc.xml aggregated CTMC approach to SEIRH model with population of 10000 (Fig.3).
• seihr-ctmc-agent.xml CTMC agent approach to SEIRH model with population of 10000 (Fig.4).