一句话：综述无限状态 Markov 链、MDP 与随机博弈的算法与复杂度，统一递归/计数器式概率程序模型。
该报告综述过去十余年关于可数无限状态 Markov 链、Markov 决策过程（MDP）与随机博弈的分析和模型检测算法及其计算复杂度的研究。此类模型通过在有限状态模型上加入递归、分支或计数器得到，可视为下推自动机、上下文无关文法和单计数器自动机的概率/控制/博弈扩展。它们覆盖多类型分支过程、拟生灭过程等经典随机过程，并为带递归的概率过程式程序提供自然模型。报告关注这些无限状态概率系统的算法设计与复杂度刻画，连接自动机理论、随机过程与程序验证。
I will survey a body of work, developed over the past decade or so, on algorithms for, and the computational complexity of, analyzing and model checking some important families of countably infinite-state Markov chains, Markov decision processes (MDPs), and stochastic games. These models arise by adding natural forms of recursion, branching, or a counter, to finite-state models, and they correspond to probabilistic/control/game extensions of classic automata-theoretic models like pushdown automata, context-free grammars, and one-counter automata. They subsume some classic stochastic processes such as multi-type branching processes and quasi-birth-death processes. They also provide a natural model for probabilistic procedural programs with recursion.