一句话：形式化马尔可夫二项链，证明无环流几乎必然终止，给出近似与精确计算终止时间的算法，并编码至概率模型检测器。
论文研究流行病学中常用的一类马尔可夫种群过程——马尔可夫二项链，它由经典隔室模型的随机时间离散化产生。作者形式化该模型，并聚焦于计算给定模型期望终止时间的问题。理论贡献包括：证明隔室间个体流无环的马尔可夫二项链几乎必然终止；给出近似终止时间的 PSPACE 算法，以及在 Blum-Shub-Smale 计算模型下求解精确问题的直接算法。最后，作者将马尔可夫二项链自然编码为概率模型检测器的通用输入语言，实现该编码并给出初步实证结果，展示形式化方法对流行病学实践的潜力。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{GonzalezHLP25,
title = {Algorithms for Markov Binomial Chains},
author = {Alejandro Alarcón Gonzalez and Niel Hens and Tim Leys and Guillermo A. Pérez},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:28)2025}
}