Algorithms for Markov Binomial Chains

TL;DR

This paper formalizes Markov binomial chains used in epidemiology, proves their termination properties, and develops algorithms for analyzing their expected termination time, including implementation and empirical evaluation.

Contribution

It introduces formal definitions, termination proofs, and algorithms for Markov binomial chains, with practical encoding for model checking and initial empirical results.

Findings

Markov binomial chains almost surely terminate if acyclic

Developed a PSPACE approximation algorithm for expected termination time

Implemented encoding for probabilistic model checkers and showcased initial results

Abstract

We study algorithms to analyze a particular class of Markov population processes that is often used in epidemiology. More specifically, Markov binomial chains are the model that arises from stochastic time-discretizations of classical compartmental models. In this work we formalize this class of Markov population processes and focus on the problem of computing the expected time to termination in a given such model. Our theoretical contributions include proving that Markov binomial chains whose flow of individuals through compartments is acyclic almost surely terminate. We give a PSPACE algorithm for the problem of approximating the time to termination and a direct algorithm for the exact problem in the Blum-Shub-Smale model of computation. Finally, we provide a natural encoding of Markov binomial chains into a common input language for probabilistic model checkers. We implemented the latter encoding and present some initial empirical results showcasing what formal methods can do for practicing epidemiologists.