单调多项式系统上牛顿法的上界与概率单计数器自动机的 P-时间模型检验
计算机科学中的逻辑
2013-04-30 v2 计算复杂性
摘要
分析和模型检验各类无限状态递归概率系统（包括拟生灭过程、多类型分支过程、随机上下文无关文法、概率下推自动机和递归马尔可夫链）的一个核心计算问题是计算终止概率，而计算这些概率又归结为计算相应单调多项式方程组（MPS）x=P(x) 的最小不动点（LFP）解。Etessami 和 Yannakakis 证明了，对于任何具有非负解的 MPS，牛顿法的一种分解变体单调收敛到 LFP 解。随后，Esparza、Kiefer 和 Luttenberger 获得了牛顿法对某些 MPS 类的收敛速度上界。最近，针对特殊 MPS 类获得了更好的上界。然而，在本文之前，对于任意（不一定强连通）MPS，作为输入 MPS x=P(x) 的编码大小 |P| 的函数，牛顿法的收敛速度上界完全未知。本文中，我们提供了分解牛顿法（即使带有舍入）收敛到 LFP 解 q* 的加性误差 epsilon > 0 以内所需迭代次数的最坏情况上界，作为输入编码大小 |P| 和 epsilon > 0 的函数。我们的上界在几个重要参数方面本质上是最优的。利用我们的上界，并在先前工作的基础上，我们获得了第一个 P-时间算法（在标准图灵计算模型中），用于在期望精度内对离散时间 QBD 和（等价地）概率单计数器自动机进行定量模型检验，针对任何（固定的）omega-正则或 LTL 性质。
引用
@article{arxiv.1302.3741,
title = {Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata},
author = {Alistair Stewart and Kousha Etessami and Mihalis Yannakakis},
journal= {arXiv preprint arXiv:1302.3741},
year = {2013}
}