Threshold Constraints with Guarantees for Parity
Objectives in Markov Decision Processes∗
Raphaël Berthon1,2 , Mickael Randour2 , and Jean-François Raskin2
1
2

ENS Rennes, France
Computer Science Department, ULB - Université libre de Bruxelles, Belgium

arXiv:1702.05472v2 [cs.LO] 27 Apr 2017

Abstract
The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [10]: it aims
at building system controllers that provide strict worst-case performance guarantees against an
antagonistic environment while ensuring higher expected performance against a stochastic model
of the environment. Our work extends the framework of [10] and follow-up papers, which focused
on quantitative objectives, by addressing the case of ω-regular conditions encoded as parity
objectives, a natural way to represent functional requirements of systems.
We focus on building strategies that satisfy a main parity objective on all plays, while ensuring
a secondary one with sufficient probability. This setting raises new challenges in comparison to
quantitative objectives, as one cannot easily mix different strategies without endangering the
functional properties of the system. Interestingly, we establish that, for all variants of this problem, deciding the existence of a strategy lies in NP∩coNP, the same complexity class as classical
parity games. Hence, our framework provides additional modeling power while staying in the
same complexity class.

1

Introduction

Beyond worst-case synthesis. Two-player zero-sum games [18, 21] and Markov decision
processes (MDPs) [17, 4] are two popular frameworks to model decision making in adversarial
and uncertain environments respectively. In the former, a system controller (player 1) and its
environment (player 2) compete antagonistically, and synthesis aims at building strategies for
the controller that ensure a specified behavior against all possible strategies of the environment.
In the latter, the system is faced with a given stochastic model of its environment, and the
focus is on satisfying a given level of expected performance, or a specified behavior with a
sufficient probability.
The beyond worst-case synthesis framework was introduced by Bruyère et al. [10] to unite
both views: in this setting, we look for strategies that provide both strict worst-case guarantees
and a good level of performance against the stochastic model. Such requirements are natural
in many practical situations (e.g., see [9, 23] for applications to the shortest path problem).
The original paper [10] dealt with mean-payoff and shortest path quantitative settings.
Substantial follow-up work include, e.g., multi-dimensional extensions [14], optimization of
the expected mean-payoff under hard Boolean constraints [1] or under energy constraints [7],
or integration of beyond worst-case concepts in the tool Uppaal [15].
Parity objectives. In this paper, we study the beyond worst-case problem for ω-regular
conditions encoded as parity objectives. Parity games have been under close scrutiny for a long
time both due to their importance (e.g., they subsume modal µ-calculus model checking [16])

∗

Work partially supported by the ERC Starting grant 279499 (inVEST) and the ARC project “Non-Zero
Sum Game Graphs: Applications to Reactive Synthesis and Beyond” (Fédération Wallonie-Bruxelles).
J.-F. Raskin is Professeur Francqui de Recherche, M. Randour is an F.R.S.-FNRS postdoctoral researcher.
© Raphaël Berthon, Mickael Randour, and Jean-François Raskin;
licensed under Creative Commons License CC-BY
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

XX:2

Threshold Constraints with Guarantees for Parity Objectives in MDPs

and their intriguing complexity: they belong to the class of problems in NP ∩ coNP [19]
and despite many efforts (see [11] for pointers), whether they belong to P is still an open
question.
In the aforementioned papers dealing with beyond worst-case problems, the focus was
on quantitative objectives (e.g., mean-payoff). While it is usually the case that qualitative
objectives, such as parity, are easier to deal with than quantitative ones, this is not true
in the setting considered in this paper. Indeed, in the context of quantitative objectives, it
is conceivable to alternate between two strategies along a play, such that one – efficient –
strategy balances the performance loss due to playing the other – less efficient – strategy
for a limited stretch of play infinitely often. In the context of qualitative objectives, this is
no more possible in general, as one strategy may induce behaviors (such as invalidating the
parity condition infinitely often) that can never be counteracted by the other one. Hence, in
comparison, we need to define more elaborate analysis techniques to detect when satisfying
both the worst-case and the probabilistic constraints with a single strategy is actually possible.
b 1, 0
1, 0

2, 1

a

d

c 2, 0

Figure 1 An MDP where player 1 can ensure p1 surely and p2 almost-surely.

I Example 1. Consider the MDP of Figure 1. Circle states are owned by player 1 (system)
and square states are owned by player 2 (environment). In the stochastic model of the
environment, square states are probabilistic, and, when not specified, we consider the uniform
distribution over their successors. Each state is labelled with a name and two integers x, y
representing priorities defined by two functions, p1 and p2 . An infinite path in the graph is
winning for player 1 and parity objective pi , i ∈ {1, 2}, if the maximal priority seen infinitely
often along the path for function pi is even. We claim that player 1 has a strategy λ to
ensure that (i) all plays consistent with λ satisfy p1 (i.e., p1 is surely satisfied) and (ii) the
probability measure induced by λ on this MDP ensures that p2 is satisfied with probability
one (i.e., almost-surely).
One such λ is as follows. It plays an infinite sequence of rounds of ni steps, i ∈ N. In
round i, in state a, the strategy chooses b for ni steps, such that the probability to reach c
during round i is larger than 1 − 2−i (this is possible as at each step c is reached from b
with probability 12 ). If during round i, c is not reached (which can happen with a small
probability) then λ goes to d once. Then the next round i + 1 is started. This infinite-memory
strategy ensures both (i) and (ii). Indeed, it can be shown that the probability that λ plays d
infinitely often is zero. Also, during each round, the maximal priority for p1 is guaranteed to
be even because if c is not visited, d is systematically played.
Finally, we can prove that player 1 needs infinite memory to ensure p1 surely and p2
almost-surely, and also, that this is the best that player 1 can do here: he has no strategy to
enforce surely both p1 and p2 at the same time.
Outline and contributions. This paper extends a preceding conference version [5]. We
consider MDPs with two parity objectives (i.e., using different priority functions). We study
the problem of deciding the existence of a strategy that ensures the first parity objective
surely (i.e., on all plays) while yielding a probability at least equal to (resp. greater than)

R. Berthon, M. Randour, and J.-F. Raskin

a given rational threshold to satisfy the second parity objective. In Section 2, we formally
define the framework and recall important results from the literature. In Section 3, as an
intermediate step, we solve the problem of ensuring the first parity objective surely while
visiting a target set of states with sufficient probability: this tool will help us several times
later. We prove that the corresponding decision problem is in NP ∩ coNP and at least as
hard as parity games, and that finite-memory strategies are sufficient. In Section 4, we solve
the problem for the two parity objectives, where the second one must hold almost-surely (i.e.,
with probability one). Our main tools are the novel notion of ultra-good end-components,
as well as the reachability problem solved in Section 3. We generalize our approach to
arbitrary probability thresholds in Section 5, in which we introduce the notion of very-good
end-components. In both the almost-sure and the arbitrary threshold cases, we prove that the
decision problem belongs to NP ∩ coNP and is at least as hard as parity games. In contrast
to the reachability case, we prove that infinite memory is in general necessary.
Additional related work. The beyond worst-case synthesis framework is an example of
the usefulness of non-zero-sum games for reactive synthesis. More can be found in these
expository papers [8, 22]. Other types of multi-objective specifications in stochastic models
have been considered in the literature: e.g., percentile queries generalize the classical threshold
probability problem to several dimensions [24].
In [3], Baier et al. study the quantitative analysis of MDPs under weak and strong
fairness constraints. They provide algorithms for computing the probability for ω-regular
properties in worst and best-case scenarios, when considering strategies that in addition
satisfy weak or strong fairness constraints almost-surely. In contrast, we are able to consider
similar objectives but for strategies that satisfy weak or strong fairness constraints surely,
i.e., with certainty and not only with probability one.
In [1], Almagor et al. consider the optimization of the expected mean-payoff under
hard Boolean constraints in weighted MDPs. Our concept of ultra-good end-component
builds upon their notion of super-good end-component. A reduction to mean-payoff parity
games [12] is part of the identification process of both types of end-components.

2
2.1

Preliminaries
Core concepts

Directed graphs. A directed graph is a pair G = (S, E) with S a set of vertices, called
states, and E ⊆ S × S a set of directed edges. We focus here on finite graphs (i.e., |S| < ∞).
Given a state s ∈ S, we denote by Succ(s) = {s0 ∈ S | (s, s0 ) ∈ E} the set of successors of s
by edges in E. We assume that graphs are non-blocking, i.e., for all s ∈ S, Succ(s) 6= ∅.
A play in G from an initial state s ∈ S is an infinite sequence of states π = s0 s1 s2 . . .
such that s0 = s and (si , si+1 ) ∈ E for all i ≥ 0. The prefix up to the (n + 1)-th state of
π is the finite sequence π(0, n) = s0 s1 . . . sn . We resp. denote the first and last states of a
prefix ρ = s0 s1 . . . sn by First(ρ) = s0 and Last(ρ) = sn . For a play π, we naturally extend
the notation to First(π). Finally, for i ∈ N, π(i) = si , and for j > i, π(i, j) = si . . . sj .
The set of plays of G is denoted by Plays(G). The corresponding set of prefixes is denoted
by Pref(G). For a set of plays Π, we will also denote by Pref(Π) the set of all prefixes of
these plays. Given two prefixes ρ = s0 . . . sm and ρ0 = s00 . . . s0n in Pref(G), we denote their
concatenation as ρ · ρ0 = s0 . . . sm s00 . . . s0n . This concatenation is not necessarily a valid prefix
of G. The same holds for a prefix concatenated with a play.
Probability distributions. Given a countable set A, a (rational) probability distribution

XX:3

XX:4

Threshold Constraints with Guarantees for Parity Objectives in MDPs

