Value Iteration for Stochastic Parity Games
July 20, 2026
Abstract
We present the first (bounded) value iteration algorithm for the quantitative analysis of stochastic parity games, a fundamental model for probabilistic verification with \(\omega\)-regular objectives. Existing algorithms are based on strategy iteration, which repeatedly computes optimal strategies for one player while fixing the other, leading to high computational cost. Our algorithm instead operates directly on a lattice-theoretic characterization of winning probabilities, exploiting structural properties of (almost-sure qualitative) winning states under parity objectives. We prove correctness and convergence of the proposed algorithm.
1 Introduction↩︎
Stochastic Parity Games. Stochastic parity games (SPGs) are zero-sum, non-terminating games played on probabilistic transition systems between two players, Even (denoted by \({\square}\)) and Odd (denoted by \({\triangle}\)).1 Each state is assigned a natural number, called a priority. At each step, the player controlling the current state selects an available action, after which the game moves to a successor state according to a predefined probability distribution decided by the chosen action. Under the parity objective, an infinite path is winning for Even if the minimum priority appearing infinitely often along the path is even; otherwise, the path is winning for Odd. Accordingly, each player aims to select actions so as to optimize their probability of winning.
Stochastic parity games play a central role in several areas of computer science. Prior theoretical work establishes that SPGs are determined, meaning that for every state the winning probabilities of the two players sum to one [1], [2]. Moreover, SPGs admit optimal strategies that are pure (deterministic) and memoryless (positional) [3], [4]. Consequently, the decision problem for SPGs lies in the complexity class \(\mathbf{NP} \cap \mathbf{coNP}\).
In addition, solving SPGs is polynomial-time equivalent to solving stochastic reachability, mean-payoff, discounted-payoff, and terminal-payoff games [5]–[7]. Due to their expressiveness, SPGs have numerous applications, including reasoning about cyber-physical systems, economic models, computer networks, software systems, and security [8]–[10].
Previous Works: Strategy Iteration. Despite extensive theoretical results on SPGs, only a few algorithms are available for quantitatively solving SPGs, i.e., computing the winning probability from a given initial state. The first such approach was proposed by Chatterjee and Henzinger [11], followed by the other by Hahn et al. [12].
Both approaches are based on the same underlying technique, namely strategy iteration. The algorithm starts with an arbitrary strategy for one player, say Even. By fixing Even’s strategy, the SPG reduces to a Markov decision process (MDP). An optimal strategy for the other player, Odd, can then be computed for this MDP using existing techniques, e.g., [13], [14].
The resulting strategy for Odd is subsequently used to improve Even’s strategy so as to increase Even’s winning probabilities. The improved Even’s strategy is then used in the next iteration, where Odd’s optimal strategy is recomputed and Even’s strategy is further refined. This process repeats until Even’s strategy cannot be improved, at which point it is optimal and the corresponding winning probabilities are obtained.
Due to its nature, strategy iteration can be computationally expensive, as it requires constructing optimal strategies in each iteration. Indeed, Hahn et al. [12] reported that a significant portion of the overall runtime is spent on repeatedly solving MDPs.
Bounded Value Iteration. Another widely used technique for computing winning probabilities is value iteration [15]. This technique has been applied to solve parity games on Markov chains and MDPs, but, to the best of our knowledge, not SPGs. In practical settings where approximate probabilities suffice, value iteration is often preferred due to its favorable performance characteristics [16], [17].
Value iteration is based on a lattice-theoretic fixed-point characterization of winning probabilities. The algorithm initializes a value for each state and repeatedly updates these values using local update rules. Owing to this local nature of the value updates, value iteration is generally more efficient in practice than global strategy-based methods.
For stochastic reachability games (also known as simple stochastic games [18]), several variants of value iteration have been proposed [19]–[26]. To provide precision guarantees, these algorithms compute both lower and upper approximations of the winning probabilities, a technique commonly referred to as bounded value iteration (BVI).
This Work: The First BVI for SPGs. In this work, we present the first bounded value iteration algorithm for the quantitative computation of winning probabilities in stochastic parity games. The main challenge stems from the fact that these winning probabilities do not correspond to the least or greatest fixed points of the one-step Bellman operator (cf. Definition [def:bellman]), in contrast to simpler objectives such as reachability or safety. Consequently, value updates based solely on local reasoning are insufficient for deriving converging lower and upper bounds.
To address this issue, we incorporate global (qualitative) information, namely the (almost-sure qualitative) winning regions of each player under the parity objective in suitably defined subgames. These subgames evolve dynamically with the current lower and upper approximations. Under an optimal play, Even avoids remaining in states that are almost-sure winning for Odd, and vice versa. Our value update operators are designed to capture this strategic behavior by adjusting values in accordance with these global considerations.
Although the structure of our algorithm may resemble that of [21], ours is based on fundamentally different principles and do not rely on any assumptions required in that work. Specifically, [21] requires that the winning probabilities correspond to the least or greatest fixed point of the one-step Bellman operator, whereas ours makes no such assumption; moreover, their approach relies on reasoning over MDPs, while ours works directly on SPGs. More details are given in Section 4.5.
Contributions. Our main technical contribution is the first BVI algorithm for SPGs called SPG-BVI (Algorithm 3). We establish its correctness and convergence, and provide a detailed illustrative example of its execution.
Organization. The remainder of the paper is structured as follows. Section 2 introduces the necessary preliminaries, and Section 3 surveys related work. In Section 4, we present our SPG-BVI algorithm for SPGs together with proofs of correctness and convergence. Section 5 concludes the paper.
2 Preliminaries↩︎
For a finite set \(S\), the set of all functions from \(S\) to \([0,1]\) is denoted by \([0,1]^S\), and the set of all discrete probability distributions on \(S\) is denoted by \({\mathrm{\mathrm{\small Dist}}}(S) := \{ d \in [0,1]^S : \sum_{s \in S} d(s) = 1 \}\).
2.1 Stochastic Parity Games↩︎
Our definition on stochastic parity games is as follows.2
A stochastic parity game (SPG) is \({\mathcal{G}}= (S, {S_{\square}}, {S_{\triangle}}, A, {\mathrm{\mathrm{\small Av}}}, \delta, \mathcal{P})\), where \(S = {S_{\square}}\uplus {S_{\triangle}}\) is a finite set of states partitioned into Even’s \(({S_{\square}})\) and Odd’s \(({S_{\triangle}})\) states, \(A\) is a finite set of actions, \({\mathrm{\mathrm{\small Av}}}: S \to 2^A \setminus \{\emptyset\}\) defines available actions, \(\delta : S \times A \to {\mathrm{\mathrm{\small Dist}}}(S)\) is a transition function, and \(\mathcal{P} : S \to \mathbb{N}\) is a priority function.
The semantics of SPGs is defined as usual [27], [28]. Let \({\mathrm{\mathrm{\small Post}}}(s,a) := \{ s' \in S : \delta(s,a,s') > 0 \}\). An infinite sequence \(\rho = s_0 a_0 s_1 a_1 \ldots \in (S \times A)^\omega\) is an infinite path through \({\mathcal{G}}\) if \(a_i \in {\mathrm{\mathrm{\small Av}}}(s_i)\) and \(s_{i+1} \in {\mathrm{\mathrm{\small Post}}}(s_i,a_i)\) for all \(i \in \mathbb{N}\). A finite sequence \(\rho = s_0 a_0 s_1 a_1 \ldots s_n \in (S \times A)^* \times S\) is a finite path through \({\mathcal{G}}\) if it is a prefix of an infinite path.
A strategy \({\sigma_{\square}}\) of Even is a function \({\sigma_{\square}}: {S_{\square}}\to A\) such that \({\sigma_{\square}}(s) \in {\mathrm{\mathrm{\small Av}}}(s)\) for all \(s \in {S_{\square}}\). A strategy \({\sigma_{\triangle}}\) of Odd is defined analogously. We restrict our consideration to strategies of this form (i.e., pure memoryless strategies) as they are complete for finite SPGs with the parity objective [3], [4]. The sets of all strategies of Even and Odd are denoted by \({\mathrm{\mathrm{\small Str}}_{\square}}\) and \({\mathrm{\mathrm{\small Str}}_{\triangle}}\), respectively.
A pair of strategies is \({\mathrm{\Sigma}}= ({\sigma_{\square}},{\sigma_{\triangle}}) \in {\mathrm{\mathrm{\small Str}}_{\square}}\times {\mathrm{\mathrm{\small Str}}_{\triangle}}\). For notational convenience, we also refer to \({\mathrm{\Sigma}}= ({\sigma_{\square}},{\sigma_{\triangle}})\) as the function \({\mathrm{\Sigma}}: S \to A\) such that \({\mathrm{\Sigma}}(s) = {\sigma_{\square}}(s)\) if \(s \in {S_{\square}}\) and \({\mathrm{\Sigma}}(s) = {\sigma_{\triangle}}(s)\) if \(s \in {S_{\triangle}}\).
Given an SPG \({\mathcal{G}}\), fixing a pair \({\mathrm{\Sigma}}\) of strategies results in a Markov chain \({\mathcal{G}}^{\mathrm{\Sigma}}\) with a transition function \(\delta^{\mathrm{\Sigma}}: S \to {\mathrm{\mathrm{\small Dist}}}(S)\) where \(\delta^{\mathrm{\Sigma}}(s,s') = \delta(s,{\mathrm{\Sigma}}(s),s')\). Under \({\mathrm{\Sigma}}\), actions \(a_i\) within a path can be omitted.
The probability \(\mathbb{P}^{\mathrm{\Sigma}}\) of a finite path \(\rho = s_0 s_1 \ldots s_n \in S^*\) is given by \(\mathbb{P}^{\mathrm{\Sigma}}(\rho) := \prod_{i \in [0,n-1]} \delta^{\mathrm{\Sigma}}(s_i,s_{i+1})\). As described in [28], the probability can be extended to all measurable sets of \(S^\omega\). For a starting state \(s \in S\) and a subset \(S' \subseteq S\), we denote the probability of eventually reaching \(S'\) from \(s\) and that of always staying in \(S'\) by \(\mathbb{P}^{\mathrm{\Sigma}}_s(\textsf{F}\,S')\) and \(\mathbb{P}^{\mathrm{\Sigma}}_s(\textsf{G}\,S')\), respectively.
Parity Objective. For an infinite path \(\rho = s_0 a_0 s_1 a_1 \ldots \in (S \times A)^\omega\), the set of states which are visited infinitely often in \(\rho\) is denoted by \({\mathrm{\mathrm{\small Inf}}}(\rho) := \{ s \in S : \forall i \in \mathbb{N}, \exists j > i, s = s_j \}\). For \(S' \subseteq S\), let \(\mathcal{P}(S') := \{ \mathcal{P}(s') : s' \in S' \}\), where \(\mathcal{P} : S \to \mathbb{N}\) is the priority function from Definition [def:game].
The (Even) parity objective requires that the minimum priority visited infinitely often along an infinite path is even. That is, we are interested in the measurable set \({\mathrm{\mathrm{\small Parity}}}_{\square}:= \{ \textrm{infinite path } \rho : \min(\mathcal{P}({\mathrm{\mathrm{\small Inf}}}(\rho))) \textrm{ is even} \}\). The Odd parity objective and the measurable set \({\mathrm{\mathrm{\small Parity}}}_{\triangle}\) are defined analogously. Throughout the paper, when a player is not specified, the parity objective refers to the Even parity objective.
The goal of this work is to determine \(\mathbb{P}^{\mathrm{\Sigma}}_s({\mathrm{\mathrm{\small Parity}}}_{\square})\) under a pair of optimal strategies \({\mathrm{\Sigma}}= ({\sigma_{\square}},{\sigma_{\triangle}})\), formally defined by the value function \(\mathcal{V} : S \to [0,1]\) as follows (the equality is proved in [4]).
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game]. The value function is the function \(\mathcal{V} : S \to [0,1]\) defined by \[\begin{align} \mathcal{V}(s) := &\max_{{\sigma_{\square}}\in {\mathrm{\mathrm{\small Str}}_{\square}}} \min_{{\sigma_{\triangle}}\in {\mathrm{\mathrm{\small Str}}_{\triangle}}} \mathbb{P}^{\mathrm{\Sigma}}_s({\mathrm{\mathrm{\small Parity}}}_{\square})\\ = &\min_{{\sigma_{\triangle}}\in {\mathrm{\mathrm{\small Str}}_{\triangle}}} \max_{{\sigma_{\square}}\in {\mathrm{\mathrm{\small Str}}_{\square}}} \mathbb{P}^{\mathrm{\Sigma}}_s({\mathrm{\mathrm{\small Parity}}}_{\square}). \end{align}\]
Example 1. Figure 1 (left) illustrates an example of an SPG, where Even’s states and Odd’s states are shown as \({\square}\) and \({\triangle}\), respectively. We denote \({\square}_i\) and \({\triangle}_i\) for Even’s and Odd’s state with priority \(i\), respectively. Optimal strategies are in bold. Its value function is \(\mathcal{V} : {\triangle}_2,{\square}_4 \mapsto 1 \mid {\square}_0 \mapsto 0.7 \mid {\triangle}_1,{\square}_2 \mapsto 0.2 \mid {\square}_3 \mapsto 0\).
End Component. The notion of end component [28] is first introduced in the context of MDPs and is then extended (e.g., as in [13], [19]–[21]) for stochastic games. We state the definition as follows.
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game]. A pair \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E)\), where \(\emptyset \neq S_E \subseteq S\) and \({\mathrm{\mathrm{\small Av}}}_E : S_E \to 2^A \setminus \{\emptyset\}\) such that \({\mathrm{\mathrm{\small Av}}}_E(s) \subseteq {\mathrm{\mathrm{\small Av}}}(s)\) for all \(s \in S_E\), is an end component (EC) if
\(\forall s \in S_E, \forall a \in {\mathrm{\mathrm{\small Av}}}_E(s), {\mathrm{\mathrm{\small Post}}}(s,a) \subseteq S_E\), and
\(\forall s',s'' \in S_E\), there exists a finite path \(\rho = s_0 a_0 s_1 a_1 \ldots s_n \in (S_E \times A)^* \times S_E\) for some \(n \in \mathbb{N}\) such that \(s_0 = s'\), \(s_n = s''\), and \(a_i \in {\mathrm{\mathrm{\small Av}}}_E(s_i)\) for all \(0 \leq i < n\).
Let \(S' \subseteq S\), \({\mathrm{\mathrm{\small Av}}}' : S \to 2^A \setminus \{\emptyset\}\), and \(E = (S_E, {\mathrm{\mathrm{\small Av}}}_E)\) be an EC. We say \(E\) is within \((S',{\mathrm{\mathrm{\small Av}}}')\) if \(S_E \subseteq S'\) and \({\mathrm{\mathrm{\small Av}}}_E(s) \subseteq {\mathrm{\mathrm{\small Av}}}'(s)\) for all \(s \in S_E\). We say \(E\) is maximal within \((S',{\mathrm{\mathrm{\small Av}}}')\) if \(E\) is within \((S',{\mathrm{\mathrm{\small Av}}}')\) and there does not exist an EC \(E' = (S_{E'}, {\mathrm{\mathrm{\small Av}}}_{E'})\) within \((S',{\mathrm{\mathrm{\small Av}}}')\) such that (i) \(S_E \subsetneq S_{E'}\), or (ii) \({\mathrm{\mathrm{\small Av}}}_{E}(s) \subsetneq {\mathrm{\mathrm{\small Av}}}_{E'}(s)\) for some \(s \in S_E\). We say \(E\) is bottom within \((S',{\mathrm{\mathrm{\small Av}}}')\) if \(E\) is within \((S',{\mathrm{\mathrm{\small Av}}}')\) and \({\mathrm{\mathrm{\small Post}}}(s,a) \subseteq S' \implies {\mathrm{\mathrm{\small Post}}}(s,a) \subseteq S_E\) for all \(s \in S_E\) and \(a \in {\mathrm{\mathrm{\small Av}}}'(s)\). We denote the set of all bottom maximal ECs (BMECs) within \((S',{\mathrm{\mathrm{\small Av}}}')\) by \(\mathrm{\small BMEC}(S',{\mathrm{\mathrm{\small Av}}}')\).
Given \(S' \subseteq S\) and \({\mathrm{\mathrm{\small Av}}}' : S \to 2^A \setminus \{\emptyset\}\), the set \(\mathrm{\small BMEC}(S',{\mathrm{\mathrm{\small Av}}}')\) can be computed in polynomial time in the size of \(S'\) and \({\mathrm{\mathrm{\small Av}}}'\) [28].
Example 2. Consider the SPG in Figure 1 (left). A pair \(E_1 = (S_{E_1},{\mathrm{\mathrm{\small Av}}}_{E_1})\), where \(S_{E_1} = \{{\square}_0,{\triangle}_1\}\) and \({\mathrm{\mathrm{\small Av}}}_{E_1} : {\square}_0 \mapsto \{\alpha\} \mid {\triangle}_1 \mapsto \{\beta\}\), is an EC. The EC \(E_1\) is not* maximal within \((S,{\mathrm{\mathrm{\small Av}}})\) since there exists an EC \(E_2 = (S_{E_2}, {\mathrm{\mathrm{\small Av}}}_{E_2})\), where \(S_{E_2} = \{{\square}_0,{\triangle}_1,{\square}_2\}\) and \({\mathrm{\mathrm{\small Av}}}_{E_2}: {\square}_0 \mapsto \{\alpha\} \mid {\triangle}_1 \mapsto \{\alpha,\beta\} \mid {\square}_2 \mapsto \{\alpha\}\), and \(S_{E_1} \subsetneq S_{E_2}\). The EC \(E_2\) is maximal within \((S,{\mathrm{\mathrm{\small Av}}})\). However, \(E_2\) is not bottom within \((S,{\mathrm{\mathrm{\small Av}}})\) since \({\mathrm{\mathrm{\small Post}}}({\square}_0,\beta) \not\subseteq S_{E_2}\). An EC \(E_3 = (S_{E_3},{\mathrm{\mathrm{\small Av}}}_{E_3})\), where \(S_{E_3} = \{{\triangle}_2\}\) and \({\mathrm{\mathrm{\small Av}}}_{E_3}: {\triangle}_2 \mapsto \{\alpha\}\), is bottom and maximal within \((S,{\mathrm{\mathrm{\small Av}}})\). In contrast, a pair \(E_4 = (S_{E_4}, {\mathrm{\mathrm{\small Av}}}_{E_4})\), where \(S_{E_4} = \{{\square}_3,{\square}_4\}\) and \({\mathrm{\mathrm{\small Av}}}_{E_4} : {\square}_3 \mapsto \{\alpha\} \mid {\square}_4 \mapsto \{\alpha,\beta\}\), is not an EC, as there is no finite path from \({\square}_3\) to \({\square}_4\) inside \(E_4\).*
2.2 Fixed Points in a Complete Lattice↩︎
Various quantitative probabilistic model checking problems, such as computing reachability probabilities, can be formulated as computations of suitable fixed points in suitable complete lattices [28]. We provide brief backgrounds on complete lattices and relevant results.
For our setting, we are interested in the complete lattice \((L := [0,1]^S, \leq)\) where, for \(f,f' \in L\), we write \(f \leq f'\) if and only if \(f(s) \leq f'(s)\) for all \(s \in S\). Its least element is \(\bot : S \to [0,1]\) with \(\bot(s) = 0\) and its greatest element is \(\top : S \to [0,1]\) with \(\top(s) = 1\) for all \(s \in S\).
A function \({\mathrm{\Psi}}: L \to L\) is monotone if \(f \leq f'\) implies \({\mathrm{\Psi}}f \leq {\mathrm{\Psi}}f'\). A lattice element \(f \in L\) is a fixed point of \({\mathrm{\Psi}}\) if \(f = {\mathrm{\Psi}}f\). The least fixed point of \({\mathrm{\Psi}}\), denoted by \(\mu{\mathrm{\Psi}}\), is a fixed point of \({\mathrm{\Psi}}\) satisfying, for any \(f \in L\), \(f = {\mathrm{\Psi}}f \implies \mu{\mathrm{\Psi}}\leq f\). The greatest fixed point of \({\mathrm{\Psi}}\), denoted by \(\nu{\mathrm{\Psi}}\), is defined in a similar manner.
Below is a notable theorem regarding the least and greatest fixed points.
Theorem 1 ((special case of) Kleene [29]). Let \((L, \leq)\) be a complete lattice and \({\mathrm{\Psi}}: L \to L\) be an \(\omega\)-continuous function (i.e., \({\mathrm{\Psi}}(\sup L') = \sup\{ {\mathrm{\Psi}}f : f \in L' \}\) for any increasing \(\omega\)-chain \(L' \subseteq L\)). Then, the bottom-up Kleene sequence \(\bot \leq {\mathrm{\Psi}}\bot \leq {\mathrm{\Psi}}^2\bot \leq \cdots\) stabilizes at \(\omega\) such that \(\mu{\mathrm{\Psi}}= {\mathrm{\Psi}}^\omega\bot = {\mathrm{\Psi}}^{\omega+1}\bot = \cdots\;\).3
Dually, let \({\mathrm{\Psi}}\) be an \(\omega^\textrm{op}\)-cocontinuous function (i.e., \({\mathrm{\Psi}}(\inf L') = \inf\{ {\mathrm{\Psi}}f : f \in L' \}\) for any decreasing \(\omega\)-chain \(L' \subseteq L\)). Then, the top-down Kleene sequence \(\top \geq {\mathrm{\Psi}}\top \geq {\mathrm{\Psi}}^2\top \geq \cdots\) stabilizes at \(\omega\) such that \(\nu{\mathrm{\Psi}}= {\mathrm{\Psi}}^\omega\top = {\mathrm{\Psi}}^{\omega+1}\top = \cdots\;\).
Value Iteration. When a problem is formulated as the computation of the least fixed point \(\mu{\mathrm{\Psi}}\) of \({\mathrm{\Psi}}\), one can apply Theorem 1 to approximate this least fixed point: starting from \(\bot\) and iteratively applying \({\mathrm{\Psi}}\) to the current lattice element. This procedure is commonly known as value iteration. Note that \({\mathrm{\Psi}}^i\bot \leq \mu{\mathrm{\Psi}}\) holds for all \(i \in \mathbb{N}\).
Since it could happen that \({\mathrm{\Psi}}^i\bot < {\mathrm{\Psi}}^\omega\bot = \mu{\mathrm{\Psi}}\) for all \(i \in \mathbb{N}\), it may not be possible to precisely compute \(\mu{\mathrm{\Psi}}\) via value iteration. Nevertheless, in practice, it is usually sufficient to compute an approximation that is \(\varepsilon\)-close to \(\mu{\mathrm{\Psi}}\) for some desired precision \(\varepsilon > 0\). The rest of Section 2.2 targets at this problem.
A straightforward approach is to stop the iteration when \(\max_{s \in S}(({\mathrm{\Psi}}^i\bot)(s)-({\mathrm{\Psi}}^{i-1}\bot)(s)) \leq \varepsilon\). However, it is shown in [30] that such \({\mathrm{\Psi}}^i\bot\) is not guaranteed to be \(\varepsilon\)-close to \(\mu{\mathrm{\Psi}}\). To our best knowledge, the bottom-up Kleene sequence alone is not sufficient to provide an \(\varepsilon\)-close approximation of \(\mu{\mathrm{\Psi}}\).
Bounded Value Iteration (BVI). When \(\mu{\mathrm{\Psi}}= \nu{\mathrm{\Psi}}\) (i.e., when \({\mathrm{\Psi}}\) has a unique fixed point), one can perform value iteration from both \(\bot\) and \(\top\). This procedure is known as bounded value iteration (also called interval iteration). Note that \({\mathrm{\Psi}}^i\top \geq \nu{\mathrm{\Psi}}\) holds for all \(i \in \mathbb{N}\). During this bounded iteration, when \(\max_{s \in S}(({\mathrm{\Psi}}^i\top)(s)-({\mathrm{\Psi}}^i\bot)(s)) \leq 2\varepsilon\), one can guarantee that \(\frac{1}{2}({\mathrm{\Psi}}^i\bot+{\mathrm{\Psi}}^i\top)\) is \(\varepsilon\)-close to \(\mu{\mathrm{\Psi}}= \nu{\mathrm{\Psi}}\).
We point out that not all functions \({\mathrm{\Psi}}\) have a unique fixed point. In the case where we would like to compute \(\mu{\mathrm{\Psi}}\) (or \(\nu{\mathrm{\Psi}}\)), it may be possible to construct \({\mathrm{\Psi}}'\) with a unique fixed point such that \(\mu{\mathrm{\Psi}}'=\nu{\mathrm{\Psi}}'=\mu{\mathrm{\Psi}}\) (or \(\nu{\mathrm{\Psi}}\)), and when possible, the construction may not be straightforward. Interested readers are referred to, e.g., [13], [24], [28] for further details.
2.3 Bellman Operator↩︎
Building on Section 2.2, we now review the Bellman operator, a key function used in computing value functions for a range of quantitative objectives. Our definition is based on a notion of state-action expectation as follows.
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game]. The state-action expectation of a function \(f \in [0,1]^S\) for a state-action pair \((s,a) \in S \times A\) is \(\phi_f(s,a) := \sum_{s' \in S} \delta(s,a,s')\cdot f(s')\).
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game]. The Bellman operator is the function \({\mathrm{\Phi}}: [0,1]^S \to [0,1]^S\) where, for \(f \in [0,1]^S\) and \(s \in S\), \[({\mathrm{\Phi}}f)(s) := \begin{cases} \textstyle\max_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_f(s,a) & \textrm{if } s \in {S_{\square}}\textrm{, and}\\ \textstyle\makebox[\widthof{\max_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_f(s,a)}][r]{\min_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_f(s,a)} & \textrm{if } s \in {S_{\triangle}}. \end{cases}\]
It is well-known that (i) \({\mathrm{\Phi}}\) is monotone, and (ii) the value function \(\mathcal{V}\) (cf. Definition [def:valfunc]) is a fixed point of the Bellman operator \({\mathrm{\Phi}}\) (i.e., \(\mathcal{V} = {\mathrm{\Phi}}\mathcal{V}\)). However, in general, \(\mathcal{V}\) does not coincide with either the least or the greatest fixed point of \({\mathrm{\Phi}}\) (i.e., \(\mathcal{V} \neq \mu{\mathrm{\Phi}}\) and \(\mathcal{V} \neq \nu{\mathrm{\Phi}}\)).
For the reachability and safety objectives, we consider the following modification of the Bellman operator.
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game], \(S' \subseteq S\), and \(c \in [0,1]\). The modified Bellman operator is the function \({\mathrm{\Phi}}_{(S',c)} : [0,1]^S \to [0,1]^S\) where, for \(f \in [0,1]^S\) and \(s \in S\), \[({\mathrm{\Phi}}_{(S',c)} f)(s) := \begin{cases} c & \textrm{if } s \in S' \textrm{,}\\ \textstyle\max_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_f(s,a) & \textrm{if } s \in {S_{\square}}\setminus S' \textrm{, and}\\ \textstyle\makebox[\widthof{\max_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_f(s,a)}][r]{\min_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_f(s,a)} & \textrm{if } s \in {S_{\triangle}}\setminus S'. \end{cases}\]
The optimal reachability probability \(\mathbb{P}^{\mathrm{\Sigma}}_s(\mathsf{F}\,S')\) under an optimal pair of strategies \({\mathrm{\Sigma}}\) is easily shown to be the least fixed point of \({\mathrm{\Phi}}_{(S',1)}\), i.e., \(\mathbb{P}^{\mathrm{\Sigma}}_s(\mathsf{F}\,S') = \mu{\mathrm{\Phi}}_{(S',1)}\). Dually, the optimal safety probability \(\mathbb{P}^{\mathrm{\Sigma}}_s(\mathsf{G}\,S')\) under an optimal pair of strategies \({\mathrm{\Sigma}}\) is easily shown to be the greatest fixed point of \({\mathrm{\Phi}}_{(S \setminus S',0)}\), i.e., \(\mathbb{P}^{\mathrm{\Sigma}}_s(\mathsf{G}\,S') = \nu{\mathrm{\Phi}}_{(S \setminus S',0)}\).
3 Related Work↩︎
3.1 Solving Qualitative SPGs↩︎
As our algorithm for solving the quantitative SPG problem relies on solving its qualitative counterpart, we review the relevant literature below.
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game] and \(\mathcal{V}\) be the value function as in Definition [def:valfunc]. The (almost-sure qualitative) winning set of Even is the set \(W_{\square}:= \{ s \in S : \mathcal{V}(s) = 1 \}\). The (almost-sure qualitative) winning set of Odd is the set \(W_{\triangle}:= \{ s \in S : \mathcal{V}(s) = 0 \}\).
Given an SPG \({\mathcal{G}}\), the qualitative SPG problem is to output the winning set \(W_{\square}\) of Even.
Note that the winning set \(W_{\triangle}\) of Odd for an SPG \({\mathcal{G}}\) is the same as the winning set \(\tilde{W}_{\square}\) of Even for the SPG \(\tilde{{\mathcal{G}}}\) where \(\tilde{\mathcal{P}}(s) := \mathcal{P}(s)+1\) for each \(s \in S\).
There are two approaches to solve the qualitative SPG problem: the nested fixed point algorithm [31] and the gadget construction [27].
Nested Fixed Point Algorithm. The first approach is a recursive-style algorithm of Hahn et al. [31]. It can be considered as an adaptation of [32], [33] for non-stochastic parity games (i.e., with a transition function \(\delta : S \times A \to S\)).
We first define attractors; they can be computed via iterative fixed-point algorithms.
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game]. The attractors are the functions \({\mathrm{\mathrm{\small Attr}}}_{{\square},\bowtie}\) and \({\mathrm{\mathrm{\small Attr}}}_{{\triangle},\bowtie}: 2^S \to 2^S\), where \(\bowtie\,\,\in \{{>0},{=1}\}\), defined by \[\begin{align} {\mathrm{\mathrm{\small Attr}}}_{{\square},\bowtie}(S') &:= \{ s \in S : \exists {\sigma_{\square}}\in {\mathrm{\mathrm{\small Str}}_{\square}}, \forall {\sigma_{\triangle}}\in {\mathrm{\mathrm{\small Str}}_{\triangle}}, \mathbb{P}^{{\mathrm{\Sigma}}}_s(\mathsf{F}\,S') \bowtie\},\\ {\mathrm{\mathrm{\small Attr}}}_{{\triangle},\bowtie}(S') &:= \{ s \in S : \exists {\sigma_{\triangle}}\in {\mathrm{\mathrm{\small Str}}_{\triangle}}, \forall {\sigma_{\square}}\in {\mathrm{\mathrm{\small Str}}_{\square}}, \mathbb{P}^{{\mathrm{\Sigma}}}_s(\mathsf{F}\,S') \bowtie\}. \end{align}\]
![Figure 2: the algorithm of [31] solving the qualitatve SPG problem.](/article/2607.18355/_pdflatex/yzmjtuec.png "fig:")
The algorithm QualitativeSPG in Algorithm 2 outputs \((W_{\square},L_{\square})\) such that \(W_{\square}\) is the winning set of Even (cf. Definition [def:winset]) and \(L_{\square}= \{ s \in S : \mathcal{V}(s) < 1 \} = S \setminus W_{\square}\). We let \({\mathcal{G}}\setminus X\) denote the subgame \({\mathcal{G}}' = (S',\, S_{\square}\setminus X,\, S_{\triangle}\setminus X,A,{\mathrm{\mathrm{\small Av}}}',\delta,\mathcal{P})\) where \(S' := S \setminus X\) and \({\mathrm{\mathrm{\small Av}}}' : S' \to 2^A \setminus \{\emptyset\}\) with \({\mathrm{\mathrm{\small Av}}}'(s') := \{ a' \in {\mathrm{\mathrm{\small Av}}}(s') : {\mathrm{\mathrm{\small Post}}}(s',a') \subseteq S' \}\) for all \(s' \in S'\).
Gadget Construction. The second approach is to translate an SPG into a non-stochastic parity game via the gadget construction by Chatterjee et al. [27]. The construction is guaranteed to preserve the winning set of one player.
After the construction, any algorithm solving non-stochastic parity games applies, e.g., [32]–[39]. Nonetheless, the size of the constructed non-stochastic parity game can increase by a factor of \(\mathcal{O}(\max(\mathcal{P}(S)))\) compared to the original SPG. This can lead to a longer solving time as observed in [31].
3.2 Solving Quantitative SPGs↩︎
Below is the definition of the problem, which is the focus of this work.
Given an SPG \({\mathcal{G}}\), an initial state \({s_\mathrm{init}}\in S\), and a precision \(\varepsilon > 0\), the quantitative SPG problem is to output a value that is \(\varepsilon\)-close to \(\mathcal{V}({s_\mathrm{init}})\) (i.e., whose difference from \(\mathcal{V}({s_\mathrm{init}})\) is no more than \(\varepsilon\)).
To the best of our knowledge, the only available approach to solve the quantitative SPG problem is by strategy iteration (also called strategy improvement) [11], [12]. The algorithm of [12] was implemented and is available as part of the EPMC model checking tool [40].
Roughly speaking, strategy iteration begins with an arbitrary strategy \(\sigma_{{\square},0}\) of Even. By fixing \(\sigma_{{\square},i}\) for \(i \in \mathbb{N}\), the SPG becomes an MDP, where one can compute an optimal strategy \(\sigma_{{\triangle},i}\) of Odd for the parity objective [13], [14]. By fixing \(\sigma_{{\triangle},i}\), one may improve \(\sigma_{{\square},i}\) to \(\sigma_{{\square},i+1}\) such that the winning probabilities of Even increase. When \(\sigma_{{\square},i}\) cannot be further improved, \(\sigma_{{\square},i}\) is optimal for Even. The value \(\mathcal{V}({s_\mathrm{init}})\) can then be computed accordingly.
It is mentioned in [12] that computing an optimal strategy for a parity objective of an MDP can become a bottleneck. Their experiment showed that more than half of the computation time was contributed to MDP solving.
4 Our BVI Algorithm for SPG↩︎
4.1 Intuition↩︎
Recall that the parity objective is determined by the set of states visited infinitely often. Any infinite path must eventually remain within some end component (EC) in order to visit a state infinitely often. We begin by defining the following classifications of ECs.
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game] and \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E)\) be an EC (cf. Definition [def:ec]). We say that \(E\) is Even-dominating if there exists a strategy \({\sigma_{\square}}\in {\mathrm{\mathrm{\small Str}}_{\square}}\) such that (i) \({\sigma_{\square}}(s) \in {\mathrm{\mathrm{\small Av}}}_E(s)\) for all \(s \in S_E \cap S_{\square}\), and (ii) for all strategies \({\sigma_{\triangle}}\in {\mathrm{\mathrm{\small Str}}_{\triangle}}\) such that \({\sigma_{\triangle}}(s) \in {\mathrm{\mathrm{\small Av}}}_E(s)\) holds for all \(s \in S_E \cap S_{\triangle}\), we have \(\mathbb{P}^{{\mathrm{\Sigma}}}_s({\mathrm{\mathrm{\small Parity}}}_{\square}) = 1\) for all \(s \in S_E\). An Odd-dominating EC is defined analogously.
Intuitively, an EC \(E\) is Even-dominating if Even can ensure winning as long as both players remain within \(E\). Since Odd loses by remaining within \(E\), it is optimal for Odd to exit \(E\) (if possible). Similarly, \(E\) is Odd-dominating if Odd can ensure winning under the same condition, and it is optimal for Even to exit \(E\) (if possible).
Based on the above intuition, our algorithm considers Even-dominating and Odd-dominating ECs, and adjusts the bounds for the winning probabilities accordingly. An example is provided in Section 4.3.
4.2 Algorithm↩︎
Here is our BVI algorithm for the quantitative SPG problem.
Our SPG-BVI algorithm for solving the quantitative SPG problem is in Algorithm 3.
The algorithm maintains two sequences of functions \(\ell_i\) and \(u_i : S \to [0,1]\) for \(i \in \mathbb{N}\). They act as the bottom-up and top-down sequences for the value function \(\mathcal{V}\), respectively. The first elements are initialized as \(\ell_0 \gets \bot\) and \(u_0 \gets \top\).
In the \(i\)-th iteration (\(i > 0\)), two new elements \(\ell_i \gets {\mathrm{\Phi}}\ell_{i-1}\) and \(u_i \gets {\mathrm{\Phi}}u_{i-1}\) are generated. After that, the algorithm computes the restricted actions for both players. For \(s \in {S_{\square}}\), an action \(a \in {\mathrm{\mathrm{\small Av}}}(s)\) is available in \({\mathrm{\mathrm{\small Av}}}'(s)\) if \(\phi_{u_i}(s,a)\) is maximum among all actions in \({\mathrm{\mathrm{\small Av}}}(s)\). For \(s \in {S_{\triangle}}\), an action \(a \in {\mathrm{\mathrm{\small Av}}}(s)\) is available in \({\mathrm{\mathrm{\small Av}}}'(s)\) if \(\phi_{\ell_i}(s,a)\) is minimum among all actions in \({\mathrm{\mathrm{\small Av}}}(s)\). Such restriction induces the estimated-optimal subgame \({\mathcal{G}}'\).
Next, the algorithm computes the winning sets \(W'_{\square}, W'_{\triangle}\) of Even and Odd (cf. Definition [def:winset]), respectively, for the estimated-optimal subgame \({\mathcal{G}}'\). We then look at each bottom maximal EC (BMEC) within \((W'_{\square},{\mathrm{\mathrm{\small Av}}}')\) (cf. Definition [def:ec]), i.e., each \(E \in \mathrm{\small BMEC}(W'_{\square},{\mathrm{\mathrm{\small Av}}}')\). We show that such \(E\) is Even-dominating (cf. Definition [def:win-EC]) in both \({\mathcal{G}}'\) and \({\mathcal{G}}\).
Lemma 1. Let \({\mathcal{G}}\) be an SPG as in Definition [def:game], \({\mathrm{\mathrm{\small Av}}}' : S \to 2^A \setminus \{\emptyset\}\) such that \({\mathrm{\mathrm{\small Av}}}'(s) \subseteq {\mathrm{\mathrm{\small Av}}}(s)\) for all \(s \in S\), \({\mathcal{G}}' = (S,S_{\square},S_{\triangle},A,{\mathrm{\mathrm{\small Av}}}',\delta,\mathcal{P})\) be a subgame of \({\mathcal{G}}\), \(W'_{\square}\) is the winning set of Even (cf. Definition [def:winset]) for \({\mathcal{G}}'\), and \(E \in \textrm{\mathrm{\small BMEC}}(W'_{\square},{\mathrm{\mathrm{\small Av}}}')\) (cf. Definition [def:ec]). Then, \(E\) is an Even-dominating EC (cf. Definition [def:win-EC]) in both \({\mathcal{G}}'\) and \({\mathcal{G}}\).
Proof. Consider an EC \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E) \in \mathrm{\small BMEC}(W'_{\square},{\mathrm{\mathrm{\small Av}}}')\). Because \(E\) is bottom within \((W'_{\square},{\mathrm{\mathrm{\small Av}}}')\), we obtain \({\mathrm{\mathrm{\small Post}}}(s,a) \subseteq W'_{\square}\implies {\mathrm{\mathrm{\small Post}}}(s,a) \subseteq S_E\) for all \(s \in S_E\) and \(a \in {\mathrm{\mathrm{\small Av}}}'(s)\). Due to the maximality of \(E\) within \((W'_{\square},{\mathrm{\mathrm{\small Av}}}')\), it must be the case that \({\mathrm{\mathrm{\small Av}}}_E\) includes all actions within \(S_E\), i.e., \({\mathrm{\mathrm{\small Post}}}(s,a) \subseteq S_E \implies a \in {\mathrm{\mathrm{\small Av}}}_E(s)\) for all \(s \in S_E\) and \(a \in {\mathrm{\mathrm{\small Av}}}'(s)\).
Since \(S_E \subseteq W'_{\square}\), any (almost-sure qualitative) winning strategy \(\sigma'_{\square}: S \to A\) (with \(\sigma'_{\square}(s) \in {\mathrm{\mathrm{\small Av}}}'(s)\) for \(s \in {S_{\square}}\)) of Even with respect to \({\mathcal{G}}'\) (which induces \(W'_{\square}\)) gives \({\mathrm{\mathrm{\small Post}}}(s,\sigma'_{\square}(s)) \subseteq W'_{\square}\) for all \(s \in S_E \cap {S_{\square}}\). Also, Odd cannot escape \(W'_{\square}\) (i.e., \({\mathrm{\mathrm{\small Post}}}(s,\sigma'_{\triangle}(s)) \subseteq W'_{\square}\) for all \(s \in S_E \cap {S_{\triangle}}\) and \(\sigma'_{\triangle}: S \to A\) with \(\sigma'_{\triangle}(s) \in {\mathrm{\mathrm{\small Av}}}'(s)\) for \(s \in {S_{\triangle}}\)). Notice that, for \({\mathrm{\Sigma}}' = (\sigma'_{\square},\sigma'_{\triangle})\), we get \({\mathrm{\mathrm{\small Post}}}(s,{\mathrm{\Sigma}}'(s)) \subseteq W'_{\square}\) for all \(s \in S_E\). This implies \({\mathrm{\mathrm{\small Post}}}(s,{\mathrm{\Sigma}}'(s)) \subseteq S_E\) and \({\mathrm{\Sigma}}'(s) \in {\mathrm{\mathrm{\small Av}}}_E(s)\) for all \(s \in S_E\). Hence, such \(\sigma'_{\square}\) gives a strategy such that \(E\) is Even-dominating. Thus, \(E\) is Even-dominating in \({\mathcal{G}}'\). As all ECs in \({\mathcal{G}}'\) are ECs in \({\mathcal{G}}\), therefore \(E\) is also Even-dominating in \({\mathcal{G}}\). 0◻ ◻
For each \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E) \in \mathrm{\small BMEC}(W'_{\square},{\mathrm{\mathrm{\small Av}}}')\), we set the value \(\ell_i(s)\) for each \(s \in S_E\) to be the maximum of \(\ell_i(s)\) and the exit value \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i)\) from \(E\) for Odd, defined below.
Let \({\mathcal{G}}\) be an SPG as in Definition [def:game], \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E)\) be an EC as in Definition [def:ec], and \(f : S \to [0,1]\) be a function. The exit values \({\mathrm{\mathrm{\small Exit}}}_{\square}\) and \({\mathrm{\mathrm{\small Exit}}}_{\triangle}\) with respect to \(E\) and \(f\) are defined as \[\begin{align} {\mathrm{\mathrm{\small Exit}}}_{\square}(E,f) &:= \max \{ \phi_f(s,a) : s \in S_E \cap S_{\square}, a \in {\mathrm{\mathrm{\small Av}}}(s) \setminus {\mathrm{\mathrm{\small Av}}}_E(s) \},\\ {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f) &:= \,\min \{ \phi_f(s,a) : s \in S_E \cap S_{\triangle}, a \in {\mathrm{\mathrm{\small Av}}}(s) \setminus {\mathrm{\mathrm{\small Av}}}_E(s) \} \end{align}\] with the convention that \(\max \emptyset = 0\) and \(\min \emptyset = 1\).
Dually, for each \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E) \in \mathrm{\small BMEC}(W'_{\triangle},{\mathrm{\mathrm{\small Av}}}')\), it is Odd-dominating in both \({\mathcal{G}}'\) and \({\mathcal{G}}\). We set the value \(u_i(s)\) for \(s \in S_E\) to be \(\min(u_i(s), {\mathrm{\mathrm{\small Exit}}}_{\square}(E,u_i))\). The while loop repeats until \(\ell_i({s_\mathrm{init}})\) and \(u_i({s_\mathrm{init}})\) are close within \(2\varepsilon\), at which point the algorithm stops and returns the middle point \(\frac{1}{2}(\ell_i({s_\mathrm{init}})+u_i({s_\mathrm{init}}))\).
4.3 Example↩︎
We present a detailed example of executing SPG-BVI (Algorithm 3) with the SPG from Figure 1 (left).
Example 3. Let \({\mathcal{G}}\) be the SPG from Figure 1 (left). We represent a function \(f : S \to [0,1]\) by a tuple, namely \(f = (f({\square}_0),f({\triangle}_1),f({\square}_2),f({\triangle}_2),f({\square}_3),f({\square}_4))\). The algorithm begins with \(\ell_0 = (0,0,0,0,0,0)\) and \(u_0 = (1,1,1,1,1,1)\).
For \(i = 1\), \(\ell_1 \gets {\mathrm{\Phi}}\ell_0 = \ell_0\) and \(u_1 \gets {\mathrm{\Phi}}u_0 = u_0\). Under \(\ell_1\) and \(u_1\), we have \({\mathrm{\mathrm{\small Av}}}' = {\mathrm{\mathrm{\small Av}}}\) (i.e., no actions are removed) and \({\mathcal{G}}' = {\mathcal{G}}\). The winning sets of both players are \(W'_{\square}= \{{\triangle}_2,{\square}_4\}\) and \(W'_{\triangle}= \{{\square}_3\}\).
The first Even-dominating BMEC is \(E = (S_E, {\mathrm{\mathrm{\small Av}}}_E)\) with \(S_E = \{{\triangle}_2\}\) and \({\mathrm{\mathrm{\small Av}}}_E : {\triangle}_2 \mapsto \{\alpha\}\). The exit value from \(E\) is \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_1) = 1\) (e.g., the set of exiting actions is empty). Thus, the algorithm sets \(\ell_1({\triangle}_2) \gets 1\). Similarly, we have \(\ell_1({\square}_4) \gets 1\) and \(u_1({\square}_3) \gets 0\). At the end of iteration \(i = 1\), we have \(\ell_1 = (0,0,0,1,0,1)\) and \(u_1 = (1,1,1,1,0,1)\).
For \(i = 2\), \(\ell_2 \gets {\mathrm{\Phi}}\ell_1 = (0.7,0,0.2,1,0,1)\) and \(u_2 \gets {\mathrm{\Phi}}u_1 = (1,0.9,1,1,0,1)\). The subgame \({\mathcal{G}}'\) and its actions under \({\mathrm{\mathrm{\small Av}}}'\) are shown in Figure 1 (middle). The winning sets of both players are \(W'_{\square}= \{{\triangle}_2,{\square}_4\}\) and \(W'_{\triangle}= \{{\square}_0,{\triangle}_1,{\square}_2,{\square}_3\}\).
The BMECs involving \({\triangle}_2,{\square}_3,{\square}_4\) do not result in any modifications of \(\ell_2\) and \(u_2\). When considering \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E) \in \mathrm{\small BMEC}(W'_{\triangle},{\mathrm{\mathrm{\small Av}}}')\) with \(S_E = \{{\triangle}_1,{\square}_2\}\) and \({\mathrm{\mathrm{\small Av}}}_E : {\triangle}_1 \mapsto \{\alpha\} \mid {\square}_2 \mapsto \{\alpha\}\), it is Odd-dominating and Even must escape via \(\beta \in {\mathrm{\mathrm{\small Av}}}({\square}_2) \setminus {\mathrm{\mathrm{\small Av}}}'({\square}_2)\). The exit value from \(E\) is \({\mathrm{\mathrm{\small Exit}}}_{\square}(E,u_2) = 0.2\), hence we obtain \(u_2({\triangle}_1) \gets 0.2\) and \(u_2({\square}_2) \gets 0.2\). At the end of iteration \(i = 2\), we have \(\ell_2 = (0.7,0,0.2,1,0,1)\) and \(u_2 = (1,0.2,0.2,1,0,1)\).
For \(i = 3\), the algorithm computes \(\ell_3 \gets {\mathrm{\Phi}}\ell_2 = (0.7,0.2,0.2,1,0,1)\) and \(u_3 \gets {\mathrm{\Phi}}u_2 = (0.7,0.2,0.2,1,0,1)\). The subgame \({\mathcal{G}}'\) and its actions under \({\mathrm{\mathrm{\small Av}}}'\) are shown in Figure 1 (right). The winning sets of both players are \(W'_{\square}= \{{\triangle}_2,{\square}_4\}\) and \(W'_{\triangle}= \{{\square}_3\}\). No further adjustments are made on both \(\ell_3\) and \(u_3\). At the end of iteration \(i = 3\), we have \(\ell_3 = u_3\). Therefore, the while loop terminates.
4.4 Correctness and Convergence↩︎
We prove the correctness and convergence of our SPG-BVI algorithm (Algorithm 3) by showing that (i) \(\ell_i \leq \ell_{i+1} \leq \mathcal{V} \leq u_{i+1} \leq u_i\) for all \(i \in \mathbb{N}\), and (ii) \(\lim_{i \to \infty} \ell_i = \mathcal{V} = \lim_{i \to \infty} u_i\). We only provide the proofs for the sequence \(\ell_i\). Similar arguments can be done for the sequence \(u_i\).
Lemma 2. Assume the setting of Algorithm 3, \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E)\) be an EC, and \(f : S \to [0,1]\) be a function. Let \(f'(s) := \max(f(s),{\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f))\) if \(s \in S_E\) and \(f'(s) := f(s)\) otherwise. If \(f \leq {\mathrm{\Phi}}f\), then \(f' \leq {\mathrm{\Phi}}f'\).
Proof. Suppose \(f \leq {\mathrm{\Phi}}f\). By the definition of \(f'\), we have \(f \leq f'\). This implies \({\mathrm{\Phi}}f \leq {\mathrm{\Phi}}f'\) by the monotonicity of \({\mathrm{\Phi}}\). If \(f'(s) = f(s)\), then \(f'(s) = f(s) \leq ({\mathrm{\Phi}}f)(s) \leq ({\mathrm{\Phi}}f')(s)\). The remaining case is that \(s \in S_E\) and \(f'(s) = {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f)\). We distinguish cases whether \(s\) belongs to Even or Odd.
If \(s \in S_E \cap S_{\square}\), then there is an action \(\hat{a} \in {\mathrm{\mathrm{\small Av}}}_E(s)\) where \({\mathrm{\mathrm{\small Post}}}(s,\hat{a}) \subseteq S_E\) (since \(E\) is an EC). Consider an arbitrary \(\hat{a}\)-successor \(s'\), that is, \(s' \in {\mathrm{\mathrm{\small Post}}}(s,\hat{a})\), we have \(s' \in S_E\) and \(f'(s') \geq {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f)\) by the definition of \(f'\). Hence, \(\phi_{f'}(s,\hat{a}) \geq {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f)\). Therefore, \[f'(s) = {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f) \leq \phi_{f'}(s,\hat{a}) \leq \max_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_{f'}(s,a) = ({\mathrm{\Phi}}f')(s).\]
If \(s \in S_E \cap S_{\triangle}\), then we consider each \(a \in {\mathrm{\mathrm{\small Av}}}(s)\) and distinguish whether \(a \in {\mathrm{\mathrm{\small Av}}}_E(s)\) or not. If \(a \in {\mathrm{\mathrm{\small Av}}}_E(s)\), we have \(\phi_{f'}(s,a) \geq {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f)\) as for \(\hat{a} \in {\mathrm{\mathrm{\small Av}}}_E(s)\) above. Otherwise, \(a \in {\mathrm{\mathrm{\small Av}}}(s) \setminus {\mathrm{\mathrm{\small Av}}}_E(s)\). By the definition of the exit value (Definition [def:exit]), \(\phi_f(s,a) \geq {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f)\). Since \(f' \geq f\), we have \(\phi_{f'}(s,a) \geq \phi_f(s,a) \geq {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f)\). From both cases, we have \(\phi_{f'}(s,a) \geq {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f)\) for any \(a \in {\mathrm{\mathrm{\small Av}}}(s)\). So, \[\begin{align} f'(s) = {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,f) \leq \min_{a \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_{f'}(s,a) = ({\mathrm{\Phi}}f')(s).\tag*{\qed} \end{align}\] ◻
In the setting of Algorithm 3, \(\ell_i \leq {\mathrm{\Phi}}\ell_i\) for all \(i \in \mathbb{N}\).
Proof. We prove by induction on \(i\). The base case \(i = 0\) is trivially true as \(\ell_0 = \bot\). For the step case, we assume that the statement is true for \(i-1\): \(\ell_{i-1} \leq {\mathrm{\Phi}}\ell_{i-1}\), and show that it is true for \(i\).
By the monotonicity of \({\mathrm{\Phi}}\) and the induction hypothesis, we have \({\mathrm{\Phi}}\ell_{i-1} \leq {\mathrm{\Phi}}({\mathrm{\Phi}}\ell_{i-1})\). As Line [alg2:line4] of Algorithm 3 performs \(\ell_i \gets {\mathrm{\Phi}}\ell_{i-1}\), this implies \(\ell_i \leq {\mathrm{\Phi}}\ell_i\) after Line [alg2:line4]. Moreover, by Lemma 2, the update of \(\ell_i\) in Line [alg2:line9] preserves such property. Thus, \(\ell_i \leq {\mathrm{\Phi}}\ell_i\) holds at the end of the iteration. 0◻ ◻
In the setting of Algorithm 3, \(\ell_i \leq \ell_{i+1}\) for all \(i \in \mathbb{N}\).
Proof. We instead show \(\ell_{i-1} \leq \ell_i\) for \(i > 0\). First, Line [alg2:line4] of Algorithm 3 performs \(\ell_i \gets {\mathrm{\Phi}}\ell_{i-1}\). By Proposition [prop:bellman-monotone], \(\ell_{i-1} \leq {\mathrm{\Phi}}\ell_{i-1} = \ell_i\). Moreover, the update of \(\ell_i\) in Line [alg2:line9] is non-decreasing. Hence, \(\ell_{i-1} \leq \ell_i\) holds at the end of the iteration. 0◻ ◻
Lemma 3. In the setting of Algorithm 3, \(\ell_i \leq \mathcal{V}\) for all \(i \in \mathbb{N}\).
Proof. We prove by induction on \(i\). The base case \(i = 0\) is trivially true as \(\ell_0 = \bot\). For the step case, we assume that the statement is true for \(i-1\): \(\ell_{i-1} \leq \mathcal{V}\), and show that it is true for \(i\).
By the monotonicity of \({\mathrm{\Phi}}\) and the induction hypothesis, we have \({\mathrm{\Phi}}\ell_{i-1} \leq {\mathrm{\Phi}}\mathcal{V} = \mathcal{V}\) (cf. Definition [def:bellman]). As Line [alg2:line4] of Algorithm 3 performs \(\ell_i \gets {\mathrm{\Phi}}\ell_{i-1}\), this implies \(\ell_i \leq \mathcal{V}\) after Line [alg2:line4]. The rest is to show that the update of \(\ell_i\) in Line [alg2:line9] preserves such property.
Consider an EC \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E) \in \mathrm{\small BMEC}(W'_{\square},{\mathrm{\mathrm{\small Av}}}')\). By Lemma 1, \(E\) is Even-dominating in \({\mathcal{G}}\), and staying in \(E\) results in the winning probability of \(1\) (under some Even’s strategy). If an infinite path instead exits \(E\), the winning probability is at least the value of the smallest exit of Odd, i.e., \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i)\). Hence, all states in \(S_E\), either staying or exiting, have the winning probability of at least \(\min(1,{\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i)) = {\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i)\). Since \(\ell_i \leq \mathcal{V}\), \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i)\) gives a lower bound for \(\mathcal{V}(s)\), i.e., \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i) \leq \mathcal{V}(s)\) for all \(s \in S_E\). As \(\ell_i(s) \leq \mathcal{V}(s)\) and \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i) \leq \mathcal{V}(s)\) for all \(s \in S_E\), we obtain \(\max(\ell_i(s),{\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell_i)) \leq \mathcal{V}(s)\). Therefore, \(\ell_i \leq \mathcal{V}\) holds at the end of the iteration. 0◻ ◻
By Proposition [prop:increasing] and Lemma 3, the sequence \(\ell_i\) is non-decreasing and bounded from above, so the limit \(\lim_{i \to \infty} \ell_i\) exists. The dual argument for \(u_i\) is straightforward.
In the setting of Algorithm 3, we define \(\ell^* := \lim_{i \to \infty} \ell_i\) and \(u^* := \lim_{i \to \infty} u_i\).
Assume the setting of Algorithm 3, and let \({\mathrm{\Theta}}: [0,1]^S \times [0,1]^S \to [0,1]^S \times [0,1]^S\) denote the update performed in each iteration of the algorithm (i.e., \({\mathrm{\Theta}}(\ell_i,u_i) = (\ell_{i+1},u_{i+1})\)). Then, \({\mathrm{\Theta}}(\ell^*,u^*) = \lim_{i \to \infty} {\mathrm{\Theta}}(\ell_i,u_i)\).
Proof. We work in the complete lattice \(([0,1]^S \times [0,1]^S,\leq)\) where \((f,g) \leq (f',g')\) if and only if \(f \leq f'\) and \(g \geq g'\). We denote the difference between two pairs of functions by \((f,g) - (f',g') := \max_{s \in S} \max((f-f')(s), (g'-g)(s))\).
We first argue \({\mathrm{\Theta}}(\ell^*,u^*) \geq \lim_{i \to \infty} {\mathrm{\Theta}}(\ell_i,u_i)\). By Proposition [prop:increasing], \({\mathrm{\Theta}}\) is monotone. For any \(i \in \mathbb{N}\), because \((\ell^*,u^*) \geq (\ell_i,u_i)\), we obtain \({\mathrm{\Theta}}(\ell^*,u^*) \geq {\mathrm{\Theta}}(\ell_i,u_i)\). This implies \({\mathrm{\Theta}}(\ell^*,u^*) \geq \lim_{i \to \infty} {\mathrm{\Theta}}(\ell_i,u_i)\).
Next, for any given \(\epsilon > 0\), there exists a sufficiently large \(n \in \mathbb{N}\) such that \((\ell^*,u^*) - (\ell_n,u_n) < \epsilon\). Moreover, when \(\epsilon\) is small enough, one can show that the restricted actions \({\mathrm{\mathrm{\small Av}}}'\) (cf. Line [alg2:line5] of Algorithm 3) constructed under \((\ell^*,u^*)\) and \((\ell_n,u_n)\) are the same. This results in the same subgame \({\mathcal{G}}'\) being analyzed. By Definition [def:exit], the exit value of each BMEC differs by at most \(\epsilon\) between the two cases. Hence, we get \({\mathrm{\Theta}}(\ell^*,u^*) - {\mathrm{\Theta}}(\ell_n,u_n) < \epsilon\).
Now we prove \({\mathrm{\Theta}}(\ell^*,u^*) = \lim_{i \to \infty} {\mathrm{\Theta}}(\ell_i,u_i)\). Suppose for the sake of contradiction that this does not hold. Then, \({\mathrm{\Theta}}(\ell^*,u^*) > \lim_{i \to \infty} {\mathrm{\Theta}}(\ell_i,u_i)\). Let \(\epsilon := {\mathrm{\Theta}}(\ell^*,u^*) - \lim_{i \to \infty} {\mathrm{\Theta}}(\ell_i,u_i) > 0\). By the aforementioned argument with \(\frac{\epsilon}{2} > 0\), there is \(n \in \mathbb{N}\) giving \({\mathrm{\Theta}}(\ell^*,u^*) - {\mathrm{\Theta}}(\ell_n,u_n) < \frac{\epsilon}{2}\). This contradicts the fact that this gap equals \(\epsilon\), since we have just shown it is strictly less than \(\frac{\epsilon}{2}\). 0◻ ◻
Assume the setting of Proposition [prop:bvi-continuous]. Then, \({\mathrm{\Theta}}(\ell^*,u^*) = (\ell^*,u^*)\), i.e., \((\ell^*,u^*)\) is a fixed point of \({\mathrm{\Theta}}\).
Proof. Following Proposition [prop:bvi-continuous], we have \[\begin{align} {\mathrm{\Theta}}(\ell^*,u^*) = \lim_{i \to \infty}{\mathrm{\Theta}}(\ell_i,u_i) = \lim_{i \to \infty}(\ell_{i+1},u_{i+1}) = \lim_{i \to \infty}(\ell_i,u_i) = (\ell^*,u^*).\tag*{\qed} \end{align}\] ◻
We now prove that \(\ell^*\) and \(u^*\) indeed coincide, which implies \(\ell^* = \mathcal{V} = u^*\). The proof follows the principle captured by [24] called the maximality inheritance principle.
Lemma 4. In the setting of Algorithm 3, \(\ell^* = u^*\).
Proof. Suppose \(\ell^* \neq u^*\). Since Lemma 3 and its dual give \(\ell^* \leq u^*\), then there is \(s \in S\) with \(\ell^*(s) < u^*(s)\). Let \(M := \{ s^\dagger \in S : \forall s \in S, (u^*-\ell^*)(s^\dagger) \geq (u^*-\ell^*)(s) \} \subseteq S\) be the gap maximizer set. Note that \(M\) is well-defined due to the finiteness of \(S\). For each \(s^\dagger \in M\), we now distinguish cases on whether \(s^\dagger \in S_{\square}\) or \(s^\dagger \in S_{\triangle}\), and show that, in both cases, gap maximality is inherited under all actions \(a^\dagger \in {\mathrm{\mathrm{\small Av}}}'(s^\dagger)\) defined in Line [alg2:line5].
Assume \(s^\dagger \in S_{\square}\). Since \(u^* = {\mathrm{\Phi}}u^*\) (by Proposition [prop:bvi-fixed-point] and \({\mathrm{\Theta}}\) includes an application of \({\mathrm{\Phi}}\)), each action \(a^\dagger \in {\mathrm{\mathrm{\small Av}}}'(s^\dagger)\) gives \(u^*(s^\dagger) = \phi_{u^*}(s^\dagger,a^\dagger)\). However, this action \(a^\dagger\) can be suboptimal for \(\ell^*\), giving \(\ell^*(s^\dagger) = \max_{a \in {\mathrm{\mathrm{\small Av}}}(s^\dagger)} \phi_{\ell^*}(s^\dagger,a) \geq \phi_{\ell^*}(s^\dagger,a^\dagger)\). So, \((u^*-\ell^*)(s^\dagger) \leq \phi_{u^*}(s^\dagger,a^\dagger)-\phi_{\ell^*}(s^\dagger,a^\dagger) = \phi_{(u^*-\ell^*)}(s^\dagger,a^\dagger) \leq^{(\star)} \max_{s' \in {\mathrm{\mathrm{\small Post}}}(s^\dagger,a^\dagger)}(u^*-\ell^*)(s') \leq (u^*-\ell^*)(s^\dagger)\), where the inequality \(\leq^{(\star)}\) is due to the average is no greater than the maximum. Hence, by squeezing, \((u^*-\ell^*)(s^\dagger) = (u^*-\ell^*)(s')\) for all \(s' \in {\mathrm{\mathrm{\small Post}}}(s^\dagger,a^\dagger)\). Therefore, we have \({\mathrm{\mathrm{\small Post}}}(s^\dagger,a^\dagger) \subseteq M\) for each \(a^\dagger \in {\mathrm{\mathrm{\small Av}}}'(s^\dagger)\).
Now assume \(s^\dagger \in S_{\triangle}\). Since \(\ell^* = {\mathrm{\Phi}}\ell^*\) (by Proposition [prop:bvi-fixed-point] and \({\mathrm{\Theta}}\) includes an application of \({\mathrm{\Phi}}\)), each action \(a^\dagger \in {\mathrm{\mathrm{\small Av}}}'(s^\dagger)\) gives \(\ell^*(s^\dagger) = \phi_{\ell^*}(s^\dagger,a^\dagger)\). However, this action \(a^\dagger\) can be suboptimal for \(u^*\), giving \(u^*(s^\dagger) = \min_{a \in {\mathrm{\mathrm{\small Av}}}(s^\dagger)}\phi_{u^*}(s^\dagger,a) \leq \phi_{u^*}(s^\dagger,a^\dagger)\). So, \((u^*-\ell^*)(s^\dagger) \leq \phi_{u^*}(s^\dagger,a^\dagger) - \phi_{\ell^*}(s^\dagger,a^\dagger) \leq (u^*-\ell^*)(s^\dagger)\). Thus, by squeezing, \((u^*-\ell^*)(s^\dagger) = (u^*-\ell^*)(s')\) for all \(s' \in {\mathrm{\mathrm{\small Post}}}(s^\dagger,a^\dagger)\). Therefore, we have \({\mathrm{\mathrm{\small Post}}}(s^\dagger,a^\dagger) \subseteq M\) for each \(a^\dagger \in {\mathrm{\mathrm{\small Av}}}'(s^\dagger)\).
Combining both cases, we obtain \(\forall s^\dagger \in M, \forall a^\dagger \in {\mathrm{\mathrm{\small Av}}}'(s^\dagger), {\mathrm{\mathrm{\small Post}}}(s^\dagger,a^\dagger) \subseteq M\). Since we restrict the available actions to \({\mathrm{\mathrm{\small Av}}}'\) for the subgame \({\mathcal{G}}'\), any infinite path in \({\mathcal{G}}'\) starting from \(s^\dagger \in M\) remains in \(M\). Hence, \(M\) contains a state that is Even-winning in \({\mathcal{G}}'\) (i.e., \(M \cap W'_{\square}\neq \emptyset\)) or \(M\) contains a state that is Odd-winning in \({\mathcal{G}}'\) (i.e., \(M \cap W'_{\triangle}\neq \emptyset\)) (or both). Without loss of generality, we assume the former case; a symmetric reasoning applies to the latter case.
Suppose \(M \cap W'_{\square}\neq \emptyset\). Because there is an infinite path, starting from \(M \cap W'_{\square}\) and staying in \(M \cap W'_{\square}\) under \({\mathrm{\mathrm{\small Av}}}'\), that makes Even wins, such path must end in some EC, i.e., there is an EC \(E = (S_E,{\mathrm{\mathrm{\small Av}}}_E) \in \mathrm{\small BMEC}(W'_{\square},{\mathrm{\mathrm{\small Av}}}')\) with \(S_E \subseteq M\). By Lemma 1, \(E\) is Even-dominating in both \({\mathcal{G}}'\) and \({\mathcal{G}}\).
We then consider the relationship between \(\ell^*\) and \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell^*)\). If Odd cannot exit \(E\) (i.e., \({\mathrm{\mathrm{\small Av}}}(s) \setminus {\mathrm{\mathrm{\small Av}}}'(s) = \emptyset\) for all \(s \in S_E \cap S_{\triangle}\)), then \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell^*) = 1\) by Definition [def:exit]. This implies \(\ell^*(s) = 1\) for all \(s \in S_E\), contradicting the assumption that \(\ell^*(s) < u^*(s) \leq 1\) for all \(s \in S_E \subseteq M\).
Otherwise, if Odd can exit \(E\), then the set \(X := \{ s \in S_E \cap S_{\triangle}: {\mathrm{\mathrm{\small Av}}}(s) \setminus {\mathrm{\mathrm{\small Av}}}'(s) \neq \emptyset\}\) is non-empty. Let \(s^\flat := \arg\min_{s \in X} \ell^*(s)\) be a state in \(X\) with smallest \(\ell^*\). By the definition of \({\mathrm{\mathrm{\small Av}}}'\) and \(\ell^* = {\mathrm{\Phi}}\ell^*\), for any \(s \in X \subseteq S_{\triangle}\), \(a' \in {\mathrm{\mathrm{\small Av}}}'(s)\), and \(a \in {\mathrm{\mathrm{\small Av}}}(s) \setminus {\mathrm{\mathrm{\small Av}}}'(s)\), we have \(\phi_{\ell^*}(s,a) > \phi_{\ell^*}(s,a') = \min_{a' \in {\mathrm{\mathrm{\small Av}}}(s)} \phi_{\ell^*}(s,a') = ({\mathrm{\Phi}}\ell^*)(s) = \ell^*(s) \geq \ell^*(s^\flat)\). Thus, \({\mathrm{\mathrm{\small Exit}}}_{\triangle}(E,\ell^*) > \ell^*(s^\flat)\), and Line [alg2:line9] modifies \(\ell^*(s^\flat)\). This contradicts Proposition [prop:bvi-fixed-point] that \(\ell^*\) is a fixed point of \({\mathrm{\Theta}}\). 0◻ ◻
Theorem 2. Our proposed \(\textrm{\mathrm{\small SPG-BVI}}({\mathcal{G}},{s_\mathrm{init}},\varepsilon)\) surely terminates and returns a value that is \(\varepsilon\)-close to \(\mathcal{V}({s_\mathrm{init}})\) for all inputs.
4.5 Comparison with [21]↩︎
The structure of our proposed Algorithm 3 may appear similar to that of [21]; however, the underlying ideas differ fundamentally. We highlight the key distinctions below.
Firstly, [21] relies on the existence of a strategy recommender [21]. A strategy recommender is a procedure that generates a sequence \((\sigma_{{\square},i},\sigma_{{\triangle},i})\) such that, for some \(i \in \mathbb{N}\), the pair is optimal. Such recommenders can be constructed for a range of objectives, including reachability, safety, total reward, and mean-payoff, since these objectives can be characterized as least or greatest fixed points of suitable operators. However, this approach does not extend to parity objectives. In contrast, our algorithm and correctness proofs do not rely on a strategy recommender and depend solely on restricted actions \({\mathrm{\mathrm{\small Av}}}'\).
Secondly, [21] adjusts the two bound sequences using reasoning based on MDPs. For example, in constructing the bottom-up sequence \(\ell_i\), they fix a strategy for Maximizer, thereby inducing an MDP controlled only by Minimizer, and compute an optimal response for Minimizer. Since the fixed Maximizer’s strategy may be suboptimal, the resulting winning probabilities can be smaller, yielding a sound lower bound. By leveraging a strategy recommender, these fixed strategies eventually become optimal, ensuring convergence of the bounds.
In contrast, rather than relying on MDP-based reasoning, we solve the qualitative SPG problem (Problem [prob:qual-prob]) to determine the winning sets of both players within the restricted subgame \({\mathcal{G}}'\). By systematically refining the bounds of these winning sets, we establish convergence of our algorithm without requiring a strategy recommender. From this perspective, our approach can be viewed as a generalization of [21].
5 Conclusions and Future Work↩︎
We introduced the first BVI algorithm for SPGs, enabling the computation of winning probabilities under parity objectives with precision guarantees. A central difficulty is that, unlike reachability or safety objectives, its value function is not characterized as either the least or greatest fixed point of the Bellman operator. Our technique resolves this by combining qualitative analysis with quantitative updates. The resulting algorithm is sound and converges with guarantees.
As future work, we aim to extend the framework to richer objectives, particularly quantitative rewards. We also plan to develop a deeper lattice-theoretic foundation for the underlying procedure, with the goal of characterizing fixed point uniqueness and enabling systematic generalizations of the approach.
5.0.1 ↩︎
This work is supported by the ASPIRE grant No. JPMJAP2301, JST.
References↩︎
The symbol \({\square}\) has an even number of sides, while \({\triangle}\) has an odd number.↩︎
We do not introduce the player Random as in [27]. Nonetheless, our definition and that of [27] are equivalent with respect to parity objectives.↩︎
For the bottom-up sequence, we define \({\mathrm{\Psi}}^\omega\bot := \sup\{{\mathrm{\Psi}}^i\bot : i \in \mathbb{N}\}\) and \({\mathrm{\Psi}}^{\omega+(i+1)}\bot := {\mathrm{\Psi}}({\mathrm{\Psi}}^{\omega+i}\bot)\) for each \(i \in \mathbb{N}\). Those for the top-down sequence are defined dually.↩︎