Multi-Environment MDPs with Prior and Universal Semantics

In previous works, MEMDPs have been studied under two different semantics: [13, 17, 6] study the model under the universal semantics and [4] studies the model under the prior semantics. In the universal (adversarial) semantics, an adversary picks the environment that the fixed controller strategy has to face; the value of a strategy is its probability to satisfy the objective in the worst environment. In the prior semantics, the environment is drawn initially at random from a fixed distribution (the prior, known to the player); the value is the corresponding expectation. In both cases, the chosen environment is not revealed to the controller. We focus on parity objectives, that are a canonical way of expressing $\omega$-regular properties, and establish structural and algorithmic links between these semantics.

Before presenting our main contributions, we note a qualitative equivalence between the two semantics. The value 1 notions coincide in both the almost-sure and limit-sure senses: there exist strategies that achieve value 1 (resp. arbitrarily close to 1) in the universal semantics if and only if there exist strategies whose prior value is 1 (resp. arbitrarily close to 1). This correspondence lets us transfer value 1 results between the two semantics (see Corollary 3).

Our main contributions can be summarized as follows:

1. 1.

   Approximating the prior value. We give an algorithm that approximates the prior value of an MEMDP to arbitrary precision. This is the most technically demanding part of our contribution. More precisely, we show how to solve algorithmically the $\epsilon$-gap problem for the prior semantics. This problem asks, given an MEMDP $M$, a prior belief $b$ about the operating environment, a parity objective $W$, a threshold , and a precision $\epsilon >0$, to answer YES if the prior value is at least $\alpha$, NO if this value is at most $\alpha -\epsilon$, with no requirement otherwise. Our algorithm runs in PSPACE when probabilities are given in unary, and in EXPSPACE otherwise (see Theorem 10).

2. 2.

   From prior to universal. We also show that the universal value equals the infimum, over all prior beliefs, of the corresponding prior values (see Theorem 11). Using this result together with the 1-Lipschitz continuity of the prior value with respect to the prior belief, we obtain a new algorithm for the universal $\epsilon$-gap problem with the same complexity as for the prior value (PSPACE for unary probabilities, EXPSPACE in general), see Theorem 15, improving on earlier doubly-exponential-space procedures proposed in [6].

3. 3.

   MEMDPs with prior semantics as a tractable POMDP subclass. A key reason for MEMDP tractability is that the hidden environment is fixed, which constrains belief dynamics: the expected (information theory) entropy of the belief about the operating environment is non-increasing. In other words, as a belief entropy measures the amount of information carried by that belief, this means that, on average, the information carried by the environment belief over time does not decrease. We show that in fact any POMDP whose belief entropy is non-increasing can be reduced to a prior-MEMDP (at an exponential cost). Thus, our algorithms apply beyond “pure” MEMDPs and capture a significant subclass of POMDPs, while avoiding classical undecidability phenomena for $\omega$-regular objectives (see Theorem 20).

As recalled above, MEMDPs were introduced under the universal semantics by Raskin and Sankur in [13] as a formal model for decision making in scenarios where the environment is fixed yet unknown, and is chosen from a finite set of candidate models. Within this framework, several qualitative $\omega$-regular synthesis problems become decidable, in contrast to the corresponding situation for POMDPs. Subsequent work has refined the qualitative complexity landscape. For almost-sure satisfaction of Rabin objectives, Suilen et al. establish a PSPACE-complete decision procedure [17]. For parity objectives, Chatterjee et al. prove that the value-1 problem is PSPACE-complete in general (and solvable in PTime when the number of environments is fixed), demonstrate that pure strategies suffice to achieve value 1, and present a double-exponential-space approximation scheme for computing the value [6]. Under the prior semantics, MEMDPs have further been proposed as a computationally tractable subclass of POMDPs with discounted payoffs, leveraging more efficient belief-state updates and a non-increasing belief-entropy property [4].

For context, classical (fully observable) MDP qualitative problems are solvable in polynomial time [1], while analogous POMDP questions are much harder as most of them are undecidable [12, 11], and only bounded horizon questions are known to be decidable [12]. So, in this context, MEMDPs occupy a particular place: they retain an interesting part of the partial-information expressiveness but avoid key undecidability barriers that arise in POMDPs. The positive results obtained in this paper add and refine those obtained in [13, 4, 17, 6].