P
on A is a function p : A → [0, 1] ∩ Q such that
a∈A p(a) = 1. We denote the set of
probability distributions on A by D(A). The support of the probability distribution p on A
is Supp(p) = {a ∈ A | p(a) > 0}.
Markov decision processes. A (finite) Markov decision process (MDP) is a tuple M =
(G, S1 , S2 , δ) where (i) G = (S, E) is a directed graph; (ii) (S1 , S2 ) is a partition of S into
states of player 1 (denoted by P1 and representing the system) and states of player 2 (denoted
by P2 and representing the stochastic environment); (iii) δ : S2 → D(S) is the transition
function that, given a stochastic state s ∈ S2 , defines the probability distribution δ(s) over
the successors of s, such that for all s ∈ S2 , Supp(δ(s)) = Succ(s) (i.e., all outgoing edges of
have non-zero probability to be taken). An MDP where for all s ∈ S1 , |Succ(s)| = 1 is a
fully-stochastic process called a Markov chain (MC).
A prefix ρ ∈ Pref(M) belongs to Pi , i ∈ {1, 2}, if Last(ρ) ∈ Si . The set of prefixes that
belong to Pi is denoted by Prefi (M).
Strategies. A strategy for P1 is a function λ : Pref1 (M) → D(S), such that for all
ρ ∈ Pref1 (M), we have Supp(λ(ρ)) ⊆ Succ(Last(ρ)). The set of all strategies in M is
denoted by Λ. Pure strategies have their support equal to a singleton for all prefixes. When
a strategy λ is pure, we simplify its notation and write λ(ρ) = s instead of λ(ρ)(s) = 1,
for any ρ ∈ Pref1 (M) and the unique state s ∈ Supp(λ(ρ)). We sometimes mention that
a strategy is randomized to stress on the need for randomness in general (i.e., when pure
strategies do not suffice).
A strategy λ for P1 can be encoded by a stochastic state machine with outputs, called
stochastic Moore machine, M = (M, m0 , αu , αn ) where (i) M is a finite or infinite set of
memory elements, (ii) m0 ∈ M is the initial memory element, (iii) αu : M × S → M is the
update function, and (iv) αn : M × S1 → D(S) is the next-action function. If the MDP is in
s ∈ S1 and m ∈ M is the current memory element, then the strategy chooses s0 , the next
state of the MDP, according to the probability distribution αn (m, s). When the MDP leaves
a state s ∈ S, the memory is updated to αu (m, s). Hence updates are deterministic and
outputs are potentially stochastic. Formally, (M, m0 , αu , αn ) defines the strategy λ such
that λ(ρ · s) = αn (b
αu (m0 , ρ), s) for all ρ ∈ Pref(M) and s ∈ S1 , where α
bu extends αu to
sequences of states starting from m0 as expected. Note that pure strategies have deterministic
next-action functions. A strategy λ is finite-memory if |M | < ∞ and memoryless if |M | = 1.
That is, it does not depend on the history but only on the current state of the MDP: in this
case, we have that λ : S1 → D(S). Finally, if the same strategy can be used regardless of the
initial state, we say that a uniform strategy exists.
A play π is said to be consistent with a strategy λ if for all n ≥ 0 such that π(n) ∈ S1 ,
we have that π(n + 1) ∈ Supp(λ(π(0, n)). This notion is defined similarly for prefixes. We
denote by OutM (λ) ⊆ Plays(G) the set of plays consistent with λ. We use OutM
s (λ) when
fixing an initial state s.
Given a strategy λ in M and a prefix ρ ∈ Pref1 (M), we define the initialized strategy
λ[ρ] as follows:
(
λ(ρ · ρ0 ) if ρ · ρ0 ∈ Pref1 (M),
0
0
∀ ρ ∈ Pref1 (M), λ[ρ](ρ ) =
λ(ρ0 ) otherwise.
Markov chain induced by a strategy. An MDP M = (G = (S, E), S1 , S2 , δ) and a
strategy λ for P1 encoded by the stochastic Moore machine M = (M, m0 , αu , αn ) determine
an MC C = (G0 , δ 0 ) on the state space S 0 = S × M as follows. For any pair of states
s01 = (s1 , m1 ) and s02 = (s2 , m2 ) in S 0 , δ 0 (s01 )(s02 ) = αn (s1 , m1 )(s2 ) if m2 = αu (s1 , m1 ) and 0

R. Berthon, M. Randour, and J.-F. Raskin

otherwise. Observe that given a finite MDP, a finite-memory (resp. infinite-memory) strategy
induces a finite (resp. infinite) MC. We define plays and prefixes of an induced MC as before,
considering only transitions with non-zero probability.
Let M = (G, S1 , S2 , δ) be an MDP, s ∈ S an initial state and λ a strategy of P1 encoded
by M = (M, m0 , αu , αn ). Let A ⊆ Plays(G). We denote by PλM,s [A] the probability of the
plays of the induced MC C (starting in (s, m0 )) whose projection (defined by removing
the memory elements) to M is in A, i.e., the probability of event A when M is executed
with initial state s and strategy λ. Note that every Borel set A has a uniquely defined
probability [25] (Carathéodory’s extension theorem induces a unique probability measure on
the Borel σ-algebra over Plays(G)). Throughout the paper, we may also write PλM,s [A] for
A a set of prefixes: this is an abuse of notation meaning that we consider the probability of
the set of plays A0 containing all consistent continuations of prefixes in A (i.e., we consider
the probability of the cylinders defined by those prefixes).
Two-player games. Observe that in MDPs, we call both P1 and P2 players, though P2
does not have controllable choices. Indeed, an MDP can be seen as a game where P1 plays
against a stochastic adversary P2 using the fixed memoryless randomized strategy δ: they
are sometimes called 1 12 -player games. Throughout this paper, we also need to consider real
two-player games, denoted G = (G = (S, E), S1 , S2 ). In those games, both players control
their actions using strategies: we extend all previous notions (e.g., strategies) to P2 and
games. In particular, any MDP M = (G, S1 , S2 , δ) can be seen as a two-player game by
forgetting about the transition function δ and letting P2 pick the strategy of its choice.
Mixing both interpretations (stochastic and antagonistic versions of P2 ) is crucial in the
beyond worst-case framework that we study here.
Objectives. Given an MDP M = (G, S1 , S1 , δ), an objective is a set of plays A ⊆ Plays(G).
We consider two classical objectives from the literature. Both define measurable events.
To define them, we introduce the following notation: given a play π ∈ Plays(G), let
inf(π) = {s ∈ S | ∀ i ≥ 0, ∃ j ≥ i, π(j) = s} be the set of states seen infinitely often along π.
Reachability. Given a target T ⊆ S, the reachability objective asks for plays that visit T :
Reach(T ) = {π ∈ Plays(G) | ∃ n ≥ 0, π(n) ∈ T }. We later use the LTL notation ♦T to
denote the event Reach(T ).
Parity. Let p : S → {1, 2, . . . , d} be a priority function that maps each state to an
integer priority, where d ≤ |S| + 1 (w.l.o.g.). The parity objective asks that, among the
priorities seen infinitely often, the maximal one be even: Parity(p) = {π ∈ Plays(G) |
max p(s) is even}. We later simply use p to denote the event Parity(p).

s∈inf(π)

2.2

Technical tools

For the following definitions, let M = (G = (S, E), S1 , S2 , δ) be an MDP.
Attractors. The attractor for Pi , i ∈ {1, 2}, of a target set of states T , denoted Attri (T ) is
computed as the fixed point of the sequence Attrn+1
(T ) = Attrni (T ) ∪ {s ∈ Si | Succ(s) ∩
i
n
n
Attri (T ) 6= ∅} ∪ {s ∈ S3−i | Succ(s) ⊆ Attri (T )} with Attr0i (T ) = T . It contains all states
from which Pi can force a visit of T . Observe that this notion interprets P2 as an antagonistic
adversary, i.e., having the choice of his strategy.
Traps, end-components and sub-MDPs. A trap for Pi , i ∈ {1, 2}, is a set R ⊆ S that
Pi cannot leave: ∀ s ∈ R ∩ Si , Succ(s) ⊆ R and ∀ s ∈ R ∩ S3−i , Succ(s) ∩ R 6= ∅.
An end-component (EC) of M is a trap C for P2 that is strongly connected, i.e., for
any two states s, s0 ∈ C, there exists a path from s to s0 that stays in C. It is well-known

XX:5

XX:6

Threshold Constraints with Guarantees for Parity Objectives in MDPs

that inside an EC C, P1 can force the visit of any state s ∈ C with probability 1 (that is,
when P2 is seen as stochastic and obeys the strategy δ), see e.g., [4]. The union of two
ECs with non-empty intersection is an EC. An EC C is thus maximal if, for every EC C 0 ,
C 0 ⊆ C ∨ C 0 ∩ C = ∅.
Given an EC C ⊆ S of M, we denote by MC the sub-MDP that is naturally defined
by MC = (G0 = (C, E ∩ C × C), S10 = S1 ∩ C, S20 = S2 ∩ C, δ 0 ), where δ 0 : S20 → D(C) is
simply the restriction of δ to the domain C. Note that MC is a well-defined MDP: it has
no deadlock since C is strongly connected and in all stochastic states s, the support of δ 0 (s)
is included in C (as C was an EC in M).
Technical lemmas. Before turning to the beyond worst-case problem, we recall some
classical results about MDPs that will be useful later on.
I Lemma 2 (Optimal reachability [4]). Given an MDP M = (G = (S, E), S1 , S2 , δ) and
a target set T ⊆ S, we can compute for each state s ∈ S the maximal probability vs∗ =
supλ∈Λ PλM,s [♦T ] to reach T , in polynomial time. There is an optimal uniform pure memoryless strategy λ∗ that enforces vs∗ from all s ∈ S.
Fix s ∈ S and c ∈ Q such that c < vs∗ . Then there exists k ∈ N such that by playing λ∗
from s for k steps, we reach T with probability larger than c.
vs∗ ,

We say that λ∗ is optimal as no strategy can achieve a probability strictly higher than
for any s ∈ S.

I Lemma 3 (Long-run appearance of ECs [4]). Given an MDP M = (G = (S, E), S1 , S2 , δ)
and E = {C ⊆ S | C is an EC in M} the set of all its end-components, for any strategy λ
of P1 and any state s ∈ S, the following holds:


PλM,s {π ∈ OutM (λ) | inf(π) ∈ E} = 1.

2.3

The beyond worst-case framework

Events and probabilistic operators. Consider an MDP M = (G = (S, E), S1 , S2 , δ).
Recall that we have defined two types of measurable events (specific subsets of Plays(G))
with respective notations ♦T for T ⊆ S (reachability), and p for p : S → {1, . . . , d} a priority
function (parity). We define three operators to reason about the probabilities of these events:
S, P∼c , and AS. Given an event A and a state s, they are used as follows:
A is sure from s, denoted s |= S(A), if there exists a strategy λ of P1 such that
OutM
s (λ) ⊆ A. Here probabilities are ignored and we consider P2 as antagonistic.
A holds with probability at least equal to (resp. greater than) c ∈ Q from s, denoted
s |= P≥c (A) (resp. s |= P>c (A)) if there exists λ such that PλM,s [A] ≥ c (resp. > c).
A is almost-sure from s, denoted s |= AS(A), if there exists λ such that PλM,s [A] = 1.
For any operator O, we say that such a λ is a witness strategy for s |= O(A) and we write
s, λ |= O(A) to denote it. We will also consider combinations of the type s |= O1 (A1 ) ∧ O2 (A2 )
for two operators and events: in this case, we require that the same strategy be a witness for
both conjuncts, i.e., that there exists λ such that s, λ |= O1 (A1 ) and s, λ |= O2 (A2 ). Finally,
we will sometimes use different MDPs, in which case we add the considered MDP M as a
subscript on |=, e.g., s |=M O(A). We drop this subscript when the context is clear.
Beyond worst-case problems. Let M = (G = (S, E), S1 , S2 , δ) be an MDP, s ∈ S be
an initial state, and p1 , p2 be two priority functions on M. Throughout this paper, we
provide algorithms to decide the existence of a witness strategy — and synthesize it — for

R. Berthon, M. Randour, and J.-F. Raskin

the following formulae combining worst-case and probabilistic guarantees regarding parity
objectives:
1. s |= S(p1 ) ∧ AS(p2 ) — this is the canonical beyond worst-case (BWC) problem;
2. s |= S(p1 ) ∧ P∼c (p2 ) for ∼ ∈ {>, ≥} and c ∈ Q ∩ [0, 1).

3

Reachability under parity constraints

In this section, we consider the synthesis of strategies that enforce to reach a target set
of states T ⊆ S with high probability while enforcing a parity condition surely. Using the
previously defined notations, we consider two variants of the problem, given a state s ∈ S
and a priority function p : S → {1, . . . d}:
1. s |= S(p) ∧ AS(♦T ),
2. s |= S(p) ∧ P∼c (♦T ) for ∼ ∈ {>, ≥} and c ∈ Q ∩ [0, 1).

3.1

Almost-sure reachability

I Theorem 4. Given an MDP M = (G = (S, E), S1 , S2 , δ), a state s0 ∈ S, a priority
function p : S → {1, . . . , d}, and a target set of states T ⊆ S, it can be decided in NP ∩ coNP
if s0 |= S(p) ∧ AS(♦T ). If the answer is Yes, then there exists a finite-memory witness
strategy. This decision problem is at least as hard as solving parity games.
Proof. A slight variant of this result has been established inside the proof of [2, Lemma 3]
(extended version of [1]), where it is asked that the parity condition holds not necessarily on
all consistent plays but only on all plays that do not reach the target set T . We reduce our
problem to the latter as follows. First, we compute all states in S from which P1 can enforce
p surely. This boils down to solving a classical parity game [19]. We remove all states that
are not surely winning for p in M as entering one of those states implies that the parity
condition will be violated on some consistent play. Then we apply the approach described in
Theorem 27 (Appendix A) to the resulting MDP: it is based on a reduction to a particular
parity-Büchi game based on the MDP. If the answer is Yes for s0 , we answer Yes to our
problem, otherwise we answer No. We claim that this reduction is correct. First, it is clear
that satisfying their constraint is a necessary condition to satisfy ours. Now, if there is a
strategy λ that ensures to reach T almost-surely in the reduced MDP and enforces p on all
the consistent plays that never reach T , then we construct a strategy λ0 that plays as λ up
to reaching T (if ever) and then switches to the strategy λp that enforces p surely. This new
strategy is a witness for our problem since the parity objective is prefix-independent. That
is, s0 , λ0 |= S(p) ∧ AS(♦T ). Since both solving the parity game and solving the parity-Büchi
game from Theorem 27 are in NP ∩ coNP, we conclude that our decision problem lies in
PNP∩coNP = NP ∩ coNP [6]. Furthermore, our problem clearly generalizes parity games: it
suffices to fix T = S to trivially ensure the second conjunct and obtain a classical parity
game. Hence, the hardness follows.
Finally, since λp is memoryless w.l.o.g. and the strategy λ obtained via Theorem 27 is
also finite-memory (due to the reduction to a parity-Büchi game), we have that our witness
strategy λ0 is also finite-memory.
J

3.2

Reachability with threshold probability

Optimal reachability strategies. We first study strategies that maximize the probability
of reaching a target set of states T ⊆ S in an MDP M. Recall that Lemma 2 states the

XX:7

XX:8

Threshold Constraints with Guarantees for Parity Objectives in MDPs

existence of an optimal uniform pure memoryless strategy λ∗ that enforces vs∗ from all s ∈ S,
where vs∗ is the maximal probability to reach T that can be achieved by P1 in s. We define
the set E ¬opt = {(s, s0 ) ∈ E | s ∈ S1 ∧ vs∗ > vs∗0 } that contains all edges that are non-optimal
choices for P1 in the sense that they result in a strict decrease of the probability to reach T .
We show that playing, for a finite number of steps, edges that are optimal for reachability
(i.e., edges in E opt = E \ E ¬opt ), and then switching to an optimal strategy to reach T , like
λ∗ , produces an optimal strategy too.
I Lemma 5. Let λ∗ be an optimal uniform pure memoryless strategy in M to reach T , from
all states in S. If λ is a strategy that plays only edges in E opt for m steps, for m ∈ N, and
then switches to λ∗ , then λ is also optimal to reach T from all states in S.
Proof. We prove this lemma by induction. For m = 0, we only play λ∗ , thus λ is trivially
optimal. Now, assume the property holds up to m − 1 steps, for m > 0, i.e., that all strategies
playing in E opt for m − 1 steps, and then playing λ∗ , are optimal. Consider a strategy λm
that does this for m steps now. Strategy λm thus chooses an edge in E opt , and then switches
to a strategy λm−1 that satisfies the induction hypothesis. So for any state s0 ∈ S1 \ T (for
s0 ∈ T , we have probability one whatever the strategy), we have that:
i
Xh m
m
λm−1
PλM,s0 [♦T ] =
PλM,s0 [{π | π(1) = s}] · PM,s
[♦T ]
s∈S

=

Xh

m

PλM,s0 [{π | π(1) = s}] · vs∗

i

(by induction hypothesis)

s∈S

≥

i
Xh m
PλM,s0 [{π | π(1) = s}] · vs∗0 = vs∗0 .

(by definition of E opt )

s∈S

Hence, we obtain that λm is also optimal from s0 , which concludes our proof.

J

Solving the problem. We now turn to the problem s0 |= S(p) ∧ P∼c (♦T ).
I Theorem 6. Given an MDP M = (G = (S, E), S1 , S2 , δ), a state s0 ∈ S, a priority
function p : S → {1, . . . , d}, a target set of states T ⊆ S, and a probability threshold
c ∈ [0, 1) ∩ Q, it can be decided in NP ∩ coNP if s0 |= S(p) ∧ P∼c (♦T ) for ∼ ∈ {>, ≥}. If the
answer is Yes, then there exists a finite-memory witness strategy. This decision problem is
at least as hard as solving parity games.
Proof. First, we remove from M the states from which P1 cannot enforce S(p). In particular
if s0 6|= S(p), the answer is No. Remember that it can be done by computing the winning
states in M seen as a parity game: a problem that belongs to NP ∩ coNP [19]. We now reason
on the MDP Mw where those losing states have been removed: it is well-defined as the set of
winning states for P1 in M is a trap for P2 . We note λp a uniform pure memoryless strategy
that ensures S(p) from any state of Mw . The proof of this theorem is easy for the case >,
and more involved for ≥. We start with the easy case.
The algorithm for the case > c is as follows. First, we compute the maximal probability
vs∗0 to reach T , as in Lemma 2. This takes polynomial time. If vs∗0 ≤ c, then the answer is
clearly No. Otherwise, we claim that the answer is Yes. Let λ∗ be an optimal uniform pure
memoryless strategy enforcing probability vs∗0 from s0 . We construct a witness strategy λ for
s0 |= S(p) ∧ P>c (♦T ) from λ∗ and λp as follows. First, starting in s0 , the strategy λ plays
as λ∗ for k steps where k is taken as in Lemma 2: hence the probability to reach T after k
steps is strictly greater than c, which implies that s0 , λ |= P>c (♦T ). Then, λ switches to λp .
Since the parity objective is prefix-independent, we have that s0 , λ |= S(p), and we are done.

R. Berthon, M. Randour, and J.-F. Raskin

XX:9

Overall, our procedure lies in PNP∩coNP = NP ∩ coNP [6]. Also observe that our strategy λ is
finite-memory since λ∗ and λp are memoryless and k is finite thanks to Lemma 2.
We now turn to the case ≥ c. The algorithm, as in the previous case, first computes the
maximal probability vs∗0 to reach T , in polynomial time. If vs∗0 > c, then we answer Yes as
we can apply the same reasoning as in the previous case. If vs∗0 < c, then we trivially answer
No. The more involved case is when vs∗0 = c. In this case, we must verify that probability c
is still achievable if, in addition, it is required to enforce S(p). To answer this question, we
modify Mw and we reduce our problem to the almost-sure case of Theorem 4. We present
the details in the following. Intuitively, we construct the MDP M0 as follows:
we enrich states with one bit that records if the set T has been visited or not;
while T has not been visited, we suppress all edges controlled by P1 that are not optimal
for reachability, i.e., all edges in E ¬opt ;
while T has not been visited, we delete all states that cannot reach T (i.e., all states that
do not have a path to T in the underlying graph) and normalize the probability of the
w
edges that survive this deletion: we note the set of states to be removed by S¬T
.
Formally, the new MDP M0 is defined as follows:
w
S 0 = (S w × {0, 1}) \ (S¬T
× {0}), S10 = S 0 ∩ (S1w × {0, 1}), and S20 = S 0 ∩ (S2w × {0, 1});
s00 is equal to (s0 , 0) if s0 6∈ T , and to (s0 , 1) if s0 ∈ T ;
E 0 = {((s, 0), (s0 , 0)) | (s, s0 ) ∈ E opt ∧ s0 6∈ T } ∪ {((s, 0), (s0 , 1)) | (s, s0 ) ∈ E opt ∧ s0 ∈ T }
∪ {((s, 1), (s0 , 1)) | (s, s0 ) ∈ E};
the probability distributions are then defined as:

for all (s, 0) ∈ S20 , and ((s, 0), (s0 , b)) ∈ E 0 , δ 0 ((s, 0))((s0 , b)) =
X
Xs =
δ(s)(t),
for

t∈S w |((s,0),(t,b))∈E 0
all (s, 1) ∈ S20 , and ((s, 1), (s0 , 1))

δ(s)(s0 )
Xs

where we define

∈ E 0 , δ 0 ((s, 1))((s0 , 1)) = δ(s)(s0 );

the priority function p0 : S 0 → {1, . . . , d} is such that for all (s, b) ∈ S 0 , p0 ((s, b)) = p(s).
Note that each prefix (resp. play) ρ0 in M0 is naturally mapped to a unique prefix γ(ρ0 )
in Mw , obtained by projecting away the additional bit of information (about visiting the
target T ). Conversely, each prefix (resp. play) ρ in Mw that does not use edges in E ¬opt
w
and states in S¬T
is naturally mapped to a unique prefix α(ρ) in M0 . Those mappings are
such that for all ρ0 in M0 , ρ0 = α(γ(ρ0 )).
Finally, we claim that s0 |= S(p) ∧ P≥c (♦T ) in Mw if, and only if, s00 |= S(p) ∧ AS(♦T 0 ) in
0
M , where T 0 = T × {1}. For the sake of readability, we postpone the correctness of this
reduction to Lemma 7. Given that the latter problem was shown to be in NP ∩ coNP in
Theorem 4, and that M0 is only polynomially larger than Mw (and thus M), we obtain the
claimed complexity for the problem, using PNP∩coNP = NP ∩ coNP [6]. The proof of Lemma 7
also implies that the witness strategy can be finite-memory.
Again, problem s0 |= S(p) ∧ P∼c (♦T ) trivially generalizes parity games, by taking T = S,
which concludes our proof.
J
I Lemma 7 (Correctness of the reduction used for Theorem 6). The following equivalence
holds:
s00 |=M0 S(p) ∧ AS(♦T 0 ) ⇐⇒ s0 |=Mw S(p) ∧ P≥c (♦T ).

XX:10

Threshold Constraints with Guarantees for Parity Objectives in MDPs

Proof. We start with the left-to-right implication. Assume that there exists a witness strategy
λ0 for P1 in M0 such that s00 , λ0 |=M0 S(p) ∧ AS(♦T 0 ). By Theorem 4, we may assume λ0 to
be finite-memory. From λ0 , we build a strategy λ in Mw as follows:
for all ρ ∈ Pref(G) that does not visit T , only uses edges in E opt and does not contain
w
states in S¬T
, λ(ρ) = γ(λ0 (α(ρ))), i.e., λ mimics λ0 ,
for all other ρ ∈ Pref(G), the strategy plays as λp , the memoryless strategy ensuring S(p)
in Mw .
Observe that λ is a finite-memory strategy: the conditions to check can be encoded using a
finite number of memory elements in addition to the finite Moore machine representing λ0 .
We now claim that s0 , λ |=Mw S(p) ∧ P≥c (♦T ).
First, consider the conjunct S(p). Along any play π ∈ Plays(G) starting in s0 , either
(i) λ always plays as λ0 , or (ii) it eventually switches to λp . In case (i), π has a unique
corresponding play in M0 , π 0 = α(π), and π 0 is consistent with λ0 . Since λ0 ensures S(p)
by hypothesis and the priority function is the same in M0 and Mw , π also satisfies the
parity objective. In case (ii), π also satisfies the parity objective by definition of λp and
prefix-independence of parity. Hence, we have that s0 , λ |=Mw S(p).
It remains to prove that s0 , λ |=Mw P≥c (♦T ). We prove it by contradiction. Assume that
PλMw ,s0 [♦T ] < c, or equivalently, that PλMw ,s0 [¬T ] > 1 − c, using the classical always LTL
operator. This means that, because of the strict inequality > 1 − c, there exists m in N such
that the set
n
BadPref = ρ ∈ Pref(G) | ρ consistent with λ ∧ |ρ| = m + 1
o
∧ ∀ continuation π of ρ consistent with λ, π 6|= ♦T
P
satisfies ρ∈BadPref PλMw ,s0 [ρ] > 1 − c. Note that this sum is indeed a lower bound on the
probability of ¬T as all prefixes of BadPref define disjoint cylinder sets.
w
Now, we claim that for all ρ ∈ BadPref, we have that Last(ρ) ∈ S¬T
. To prove it, recall
the definition of λ. If it were not true, then λ would have mimicked λ0 all along ρ (i.e., not
switching to λp ). But since all continuations of ρ consistent with λ in Mw never reach T , this
would also hold for continuations of α(ρ) consistent with λ0 in M0 . Hence prefix α(ρ) would
0
prove that PλM0 ,s0 [♦T 0 ] < 1, which contradicts the hypothesis stating that s00 , λ0 |= AS(♦T 0 ).
0
w
Hence, we can now confirm that for all ρ ∈ BadPref, we have that Last(ρ) ∈ S¬T
.
w
r
To pursue, we define a new strategy on M , λ : it plays as λ, which only using edges in
E opt , for m steps (m as defined above), then switches to λ∗ , the optimal strategy to reach T
in Mw , which ensures probability vs∗0 = c of reaching T from s0 (see Proof of Theorem 6).
r
By Lemma 5, we have that λr is still optimal, hence that PλMw ,s0 [♦T ] = c. But by the
previous arguments, we also have that
X
r
PλMw ,s0 [¬T ] ≥
PλMw ,s0 [ρ] > 1 − c,
ρ∈BadPref
r

hence that PλMw ,s0 [♦T ] < c. We have obtained the contradiction, hence proving that
s0 , λ |=Mw P≥c (♦T ) and concluding the proof of the left-to-right implication.
We now prove the right-to-left implication. Assume that there exists a witness strategy
λ for P1 in Mw such that s0 , λ |=Mw S(p) ∧ P≥c (♦T ). Recall that the maximal achievable
probability to reach T in Mw is vs∗0 = c. Hence, it can be shown that λ must restrict its
choices to E opt before reaching T , otherwise it would not be possible to ensure P≥c (♦T ).
Similarly, we can assume w.l.o.g. that λ switches to λp , the strategy ensuring S(p), after T

R. Berthon, M. Randour, and J.-F. Raskin

w
or S¬T
is reached: if not the case, we can build a strategy with those properties based on λ
that is still a witness for the considered property. We first study λ0 , which is simply λ played
on M0 , and show that it is a witness for s00 |=M0 S(p).
To prove that s00 , λ0 |=M0 S(p), observe that on any play π 0 consistent with λ0 , we either
(i) reach T 0 and switch to λp (more precisely, its translation over M0 ), (ii) do not reach T 0 but
w
neither reach S¬T
(by construction), hence keep playing like λ. In case (i), and since all edges
from the initial MDP Mw are present after reaching T 0 , λp can be implemented faithfully
and any consistent play π 0 will satisfy the parity objective thanks to prefix-independence.
In case (ii), any consistent play π 0 of λ0 has a unique corresponding play π = γ(π 0 ) in Mw
that is consistent with λ, hence satisfies the parity objective since λ ensures S(p). We thus
conclude that λ0 is a witness for s00 |=M0 S(p).
We now show that T 0 is dense in λ0 , i.e., that any prefix ρ0 consistent with λ0 has a
continuation π 0 such that π 0 |= ♦T 0 . In other words, seeing strategy λ0 as an execution tree,
there is no subtree such that all branches in this subtree never visit T 0 . Formally, this is
saying that the following set must be empty:
n
BadPref0 = ρ0 ∈ Pref(G0 ) | ρ0 consistent with λ0
o
∧ ∀ continuation π 0 of ρ0 consistent with λ0 , π 0 6|= ♦T 0 .

We prove its emptiness by contradiction. Assume there exists a prefix ρ0 in BadPref0 . Since
w
it is a prefix in M0 , it implies by construction that Last(γ(ρ0 )) 6∈ S¬T
in Mw , hence that
0
0
some paths reach T from Last(γ(ρ )) in the underlying graph. Hence, we can define a new
strategy λr in Mw that plays exactly as λ except after prefix γ(ρ0 ), where it switches to
the optimal reachability strategy λ∗ : the probability to reach T after γ(ρ0 ) under λr is thus
strictly positive, say equal to q > 0. We know have that
r

r

PλMw ,s0 [♦T ] = c + PλMw ,s0 [γ(ρ0 )] · q > c
which is in contradiction with c = vs∗0 being the maximal achievable probability. Hence, we
deduce that BadPref0 is indeed empty and that T 0 is dense for λ0 . Now, using the reduction
to a parity-Büchi game which underlies Theorem 4, we deduce from the density argument
presented in Appendix A that we can build λ00 from λ0 such that s00 , λ00 |=M0 S(p) ∧ AS(♦T 0 ).
This concludes the proof of the right-to-left implication and of this lemma.
J

4

Almost-sure parity under parity constraints

Overview and key lemma. Here, we study strategies that enforce a parity objective p1
surely (i.e., on all consistent plays) and a parity objective p2 almost-surely (i.e., with
probability one). Formally, we look at the problem s |= S(p1 ) ∧ AS(p2 ). The cornerstone
of our approach is the notion of ultra-good end-component. Throughout this section, we
consider an MDP M = (G = (S, E), S1 , S1 , δ) with two priority functions p1 and p2 .
I Definition 8. An end-component C of M is ultra-good (UGEC) if in the sub-MDP MC ,
the following two properties hold:
max
(1U ) ∀ s ∈ C, s |=MC S(p1 ) ∧ AS(♦Ceven
(p1 )), where

max
Ceven
(pi ) = s ∈ C | (pi (s) is even) ∧ (∀ s0 ∈ C, pi (s0 ) is odd =⇒ pi (s0 ) < pi (s))

contains the states with even priorities that are larger than any odd priority in C (this
set can be empty for arbitrary ECs but needs to be non-empty for UGECs);

XX:11

XX:12

Threshold Constraints with Guarantees for Parity Objectives in MDPs

(2U ) ∀ s ∈ C, s |=MC AS(p1 ) ∧ AS(p2 ), or equivalently, s |=MC AS(p1 ∩ p2 ).
We introduce the following notations:
UGEC(M) is the set of all UGECs of M,
U = ∪U ∈UGEC(M) U is the set of states that belong to a UGEC in M.
max
Intuitively, within a UGEC, P1 has a strategy to almost-surely visit Ceven
(p1 ) while
guaranteeing S(p1 ), and he also has a (generally different) strategy that almost-surely ensures
both parity objectives. Figure 2 gives an example of UGEC: here, the strategy ensuring (1U )
is to go to d, and the strategy ensuring (2U ) is to go to b.

a

b

c

d

e

2, 0

1, 0

1, 0

4, 1

3, 1

Figure 2 This MDP is a UGEC: going to d satisfies (1U ), whereas going to b satisfies (2U ).

The notion of UGEC strengthens the concept of super-good EC that was introduced in [1]:
essentially, the super-good ECs are exactly the ECs satisfying (1U ). Thus, every UGEC is a
super-good EC, but the converse is false.
The central lemma underpinning our approach is the following.
I Lemma 9. The following equivalence holds:
s0 |= S(p1 ) ∧ AS(♦U) ⇐⇒ s0 |= S(p1 ) ∧ AS(p2 ).
Essentially, this lemma permits to reduce the problem under study to the one treated in
Theorem 4, provided that we are able to compute U, the set of states appearing in a UGEC.
The rest of this section is dedicated to the proof of this lemma and its consequences: in
Sect. 4.1, we prove the left-to-right implication, in Sect. 4.2, we prove its converse, and finally,
in Sect. 4.3, we establish an algorithm to solve problem s0 |= S(p1 ) ∧ AS(p2 ) based on this
reduction and we study its complexity.

4.1

Left-to-right implication (sufficient condition)

Available strategies in UGECs. We first focus on witness strategies for conditions (1U )
and (2U ) of Definition 8. For (1U ), it was shown in the proof of [2, Lemma 3] (extended
version of [1]) that deciding if the condition holds is in NP ∩ coNP and that uniform finitememory witness strategies exist. For (2U ), we establish the following lemma.
I Lemma 10. Let C be an EC of M. The following assertions hold.
1. It can be decided in polynomial time if condition (2U ) holds.
2. If the answer is Yes, then there exists a (uniform randomized) memoryless witness
max
max
strategy λ2,C and a sub-EC D ⊆ C such that Deven
(p1 ) 6= ∅, Deven
(p2 ) 6= ∅, and for all
s ∈ C,


λ
PM2,C
{π ∈ OutMC (λ2,C ) | inf(π) = D} = 1.
C ,s
3. Furthermore, λ2,C satisfies the following property: ∀ s ∈ C, ∀ ε > 0, ∃ n ∈ N such that


λ
max
PM2,C
π ∈ OutMC (λ2,C ) | ∃ i, 0 ≤ i ≤ n, π(i) ∈ Deven
(p1 ) ≥ 1 − ε.
C ,s

R. Berthon, M. Randour, and J.-F. Raskin

Proof. We first prove Point 2. Let C be an EC that satisfies condition (2U ), and a
corresponding witness strategy λ (that could use memory in full generality). By Lemma 3,
we know that for any state s ∈ C,


PλMC ,s {π ∈ OutMC (λ) | inf(π) ∈ E} = 1,
where E is the set of ECs of MC . We claim that for any D ∈ E for which


PλMC ,s {π ∈ OutMC (λ) | inf(π) = D} > 0,
max
max
we necessarily have that Deven
(p1 ) 6= ∅ and Deven
(p2 ) 6= ∅. Indeed, assume this is false
for pi . Then, with probability strictly greater than zero, λ induces plays π such that
maxs0 ∈inf(π) pi (s0 ) is odd (as the maximal priority in inf(π) = D is odd). This contradicts
the fact that λ is a witness strategy for s |=MC AS(p1 ) ∧ AS(p2 ) (condition (2U )).
Assume that λ is a witness strategy, potentially leading to several ECs Dj satisfying
the above property with non-zero probability, and potentially using memory. Since each
Dj is included in the EC C, it is easy to conceive a witness strategy λ2,C that reaches and
stays in only one of those ECs with probability one (we call it D from now on) and without
using any memory: indeed, each state of an EC can be almost-surely visited using a uniform
randomized memoryless strategy [4].
max
Second, to prove Point 3, it suffices to use Lemma 2. See that λ2,C reaches Deven
(p1 )
almost-surely from any state s ∈ C. By taking n = k for the k given in Lemma 2 for c = 1 − ε,
we obtain the desired property.
Finally, consider Point 1. We claim that (i) the existence of a sub-EC D such that
max
max
Deven
(p1 ) 6= ∅ and Deven
(p2 ) 6= ∅ is not only necessary but also sufficient to satisfy condition
(2U ), and (ii) the existence of such a set can be decided in polynomial time.
For (i), as discussed above, for any sub-EC of C, in particular for D, we can build a
uniform randomized memoryless strategy λ such that


PλMC ,s {π ∈ OutMC (λ) | inf(π) = D} = 1.

By hypothesis on D, we thus have that p1 and p2 are almost-surely satisfied by λ, hence that
λ is a witness for s |=MC AS(p1 ) ∧ AS(p2 ) and that condition (2U ) holds in C.
It remains to check the existence of such a set D ⊆ C in polynomial time. First, we check
max
max
if Ceven
(p1 ) 6= ∅ and Ceven
(p2 ) 6= ∅. If this holds, then D = C and the answer is Yes (it
takes linear time obviously). If it does not hold, then we compute the sets

max
Codd
(pi ) = s ∈ C | (pi (s) is odd) ∧ (∀ s0 ∈ C, pi (s0 ) is even =⇒ pi (s0 ) < pi (s))
and we iterate this procedure in the sub-EC C 0 ⊂ C defined as

max
max
C 0 = C \ Attr2 Codd
(p1 ) ∪ Codd
(p2 ) .
It is easy to see that a suitable D exists if and only if this procedure stops before C 0 = ∅. In
addition, this procedure takes at most |C| iterations (as we remove at least one state at each
step) and each iteration takes linear time. This implies Point 3 and concludes our proof. J
Inside UGECs. We will now prove that inside any UGEC, there is a strategy for the
beyond worst-case problem S(p1 ) ∧ AS(p2 ). From now on, let C be a UGEC of M, λ1,C
be a uniform finite-memory witness strategy for condition (1U ) of Definition 8, and λ2,C
be a uniform randomized memoryless one for condition (2U ), additionally satisfying the
properties of Lemma 10. We build a strategy λC based on λ1,C and λ2,C .

XX:13

XX:14

Threshold Constraints with Guarantees for Parity Objectives in MDPs

I Definition 11. Let C ∈ UGEC(M). Let (ni )i∈N be a sequence of naturals ni such that
λ

PM2,C
C ,s



max
π ∈ OutMC (λ2,C ) | ∃ i, 0 ≤ i ≤ ni , π(i) ∈ Deven
(p1 )



≥ 1 − 2−i ,

whose existence is guaranteed by Lemma 10. We build the beyond worst-case strategy λC as
follows, starting with i = 0.
a) Play λ2,C for ni steps. Then i = i + 1 and go to b).
max
b) If Deven
(p1 ) was visited in phase a), then go to a).
max
Else, play λ1,C until Ceven
(p1 ) is reached and then go to a).
Observe that λC requires infinite memory. In the next lemma, we prove that λC is a
proper witness for S(p1 ) ∧ AS(p2 ) in the UGEC C.
I Lemma 12. Let C ∈ UGEC(M). For all s ∈ C, it holds that s, λC |= S(p1 ) ∧ AS(p2 ).
Proof. Consider the strategy λC as described in Definition 11 and any state s ∈ C. We first
M
prove that s, λC |= S(p1 ). We want to show that for any π ∈ Outs C (λC ), maxs0 ∈inf(π) p1 (s0 )
is even. Fix such a play π. Three cases are possible: (i) λC switches infinitely often between
λ1,C and λ2,C , (ii) it eventually plays λ1,C forever, and (iii) it eventually plays λ2,C forever.
max
In case (i), we have that Ceven
(p1 ) is visited infinitely often along π. Since any state in this set
has an even priority higher than any odd priority in C by definition, we have that π satisfies
the parity objective p1 . In case (ii), we eventually always play as λ1,C and by hypothesis, we
know that s, λ1,C |= S(p1 ). By prefix-independence, we thus have that π satisfies the parity
max
objective p1 . Finally, in case (iii), we have that Deven
(p1 ) is visited infinitely often, and that
eventually, play π never leaves the sub-EC D associated to strategy λ2,C (by definition of
max
λ2,C , the fact that Deven
(p1 ) ⊆ D is reached, and that we never switch to λ1,C from some
max
point on). Since any state in Deven
(p1 ) has an even priority higher than any odd priority in D,
we have that π satisfies the parity objective p1 . Therefore, we conclude that s, λC |= S(p1 ).
It remains to show that s, λC |= AS(p2 ). To do so, we will prove that λC almost-surely
ends up in playing only λ2,C (which ensures AS(p2 )). First, observe that λ1,C almost-surely
max
reaches Ceven
(p1 ), hence each phase b) of strategy λC terminates with probability one. Now,
consider the probability xi that λ1,C is never played again after round i (in which λ2,C is
Q∞
played for ni steps). For any round i ≥ 1, it is equal to xi = j=i (1 − 2−j ) thanks to the
P∞
choice of ni . Since (1 − 2−j ) > 0 for any j > 1, we have that log(xi ) = j=i log(1 − 2−j ).
Now, for any z ∈ [0, 21 ], we have the following inequalities:
Z

