Model Checking of Recursive Probabilistic Systems
Model Checking of Recursive Probabilistic Systems
复制标题
递归概率系统的模型检查
DOI：
10.1145/2159531.2159534
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
M. Yannakakis
中科院分区：
文献类型：
--
作者：
K. Etessami;M. Yannakakis
递归马尔可夫链（RMCs）是过程概率规划及相关递归和概率系统的自然抽象模型。他们简明地定义了一类可计数马尔可夫链，推广了其他几种随机模型，它们在精确意义上等价于概率下推系统。在本文中，我们研究了RMC是否符合ω-正则规范的模型检验问题，该规范是由一个<s:1>自动机或线性时间逻辑（LTL）公式给出的。也就是说，给定一个RMC A和一个属性，我们希望知道A的执行满足属性的概率。我们为定性问题（概率是= 1还是= 0?）和定量问题（概率是否≥p?）建立了许多强上界和下界。（或将概率近似到所需的精度范围内）。我们得到的自动机和LTL性质的复杂度上界是相似的，尽管算法不同。
Recursive Markov Chains (RMCs) are a natural abstract model of procedural probabilistic programs and related systems involving recursion and probability. They succinctly define a class of denumerable Markov chains that generalize several other stochastic models, and they are equivalent in a precise sense to probabilistic Pushdown Systems. In this article, we study the problem of model checking an RMC against an ω-regular specification, given in terms of a Büchi automaton or a Linear Temporal Logic (LTL) formula. Namely, given an RMC A and a property, we wish to know the probability that an execution of A satisfies the property. We establish a number of strong upper bounds, as well as lower bounds, both for qualitative problems (is the probability = 1, or = 0?), and for quantitative problems (is the probability ≥ p?, or, approximate the probability to within a desired precision). The complexity upper bounds we obtain for automata and LTL properties are similar, although the algorithms are different.
We present algorithms for the qualitative model checking problem that run in polynomial space in the size |A| of the RMC and exponential time in the size of the property (the automaton or the LTL formula). For several classes of RMCs, including single-exit RMCs (a class that encompasses some well-studied stochastic models, for instance, stochastic context-free grammars) the algorithm runs in polynomial time in |A|. For the quantitative model checking problem, we present algorithms that run in polynomial space in the RMC and exponential space in the property. For the class of linearly recursive RMCs we can compute the exact probability in time polynomial in the RMC and exponential in the property. For deterministic automata specifications, all our complexities in the specification come down by one exponential.
For lower bounds, we show that the qualitative model checking problem, even for a fixed RMC, is already EXPTIME-complete. On the other hand, even for simple reachability analysis, we know from our prior work that our PSPACE upper bounds in A can not be improved substantially without a breakthrough on a well-known open problem in the complexity of numerical computation.