决定性马尔可夫链

我们考虑无限状态马尔可夫链的定性和定量验证问题。如果一条马尔可夫链关于给定目标状态集 F 几乎必然最终到达 F 或到达一个无法再到达 F 的状态，则称其关于 F 是决定性的 (decisive)。虽然所有有限马尔可夫链对于任意集合 F 都是平凡决定性的，但这一性质也适用于许多类无限马尔可夫链。包含有限吸引子 (finite attractor) 的无限马尔可夫链关于任意集合 F 都是决定性的；特别是，这适用于概率有损信道系统 (PLCS)。此外，所有全局粗粒度 (globally coarse) 马尔可夫链也是决定性的，该类包括概率向量加法系统 (PVASS) 和概率噪声图灵机 (PNTM)。我们考虑了决定性马尔可夫链的安全性和活性 (liveness) 问题，即给定状态集 F 最终被到达或被无限次到达的概率。1. 我们以抽象术语表达了决定性马尔可夫链的定性问题，并展示了 PLCS、PVASS 和 PNTM 可判定性的几乎完整图景。2. 我们还证明了 Iyer 和 Narasimha 的路径枚举算法对决定性马尔可夫链终止，因此可用于解决近似定量安全性问题；该算法的修改变体可解决近似定量活性问题。3. 最后，我们表明，对于 PLCS、PVASS 或 (P)NTM，无法在 Tarski 代数中以统一方式有效表达（重复）到达 F 的精确概率。