1

0 ≥ log(1 − z) = −(log(1) − log(1 − z)) = −
1−z

1
dy ≥ −2
y

Z

1

dy = −2z.
1−z

Using these, we can bound log(xi ) as follows:
∞
X

−2 · 2−j ≤ log(xi ) ≤ 0 ⇐⇒ −2 · 2−i

j=i

∞
X

2−j ≤ log(xi ) ≤ 0

j=0
−(i−2)

⇐⇒ −2
i→+∞

≤ log(xi ) ≤ 0.

Hence, log(xi ) −−−−→ 0, and by continuity of the exponential function, we finally obtain
i→+∞
that xi −−−−→ 1. This proves that λC almost-surely consists in playing as λ2,C forever from
some point on, which combined with the prefix-independence of the parity objective, implies
that λC ensures AS(p2 ), and concludes our proof.
J

R. Berthon, M. Randour, and J.-F. Raskin

Global strategy. We can now prove the left-to-right implication of Lemma 9. For this,
assume that for s0 ∈ S, we have that λU is a witness for s0 |= S(p1 ) ∧ AS(♦U), where we recall
that U represents the union of all UGECs of the MDP M. Note that such a strategy can be
finite-memory w.l.o.g. as proved in Theorem 4. We build a global strategy λ as follows.
I Definition 13. Based on strategies λU and λC for all C ∈ UGEC(M), we build the global
strategy λ as follows.
a) Play λU until a UGEC C is reached, then go to b).
b) Play λC forever.
This strategy requires infinite memory because it is needed for the strategies λC . We prove
that λ is a witness for the beyond worst-case problem S(p1 ) ∧ AS(p2 ).
I Lemma 14. It holds that s0 , λ |= S(p1 ) ∧ AS(p2 ).
Proof. First, we consider S(p1 ). Along any play π consistent with λ, either (i) a UGEC C is
eventually reached and λ switches to λC , or (ii) λ behaves as λU forever. Since all strategies
λC and strategy λU ensure S(p1 ) and the parity objective is prefix-independent, we have that
s0 , λ |= S(p1 ).
Second, with probability one, λU reaches some UGEC C, in which λC ensures AS(p2 ).
Again invoking prefix-independence, we conclude that λ is also a witness for s0 |= AS(p2 ),
which ends our proof.
J

