Abstract
There is a growing interest in modeling and analyzing the spread of diseases like the SARS-CoV-2 infection using stochastic models. These models are typically analyzed quantitatively and are not often subject to validation using formal verification approaches, nor leverage policy syntheses and analysis techniques developed in formal verification.
In this paper, we take a Markovian stochastic model for the spread of a SARS-CoV-2-like infection. A state of this model represents the number of subjects in different health conditions. The considered model considers the different parameters that may have an impact on the spread of the disease and exposes the various decision variables that can be used to control it. We show that the modeling of the problem within state-of-the-art model checkers is feasible and it opens several opportunities. However, there are severe limitations due to i) the espressivity of the existing stochastic model checkers on one side, and ii) the size of the resulting Markovian model even for small population sizes.
This work is partially funded by the grant MOSES, Bando interno 2020 Università di Trento “Covid 19”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
As shown in [19], this model is such that, for a population of N subjects, assuming there are n possible configurations (in our case \(n=8\)), the maximum number of possible states that can be generated is \(\left( {\begin{array}{c}N+n-1\\ N\end{array}}\right) \) that corresponds to the Bose-Einstein statistics.
- 2.
- 3.
We refer the reader to [19] for a more detailed discussion of the literature on modeling and analyzing the spread of diseases with analytical models.
References
Allen, L., et al.: Mathematical Epidemiology. Lecture Notes in Mathematics, Springer, Berlin (2008)
Anderson, R., May, R.: Infectious Diseases of Humans: Dynamics and Control. OUP, Oxford (1992)
Bernoulli, D.: Essai d’une nouvelle analyse de la mortalite causee par la petite verole, et des avantage de l’inoculation pour la prevenir. Mem. phys. Acade. Roy. Sci. 1(6), 1-45 (1760)
Blanchini, F., Franco, E., Giordano, G., Mardanlou, V., Montessoro, P.L.: Compartmental flow control: decentralization, robustness and optimality. Automatica 64, 18–28 (2016)
Brauer, F., Castillo-Chavez, C., Feng, Z.: Mathematical Models in Epidemiology. Texts in Applied Mathematics, Springer, New York (2019)
Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer Science & Business Media, Berlin (2009)
Chauhan, K.: Epidemic analysis using traditional model checking and stochastic simulation. Master’s thesis, Indian Institute of Technology Hyderabad (2015)
Dobay, M.P., Dobay, A., Bantang, J., Mendoza, E.: How many trimers? modeling influenza virus fusion yields a minimum aggregate size of six trimers, three of which are fusogenic. Mol. BioSyst. 7, 2741–2749 (2011)
Gani, J., Jerwood, D.: Markov chain methods in chain binomial epidemic models. Biometrics 27, 591–603 (1971)
Ghezzi, L.L., Piccardi, C.: PID control of a chaotic system: an application to an epidemiological model. Automatica 33(2), 181–191 (1997)
Giordano, G., et al.: Modelling the COVID-19 epidemic and implementation of population-wide interventions in Italy. Nature Med. 26(6), 1–6 (2020)
Haksar, R.N., Schwager, M.: Controlling large, graph-based MDPS with global control capacity constraints: an approximate LP solution. In: 2018 IEEE Conference on Decision and Control (CDC), pp. 35–42 (2018). https://doi.org/10.1109/CDC.2018.8618745
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)
Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Trans. 24, 1–22 (2021). https://doi.org/10.1007/s10009-021-00633-z
Kermack, W.O., McKendrick, A.G., Walker, G.T.: A contribution to the mathematical theory of epidemics. In: Proceedings of the Royal Society of London. Series A, Containing Papers of a Mathematical and Physical Character, vol. 115, no. 772, pp. 700–721 (1927)
Khanafer, A., Başar, T., Gharesifard, B.: Stability of epidemic models over directed graphs: a positive systems approach. Automatica 74, 126–134 (2016)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47
Nasir, A., Baig, H.R., Rafiq, M.: Epidemics control model with consideration of seven-segment population model. SN Appl. Sci. 2(10), 1–9 (2020). https://doi.org/10.1007/s42452-020-03499-z
Palopoli, L., Fontanelli, D., Frego, M., Roveri, M.: A Markovian model for the spread of the SARS-CoV-2 virus. CoRR abs/2204.11317 (2022)
Razzaq, M., Ahmad, J.: Petri net and probabilistic model checking based approach for the modelling, simulation and verification of internet worm propagation. PLOS ONE 10(12), 1–22 (2016)
Riccardo, F., Ajelli, M., Andrianou, X.D., et al.: Epidemiological characteristics of COVID-19 cases and estimates of the reproductive numbers 1 month into the epidemic, Italy, 28 January to 31 March 2020. Eurosurveillance 25(49) (2020)
Roveri, M., Ivankovic, F., Palopoli, L., Fontanelli, D.: Verifying a stochastic model for the spread of a sars-cov-2-like infection: opportunities and limitations (2022). https://doi.org/10.48550/ARXIV.2211.00605, https://arxiv.org/abs/2211.00605
Sattenspiel, L.: Modeling the spread of infectious disease in human populations. Am. J. Phys. Anthropol. 33(S11), 245–276 (1990)
Tuckwell, H.C., Williams, R.J.: Some properties of a simple stochastic epidemic model of sir type. Math. Biosci. 208(1), 76–97 (2007)
Yousefpour, A., Jahanshahi, H., Bekiros, S.: Optimal policies for control of the novel coronavirus disease (COVID-19) outbreak. Chaos Solitons Fractals 136, 109883 (2020)
Zardini, A., et al.: A quantitative assessment of epidemiological parameters required to investigate COVID-19 burden. Epidemics 37, 100530 (2021)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Roveri, M., Ivankovic, F., Palopoli, L., Fontanelli, D. (2023). Verifying a Stochastic Model for the Spread of a SARS-CoV-2-Like Infection: Opportunities and Limitations. In: Dovier, A., Montanari, A., Orlandini, A. (eds) AIxIA 2022 – Advances in Artificial Intelligence. AIxIA 2022. Lecture Notes in Computer Science(), vol 13796. Springer, Cham. https://doi.org/10.1007/978-3-031-27181-6_30
Download citation
DOI: https://doi.org/10.1007/978-3-031-27181-6_30
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-27180-9
Online ISBN: 978-3-031-27181-6
eBook Packages: Computer ScienceComputer Science (R0)