Decisiveness for countable MDPs and insights for NPLCSs and POMDPs

TL;DR

This paper extends the concept of decisiveness to countable MDPs, providing a unified framework for analysis and approximation of reachability and safety probabilities, with applications to lossy channel systems and POMDPs.

Contribution

It introduces a general decisiveness framework for countable MDPs, enabling simple model-checking algorithms and broad applicability to various classes of models.

Findings

Decisiveness facilitates approximation of reachability and safety probabilities.

The framework applies to non-deterministic probabilistic lossy channel systems.

It provides algorithms for safety probability estimation in POMDPs.

Abstract

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 proven 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 is a sufficient condition for simple qualitative and approximate quantitative model-checking algorithms to exist. In contrast, existing works on the formal analysis of countable MDPs usually rely on ad hoc techniques tailored to specific classes. We provide here a general framework to analyse countable MDPs by extending the notion of decisiveness. Compared to Markov chains, MDPs exhibit extra non-determinism 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 reachability and safety probabilities in countable MDPs using simple model-checking procedures. We then instantiate our generic approach to two concrete classes of models inducing countable MDPs: non-deterministic probabilistic lossy channel systems and partially observable MDPs. This leads to an algorithm to approximately compute safety probabilities in each of these classes.