4.2

Right-to-left implication (necessary condition)

We now turn to the converse implication of Lemma 9, i.e., that s0 |= S(p1 ) ∧ AS(p2 ) implies
s0 |= S(p1 ) ∧ AS(♦U). This in particular requires U to be non-empty, i.e., the existence of a
UGEC in M.
Initialized strategies. We start by an intermediate lemma regarding witness strategies for
the beyond worst-case problem. It establishes that all states reachable via such a strategy
also satisfy the property.
I Lemma 15. For every state s ∈ S, every strategy λ such that s, λ |= S(p1 ) ∧ AS(p2 ), and
every prefix ρ ∈ Pref(OutM
s (λ)), we have that Last(ρ) |= S(p1 ) ∧ AS(p2 ).
Proof. Fix s ∈ S, λ a witness for s |= S(p1 ) ∧ AS(p2 ), and a prefix ρ ∈ Pref(OutM
s (λ)). We
claim that the initialized strategy λ[ρ], that behaves as λ behaves after prefix ρ, is a witness
for Last(ρ) |= S(p1 ) ∧ AS(p2 ).
M
We first consider S(p1 ). For all π ∈ OutM
Last(ρ) (λ[ρ]), we have that ρ · π ∈ Outs (λ).
Furthermore, maxs0 ∈inf(ρ·π) p1 (s0 ) = maxs0 ∈inf(π) p1 (s0 ) is even since s, λ |= S(p1 ). Hence, we
conclude that Last(ρ), λ[ρ] |= S(p1 ).
Now, consider AS(p2 ). By contradiction, assume that Last(ρ), λ[ρ] 6|= AS(p2 ), i.e., that
λ[ρ]
q = PM,Last(ρ) [p2 ] < 1. It implies that PλM,s [p2 ] ≤ 1 − PλM,s [ρ] · (1 − q) < 1 (since any prefix
ρ ∈ Pref(OutM
s (λ)) has strictly positive probability). This contradicts the hypothesis that
s, λ |= AS(p2 ). Hence it holds that Last(ρ), λ[ρ] |= AS(p2 ) and we are done.
J
Existence of UGECs. The next lemma establishes that at least one UGEC must exist
in M since s0 |= S(p1 ) ∧ AS(p2 ).
I Lemma 16. The following holds: s0 |= S(p1 ) ∧ AS(p2 ) =⇒ UGEC(M) 6= ∅.

