Decisiveness for countable MDPs and insights for NPLCSs and POMDPs

TL;DR

This work extends decisiveness, a key property for infinite Markov chains, to countable Markov decision processes (MDPs) by introducing $\inf$-decisiveness and $\sup$-decisiveness. It develops two generic approximation schemes that compute lower and upper bounds for infimum and supremum reachability probabilities, with convergence guaranteed under well-founded decisiveness conditions. The authors instantiate the framework to non-deterministic probabilistic lossy channel systems (NPLCSs) and partially observable MDPs (POMDPs), obtaining algorithms to approximate infimum reachability probabilities in these challenging infinite-state models. These results enable robust quantitative analysis of infinite-state systems and provide a foundation for extending automated verification techniques to broader classes of MDPs with nondeterminism and partial observability.

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.

Figures (9)

• Figure 1: Example of a finitely branching MDP with infinite state space. For readability, the absorbing states ${{\textnormal{\large\smiley}}}$ and ${{\textnormal{\large\frownie}}}$ are duplicated in the figure. Self-loops on absorbing states are omitted.
• Figure 2: Left: MDP $\calM^{\mathtt{L}}$ for which $\mathbb{P}^{\inf}_{\calM^{\mathtt{L}}, s_0}( \text{\rmfamily\upshape\bfseries {F}}_{{}} \,\xspace{{\textnormal{\large\smiley}}}) = 0$, yet for every scheduler $\sigma$, $\mathbb{P}^{\sigma}_{\calM^{\mathtt{L}}, s_0}( \text{\rmfamily\upshape\bfseries {F}}_{{}} \,\xspace{{\textnormal{\large\smiley}}}) > 0$. Right: MDP $\calM^{\mathtt{R}}$ such that $\mathsf{Avoid}^{\sup}_{\calM^{\mathtt{R}}}({{\textnormal{\large\smiley}}}) \neq \mathsf{Avoid}^\sigma_{\calM^{\mathtt{R}}}({{\textnormal{\large\smiley}}})$ for some scheduler $\sigma$.
• Figure 3: An infinitely branching MDP $\calM$ such that $0 = \lim_n \inf_\sigma \mathbb{P}^{\sigma}_{\calM,s_0}( \text{\rmfamily\upshape\bfseries {F}}_{{\le n}} \,\xspace {{\textnormal{\large\smiley}}}) < \inf_\sigma \lim_n \mathbb{P}^{\sigma}_{\calM,s_0}( \text{\rmfamily\upshape\bfseries {F}}_{{\le n}} \,\xspace {{\textnormal{\large\smiley}}}) = 1$.
• Figure 4: Construction of the sliced MDP $\calM^{\textup{\sffamily opt}\xspace}_n$ (right) from $\calM^{\textup{\sffamily opt}\xspace}$ (left).
• Figure 5: A simple example of a channel system (with a single FIFO channel).

Theorems & Definitions (74)

• definition 1
• definition 2
• remark 1
• lemma 1
• lemma 2
• definition 3
• definition 4: Decisiveness
• remark 2
• definition 5
• remark 3