论文标题
验证一个随机模型，以传播SARS-COV-2样感染：机会和局限性
Verifying a stochastic model for the spread of a SARS-CoV-2-like infection: opportunities and limitations
论文作者
论文摘要
使用随机模型对诸如SARS-COV-2感染（SARS-COV-2感染）等疾病的传播进行建模和分析越来越兴趣。这些模型通常经过定量分析，并且通常不经常使用正式验证方法进行验证，也不利用在正式验证中开发的政策合成和分析技术。在本文中，我们采用了Markovian随机模型，用于SARSCOV-2样感染的传播。该模型的状态代表不同健康状况下的受试者的数量。考虑的模型考虑了可能影响疾病传播的不同参数，并暴露了可用于控制疾病的各种决策变量。我们表明，在最新的模型检查器中对问题的建模是可行的，并且打开了几个机会。但是，由于i）一侧现有随机模型检查器的浓缩性以及ii）所得的马尔可夫模型的大小，即使对于小种群的大小，也存在严重的限制。
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 SARSCoV-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.
