可数MDP的决断性及其对NPLCSs和POMDPs的启示
Decisiveness for countable MDPs and insights for NPLCSs and POMDPs
AI总结：
本文扩展决断性概念至可数MDP，提出通用框架，以对抗或合作方式处理非确定性，实现可达性和安全性概率的近似计算，并应用于非确定性概率损失信道系统和部分可观察MDP。
摘要：
马尔可夫链和马尔可夫决策过程（MDP）是成熟的概率模型。虽然有限马尔可夫模型已被充分理解，但分析其无限对应物仍然是一个重大挑战。决断性已被证明是可数马尔可夫链的一个优雅性质：它足够通用，可被几类自然的可数马尔可夫链满足，并且它是简单定性和近似定量模型检测算法存在的充分条件。相比之下，现有的可数MDP形式分析工作通常依赖于针对特定类别的临时技术。我们通过扩展决断性的概念，提供了一个分析可数MDP的通用框架。与马尔可夫链相比，MDP表现出额外的非确定性，这种非确定性可以以对抗性或合作性的方式解决，导致多种自然的决断性概念。我们表明，这些概念使得使用简单模型检测程序近似计算可数MDP中的可达性和安全性概率成为可能。然后，我们将我们的通用方法实例化到两类产生可数MDP的具体模型：非确定性概率损失信道系统和部分可观察MDP。这导致了一种算法，可以在每类中近似计算安全性概率。
英文摘要：
Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analysing their infinite counterparts remains a significant challenge. Decisiveness has proved to be an elegant property for countable Markov chains: it is general enough to be satisfied by several natural classes of countable Markov chains, and it guarantees the termination of simple qualitative and approximate quantitative model-checking algorithms. In contrast, existing work on the formal analysis of countable MDPs usually relies on ad hoc techniques tailored to specific classes. In this paper, we provide a general framework to analyse countable MDPs (with finitely many enabled actions per state) by extending the notion of decisiveness. Compared to Markov chains, MDPs exhibit an additional nondeterministic choice that can be resolved in an adversarial or cooperative way, leading to multiple natural notions of decisiveness. We show that these notions enable the approximation of supremum reachability and infimum reachability (equivalently, supremum safety) probabilities in countable MDPs using generic approximation schemes. We then instantiate our generic approach to two concrete classes of models inducing countable MDPs: nondeterministic probabilistic lossy channel systems (NPLCSs) and partially observable MDPs (POMDPs). This leads to concrete algorithms to compute approximations to supremum safety probabilities in each of these classes.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
