决定性马尔可夫链
Decisive Markov Chains
摘要：
我们考虑定性和定量验证问题的无限状态马尔可夫链。我们称马尔可夫链为决定性w.r.t.给定的一组目标状态F，如果它几乎肯定最终达到F或一个不再能达到F的状态。虽然所有的有限马尔可夫链都是平凡决定的（对于每一个集合F），这也适用于许多类的无限马尔可夫链。含有有限吸引子的无穷马氏链是决定性的。每个集合F.特别地，这适用于概率有损信道系统（PLCS）。此外，所有全局粗马尔可夫链都是决定性的。这一类包括概率向量加法系统（PVASS）和概率噪声图灵机（PNTM）。我们考虑了决定性马尔可夫链的安全性和活性问题，即，一组给定的状态F最终达到或无限频繁地达到的概率。1.我们表达的定性问题在抽象的条件下，决定性的马尔可夫链，并显示了一个几乎完整的图片，其可决定性的PLCS，PVASS和PNTM。2.我们还表明，Iyer和Narasimha的路径枚举算法终止的决定性马尔可夫链，因此可以用来解决近似定量的安全问题。该算法的一个修改的变体解决了近似定量活性问题。3.最后，我们证明了（重复）到达F的确切概率不能有效地表示（以统一的方式）在塔斯基代数的PLCS，PVASS或（P）NTM。
英文摘要：
We consider qualitative and quantitative verification problems for infinite-state Markov chains. We call a Markov chain decisive w.r.t. a given set of target states F if it almost certainly eventually reaches either F or a state from which F can no longer be reached. While all finite Markov chains are trivially decisive (for every set F), this also holds for many classes of infinite Markov chains. Infinite Markov chains which contain a finite attractor are decisive w.r.t. every set F. In particular, this holds for probabilistic lossy channel systems (PLCS). Furthermore, all globally coarse Markov chains are decisive. This class includes probabilistic vector addition systems (PVASS) and probabilistic noisy Turing machines (PNTM). We consider both safety and liveness problems for decisive Markov chains, i.e., the probabilities that a given set of states F is eventually reached or reached infinitely often, respectively. 1. We express the qualitative problems in abstract terms for decisive Markov chains, and show an almost complete picture of its decidability for PLCS, PVASS and PNTM. 2. We also show that the path enumeration algorithm of Iyer and Narasimha terminates for decisive Markov chains and can thus be used to solve the approximate quantitative safety problem. A modified variant of this algorithm solves the approximate quantitative liveness problem. 3. Finally, we show that the exact probability of (repeatedly) reaching F cannot be effectively expressed (in a uniform way) in Tarski-algebra for either PLCS, PVASS or (P)NTM.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