XX:15

XX:16

Threshold Constraints with Guarantees for Parity Objectives in MDPs

Proof. Given a set of plays Π ⊆ Plays(G), we define
States(Π) = {s ∈ S | ∃ π ∈ Π, ∃ n ∈ N, π(n) = s}.
To prove this lemma, we first study the following set S of subsets of S:

S = R ⊆ S | ∃ s ∈ S, ∃ λ ∈ Λ, (s, λ |= S(p1 ) ∧ AS(p2 )) ∧ (R = States(OutM
s (λ))) .
Intuitively, this set contains any subset of S that captures all states reachable by some
witness strategy λ, from some state s ∈ S. First note that s0 |= S(p1 ) ∧ AS(p2 ) implies that
S is non-empty, as for a witness strategy λ, R = States(OutM
s0 (λ)) ∈ S, by definition.
Second, we show that all minimal elements of S for set inclusion ⊆ are UGECs, i.e.,
that for all R ∈ min⊆ (S), it holds that R ∈ UGEC(M). This will establish our lemma. By
Definition 8, we have to prove that for each R ∈ min⊆ (S), the following properties hold:
a) R is an EC in M,
max
b) ∀ s ∈ R, s |=MR S(p1 ) ∧ AS(♦Reven
(p1 )),
c) ∀ s ∈ R, s |=MR AS(p1 ) ∧ AS(p2 ).
Before proving those three items, we claim that for all R ∈ min⊆ (S), and s ∈ R, there
exists a strategy λR such that s, λR |=MR S(p1 ) ∧ AS(p2 ), i.e., λR satisfies the property
without leaving R. This is a direct consequence of Lemma 15 and the minimality of R in S
for the ⊆ order. We use strategy λR in the rest of the proof.
Item a). We first prove that R is strongly connected. By contradiction, assume it is not
the case, i.e., that there exist s, s0 ∈ R such that there is no path in R from s to s0 . Then, let
R0 be the set of states reachable with strategy λR from a prefix ρ ending in s. By Lemma 15,
we have that R0 ∈ S. But as there is no path from s to s0 in R, we have that s0 6∈ R0
and R0 ( R. This contradicts the minimality of R, hence we conclude that R is strongly
connected. We now have to prove that R is a trap for P2 . Clearly, for any state s ∈ R ∩ S1 ,
we have Succ(s) ∩ R 6= ∅, as R is strongly connected. Hence, it remains to show that for all
s ∈ R ∩ S2 , we have Succ(s) ⊆ R. By contradiction, fix some s ∈ R ∩ S2 and assume there
exists s0 6∈ R such that (s, s0 ) ∈ E. As R belongs to S, recall that R = States(OutM
s00 (λ)) for
some strategy λ and state s00 . Since s ∈ R, there exists a prefix ρ ∈ Pref(OutM
s00 (λ)) such
0
that Last(ρ) = s. But then, prefix ρ0 = ρ · s0 also belongs to Pref(OutM
s00 (λ)), and s ∈ R.
Thus, we conclude that R is indeed a trap for P2 .
max
Item b). Fix any s ∈ R and let us prove that s |=MR S(p1 ) ∧ AS(♦Reven
(p1 )). As seen
above, from the minimality of R and Lemma 15, we know that s, λR |=MR S(p1 ) ∧ AS(p2 ).
Now, again from the minimality of R in S, we know that in the subtree induced by OutM
s (λR ),
any non-empty subset R0 ⊆ R is dense. That is, for every prefix ρ, the subtree defined by λR
from ρ reaches a state of R0 , and this holds in all subsequent subtrees. Using the reduction
to a parity-Büchi game which underlies Theorem 4, we deduce from the density argument
presented in Appendix A that we can build λ from λR such that s, λ |=MR S(p1 ) ∧ AS(♦R0 ).
max
It remains to argue that Reven
(p1 ) is non-empty to prove this item. This is necessarily true,
max
max
otherwise Rodd (p1 ) would be non-empty and λR would not ensure S(p1 ) in R (as Rodd
(p1 )
would be a dense subset).
Item c). This is trivial as, for s ∈ R, λR enforces s, λR |=MR S(p1 ) ∧ AS(p2 ), a stronger
property.
J
Reaching UGECs. Let us now collect in Umin = ∪R∈min⊆ (S) R all states that belong to
minimal sets R of S, and establish that Umin can be reached almost-surely if it holds that
s0 |= S(p1 ) ∧ AS(p2 ).

