Verifying a stochastic model for the spread of a SARS-CoV-2-like infection: opportunities and limitations

TL;DR

This paper explores the use of formal verification techniques on a stochastic Markovian model of SARS-CoV-2 spread, highlighting both opportunities for validation and control, and limitations due to model complexity and tool expressivity.

Contribution

It demonstrates the feasibility of modeling disease spread within state-of-the-art model checkers and discusses the challenges faced in applying formal verification to such stochastic models.

Findings

Model checking of SARS-CoV-2 spread is feasible with current tools.

Significant limitations exist due to model size and expressivity constraints.

Formal verification can aid in analyzing disease control strategies.

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