Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Inform: From Compartmental Models to Stochastic Bounded Counter Machines

Tim Leys, Guillermo A. Perez

TL;DR

The paper addresses the challenge of analyzing stochastic compartmental models by encoding them as bounded stochastic counter machines, yielding finite Markov chains when counters are restricted. It provides an automated translator, Inform, to generate PRISM models and evaluates analysis with probabilistic model checkers STORM and Modest on simple SIR and Belgian COVID-19 models. Findings show that state-of-the-art tools face scalability limits for large epidemiological models, highlighting the need for abstractions and approximate methods, while still demonstrating a principled path to exact and approximate verification of epidemic dynamics. The work offers a foundation for integrating reinforcement learning to optimize intervention policies within this verification framework.

Abstract

Compartmental models are used in epidemiology to capture the evolution of infectious diseases such as COVID-19 in a population by assigning members of it to compartments with labels such as susceptible, infected, and recovered. In a stochastic compartmental model the flow of individuals between compartments is determined probabilistically. We establish that certain stochastic compartment models can be encoded as probabilistic counter machines where the configurations are bounded. Based on the latter, we obtain simple descriptions of the models in the PRISM language. This enables the analysis of such compartmental models via probabilistic model checkers. Finally, we report on experimental results where we analyze results from a Belgian COVID-19 model using a probabilistic model checkers.

Inform: From Compartmental Models to Stochastic Bounded Counter Machines

TL;DR

The paper addresses the challenge of analyzing stochastic compartmental models by encoding them as bounded stochastic counter machines, yielding finite Markov chains when counters are restricted. It provides an automated translator, Inform, to generate PRISM models and evaluates analysis with probabilistic model checkers STORM and Modest on simple SIR and Belgian COVID-19 models. Findings show that state-of-the-art tools face scalability limits for large epidemiological models, highlighting the need for abstractions and approximate methods, while still demonstrating a principled path to exact and approximate verification of epidemic dynamics. The work offers a foundation for integrating reinforcement learning to optimize intervention policies within this verification framework.

Abstract

Compartmental models are used in epidemiology to capture the evolution of infectious diseases such as COVID-19 in a population by assigning members of it to compartments with labels such as susceptible, infected, and recovered. In a stochastic compartmental model the flow of individuals between compartments is determined probabilistically. We establish that certain stochastic compartment models can be encoded as probabilistic counter machines where the configurations are bounded. Based on the latter, we obtain simple descriptions of the models in the PRISM language. This enables the analysis of such compartmental models via probabilistic model checkers. Finally, we report on experimental results where we analyze results from a Belgian COVID-19 model using a probabilistic model checkers.
Paper Structure (20 sections, 5 theorems, 5 equations, 6 figures, 6 tables)

This paper contains 20 sections, 5 theorems, 5 equations, 6 figures, 6 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Stochastic Compartmental Models
  4. Compartment Flows and Time.
  5. System States and Transitions.
  6. Transition Probabilities.
  7. Reaching Probabilities.
  8. Discrete Time Markov Chains
  9. Stochastic Counter Machines
  10. Runs and Probabilities.
  11. Relation with Markov chains.
  12. Towards Stochastic Counter Machines
  13. Experimental Results
  14. Conclusion
  15. Properties in Prism Format
  16. ...and 5 more sections

Key Result

theorem 1

Let $\mathcal{A}$ be an SCM and let $\chi,\chi'$ be configurations in $\mathcal{A}$. Then, there is a Markov chain $\mathcal{M}$ with a state $s$ in such that $\Pr(\chi \xrightarrow{*} \chi')$ iff $\Pr(\Diamond s)$.

Figures (6)

  • Figure 1: The standard binomial gadget: solidly filled circles represent a distribution and arrows from them lead to all possible successors; guards are shown as systems of linear constraints in square brackets on the edge between state and distribution; updates, within braces on edges from distributions to states
  • Figure 2: An SCM on the left; A simple compartmental model on the right
  • Figure 3: The SCM of the SIR model, where $p_0 = 1-\exp(0.4)$ and $p_1 = 1-\exp(0.5)$.
  • Figure 4: The a plot of Modest run-times vs. large populations for PopInc.
  • Figure 5: On the left the graph representation of the SIR model, on the right the cms file of the SIR model.
  • ...and 1 more figures

Theorems & Definitions (7)

  • theorem 1
  • lemma 1
  • lemma 2
  • lemma 3
  • theorem 2
  • proof
  • proof