R. Berthon, M. Randour, and J.-F. Raskin

I Lemma 17. The following holds: s0 |= S(p1 ) ∧ AS(p2 ) =⇒ s0 |= S(p1 ) ∧ AS(♦Umin ).
Proof. Let λ be a witness for s0 |= S(p1 ) ∧ AS(p2 ). By Lemma 16, we know that UGEC(M)
is non-empty, and so is Umin . Furthermore, we claim that Umin is dense in the tree induced
M
by OutM
s0 (λ). Indeed, by Lemma 15, after any prefix ρ ∈ Pref(Outs0 (λ)), the following
property holds: Last(ρ), λ[ρ] |= S(p1 ) ∧ AS(p2 ) (hence Umin is reached, repeating the previous
arguments). Since this holds for all consistent prefixes, we have that Umin is indeed dense in
the tree of λ. Hence, again using the density argument presented in Appendix A, we can
build λ0 from λ such that s0 , λ0 |= S(p1 ) ∧ AS(♦Umin ).
J

4.3

Algorithm

Lemma 14 and Lemma 17 prove the correctness of the reduction presented in Lemma 9. It is
the cornerstone of our algorithm deciding whether the property s0 |= S(p1 ) ∧ AS(p2 ) holds.
I Theorem 18. Given an MDP M = (G = (S, E), S1 , S2 , δ), a state s0 ∈ S, and two priority
functions pi : S → {1, . . . , d}, i ∈ {1, 2}, it can be decided in NP∩coNP if s0 |= S(p1 )∧AS(p2 ).
If the answer is Yes, then there exists an infinite-memory witness strategy, and infinite
memory is in general necessary. This decision problem is at least as hard as solving parity
games.
Proof. The algorithm can be sketched as follows:
1. Compute the set max⊆ (SGEC(M)) of maximal super-good ECs, using [1]. Those are
the maximal ECs satisfying condition (1U ) in Definition 8. There are only polynomially
many of them, and their computation is in NP ∩ coNP.
2. For each of them, check if condition (2U ) holds using Lemma 10. This can be done in
polynomial time, and if a super-good EC does not satisfy (2U ), then it is also the case of
all its sub-ECs (as seen in the proof of Lemma 10). Hence, we have that


U = C ∈ max(SGEC(M)) | C satisfies (2U ) .
⊆

3. Decide if s0 |= S(p1 ) ∧ AS(♦U) using Theorem 4. This is in NP ∩ coNP. If it holds, then
answer Yes, otherwise answer No.
The correctness of this algorithm was established in Lemma 9. It belongs to PNP∩coNP =
NP ∩ coNP [6], and it trivially generalizes classical parity games (e.g., by taking p2 : s 7→ 0
for all s ∈ S).
Finally, let us discuss strategies. A witness strategy λ plays as follows: (i) it plays as the
finite-memory strategy witness for s0 |= S(p1 ) ∧ AS(♦U) given by Theorem 4 until a UGEC C
is reached, (ii) then it switches to the infinite-memory strategy λC described in Definition 11.
It is clear that such a strategy is a witness for s0 |= S(p1 ) ∧ AS(p2 ), as expected.
Infinite memory is required in general, as shown in the UGEC C depicted in Figure 2:
there exists no finite-memory witness strategy in C. Indeed, assume P1 is restricted to a
finite-memory strategy λ. To be able to ensure p1 on the play in which P2 always goes to c
from b, P1 must visit d infinitely often, and because of the finite memory of λ, he must do
it after a bounded number of steps along which a is not visited: say n steps. Hence, the
n
probability to do it will be bounded from below by a strictly positive constant, here 2− 2 (the
probability that P2 chooses c for n2 times in a row), all along a consistent play. Therefore,
P1 will almost-surely visit d infinitely often, and p2 will actually be satisfied with probability
zero.
J

XX:17

XX:18

Threshold Constraints with Guarantees for Parity Objectives in MDPs

5

Parity with threshold probability under parity constraints

We now turn to the problem s0 |= S(p1 ) ∧ P∼c (p2 ) for ∼ ∈ {>, ≥} and c ∈ Q ∩ [0, 1).
Very-good end-components. In addition to UGECs, we need the new notion of very-good
end-component.
I Definition 19. An end-component C of M is very-good (VGEC) if the following two
properties hold:
(1V ) ∀ s ∈ C, s |=M S(p1 );
(2V ) ∀ s ∈ C, s |=MC AS(p1 ) ∧ AS(p2 ), or equivalently, s |=MC AS(p1 ∩ p2 ).
We introduce the following notations:
VGEC(M) is the set of all VGECs of M,
V = ∪V ∈VGEC(M) V is the set of states that belong to a VGEC in M.
Note that in condition (1V ), P1 is allowed to leave C to ensure S(p1 ): this is in contrast
to condition (1U ) for UGECs, in Definition 8. On the contrary, condition (2V ) is exactly
the same as (2U ).
From these definitions, it is trivial to see that any UGEC is also a VGEC, but the converse
is false. Consider Figure 3 (δ is the uniform distribution): {a, b, c} is a VGEC. The strategy
ensuring (2V ) from a is to go to b, and the strategy ensuring (1V ) from a is to go to d.
As we will prove in Lemma 21 and as in all VGECs, P1 can ensure a |= S(p1 ) ∧ P>1−ε (p2 )
for any ε > 0. Still, {a, b, c} is not a UGEC: no strategy ensures S(p1 ) on M{a,b,c} , as P2
can enforce the play (ab)ω that has odd maximal priority. This illustrates why the notion
of UGEC is too strong when reasoning about threshold probability instead of almost-sure
satisfaction, hence why we need to introduce VGECs.
b 1, 1
1, 1

0, 1

a

d

c 2, 2

Figure 3 The EC {a, b, c} is very-good but not ultra-good, as P1 has to leave it to ensure S(p1 ).

Available strategies in VGECs. As for UGECs, we will use witness strategies for
conditions (1V ) and (2V ). Deciding if condition (1V ) holds is solving a classical parity game,
which lies in NP ∩ coNP [19]. Uniform pure memoryless witness strategies exist. We denote
by λ1 such a witness. For simplicity of presentation, we assume in the following that all states
of M satisfy (1V ), as otherwise they will trivially not satisfy the properties we consider (as
S(p1 ) will not be ensured). For condition (2V ), we established in Lemma 10 that deciding if
it holds can be done in polynomial time and that uniform randomized memoryless witness
strategies exist. We denote by λ2,C such a witness.
Reaching VGECs. We prove a strong relationship between the measure of paths that
satisfy the two parity objectives p1 and p2 , and the measure of paths that reach VGECs,
under any strategy.
I Lemma 20. For all s ∈ S, and all λ ∈ Λ, the following holds: PλM,s [♦V] ≥ PλM,s [p1 ∩ p2 ].

R. Berthon, M. Randour, and J.-F. Raskin

Proof. Let Π = {π ∈ OutM
s (λ) | maxs∈inf(π) p1 (s) and maxs∈inf(π) p2 (s) are even} be the
set of consistent plays from s that are winning for both p1 and p2 . Let q ∈ [0, 1] be the
measure of Π under λ. Now, let us define the set Π0 as Π from which we remove the plays π
such that inf(π) is not an EC. By Lemma 3, the measure of Π \ Π0 is equal to zero, and so
the measure of Π0 is also q. Now, let us note that any remaining play π in Π0 visits (even
infinitely many times) the EC inf(π), and by definition of Π, there exists a witness for (2V ):
it suffices to play uniformly at random in inf(π). Since (1V ) is satisfied everywhere, we have
that inf(π) is a VGEC. All the states of such VGECs belong to V by definition, and so we
are done as we have proved that PλM,s [♦V] ≥ q.
J
Limit-sure satisfaction in VGECs. For each state in a VGEC, we claim that the parity
objective p2 can be satisfied with probability arbitrarily close to one, while ensuring p1 surely.
I Lemma 21. Let C ∈ VGEC(M). For all s ∈ C and ε ∈ (0, 1], the following property
holds: s |= S(p1 ) ∧ P>1−ε (p2 ).
Proof. Our goal is to define a witness strategy λε . First, for ε ∈ (0, 1], we fix an infinite
sequence of strictly positive rational probabilities f : N → Q ∩ (0, 1] such that the product of
Q
all those probabilities is larger than 1 − ε, i.e., i∈N f (i) > 1 − ε. Such a sequence always
exists. In turn, we use Lemma 10 to associate to f a sequence of natural numbers g : N → N
such that if λ2,C (the witness strategy for (2V )) is played for g(i) steps from any s0 ∈ C,
max
then the set Deven
(p1 ) associated to λ2,C is visited during those g(i) steps with probability
larger than f (i).
Now, we are in position to define for all ε ∈ (0, 1], a strategy λε,C that enforces, from
s ∈ C, the property S(p1 ) ∧ P>1−ε (p2 ). The strategy λε,C uses a counter i whose value is
initially equal to 0. At round i, the strategy plays as λ2,C for g(i) steps. During those last
max
g(i) steps, if the set Deven
(p1 ) is visited, then the counter i is incremented and the next
round is executed. Otherwise, the strategy switches to λ1 forever.
It is easy to see that, because of the definition that we have used for the sequence g, the
probability that we ever switch to the strategy λ1 is less than ε. So with probability larger
than 1 − ε, we always play λ2,C , which implies that λε,C ensures P>1−ε (p2 ). Also, on all
consistent plays in which strategy λ2,C is played forever, we know that the maximal priority
max
seen infinitely often for p1 is even (by definition of Deven
(p1 )). On the other plays, as we
play λ1 , we also have that the maximal priority seen infinitely often for p1 is even. So, we
can also conclude that λε,C ensures S(p1 ), which concludes our proof.
J

5.1

The strict threshold case

We first solve the strict threshold case with an approach that relies on VGECs. Similarly
to what we did in Section 4, we will establish a reduction of the decision problem for
s0 |= S(p1 ) ∧ P>c (p2 ) to a reachability problem toward the set V, i.e., the union of VGECs.
The actual algorithm will be detailed in Section 5.3.
The first lemma gives a sufficient condition under which the property is satisfied. Note
that its proof is constructive and tells us how to construct witness strategies.
I Lemma 22. The following holds: s0 |= S(p1 ) ∧ P>c (♦V) =⇒ s0 |= S(p1 ) ∧ P>c (p2 ).
Proof. Let λ♦V be a uniform pure memoryless strategy that ensures to reach V with
probability q > c from s0 (it exists by Lemma 2). Recall that λ1 is a uniform pure
c
memoryless strategy that enforces S(p1 ) from any state in M. Let ε be such that q > 1−ε
,

XX:19

XX:20

Threshold Constraints with Guarantees for Parity Objectives in MDPs

