Algorithms for Markov Binomial Chains
<|reference_start|>Algorithms for Markov Binomial Chains: 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 epidemilogists.<|reference_end|>
@article{gonzalez2024algorithms,
    title={Algorithms for Markov Binomial Chains},
    author={Alejandro Alarc'on Gonzalez, Niel Hens, Tim Leys, Guillermo A.
  P'erez},
    journal={arXiv preprint arXiv:2408.04902},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.04902},
    primaryClass={cs.LO}
}