In [7], the authors independently introduced a subclass of POMDPs, coined Posterior-Deterministic POMDPs, which coincides with the Dirac-preserving POMDPs that we define in Section 5.

We additionally refer to [3], which consider Multi-environment POMDPs to both handle partial observability and multiple environments, and studies both finite-horizon and infinite-horizon discounted-reward objectives. Although their framework is more general than ours, they target a different class of objectives, since we focus on undiscounted infinite-horizon objectives. In this setting, the authors propose both exact and approximate solution algorithms.

Section 2 fixes the notation and formally defines MEMDPs together with the universal and prior values. Section 3 addresses the qualitative and quantitative problems for the prior semantics: it establishes the value-1 equivalence with the universal semantics and develops our approximation algorithm for the prior $\epsilon$-gap problem. Section 4 relates the two semantics by proving that the universal value is the infimum of prior values over all beliefs, and derives an improved complexity for the universal gap problem. Section 5 characterizes MEMDPs as exactly the POMDPs with non-increasing belief entropy, up to an exponential blow-up. Missing details and full proofs can be found in the extended version of the paper [2].

A Markov Decision Process (MDP for short) $𝖦$ is a tuple $𝖦=(Q,A,\delta )$ where $Q$ is a non-empty finite set of states, $A$ is a non-empty finite set of actions, and $\delta :Q\times A\to 𝒟(Q)$ is the transition function mapping each state-action pair to a probability distribution over successor states. An element in $Q\cdot {(A\cdot Q)}^{\ast }$ (resp. ${(Q\cdot A)}^{\omega }$) is called a finite (resp. infinite) run, an element in $Q^{\ast }$ (resp. $Q^{\omega }$) is called a finite (resp. infinite) path. A strategy on $(Q,A)$ is a function $\sigma :Q\cdot {(A\cdot Q)}^{\ast }\to 𝒟(A)$ mapping finite runs to probability distributions over actions. We let $\mathrm{𝖲𝗍𝗋𝖺𝗍}(Q,A)$ denote the set of all strategies on $(Q,A)$.

Consider a non-empty finite set $Q$. An objective $W\subseteq Q^{\omega }$ is a Borel set: $W\in \mathrm{𝖡𝗈𝗋𝖾𝗅}(Q)$. We focus on parity objectives, i.e. objectives $W\in \mathrm{𝖡𝗈𝗋𝖾𝗅}(Q)$ such that there is a labeling function $f:Q\to \mathbb{N}$ such that $W$ is the set of infinite paths whose highest label seen infinitely often is even: $W=\{\rho \in Q^{\omega }\mid \max \{n\in \mathbb{N}\mid \forall i\in \mathbb{N},\exists j\ge i:f({\rho }_j)=n\}\text{ is even}\}$.

Consider an MDP $𝖦=(Q,A,\delta )$. A strategy $\sigma :Q\cdot {(A\cdot Q)}^{\ast }\to 𝒟(A)$ induces a probability measure on the set of finite runs, which can be canonically extended to the associated Borel $\sigma$-algebra over infinite runs. We first define the probability measure induced by a strategy after a fixed finite run $\rho \in Q\cdot {(A\cdot Q)}^{\ast }$. For $\pi \in Q\cdot {(A\cdot Q)}^{\ast }$, we define the value ${\mathbb{P}}_{\rho }^{\sigma }(𝖦,\pi )\in [0,1]$ by induction on the length of $\pi$ as follows. If $|\pi |\le |\rho |$, then we put ${\mathbb{P}}_{\rho }^{\sigma }(𝖦,\pi ):=1$ if $\pi$ is a prefix of $\rho$, and ${\mathbb{P}}_{\rho }^{\sigma }(𝖦,\pi ):=0$ otherwise. For all $\pi \in Q\cdot {(A\cdot Q)}^{\ast }$ such that $\rho$ is a prefix of $\pi$ and for all $(a,t)\in A\times Q$, we define ${\mathbb{P}}_{\rho }^{\sigma }(𝖦,\pi \cdot (a,t)):={\mathbb{P}}_{\rho }^{\sigma }(𝖦,\pi )\cdot \sigma (\pi )(a)\cdot \delta (\mathrm{𝗅𝖺𝗌𝗍}(\pi ),a)(t).$