and for all C ∈ VGEC(M), let λε,C be a strategy that ensures S(p1 ) ∧ P>1−ε (p2 ) when
played from any state in C, as defined in the proof of Lemma 21.
We construct the strategy λ that witnesses the desired property starting from the elements
defined above. Let r be a number of steps sufficient to ensure that V is reached with a
c
probability larger than 1−ε
when playing λ♦V from s0 : it exists by Lemma 2. Strategy λ plays
as λ♦V for r steps. If a VGEC C of M is reached during those r steps, λ immediately switches
to λε,C . Otherwise, after the r steps, λ switches to λ1 forever. It is easy to verify that, when
c
λ is played, the probability that p2 holds is larger than 1−ε
· (1 − ε), and so it is larger than c.
Furthermore, p1 holds on all consistent plays, which proves that s0 , λ |= S(p1 ) ∧ P>c (p2 )
holds.
J
This second lemma gives a necessary condition for the property to hold.
I Lemma 23. The following holds: s0 |= S(p1 ) ∧ P>c (p2 ) =⇒ s0 |= S(p1 ) ∧ P>c (♦V).
Proof. First, recall that λ1 is a uniform pure memoryless strategy that enforces S(p1 ) from
any state in M. Second, as s0 |= S(p1 ) ∧ P>c (p2 ), by Lemma 20 and Lemma 2, there exists a
uniform pure memoryless strategy λ♦V that reaches V with probability q > c from s0 .
We construct a strategy λ that witnesses s0 |= S(p1 ) ∧ P>c (♦V) starting from λ1 and
λ♦V above. Let r be a number of steps such that, if λ♦V is played for r steps, then the
probability to reach V from s0 is larger than c: it exists by Lemma 2. Strategy λ starts
from s0 by playing as λ♦V . It stops as soon as V is reached or if r steps have been played
and V has not been reached: in both cases, it switches to λ1 forever. It is easy to check
that λ reaches V with probability larger than c and it enforces S(p1 ) by definition of λ1 and
prefix-independence of the parity objective. Hence, it holds that s0 , λ |= S(p1 ) ∧ P>c (♦V). J

5.2

The non-strict threshold case

First, we note that, as we have solved the strict case above, the only interesting remaining
case is when P1 , while surely forcing p1 , can force p2 with probability c, but no more. The
following two lemmas present a solution to this case. The main conceptual tool here is
UGECs. As for the strict case, the corresponding algorithm will be detailed in Section 5.3.
The first lemma gives a sufficient condition. Its proof is constructive: it explains how to
build witness strategies. Recall that U = ∪U ∈UGEC(M) U is the set of states that belong to a
UGEC in M.
I Lemma 24. The following holds: s0 |= S(p1 ) ∧ P≥c (♦U) =⇒ s0 |= S(p1 ) ∧ P≥c (p2 ).
Proof. Let λ♦U be a finite-memory strategy that witnesses property s0 |= S(p1 ) ∧ P≥c (♦U).
It exists by Theorem 6. For all C ∈ UGEC(M), let λC be an infinite-memory witness for
s |= S(p1 ) ∧ AS(p2 ), for all s ∈ C: it exists by Lemma 12. From those strategies, we define the
strategy λ as follows. From s0 , λ plays as λ♦U up to reaching a UGEC C of M, or forever if
U is never reached. If some UGEC C is reached, then it switches to λC forever.
We claim that λ is a witness for s0 |= S(p1 )∧P≥c (p2 ). First, S(p1 ) clearly holds as strategy
λ♦U and all strategies λC ensure it. Second, λ♦U ensures to reach U with probability at
least c, and when some UGEC C ⊆ U is reached, the strategy λC ensures p2 with probability
one. Thus, λ ensures p2 with probability at least c from s0 , and we are done.
J
We now turn to a lemma that gives a necessary condition, keeping in mind that we are
interested in the case where P1 cannot ensure probability strictly larger than c.

R. Berthon, M. Randour, and J.-F. Raskin

I Lemma 25. The following holds:
(s0 |= S(p1 ) ∧ P≥c (p2 )) ∧ (s0 6|= S(p1 ) ∧ P>c (p2 )) =⇒ s0 |= S(p1 ) ∧ P≥c (♦U).
Proof. Let λ be a strategy that witnesses s0 |= S(p1 ) ∧ P≥c (p2 ). As s0 6|= S(p1 ) ∧ P>c (p2 ), the
measure of Π = {π ∈ OutM
s0 (λ) | maxs∈inf(π) p1 (s) and maxs∈inf(π) p2 (s) are even} is exactly
0
equal to c. We define Π as Π from which we remove all play π such that inf(π) is not an
EC. By Lemma 3, the measure of Π0 is equal to the one of Π. As all plays in Π0 satisfy both
p1 and p2 and are such that inf(π) is an EC, we conclude that they all reach a VGEC (as
conditions (1V ) and (2V ) are satisfied in inf(π)).
Let π ∈ Π0 and let ρ be a prefix of π such that Last(ρ) ∈ C for some C ∈ VGEC(M). We
claim that Last(ρ), λ[ρ] |= S(p1 ) ∧ AS(p2 ). We prove it by contradiction. Assume that λ[ρ]
only enforces p2 with probability 1 − ε for some ε > 0. As Last(ρ) belongs to the VGEC C,
we invoke Lemma 21 to build a strategy λρ such that Last(ρ), λρ |= S(p1 ) ∧ P>1−ε0 (p2 ) for
ε0 < ε. Now, to obtain the contradiction, we construct a new strategy λ0 from s0 that plays as
λ but switches to λρ after prefix ρ. We have that s0 , λ0 |= S(p1 ) ∧ P>c (p2 ), which contradicts
our hypothesis. Hence, we conclude that Last(ρ), λ[ρ] |= S(p1 ) ∧ AS(p2 ) holds.
Finally, applying Lemma 17 to Last(ρ), we know that Last(ρ) |= S(p1 ) ∧ AS(♦U). As
the measure of Π0 is equal to c and this reasoning holds for any π ∈ Π0 , we conclude that
s0 , λ |= S(p1 ) ∧ P≥c (♦U) and we are done.
J

5.3

Algorithm

Based on the reductions shown above, we can now establish an algorithm and complexity
results for the threshold problem.
I Theorem 26. Given an MDP M = (G = (S, E), S1 , S2 , δ), a state s0 ∈ S, and two priority
functions pi : S → {1, . . . , d}, i ∈ {1, 2}, it can be decided in NP∩coNP if s0 |= S(p1 )∧P∼c (p2 )
for ∼ ∈ {>, ≥} and c ∈ Q ∩ [0, 1). If the answer is Yes, then there exists an infinite-memory
witness strategy, and infinite memory is in general necessary. This decision problem is at
least as hard as solving parity games.
Proof. The algorithm can be sketched as follows:
1. Remove from M all states where S(p1 ) does not hold, as well as their attractor for P2 :
if s0 is removed, then answer No. Let M0 be the remaining MDP. This operation is in
NP ∩ coNP as it consists in solving a classical parity game [19].
2. Compute the set V representing the union of VGECs in M0 . This can be done in
polynomial time by computing the maximal ECs of M0 and applying Lemma 10 to check
condition (2V ) for each of them (condition (1V ) holds thanks to the previous step).
3. Decide if s0 |= S(p1 ) ∧ P>c (♦V) using Theorem 6. This is in NP ∩ coNP. If it holds, then
answer Yes. If it does not hold and ∼ is >, then answer No, otherwise, i.e., if ∼ is ≥,
continue with the next step.
4. Use the sub-algorithm described in Theorem 18 to compute the set U representing the
union of UGECs in M0 . This is in NP ∩ coNP.
5. Decide if s0 |= S(p1 ) ∧ P≥c (♦U) using Theorem 6. This is in NP ∩ coNP. If it holds,
answer Yes, otherwise answer No.
The correctness of this algorithm follows from Lemma 22, Lemma 23, Lemma 24, and
Lemma 25. It belongs to PNP∩coNP = NP ∩ coNP [6], and it trivially generalizes classical
parity games (e.g., by taking p2 : s 7→ 0 for all s ∈ S).

XX:21

XX:22

Threshold Constraints with Guarantees for Parity Objectives in MDPs

Finally, let us discuss strategies. Witness strategies for the case > (resp. ≥) were described
in Lemma 22 (resp. Lemma 24). In both cases, infinite memory is in general required, because
it is in general necessary to play optimally in both VGECs and UGECs. For UGECs, see
Theorem 18 for an example. For VGECs, consider the VGEC {a, b, c} in the MDP of Figure 3.
We claim that for every finite-memory strategy λ ensuring S(p1 ), the probability to ensure p2
is zero, hence there is no finite-memory witness for a |= S(p1 ) ∧ P>1−ε (p2 ). As argued for the
UGEC case, in order to ensure p1 on the play in which P2 always goes to a from b, P1 must
go to d at some point, and because of the finite memory of λ, he must do it after a bounded
number of steps along which c is not visited: say n steps. Again, the probability to do it will
n
be bounded from below by a strictly positive constant, here 2− 2 (the probability that P2
chooses a for n2 times in a row), all along a consistent play. Therefore, P1 will almost-surely
go to d, and p2 will actually be satisfied with probability zero.
J

6

Conclusion

We further extended the beyond worst-case synthesis framework by providing tools to reason
about ω-regular conditions, representing functional requirements of systems. We studied the
case of two parity objectives and proved NP ∩ coNP membership for all considered variants.
It is interesting to note that our algorithms can easily be generalized to more than two
parity objectives as long as we consider only the S and AS operators. Indeed, we have that
for any MDP M, any state s in M, and any number
of priority
 functions p1 , . . . pn , it holds
V
V
V 
V
that s |= i S(pi ) j AS(pj ) ⇐⇒ s |= S i pi ∧ AS j pj , and it is easy to reduce the
latter problem to s0 |= S(p0 ) ∧ AS(p00 ) on a (larger) MDP M0 , using classical techniques (e.g.,
any conjunction of parity objectives can be expressed as a Muller condition [13], that in
turn can be transformed into a single parity condition on a larger graph [20]). Extending
this generalization to the operator P∼c is more challenging and would require to mix our
techniques to methods for percentile queries [24]: an interesting direction for future work.
Another question is the limits of finite-memory strategies. We saw that in general, infinite
memory is needed to satisfy problems involving two parity objectives. We would like to
investigate under which additional conditions finite-memory strategies suffice, and to develop
corresponding algorithms, as finite-memory strategies are of great practical interest.
References
1

2

3

4

Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing expected cost under
hard boolean constraints, with applications to quantitative synthesis. In Josée Desharnais
and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory,
CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages
9:1–9:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. doi:10.4230/LIPIcs.
CONCUR.2016.9.
Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing expected cost under hard
boolean constraints, with applications to quantitative synthesis. CoRR, abs/1604.07064,
2016. URL: http://arxiv.org/abs/1604.07064.
Christel Baier, Marcus Größer, and Frank Ciesinski. Quantitative analysis under fairness
constraints. In Zhiming Liu and Anders P. Ravn, editors, Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October
14-16, 2009. Proceedings, volume 5799 of Lecture Notes in Computer Science, pages 135–
150. Springer, 2009. doi:10.1007/978-3-642-04761-9_12.
Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.

R. Berthon, M. Randour, and J.-F. Raskin

5

6
7

8

9

10

11

12

13

14

