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.

翻译：暂无翻译