Fluid Model-Checking in UPPAAL for Covid-19

Peter Gjøl Jensen; Kenneth Yrke Jørgensen; Kim Guldstrand Larsen; Marius Mikučionis; Marco Antonio Muniz Rodriguez; Danny Bøgsted Poulsen

doi:10.1007/978-3-030-61362-4_22

Fluid Model-Checking in UPPAAL for Covid-19

Peter Gjøl Jensen, Kenneth Yrke Jørgensen, Kim Guldstrand Larsen, Marius Mikučionis, Marco Antonio Muniz Rodriguez, Danny Bøgsted Poulsen

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

3 Citations (Scopus)

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.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation : Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
Editors	Tiziana Margaria, Bernhard Steffen
Number of pages	19
Publisher	Springer
Publication date	2020
Pages	385-403
ISBN (Print)	978-3-030-61361-7
ISBN (Electronic)	978-3-030-61362-4
DOIs	https://doi.org/10.1007/978-3-030-61362-4_22
Publication status	Published - 2020
Event	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 - Rhodes, Greece Duration: 20 Oct 2020 → 30 Oct 2020

Conference

Conference	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
Country/Territory	Greece
City	Rhodes
Period	20/10/2020 → 30/10/2020

Series	Lecture Notes in Computer Science
Volume	12476
ISSN	0302-9743

Bibliographical note

Funding Information:
The project was funded by Poul Due Jensens Foundation grant.

Funding Information:
– In early April researchers at Danmarks Tekniske Universitet (DTU) and Aal-borg Universitet (AAU) started a research project funded by Novo Nordisk Fonden (NNF) to develop and improve modelling tools of Covid-19 to assist decision makers to evaluate the effectiveness and impact of preventive mea-sures. The project has been carried out in collaboration with SSI.

Publisher Copyright:
© 2020, Springer Nature Switzerland AG.

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-030-61362-4_22

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

Jensen, P. G., Jørgensen, K. Y., Larsen, K. G., Mikučionis, M., Rodriguez, M. A. M., & Poulsen, D. B. (2020). Fluid Model-Checking in UPPAAL for Covid-19. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings (pp. 385-403). Springer. https://doi.org/10.1007/978-3-030-61362-4_22

Jensen, Peter Gjøl ; Jørgensen, Kenneth Yrke ; Larsen, Kim Guldstrand et al. / Fluid Model-Checking in UPPAAL for Covid-19. Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer, 2020. pp. 385-403 (Lecture Notes in Computer Science, Vol. 12476).

@inproceedings{1b96b28833ae49c29a967887c9347a4b,

title = "Fluid Model-Checking in UPPAAL for Covid-19",

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.",

author = "Jensen, {Peter Gj{\o}l} and J{\o}rgensen, {Kenneth Yrke} and Larsen, {Kim Guldstrand} and Marius Miku{\v c}ionis and Rodriguez, {Marco Antonio Muniz} and Poulsen, {Danny B{\o}gsted}",

note = "Funding Information: The project was funded by Poul Due Jensens Foundation grant. Funding Information: – In early April researchers at Danmarks Tekniske Universitet (DTU) and Aal-borg Universitet (AAU) started a research project funded by Novo Nordisk Fonden (NNF) to develop and improve modelling tools of Covid-19 to assist decision makers to evaluate the effectiveness and impact of preventive mea-sures. The project has been carried out in collaboration with SSI. Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020",

year = "2020",

doi = "10.1007/978-3-030-61362-4_22",

language = "English",

isbn = "978-3-030-61361-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "385--403",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",

address = "Germany",

}

Jensen, PG, Jørgensen, KY, Larsen, KG , Mikučionis, M , Rodriguez, MAM & Poulsen, DB 2020, Fluid Model-Checking in UPPAAL for Covid-19. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Springer, Lecture Notes in Computer Science, vol. 12476, pp. 385-403, 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020, Rhodes, Greece, 20/10/2020. https://doi.org/10.1007/978-3-030-61362-4_22

Fluid Model-Checking in UPPAAL for Covid-19. / Jensen, Peter Gjøl; Jørgensen, Kenneth Yrke; Larsen, Kim Guldstrand et al.
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer, 2020. p. 385-403 (Lecture Notes in Computer Science, Vol. 12476).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - Fluid Model-Checking in UPPAAL for Covid-19

AU - Jensen, Peter Gjøl

AU - Jørgensen, Kenneth Yrke

AU - Larsen, Kim Guldstrand

AU - Mikučionis, Marius

AU - Rodriguez, Marco Antonio Muniz

AU - Poulsen, Danny Bøgsted

N1 - Funding Information: The project was funded by Poul Due Jensens Foundation grant. Funding Information: – In early April researchers at Danmarks Tekniske Universitet (DTU) and Aal-borg Universitet (AAU) started a research project funded by Novo Nordisk Fonden (NNF) to develop and improve modelling tools of Covid-19 to assist decision makers to evaluate the effectiveness and impact of preventive mea-sures. The project has been carried out in collaboration with SSI. Publisher Copyright: © 2020, Springer Nature Switzerland AG.

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85097411688&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-61362-4_22

DO - 10.1007/978-3-030-61362-4_22

M3 - Article in proceeding

AN - SCOPUS:85097411688

SN - 978-3-030-61361-7

T3 - Lecture Notes in Computer Science

SP - 385

EP - 403

BT - Leveraging Applications of Formal Methods, Verification and Validation

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020

Y2 - 20 October 2020 through 30 October 2020

ER -

Jensen PG, Jørgensen KY, Larsen KG , Mikučionis M , Rodriguez MAM , Poulsen DB. Fluid Model-Checking in UPPAAL for Covid-19. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Springer. 2020. p. 385-403. (Lecture Notes in Computer Science, Vol. 12476). doi: 10.1007/978-3-030-61362-4_22

Fluid Model-Checking in UPPAAL for Covid-19

Abstract

Conference

Bibliographical note

UN SDGs

Access to Document

AUB Link

Other files and links

Fingerprint

BEO-COVID: Decision making tool based on evaluation and optimisation of models in UPPAAL

Cite this

Fluid Model-Checking in UPPAAL for Covid-19

Abstract

Conference

Bibliographical note

UN SDGs

Access to Document

AUB Link

Other files and links

Fingerprint

Projects

BEO-COVID: Decision making tool based on evaluation and optimisation of models in UPPAAL

Cite this