15

Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold constraints with
guarantees for parity objectives in Markov decision processes. In Proc. of ICALP, LIPIcs.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. To appear.
Gilles Brassard. A note on the complexity of cryptography (corresp.). IEEE Transactions
on Information Theory, 25(2):232–233, 1979.
Tomás Brázdil, Antonín Kucera, and Petr Novotný. Optimizing the expected mean payoff
in energy Markov decision processes. In Cyrille Artho, Axel Legay, and Doron Peled, editors,
Automated Technology for Verification and Analysis - 14th International Symposium, ATVA
2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in
Computer Science, pages 32–49, 2016. doi:10.1007/978-3-319-46520-3_3.
Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-zero sum games
for reactive synthesis. In Adrian-Horia Dediu, Jan Janousek, Carlos Martín-Vide, and
Bianca Truthe, editors, Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 3–23. Springer, 2016.
doi:10.1007/978-3-319-30000-9_1.
Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Expectations or guarantees? I want it all! A crossroad between games and MDPs. In Fabio
Mogavero, Aniello Murano, and Moshe Y. Vardi, editors, Proceedings 2nd International
Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, volume 146
of EPTCS, pages 1–8, 2014. doi:10.4204/EPTCS.146.1.
Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet
your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In
Ernst W. Mayr and Natacha Portier, editors, 31st International Symposium on Theoretical
Aspects of Computer Science, STACS 2014, March 5-8, 2014, Lyon, France, volume 25 of
LIPIcs, pages 199–213. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. doi:
10.4230/LIPIcs.STACS.2014.199.
Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an
alternative approach toward parity games with time bounds. In Domenico Cantone and
Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games,
Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, volume 226 of EPTCS, pages 135–148, 2016. doi:10.4204/EPTCS.226.10.
Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Mean-payoff parity
games. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June
2005, Chicago, IL, USA, Proceedings, pages 178–187. IEEE Computer Society, 2005. doi:
10.1109/LICS.2005.26.
Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Generalized parity games.
In Helmut Seidl, editor, Foundations of Software Science and Computational Structures,
10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April
1, 2007, Proceedings, volume 4423 of Lecture Notes in Computer Science, pages 153–167.
Springer, 2007. doi:10.1007/978-3-540-71389-0_12.
Lorenzo Clemente and Jean-François Raskin. Multidimensional beyond worst-case and
almost-sure problems for mean-payoff objectives. In 30th Annual ACM/IEEE Symposium
on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 257–268.
IEEE Computer Society, 2015. doi:10.1109/LICS.2015.33.
Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime,
Mathias Grund Sørensen, and Jakob Haahr Taankvist. On time with minimal expected
cost! In Franck Cassez and Jean-François Raskin, editors, Automated Technology for

XX:23

XX:24

Threshold Constraints with Guarantees for Parity Objectives in MDPs

16

17
18

19
20

21

22

23

24

25

Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW,
Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer
Science, pages 129–145. Springer, 2014. doi:10.1007/978-3-319-11936-6_10.
E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model-checking for fragments of µ-calculus. In Costas Courcoubetis, editor, Computer Aided Verification, 5th
International Conference, CAV’93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science, pages 385–396. Springer, 1993.
doi:10.1007/3-540-56922-7_32.
Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer, 1997.
Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and
Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February
2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002.
Marcin Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Inf. Process.
Lett., 68(3):119–124, 1998. doi:10.1016/S0020-0190(98)00150-1.
Christof Löding. Optimal bounds for transformations of omega-automata. In C. Pandu
Rangan, Venkatesh Raman, and Ramaswamy Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings, volume 1738 of Lecture Notes in Computer Science, pages
97–109. Springer, 1999. doi:10.1007/3-540-46691-6_8.
Mickael Randour. Automated synthesis of reliable and efficient systems through game
theory: A case study. In Proc. of ECCS 2012, Springer Proceedings in Complexity XVII,
pages 731–738. Springer, 2013. doi:10.1007/978-3-319-00395-5\_90.
Mickael Randour. Reconciling rationality and stochasticity: Rich behavioral models in
two-player games. CoRR, abs/1603.05072, 2016. GAMES 2016, the 5th World Congress of
the Game Theory Society, Maastricht, Netherlands. URL: http://arxiv.org/abs/1603.
05072.
Mickael Randour, Jean-François Raskin, and Ocan Sankur. Variations on the stochastic shortest path problem. In Deepak D’Souza, Akash Lal, and Kim Guldstrand Larsen,
editors, Verification, Model Checking, and Abstract Interpretation - 16th International
Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, volume
8931 of Lecture Notes in Computer Science, pages 1–18. Springer, 2015. doi:10.1007/
978-3-662-46081-8_1.
Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multidimensional Markov decision processes. Formal Methods in System Design, 50(2):207–248,
2017. doi:10.1007/s10703-016-0262-7.
Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs.
In 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA,
21-23 October 1985, pages 327–338. IEEE Computer Society, 1985. doi:10.1109/SFCS.
1985.12.

R. Berthon, M. Randour, and J.-F. Raskin

A

XX:25

Additional tools related to density

In this section, we develop a density argument that is needed to prove the right-to-left
implications of Lemma 7, and Lemma 9 in Section 4.2. We place this argument in appendix,
as it essentially gives an explicit presentation of results that implicitly follow from [1]: hence
it is not a new contribution.
Density. Let M = (G = (S, E), S1 , S2 , δ) be an MDP, s ∈ S an initial state, λ a strategy,
and R ⊆ S. We say that R is dense in λ from s if and only if for all ρ ∈ Pref(OutM
s (λ)),
0
there exists ρ0 such that ρ · ρ0 ∈ Pref(OutM
(λ))
and
Last(ρ
)
∈
R.
That
is,
after
all
prefixes
s
in the tree OutM
s (λ), there is a continuation that visits R.
Büchi objective. The Büchi objective is a parity objective with priorities in {1, 2}, where
states with priority 2 are called Büchi accepting states, defining a set B: Büchi(B) = {π ∈
Plays(G) | inf(π) ∩ B 6= ∅}.
Almost-sure reachability under parity constraints. We first give explicitly the construction of [2, Lemma 3] (extended version of [1]), that we used implicitly in Theorem 4.
I Theorem 27 ([1, 2]). Given an MDP M = (G = (S, E), S1 , S2 , δ), a state s0 ∈ S, a
priority function p : S → {1, 2, . . . , d}, and a target set R ⊆ S, it can be decided in NP ∩ coNP
if s0 |= S(¬(♦R) → p) ∧ AS(♦R). If the answer is Yes, then there exists a finite-memory
witness strategy. This decision problem is at least as hard as parity games.
To solve the decision problem of Theorem 27, Almagor et al. construct a two-player zerosum game with a conjunction of a Büchi and a parity objectives. We recall the construction
here. To simplify the formal definition and w.l.o.g., we make the hypothesis that in M,
E ⊆ S1 × S2 ∪ S2 × S1 , i.e., states of P1 and P2 alternate. Then the game GM
R,p is defined as
follows.
The state space of GM
R,p is a copy of the state space of M where the states in S2 \ R
have been duplicated in three copies as shown in Figure 4. Then S 0 is defined as
S 0 = S1 ∪S2 ∪(S2 \R)×{square, circle}: P1 owns the states in S1 and (S2 \R)×{circle},
and P2 owns the states in S2 and (S2 \ R) × {square}.
The set of edges are defined according to Figure 4 with the additional property that
states in R are made absorbing. That is, E 0 is the union of the following sets:
{(s, s0 ) | (s, s0 ) ∈ E ∩ ((S1 \ R) × S2 )},
{(s, (s, ?)) | s ∈ S2 \ R, ? ∈ {square, circle})},
{((s, ?), s0 ) | (s, s0 ) ∈ E ∩ ((S2 \ R) × S1 ), ? ∈ {square, circle}},
{(s, s) | s ∈ R}.
The priority function p0 is defined as p0 (s) = p(s) for all s ∈ S1 ∪ S2 \ R, p0 ((s, ?)) = 0 for
all s ∈ S2 \ R and ? ∈ {square, circle}, and p0 (s) = 0 for all s ∈ R.
The set of Büchi states is B = R ∪ {(s, square) | s ∈ S2 \ R}.

0
i

=⇒

i
0

Figure 4 Replacing a P2 state with priority i by three new states, including a Büchi one.

XX:26

Threshold Constraints with Guarantees for Parity Objectives in MDPs

Careful inspection of [1, 2] reveals that s0 |= S(¬(♦R) → p) ∧ AS(♦R) if and only if P1
has a winning strategy in the Büchi parity game GM
R,p from state s0 , and that finite-memory
strategies suffice on both sides. Indeed, finite-memory strategies suffice for Büchi parity games
(as they are a particular case of generalized parity games [13]), and from a finite-memory
strategy in the Büchi parity game, one obtains straightforwardly a witness strategy for
property S(¬(♦R) → p) ∧ AS(♦R). The proof presented in [1, 2] further reduces the problem
of deciding the winner in the Büchi parity game to the same problem on a mean-payoff
parity game [12], in order to benefit from the NP ∩ coNP complexity of the latter. This
reduction does hold since we can restrict ourselves to finite-memory strategies without loss
of generality.
We now prove a related result that uses the notion of density of a set of states in a
strategy tree.
I Lemma 28. Given an MDP M = (G = (S, E), S1 , S2 , δ), a state s ∈ S, a priority function
p : S → {1, 2, . . . , d}, a set R ⊆ S, and a strategy λ such that s, λ |= S(p1 ) and R is dense in
λ from s, there is a winning strategy from s in the associated Büchi parity game GM
R,p from
state s.
Proof. We construct a strategy λ0 for P1 to play in GM
R,p starting from the strategy λ, and
we show that λ0 is winning for the Büchi parity objective.
Let α : S 0 → S be a mapping from the states in GM
R,p to states in M such that α(s) = s
for all s ∈ S1 ∪ S2 and α(s, ?) =  for all (s, ?) ∈ (S2 \ R) × {square, circle}. Then we
extend α to map prefixes in GM
R,p to prefixes in M.
Now, we label each prefix ρ ∈ Pref(OutM
s (λ)) such that Last(ρ) ∈ S2 by a finite
0
0
0
continuation lab(ρ) = ρ such that (i) ρ · ρ ∈ Pref(OutM
s (λ)) and last(ρ ) ∈ R; and (ii) if
0
0
0
0
0
ρ = ρ1 · s · ρ2 is the label of ρ and s ∈ S2 , then lab(ρ · ρ1 · s) = ρ2 . It should be clear that
due to the density of R, such a labelling is always possible.
Now, we define the strategy λ0 from λ and this labelling:
For a prefix ρ in the game such that Last(ρ) ∈ R, the only possible choice is Last(ρ) as
R is absorbing in the game.
For a prefix ρ such that Last(ρ) ∈ S1 ∪ (S2 \ R) × {circle} and such that α(ρ) is not
consistent with λ, we choose any s0 such that (Last(ρ), s0 ) ∈ E 0 .
For a prefix ρ such that Last(ρ) ∈ S1 and such that α(ρ) is consistent with λ, we define
λ0 (ρ) = λ(α(ρ))
For a prefix ρ such that Last(ρ) ∈ (S2 \ R) × {circle} and such that α(ρ) is consistent
0
with λ, then α(ρ) in the tree OutM
s (λ) is labelled with a finite path ρ that leads to a
state in R, i.e., lab(α(ρ)) = ρ0 , then we define λ0 (ρ) = First(ρ0 ).
Let us now show that λ0 wins the Büchi B and parity p0 objectives in the game GM
R,p from
0
state s. First, as λ is enforcing p in M, p replicates the priorities given by p, and absorbing
states in R have even priorities for p0 , it is clear that λ0 enforces p0 in the game GM
R,p . Now,
for the Büchi objective, we consider the following case study on the plays π consistent with
λ0 in the game.
If π ends up in R, then it is clearly Büchi accepting.
If π is such that after a finite prefix ρ, P2 always chooses from states s0 ∈ S2 the copy
(s0 , circle), then according to the definition of λ0 , the play will follow a finite path ρ0 to
a state in R, and so π reaches R and as a consequence π is Büchi accepting.

R. Berthon, M. Randour, and J.-F. Raskin

XX:27

Finally, if π is such that it is never the case that P2 always chooses from a state s0 the
copy (s0 , circle), then P2 chooses infinitely often the copy (s0 , square), and because
(s0 , square) ∈ B, we have that π is also Büchi accepting.
So in all cases, play π satisfies the Büchi objective, and we are done.

J

Consequence. Lemma 28, in combination with Theorem 27 and the reduction of Theorem 4,
has the interesting consequence that if λ is such that s, λ |= S(p1 ) and R is dense in λ from s,
then we can build λ0 such that s, λ0 |= S(p1 ) ∧ AS(♦R). This is the property that we use in
Lemma 7, but also in Lemma 16 and Lemma 17 to prove the right-to-left implication of
Lemma 9.