Then, for all $\pi \in Q\cdot {(A\cdot Q)}^{\ast }$, we define the probability ${\mathbb{P}}_{\rho }^{\sigma }[𝖦,\mathrm{𝖼𝗒𝗅}(\pi )]$ of the cylinder set $\mathrm{𝖼𝗒𝗅}(\pi ):=\{\pi \cdot {\rho }^{\prime }\mid {\rho }^{\prime }\in {(A\cdot Q)}^{\omega }\}\in \mathrm{𝖡𝗈𝗋𝖾𝗅}(Q\cdot A)$ by ${\mathbb{P}}_{\rho }^{\sigma }[𝖦,\mathrm{𝖼𝗒𝗅}(\pi )]:={\mathbb{P}}_{\rho }^{\sigma }(𝖦,\pi )\in [0,1]$. We naturally extend this into a probability measure on Borel sets: ${\mathbb{P}}_{\rho }^{\sigma }[𝖦,\cdot ]:\mathrm{𝖡𝗈𝗋𝖾𝗅}(Q\cdot A)\to [0,1]$. We obtain the probability measure of Borel sets in $\mathrm{𝖡𝗈𝗋𝖾𝗅}(Q)$ via projection.

A Multi-Environment Markov Decision Process (MEMDP for short) $\mathrm{\Gamma }$ is a tuple $\mathrm{\Gamma }=(Q,A,E,{({\delta }_e)}_{e\in E})$ where $E$ is a non-empty finite set of environments, and for all $e\in E$, $(Q,A,{\delta }_e)$ is an MDP, which we denote $\mathrm{\Gamma }[e]$. Unless otherwise stated, an MEMDP $\mathrm{\Gamma }$ refers to the tuple $\mathrm{\Gamma }=(Q,A,E,{({\delta }_e)}_{e\in E})$. For all $e\ne e^{\prime }\in E$, a state-action pair $(q,a)\in Q\times A$ is $(e,e^{\prime })$-distinguishing if ${\delta }_e(q,a)\ne {\delta }_{e^{\prime }}(q,a)$. We let $\mathrm{𝖣𝗌𝗍𝗀}(\mathrm{\Gamma },e,e^{\prime })$ denote the set of all $(e,e^{\prime })$-distinguishing state-action pairs. We also let $\mathrm{𝖣𝗌𝗍𝗀}(\mathrm{\Gamma }):={\cup }_{e\ne e^{\prime }\in E}\mathrm{𝖣𝗌𝗍𝗀}(\mathrm{\Gamma },e,e^{\prime })$.

Consider an MEMDP and a parity objective whose probability we seek to maximize. When synthesizing a strategy in an MEMDP, we do not know in which environment it executes. Thus, when defining the value of a synthesized strategy, we may require either that it performs well in all environments or, given a prior belief on the operating environment, that it performs well on average. The goal of this paper is to study the latter “prior” value, and to link it to the former “universal” value. Specifically, given an MEMDP $\mathrm{\Gamma }$, a state $q\in Q$, and a parity objective $W\in \mathrm{𝖡𝗈𝗋𝖾𝗅}(Q)$, we define $\mathrm{𝗎𝗇𝗂}$-values

and $\mathrm{𝗉𝗋}$-values, given a prior belief $b\in 𝒟(E)$

Lemmas 13 and 14 together imply Theorem 11. This theorem gives us that computing the $\mathrm{𝗎𝗇𝗂}$-value amounts to computing the infimum of $\mathrm{𝗉𝗋}$-values over all prior beliefs. Furthermore, Lemma 7 gives us that $\mathrm{𝗉𝗋}$-values induced by two close beliefs are not far-off. Therefore, we can obtain an $\epsilon$-approximation of the $\mathrm{𝗎𝗇𝗂}$-value by computing the $\mathrm{𝗉𝗋}$-value for enough prior beliefs that tightly cover the set of all beliefs. We deduce the theorem below that significantly improves the doubly-exponential-space complexity established in [6].