11institutetext: CNRS & LMF, ENS Paris-Saclay, France 22institutetext: LIGM,
Université Gustave Eiffel

# Bounds for Synchronizing
Markov Decision Processes

Laurent Doyen 11 Marie van den Bogaard 22

###### Abstract

We consider Markov decision processes with synchronizing objectives, which
require that a probability mass of $1-\varepsilon$ accumulates in a designated
set of target states, either once, always, infinitely often, or always from
some point on, where $\varepsilon=0$ for sure synchronizing, and
$\varepsilon\to 0$ for almost-sure and limit-sure synchronizing.

We introduce two new qualitative modes of synchronizing, where the probability
mass should be either _positive_ , or _bounded_ away from $0$. They can be
viewed as dual synchronizing objectives. We present algorithms and tight
complexity results for the problem of deciding if a Markov decision process is
positive, or bounded synchronizing, and we provide explicit bounds on
$\varepsilon$ in all synchronizing modes. In particular, we show that deciding
positive and bounded synchronizing always from some point on, is coNP-
complete.

##  1 Introduction

Markov decision processes (MDP) are finite-state probabilistic systems with
controllable (non-deterministic) choices. They play a central role in several
application domains for practical purpose [15, 20], and in theoretical
computer science as a basic model for the analysis of stochastic transition
systems [2, 11].

In the traditional state-based semantics, we consider the _sequences of
states_ that form a path in the underlying graph of the MDP. When a control
policy (or strategy) for the non-deterministic choices is fixed, we obtain a
purely stochastic process that induces a probability measure over sets of
paths [2, 9].

In the more recent distribution-based semantics, the outcome of a stochastic
process is a sequence of distributions over states [3, 19]. This alternative
semantics has received some attention recently for theoretical analysis of
probabilistic bisimulation [17] and is adequate to describe large populations
of agents [14, 10] with applications in system biology [19, 1]. The behaviour
of an agent is modeled as an MDP with some state space $Q$, and a large
population of identical agents is described by a (continuous) distribution
$d:Q\to[0,1]$ that gives the fraction $d(q)$ of agents in the population that
are in each state $q\in Q$. The control problem is to construct a strategy for
the agents that guarantees a specified global outcome of the agents, defined
in terms of _sequences of distributions_. Specifications of interest include
safety objectives [1] and synchronization objectives [14]. A distribution is
$p$-synchronized in a set $T$ of states if it assigns to the states in $T$ a
mass of probability at least $p$. Synchronization objectives require that
$p$-synchronized distributions occur in the outcome sequence, either, at some
position (eventually), at all positions (always), infinitely often (weakly),
or always from some point on (strongly), where synchronization is sure winning
for $p=1$, and almost-sure or limit-sure winning for $p$ arbitrarily close to
$1$ [14].

Consider eventually synchronizing as an illustration. Formally, denoting by
$d_{i}^{\sigma}(T)$ the probability mass in a set $T$ under strategy $\sigma$
at position $i$ in a given MDP, the three winning modes for eventually
synchronizing correspond to the following three possible orders of the
quantifiers:

  * •

$\forall\varepsilon>0\cdot\exists\sigma\cdot\exists i:d_{i}^{\sigma}(T)\geq
1-\varepsilon$, for limit-sure winning,

  * •

$\exists\sigma\cdot\forall\varepsilon>0\cdot\exists i:d_{i}^{\sigma}(T)\geq
1-\varepsilon$, for almost-sure winning,

  * •

$\exists\sigma\cdot\exists i\cdot\forall\varepsilon>0:d_{i}^{\sigma}(T)\geq
1-\varepsilon$, for sure winning.

Note that the formula $\forall\varepsilon>0:d_{i}^{\sigma}(T)\geq
1-\varepsilon$ is equivalent to $d_{i}^{\sigma}(T)=1$ in the case of sure
winning. Defining the value of a strategy $\sigma$ as
$\mathrm{val}(\sigma)=\sup_{i}d_{i}^{\sigma}(T)$, the question for limit-sure
winning is analogous to the cutpoint isolation problem for value $1$, i.e.
whether the value $1$ can be approached arbitrarily closely [21, 4]. Previous
work [14] shows that the above three questions are PSPACE-complete, and
presents a construction of the (existentially quantified) strategy $\sigma$
when one exists.

$q_{0}$$q_{1}$$\frac{1}{2}$$\frac{1}{2}$ Figure 1: A Markov chain that is
positively but not boundedly synchronizing (for all modes except eventually).

In this paper, we consider dual synchronization objectives obtained either by
taking the negation of the synchronization objectives, or by replacing the
existential quantifier on strategies by a universal quantifier.

1\. Taking the negation corresponds to the control player having no strategy
to satisfy the synchronization objective. In that case, we show that a more
precise information can be derived, namely bounds on the value of
$\varepsilon$, which is existentially quantified, and we construct explicit
values for the four synchronizing modes. These values give bounds on the
isolation distance of the value $1$. For instance, the negation of limit-sure
eventually synchronizing in $T$ is given by the formula:

$\exists\varepsilon>0\cdot\forall\sigma\cdot\forall i:d^{\sigma}_{i}(T)\leq
1-\varepsilon.$

We show that the statement holds for a value
$\varepsilon=\varepsilon_{e}(n,\alpha,\alpha_{0})$ that depends on the number
$n$ of states of the MDP, the smallest positive probability $\alpha$ in the
transitions of the MDP, and the smallest positive probability $\alpha_{0}$ in
the initial distribution $d_{0}$ (see Theorem 3.1). The most interesting case
is when limit-sure weakly synchronizing does not hold, that is:

$\exists\varepsilon>0\cdot\forall\sigma\cdot\exists N\cdot\forall i\geq
N:d^{\sigma}_{i}(T)\leq 1-\varepsilon.$

Given the value $\varepsilon=\varepsilon_{w}$ that satisfies this condition
(see Theorem 4.1), the value of $N$ can be arbitrarily large (depending on the
strategy $\sigma$). Nevertheless, we can effectively construct a constant
$N_{w}$ such that, for all strategies $\sigma$, in the sequence
$(d^{\sigma}_{i})_{i\in\mathbb{N}}$ there are at most $N_{w}$ distributions
that are $(1-\varepsilon_{w})$-synchronized in $T$.

2\. Replacing the existential strategy quantifier by a universal quantifier
corresponds to an adversarial MDP where all strategies need to satisfy the
requirement, or after taking the negation, to the existence of a strategy that
violates a dual of the synchronizing requirement. Note that there is no more
alternation of quantifiers on $\varepsilon$ and on $\sigma$
($\forall\varepsilon\cdot\forall\sigma$ is the same as
$\forall\sigma\cdot\forall\varepsilon$), which gives rise to only two new
winning modes in existential form:

  * •

$\exists\sigma\cdot\exists\varepsilon>0\cdot\forall
i:d_{i}^{\sigma}(T)\geq\varepsilon$, that we call _bounded_ winning,

  * •

$\exists\sigma\cdot\forall
i\cdot\exists\varepsilon>0:d_{i}^{\sigma}(T)\geq\varepsilon$, that we call
_positive_ winning (since this is equivalent to $\exists\sigma\cdot\forall
i:d_{i}^{\sigma}(T)>0$).

Table 1:  Positive and Bounded winning modes for always, strongly, weakly, and eventually synchronizing objectives.  | Always | Strongly
---|---|---
Positively | $\exists\sigma$ | $\forall i$ |  $d^{\sigma}_{i}(T)>0$ | $\exists\sigma$ | $\exists N\>\forall i\geq N$ |  $d^{\sigma}_{i}(T)>0$
Boundedly | $\exists\sigma$ | $\inf_{i}$ |  $d^{\sigma}_{i}(T)>0$ | $\exists\sigma$ | $\liminf_{i\to\infty}$ |  $d^{\sigma}_{i}(T)>0$
| Weakly | Eventually
Positively | $\exists\sigma$ | $\forall N\>\exists i\geq N$ |  $d^{\sigma}_{i}(T)>0$ | $\exists\sigma$ | $\exists i$ |  $d^{\sigma}_{i}(T)>0$
Boundedly | $\exists\sigma$ | $\limsup_{i\to\infty}$ |  $d^{\sigma}_{i}(T)>0$ | $\exists\sigma$ | $\sup_{i}$ |  $d^{\sigma}_{i}(T)>0$

Table 1 presents the analogous definitions of bounded and positive winning for
the four synchronizing modes. It is easy to see that for eventually
synchronizing, the positive and bounded mode coincide, while for the other
synchronizing modes the positive and bounded modes are distinct, already in
Markov chains (see Figure 1).

We establish the complexity of deciding bounded and positive winning in the
four synchronizing modes, given an MDP and initial distribution (which we call
the membership problem), and we also construct explicit values for
$\varepsilon$. Adversarial MDPs are a special case of two-player stochastic
games [9] in which only the second player (the adversary of the first player)
is non-trivial. The results of this paper will be useful for the analysis of
adversarial MDPs obtained from a game by fixing a strategy of the first
player. The complexity results are summarized in Table 2. For positive
winning, memoryless winning strategies exist (playing all actions uniformly at
random is sufficient), and the problem can be solved by graph-theoretic
techniques on Markov chains. For bounded winning, the most challenging case is
strongly synchronizing, where we show that a simple form of strategy with
memory is winning, and that the decision problem is coNP-complete. We give a
structural characterization of bounded strongly synchronizing MDPs, and show
that it can be decided in coNP. Note that the coNP upper bound is not obtained
by guessing a strategy, since the coNP lower bound holds in the case of Markov
chains where strategies play no role.

#### Related works.

The distribution-based semantics of MDPs [3, 19] has received an increased
amount of attention recently, with works on safety objectives [1] and
synchronizing objectives [14] (see also references therein). Logic and
automata-based frameworks express distribution-based properties, by allowing
different order of the logical quantifiers, such as $\forall\sigma\exists i$
in standard reachability which becomes $\exists i\forall\sigma$ in
synchronized reachability [3, 18, 8]. The bounded and positive winning modes
introduced in this paper have not been considered before. They bear some
similarity with the qualitative winning modes in concurrent games [13].

Applications are found in modeling of large populations of identical agents,
such as molecules, yeast, bacteria, etc. [19, 1] where the probability
distributions represent concentrations of each agent in the system. Analogous
models have been considered in a discrete setting where the number of agents
is a parameter $n$, giving rise to control problems for parameterized systems,
asking if there exists a strategy that brings all $n$ agents synchronously to
a target state [5, 10].

Table 2: Computational complexity of the membership problem (for eventually synchronizing, the positive and bounded modes coincide). | Always | Eventually | Weakly | Strongly
---|---|---|---|---
Positively | coNP-C | NL-C | NL-C | coNP-C
Boundedly | coNP-C | NL-C | coNP-C

##  2 Definitions

A _probability distribution_ over a finite set $Q$ is a function $d:Q\to[0,1]$
such that $\sum_{q\in Q}d(q)=1$. The _support_ of $d$ is the set ${\sf
Supp}(d)=\\{q\in Q\mid d(q)>0\\}$. We denote by ${\cal D}(Q)$ the set of all
probability distributions over $Q$. Given a set $T\subseteq Q$, let
$d(T)=\sum_{s\in T}d(s)$.

A _Markov decision process_ (MDP) is a tuple ${\cal M}=\langle Q,{\sf
A},\delta\rangle$ where $Q$ is a finite set of states, ${\sf A}$ is a finite
set of labels called actions, and $\delta:Q\times{\sf A}\to{\cal D}(Q)$ is a
probabilistic transition function. A _Markov chain_ is an MDP with singleton
action set $\lvert{\sf A}\rvert=1$. Given a state $q\in Q$ and an action
$a\in{\sf A}$, the successor state of $q$ under action $a$ is $q^{\prime}$
with probability $\delta(q,a)(q^{\prime})$.

Given $X,Y\subseteq Q$, let

${\sf APre}(Y,X)=\\{q\in Q\mid\exists a\in{\sf A}:{\sf
Supp}(\delta(q,a))\subseteq Y\land{\sf Supp}(\delta(q,a))\cap
X\neq\varnothing\\},$

be the set of states from which there is an action to ensure that all
successor states are in $Y$ and that with positive probability the successor
state is in $X$, and for $X=Q$, let

${\sf Pre}(Y)={\sf APre}(Y,Q)=\\{q\in Q\mid\exists a\in{\sf A}:{\sf
Supp}(\delta(q,a))\subseteq Y\\}$

be the set of states from which there is an action to ensure (with probability
$1$) that the successor state is in $Y$. For $k>0$, let ${\sf Pre}^{k}(Y)={\sf
Pre}({\sf Pre}^{k-1}(Y))$ with ${\sf Pre}^{0}(Y)=Y$. Note that the sequence
${\sf Pre}^{k}(Y)$ of iterated predecessors is ultimately periodic, precisely
there exist $k_{1}<k_{2}\leq 2^{\lvert Q\rvert}$ such that ${\sf
Pre}^{k_{1}}(Y)={\sf Pre}^{k_{2}}(Y)$.

#### Strategies.

A (randomized) _strategy_ in ${\cal M}$ is a function $\sigma:(Q{\sf
A})^{*}Q\to{\cal D}({\sf A})$ that, given a finite sequence
$\rho=q_{0}a_{0}q_{1}a_{1}\dots q_{k}$, chooses the next action $a_{k}$ with
probability $\sigma(\rho)(a_{k})$. We write $\sigma_{1}\subseteq\sigma_{2}$ if
${\sf Supp}(\sigma_{1}(\rho))\subseteq{\sf Supp}(\sigma_{2}(\rho))$ for all
$\rho\in(Q{\sf A})^{*}Q$. A strategy $\sigma$ is _pure_ if for all
$\rho\in(Q{\sf A})^{*}Q$, there exists an action $a\in{\sf A}$ such that
$\sigma(\rho)(a)=1$. In all problems considered in this paper, it is known
that pure strategies are sufficient [14]. However, the bounds we provide in
case there is no winning strategy hold for all strategies, pure or randomized.

Given an initial distribution $d_{0}\in{\cal D}(Q)$ and a strategy $\sigma$ in
${\cal M}$, the probability of a finite sequence
$\rho=q_{0}a_{0}q_{1}a_{1}\dots q_{k}$ is defined by
$\Pr^{\sigma}_{d_{0}}(\rho)=d_{0}(q_{0})\cdot\prod_{j=0}^{k-1}\sigma(q_{0}a_{0}\dots
q_{j})(a_{j})\cdot\delta(q_{j},a_{j})(q_{j+1}).$ For an initial distribution
$d_{0}$ such that $d_{0}(q_{0})=1$, we sometimes write
$\Pr^{\sigma}_{q_{0}}(\cdot)$ and say that $q_{0}$ is the initial state. We
say that $\rho$ is _compatible_ with $\sigma$ and $d_{0}$ if
$\Pr^{\sigma}_{d_{0}}(\rho)>0$. By extension, an infinite sequence
$\pi\in(Q{\sf A})^{\omega}$ is compatible with $\sigma$ and $d_{0}$ if all
prefixes of $\pi$ that end in a state are compatible. It is standard to extend
(in a unique way) $\Pr^{\sigma}_{d_{0}}$ over Borel sets of infinite paths in
$(Q{\sf A})^{\omega}$ (called events), by assigning probability
$\Pr^{\sigma}_{d_{0}}(\rho)$ to the basic cylinder set containing all infinite
paths with prefix $\rho$ [23, 2]. Given a set $T\subseteq Q$ of target states,
and $k\in\mathbb{N}$, we define the following events (sometimes called
objectives):

  * •

$\Box T=\\{q_{0}a_{0}q_{1}\dots\in(Q{\sf A})^{\omega}\mid\forall i:q_{i}\in
T\\}$ the safety event of staying in $T$;

  * •

$\Diamond T=\\{q_{0}a_{0}q_{1}\dots\in(Q{\sf A})^{\omega}\mid\exists
i:q_{i}\in T\\}$ the event of reaching $T$;

  * •

$\Diamond^{k}\,T=\\{q_{0}a_{0}q_{1}\dots\in(Q{\sf A})^{\omega}\mid q_{k}\in
T\\}$ the event of reaching $T$ after exactly $k$ steps;

A distribution $d_{0}$ is _almost-sure winning_ for an event $\Omega$ if there
exists a strategy $\sigma$ such that $\Pr^{\sigma}_{d_{0}}(\Omega)=1$, and
_limit-sure winning_ if $\sup_{\sigma}\Pr^{\sigma}_{d_{0}}(\Omega)=1$, that is
the event $\Omega$ can be realized with probability arbitrarily close to $1$.
Finally $d_{0}$ is _sure winning_ for $\Omega$ if there exists a strategy
$\sigma$ such that all paths compatible with $\sigma$ and $d_{0}$ belong to
$\Omega$.

Safety and reachability events are dual, in the sense that $\Diamond T$ and
$\Box(Q\setminus T)$ form a partition of $(Q{\sf A})^{\omega}$. It is known
for safety objectives $\Box T$ that the three winning regions (sure, almost-
sure winning, and limit-sure winning) coincide in MDPs, and for reachability
objectives $\Diamond T$, almost-sure and limit-sure winning coincide [12]. It
follows that if the negation of almost-sure reachability holds, that is
$\Pr^{\sigma}_{d_{0}}(\Diamond T)<1$ for all strategies $\sigma$, then
equivalently $\inf_{\sigma}\Pr^{\sigma}_{d_{0}}(\Box(Q\setminus T))>0$ (note
the strict inequality), the probability mass that remains always outside $T$
can be bounded. An explicit bound can be obtained from the classical
characterization of the winning region for almost-sure reachability [11].

###### Lemma 1

If a distribution $d_{0}$ is not almost-sure winning for a reachability
objective $\Diamond T$ in an MDP ${\cal M}$, then for all strategies $\sigma$,
for all $i\geq 0$, we have $Pr^{\sigma}_{d_{0}}(\Diamond^{i}\,T)\leq
1-\alpha_{0}\cdot\alpha^{n}$ where $n=\lvert Q\rvert$ is the number of states
and $\alpha$ the smallest positive probability in ${\cal M}$, and
$\alpha_{0}=\min\\{d_{0}(q)\mid q\in{\sf Supp}(d_{0})\\}$ is the smallest
positive probability in the initial distribution $d_{0}$.

###### Proof

The set of almost-sure winning states for the reachability objective $\Diamond
T$ can be computed by graph-theoretic algorithms [11], and can be expressed
succinctly by the fixpoint $\mu$-calculus formula $\varphi_{{\sf AS}}=\nu
Y.\mu X.~{}\\!T\cup{\sf APre}(Y,X)$. We briefly recall the interpretation of
$\mu$-calculus formulas [6, 7] based on Knaster-Tarski theorem. Given a
monotonic function $\psi:2^{Q}\to 2^{Q}$ (i.e., such that $X\subseteq Y$
implies $\psi(X)\subseteq\psi(Y)$), the expression $\nu Y.\psi(Y)$ is the
(unique) greatest fixpoint of $\psi$, which can be computed as the limit of
the sequence $(Y_{i})_{i\in\mathbb{N}}$ defined by $Y_{0}=Q$, and
$Y_{i}=\psi(Y_{i-1})$ for all $i\geq 1$. Dually, the expression $\mu
X.~{}\psi(X)$ is the (unique) least fixpoint of $\psi$, and the limit of the
sequence $(X_{i})_{i\in\mathbb{N}}$ defined by $X_{0}=\varnothing$, and
$X_{i}=\psi(X_{i-1})$ for all $i\geq 1$. If $\lvert Q\rvert=n$, then it is not
difficult to see that the limit of those sequences is reached after at most
$n$ iterations, $X_{n}=X_{n+1}$ and $Y_{n}=Y_{n+1}$.

Intuitively, the formula $\varphi_{{\sf AS}}$ computes the largest set $S$ of
states such that every state $q\in S$ has a strategy to ensure reaching $T$
with positive probability, while at the same time staying in $S$ with
probability $1$. It follows that $S$ is the set of all states from which there
exists a strategy to reach $T$ with probability $1$.

Now consider the states $q_{0}\not\in\varphi_{{\sf AS}}$ that are not almost-
sure winning, and let the rank of $q_{0}$ be the least integer $i$ such that
$q_{0}\in Y_{i}$ and $q_{0}\not\in Y_{i+1}$. Let $\Omega_{i}=Y_{i}\setminus
Y_{i+1}$ for all $i\geq 0$ be the set of states of rank $i$, and for
$\mbox{$\sim$}\\!\in\\!\\{<,\leq\\}$ let $\Omega_{\sim i}=\bigcup_{j\sim
i}\Omega_{j}$. It is easy to show by induction that $Q\setminus
Y_{i}=\Omega_{<i}$ since $\Omega_{<i}=(Y_{0}\setminus
Y_{1})\cup(Y_{1}\setminus Y_{2})\cup\dots\cup(Y_{i-1}\setminus Y_{i})$ and
$Y_{0}=Q$. Moreover since $T\subseteq Y_{i}$ we have $\Omega_{i}\cap
T=\varnothing$.

For $q_{0}\in\Omega_{i}$, we show that
$\Pr^{\sigma}_{q_{0}}(\Box\Omega_{i}\cup\Diamond\Omega_{<i})\geq\alpha$ for
all strategies $\sigma$ (where $\alpha$ is the smallest positive probability
in the transitions of the MDP). Since $q_{0}\not\in Y_{i+1}=\mu X.~{}T\cup{\sf
APre}(Y_{i},X)$, we have $q_{0}\not\in{\sf APre}(Y_{i},Y_{i+1})$. Then for all
actions $a\in{\sf A}$ we have:

$\text{either }{\sf Supp}(\delta(q_{0},a))\not\subseteq Y_{i},\text{ or }{\sf
Supp}(\delta(q_{0},a))\cap Y_{i+1}=\varnothing,$

that is

$\text{either }{\sf
Supp}(\delta(q_{0},a))\cap\Omega_{<i}\neq\varnothing,\text{ or }{\sf
Supp}(\delta(q_{0},a))\subseteq\Omega_{\leq i}.$

It follows in both cases that if not all successors of $q_{0}$ on action $a$
are in $\Omega_{i}$, then at least one of them is in $\Omega_{<i}$, which
entails that
$\Pr^{\sigma}_{q_{0}}(\Box\Omega_{i}\cup\Diamond\Omega_{<i})\geq\alpha$. For
$i=0$, since $\Omega_{<0}=\varnothing$, we have
$\Pr^{\sigma}_{q_{0}}(\Box\Omega_{0})=1$ and thus
$\Pr^{\sigma}_{q_{0}}(\Box(Q\setminus T))=1$ for all $q_{0}\in\Omega_{0}$ and
all strategies $\sigma$. Inductively, if $\Pr^{\sigma}_{q_{0}}(\Box(Q\setminus
T))\geq p_{i}$ for all $q_{0}\in\Omega_{<i}$ and all strategies $\sigma$, then
$\Pr^{\sigma}_{q_{0}}(\Box(Q\setminus T))\geq\alpha\cdot p_{i}$ for all
$q_{0}\in\Omega_{i}$ and all strategies $\sigma$.

It follows that if $q_{0}\not\in\varphi_{{\sf AS}}$ is not almost-sure winning
for the reachability objective $\Diamond T$, then $q_{0}\in\Omega_{<n}$ and
$\Pr^{\sigma}_{q_{0}}(\Box(Q\setminus T))\geq\alpha^{n}$ for all strategies
$\sigma$, which entails the result of the lemma. ∎

In Lemma 1 it is crucial to notice that the bound $\alpha_{0}\cdot\alpha^{n}$
is independent of the number $i$ of steps.

#### Synchronizing objectives.

We consider MDPs as generators of sequences of probability distributions over
states [19]. Given an initial distribution $d_{0}\in{\cal D}(Q)$ and a
strategy $\sigma$ in ${\cal M}$, the sequence ${\cal M}^{\sigma}=({\cal
M}^{\sigma}_{i})_{i\in\mathbb{N}}$ of probability distributions (from $d_{0}$,
which we assume is clear from the context) is defined by ${\cal
M}^{\sigma}_{i}(q)=Pr^{\sigma}_{d_{0}}(\Diamond^{i}\,\\{q\\})$ for all $i\geq
0$ and $q\in Q$. Hence, ${\cal M}^{\sigma}_{i}$ is the probability
distribution over states after $i$ steps under strategy $\sigma$. Note that
${\cal M}^{\sigma}_{0}=d_{0}$.

Informally, synchronizing objectives require that the probability of some set
$T$ of states tends to $1$ in the sequence $({\cal
M}^{\sigma}_{i})_{i\in\mathbb{N}}$, either always, once, infinitely often, or
always after some point [14]. Given a target set $T\subseteq Q$, we say that a
probability distribution $d$ is _$p$ -synchronized_ in $T$ if $d(T)\geq p$
(and strictly $p$-synchronized in $T$ if $d(T)>p$), and that a sequence
$d_{0}d_{1}\dots$ of probability distributions is:

  * $(a)$

_always $p$-synchronizing_ if $d_{i}$ is $p$-synchronized (in $T$) for all
$i\geq 0$;

  * $(b)$

_event(ually) $p$-synchronizing_ if $d_{i}$ is $p$-synchronized (in $T$) for
some $i\geq 0$;

  * $(c)$

_weakly $p$-synchronizing_ if $d_{i}$ is $p$-synchronized (in $T$) for
infinitely many $i$’s;

  * $(d)$

_strongly $p$-synchronizing_ if $d_{i}$ is $p$-synchronized (in $T$) for all
but finitely many $i$’s.

Given an initial distribution $d_{0}$, we say that for the objective of
{always, eventually, weakly, strongly} synchronizing from $d_{0}$, the MDP
${\cal M}$ is:

  * •

_sure winning_ if there exists a strategy $\sigma$ such that the sequence
${\cal M}^{\sigma}$ from $d_{0}$ is {always, eventually, weakly, strongly}
$1$-synchronizing in $T$;

  * •

_almost-sure winning_ if there exists a strategy $\sigma$ such that for all
$\varepsilon>0$ the sequence ${\cal M}^{\sigma}$ from $d_{0}$ is {always,
eventually, weakly, strongly} $(1-\varepsilon)$-synchronizing in $T$;

  * •

_limit-sure winning_ if for all $\varepsilon>0$, there exists a strategy
$\sigma$ such that the sequence ${\cal M}^{\sigma}$ from $d_{0}$ is {always,
eventually, weakly, strongly} $(1-\varepsilon)$-synchronizing in $T$;

For $\lambda\in\\{always,event,weakly,strongly\\}$, we denote by
$\langle\\!\langle 1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{\lambda}}(T)$
the _winning region_ defined as the set of initial distributions $d_{0}$ such
that ${\cal M}$ is sure winning for $\lambda$-synchronizing in $T$ (in this
notation, we assume that ${\cal M}$ is clear from the context). We define
analogously the winning regions $\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{\lambda}}(T)$ and
$\langle\\!\langle 1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{\lambda}}(T)$
of almost-sure and limit-sure winning distributions.

It is known that for all winning modes, only the support of the initial
distributions is relevant, that is for every winning region
$W=\langle\\!\langle 1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{\lambda}}(T)$
(where $\mu\in\\{sure,almost,limit\\}$), for all distributions $d,d^{\prime}$,
if ${\sf Supp}(d)={\sf Supp}(d^{\prime})$, then $d\in W$ if and only if
$d^{\prime}\in W$ [14]. Therefore, in the sequel we sometimes write
$S\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{\lambda}}(T)$, which can be read as
any distribution $d$ with support $S$ is in $\langle\\!\langle
1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{\lambda}}(T)$. For each
synchronizing mode $\lambda$ and winning mode $\mu$, the membership problem
asks to decide, given an MDP ${\cal M}$, a target set $T$, and a set $S$,
whether $S\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{\lambda}}(T)$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\frac{1}{2}$$\frac{1}{2}$$b$$a$$a,b$$a,b$ Figure
2: An MDP where $\\{q_{0}\\}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(\\{q_{2}\\}).$

Consider the MDP in Figure 2, with initial state $q_{0}$ and target set
$T=\\{q_{2}\\}$. The probability mass cannot loop through $q_{2}$ and
therefore, it is immediate that the MDP is neither always, nor weakly, nor
strongly $(1-\varepsilon)$-synchronizing, thus
$\\{q_{0}\\}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{\lambda}}(T)$ for
$\lambda=always,weakly,strongly$, and thus also
$\\{q_{0}\\}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{\lambda}}(T)$.

For eventually synchronizing in $q_{2}$, at every step, half of the
probability mass in $q_{0}$ stays in $q_{0}$ while the other half is sent to
$q_{1}$. Thus, the probability mass in $q_{0}$ tends to $0$ but is strictly
positive at every step, and the MDP is not sure eventually synchronizing,
$\\{q_{0}\\}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T)$. In state $q_{1}$,
action $a$ keeps the probability mass in $q_{1}$, while action $b$ sends it to
the target state $q_{2}$. If action $b$ is never chosen, then $q_{2}$ is never
reached, and whenever $b$ is chosen, a strictly positive probability mass
remains in $q_{0}$, thus the MDP is not almost-sure eventually synchronizing,
$\\{q_{0}\\}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{event}}(T)$. On the other hand,
for every $\varepsilon>0$, the strategy that plays $a$ in $q_{1}$ for $k$
steps such that $\frac{1}{2^{k}}<\varepsilon$, and then plays $b$, is winning
for eventually $(1-\varepsilon)$-synchronizing in $T$. Thus the MDP is limit-
sure eventually synchronizing, $\\{q_{0}\\}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T)$.

The MDP in Figure 3 is also limit-sure eventually synchronizing in
$\\{q_{2}\\}$. As the probability mass is sent back to $q_{0}$ from $q_{2}$,
the MDP is even almost-sure weakly (and eventually) synchronizing, using a
strategy that plays action $a$ in $q_{1}$ for $k$ steps to accumulate
probability mass $1-\frac{1}{2^{k}}$ in $q_{1}$, then plays action $b$ and
repeats the same pattern for increasing values of $k$.

$q_{0}$$q_{1}$$q_{2}$$\frac{1}{2}$$\frac{1}{2}$$b$$a$$a,b$ Figure 3: An MDP
where $\\{q_{0}\\}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{weakly}}(\\{q_{2}\\}).$

#### End-components.

Given a state $q\in Q$ and a set $S\subseteq Q$, let ${\sf A}_{S}(q)$ be the
set of all actions $a\in{\sf A}$ such that ${\sf Supp}(\delta(q,a))\subseteq
S$. A _closed_ set in an MDP is a set $S\subseteq Q$ such that ${\sf
A}_{S}(q)\neq\varnothing$ for all $q\in S$. A set $S\subseteq Q$ is an end-
component [12, 2] if (i) $S$ is closed, and (ii) the graph $(S,E_{S})$ is
strongly connected where $E_{S}=\\{(q,q^{\prime})\in S\times
S\mid\delta(q,a)(q^{\prime})>0\text{ for some }a\in{\sf A}_{S}(q)\\}$ denote
the set of edges given the actions. In the sequel, end-components should be
considered _maximal_ , that is such that no strict superset is an end-
component. We denote by ${\cal E}$ the union of all end-components, and for
$q\in{\cal E}$, we denote by ${\cal E}(q)$ the maximal end-component
containing $q$. A fundamental property of end-components is that under
arbitrary strategies, with probability $1$ the set of states visited
infinitely often along a path is an end-component.

######  Lemma 2 ([11, 12])

Let ${\cal M}$ be an MDP. For all strategies $\sigma$, we have
$\liminf_{i\to\infty}{\cal M}^{\sigma}_{i}({\cal E})=1$.

#### Tracking counter in MDPs.

It will be useful to track the number of steps (modulo a given number $r$) in
MDPs. Given a number $r\in\mathbb{N}$, define the MDP ${\cal
M}\times[r]=\langle Q_{r},{\sf A},\delta_{r}\rangle$ where
$Q_{r}=Q\times\\{r-1,\dots,1,0\\}$ and $\delta_{r}$ is defined as follows, for
all $\langle q,i\rangle,\langle q^{\prime},j\rangle\in Q_{r}$ and $a\in{\sf
A}$:

$\delta_{r}(\langle q,i\rangle,a)(\langle
q^{\prime},j\rangle)=\begin{cases}\delta(q,a)(q^{\prime})&\text{ if
}j=i-1\\!\\!\mod r,\\\ 0&\text{ otherwise.}\end{cases}$

For a distribution $d\in{\cal D}(Q)$ and $0\leq t<r$, we denote by
$d\times\\{t\\}$ the distribution defined, for all $q\in Q$, by
$d\times\\{t\\}(\langle q,i\rangle)=d(q)$ if $t=i$, and
$d\times\\{t\\}(\langle q,i\rangle)=0$ otherwise. Given a finite sequence
$\rho=q_{0}a_{0}q_{1}a_{1}\dots q_{n}$ in ${\cal M}$, and $0\leq t<r$, there
is a corresponding sequence $\rho^{\prime}=\langle q_{0},k_{0}\rangle
a_{0}\langle q_{1},k_{1}\rangle a_{1}\dots\langle q_{n},k_{n}\rangle$ in
${\cal M}\times[r]$ where $k_{0}=t$ and $k_{i+1}=k_{i}-1\mod r$ for all $0\leq
i<n$. Since the sequence $\rho^{\prime}$ is uniquely defined from $\rho$ and
$t$, there is a clear bijection between the paths in ${\cal M}$ starting in
$q_{0}$ and the paths in ${\cal M}\times[r]$ starting in $\langle
q_{0},t\rangle$. In the sequel, we freely omit to apply and mention this
bijection. In particular, we often consider that a strategy $\sigma$ in ${\cal
M}$ can be played directly in ${\cal M}\times[r]$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$\frac{1}{2}$$\frac{1}{2}$ Figure 4: A
Markov chain with two periodic end-components.

Consider the MDP in Figure 4 (which is in fact a Markov chain), with initial
state $q_{0}$ and target set $T=\\{q_{2},q_{3}\\}$. There are two end-
components, $S_{1}=\\{q_{1},q_{2}\\}$ and $S_{2}=\\{q_{3},q_{4}\\}$. Although
both $S_{1}$ and $S_{2}$ are sure eventually synchronizing in $T$ (from
$q_{1}$ and $q_{3}$ respectively), the uniform distribution over
$\\{q_{1},q_{3}\\}$ is not even limit-sure eventually synchronizing in $T$.

##  3 Eventually synchronizing

In the rest of this paper, fix an MDP ${\cal M}=\langle Q,{\sf
A},\delta\rangle$ and let $n=\lvert Q\rvert$ be the size of ${\cal M}$, and
let $\alpha$ be the smallest positive probability in the transitions of ${\cal
M}$. We first consider eventually synchronizing, that is synchronization must
happen once.

###  3.1 Sure winning

We recall the following characterization of the sure-winning region for
eventually synchronizing [14, Lemma 7]: $d\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T)$ if and only if there
exists $k\geq 0$ such that ${\sf Supp}(d)\subseteq{\sf Pre}^{k}(T)$.
Intuitively, from all states in ${\sf Pre}^{i}(T)$, there exists an action to
ensure that the successor is in ${\sf Pre}^{i-1}(T)$ (for all $i>0$), and
therefore there exists a strategy to ensure that the probability mass in ${\sf
Pre}^{k}(T)$ reaches $T$ in exactly $k$ steps. Now, if $q_{0}\not\in{\sf
Pre}^{k}(T)$, then for all sequences of actions $a_{0},\dots,a_{k-1}$ there is
a path $q_{0}a_{0}q_{1}a_{1}\dots q_{k}$ of length $k$ that ends in $q_{k}\in
Q\setminus T$. It is easy to derive the following result from this
characterization.

###### Lemma 3

If $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T)$ is not sure eventually
synchronizing in $T$, then for all strategies $\sigma$, for all $i\geq 0$, we
have:

${\cal M}^{\sigma}_{i}(T)\leq 1-\alpha_{0}\cdot\alpha^{i}$

where $\alpha_{0}$ is the smallest positive probability in $d_{0}$.

Note that the bound $1-\alpha_{0}\cdot\alpha^{i}$ tends to $1$ as
$i\to\infty$, which is unavoidable since MDPs that are not sure eventually
synchronizing may be almost-sure eventually synchronizing [14]. The following
variant of Lemma 3 will be useful in the sequel.

###### Remark 1

If $\\{q_{0}\\}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T)$ and we take
$\alpha^{\prime}_{0}=d_{0}(q_{0})$, then from the initial distribution $d_{0}$
we have, for all strategies $\sigma$, for all $i\geq 0$:

${\cal M}^{\sigma}_{i}(T)\leq 1-\alpha^{\prime}_{0}\cdot\alpha^{i}.$

###  3.2 Limit-sure winning

If the MDP ${\cal M}$ is not limit-sure winning for eventually synchronizing
in $T$, then the probability in $Q\setminus T$ is bounded away from $0$ in all
distributions in ${\cal M}^{\sigma}$ (for all strategies $\sigma$). We give an
explicit bound $\varepsilon_{e}$ as follows.

###### Theorem 3.1

Given an initial distribution $d_{0}$, let $\alpha_{0}$ be the smallest
positive probability in $d_{0}$, and let
$\varepsilon_{e}=\alpha_{0}\cdot\alpha^{(n+1)\cdot 2^{n}}$. If
$d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T)$ is not limit-sure
eventually synchronizing in $T$, then for all strategies $\sigma$, for all
$i\geq 0$, we have:

${\cal M}^{\sigma}_{i}(T)\leq 1-\varepsilon_{e},$

that is, no distribution in ${\cal M}^{\sigma}$ is strictly
$(1-\varepsilon_{e})$-synchronizing in $T$.

###### Proof

We recall the characterization111The results of [14, Lemma 11 & 12] consider a
more general definition of limit-sure synchronizing, where the support of the
$(1-\varepsilon)$-synchronizing distribution is required to have its support
contained in a given set $Z$. We release this constraint by taking $Z=Q$. of
[14, Lemma 11] for limit-sure synchronizing in an arbitrary set $T$. For all
$k\geq 0$, we have

$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T)\cup\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(R),$

where $R={\sf Pre}^{k}(T)$.

We use this characterization with a specific $k$ (and $R$) as follows.
Consider the sequence of predecessors ${\sf Pre}^{i}(T)$ (for $i=1,2,\dots$),
which is ultimately periodic. Let $0\leq k<2^{n}$ and $1\leq r<2^{n}$ be such
that ${\sf Pre}^{k}(T)={\sf Pre}^{k+r}(T)$, and let $R={\sf Pre}^{k}(T)$. Thus
$R={\sf Pre}^{k+r}(T)={\sf Pre}^{r}(R)$.

Since $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T)$, we have:

$(a)~{}d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T),\ \text{ and }\
(b)~{}d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(R).$

By $(a)$, it follows from Lemma 3 that ${\cal M}^{\sigma}_{i}(T)\leq
1-\alpha_{0}\cdot\alpha^{i}$ for all strategies $\sigma$ and all $i\geq 0$,
which establishes the bound in the lemma for the first $2^{n}$ steps, since
$\alpha_{0}\cdot\alpha^{i}\geq\varepsilon_{e}$ for all $i\leq 2^{n}$.

We now recall the characterization11footnotemark: 1 of [14, Lemma 12] for
limit-sure synchronizing in the set $R$, which has the property that $R={\sf
Pre}^{r}(R)$: $d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(R)$ if and only if there
exists $0\leq t<r$ such that $d_{0}\times\\{t\\}$ is almost-sure winning for
the reachability objective $\Diamond(R\times\\{0\\})$ in the MDP ${\cal
M}\times[r]$. By $(b)$, it follows that for all $0\leq t<r$, the distribution
$d_{0}\times\\{t\\}$ is _not_ almost-sure winning for the reachability
objective $\Diamond(R\times\\{0\\})$ in the MDP ${\cal M}\times[r]$.

Let ${\cal N}={\cal M}\times[r]$. By Lemma 1, from all distributions
$d_{0}\times\\{t\\}$ (for all $0\leq t<r$), for all strategies $\sigma$ and
all $i\geq 0$, we have:

${\cal N}^{\sigma}_{i}(R\times\\{0\\})\leq 1-\alpha_{0}\cdot\alpha^{\lvert
Q_{r}\rvert}=1-\alpha_{0}\cdot\alpha^{n\cdot 2^{n}}.$

Since this holds for all $t=0,\dots,r-1$, we conclude that ${\cal
M}^{\sigma}_{i}(Q\setminus R)\geq\alpha_{0}\cdot\alpha^{n\cdot 2^{n}}$ in the
original MDP ${\cal M}$ from $d_{0}$, for all strategies $\sigma$ and all
$i\geq 0$.

Since $R={\sf Pre}^{k}(T)$, it follows from Lemma 3 and Remark 1 that, if at
step $i$ a mass of probability $p$ is outside $R$, then at step $i+k$ a mass
of probability at least $p\cdot\alpha^{k}$ is outside $T$. Hence we have
${\cal M}^{\sigma}_{i+k}(Q\setminus T)\geq\alpha_{0}\cdot\alpha^{n\cdot
2^{n}}\cdot\alpha^{k}\geq\alpha_{0}\cdot\alpha^{(n+1)\cdot 2^{n}}$ for all
strategies $\sigma$ and for all $i\geq 0$, which implies ${\cal
M}^{\sigma}_{i}(Q\setminus T)\geq\alpha_{0}\cdot\alpha^{(n+1)\cdot 2^{n}}$ for
all $i\geq 2^{n}$ (since $k<2^{n}$).

Combining the results for $i\leq 2^{n}$ and for $i\geq 2^{n}$, we get ${\cal
M}^{\sigma}_{i}(T)\leq 1-\varepsilon_{e}$ for all $i\geq 0$, which concludes
the proof. ∎

Theorem 3.1 also gives a sufficient condition that can be used as an
alternative to [14, Lemma 11] to show that an MDP is limit-sure eventually
synchronizing. This will be useful in the proof of our main result (Theorem
4.1).

A variant of Theorem 3.1 is obtained by observing that if
$d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T)$, there exists a set
$S_{0}\subseteq{\sf Supp}(d_{0})$ such that $S_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T)$. It may be that
$S_{0}$ is a strict subset of ${\sf Supp}(d_{0})$, and then it is sufficient
to consider $\alpha_{0}$ as the smallest positive probability of $d_{0}$ on
$S_{0}$.

###### Remark 2

If $S_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T)$ and
$S_{0}\subseteq{\sf Supp}(d_{0})$, then we can define $\alpha_{0}$ by
$\min\\{d_{0}(q)\mid q\in S_{0}\\}$ in the bound $\varepsilon_{e}$ of Theorem
3.1.

###  3.3 Almost-sure winning

A simple argument shows that the almost-sure winning region for eventually
synchronizing consists of the union of the sure winning region for eventually
synchronizing and the almost-sure winning region for weakly synchronizing [22,
Section 5.1.2], that is $\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{event}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T)\cup\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{weakly}}(T)$.

It follows that if $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{event}}(T)$, then both
$d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{event}}(T)$ and
$d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{weakly}}(T)$, and we can use
both the results of Lemma 3 and Theorem 4.1.

##  4 Weakly synchronizing

We now consider weakly synchronizing, which intuitively requires that
synchronization happens infinitely often.

###  4.1 Sure winning

We recall the following characterization of the sure-winning region for weakly
synchronizing [14, Lemma 18]: for all distributions $d_{0}\in{\cal D}(Q)$, we
have $d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{weakly}}(T)$ if and only if there
exists a set $S\subseteq T$ such that ${\sf Supp}(d)\subseteq{\sf Pre}^{k}(S)$
for some $k\geq 0$, and $S\subseteq{\sf Pre}^{r}(S)$ for some $r\geq 1$.

###### Lemma 4

If $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{weakly}}(T)$ is not sure weakly
synchronizing in $T$, then for all strategies $\sigma$, in the sequence ${\cal
M}^{\sigma}$ there are at most $2^{n}$ distributions that are $1$-synchronized
in $T$, that is ${\cal M}^{\sigma}_{i}(T)=1$ for at most $2^{n}$ values of
$i$.

###### Proof

Consider the support $S_{j}={\sf Supp}({\cal M}^{\sigma}_{i_{j}})$ (where
$i_{1}<i_{2}<\dots$) of the distributions in the sequence ${\cal M}^{\sigma}$
that are $1$-synchronized in $T$. We show by contradiction, that all $S_{j}$
are distinct, which establishes the result since they can take at most $2^{n}$
different values.

If $S_{j}=S_{k}$ for some $j<k$, then it is easy to show that ${\cal M}$ is
sure-winning for eventually synchronizing in $S=S_{j}$ from $d_{0}$, and
${\cal M}$ is also sure-winning for eventually synchronizing in $S=S_{k}$ from
$S=S_{j}$, which implies by the characterization of the sure-winning region
for eventually synchronizing (Section 3.1) that ${\sf Supp}(d)\subseteq{\sf
Pre}^{i_{j}}(S)$ and $S\subseteq{\sf Pre}^{i_{k}-i_{j}}(S)$, thus
$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{weakly}}(T)$, which contradicts
the assumption of the lemma. ∎

###  4.2 Limit-sure and almost-sure winning

The winning region for limit-sure and almost-sure weakly synchronizing
coincide [14, Theorem 7]. Therefore, in the sequel we treat them
interchangeably. We recall the following characterization of almost-sure
weakly synchronizing.

######  Lemma 5 ([14, Lemma 23,Theorem 7])

For all distributions $d_{0}$, the following equivalence holds:
$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{weakly}}(T)$ if and only if
there exists a set $T^{\prime}\subseteq T$ such that:

$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T^{\prime})\ \text{ and
}\ T^{\prime}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}({\sf Pre}(T^{\prime})).$

The condition in Lemma 5 ensures that from $d_{0}$ almost all the probability
mass (namely $1-\varepsilon$ for arbitrarily small $\varepsilon>0$) can be
injected in a set $T^{\prime}$ of target states in $0$ or more steps, and that
from $T^{\prime}$ almost all the probability mass can be injected in ${\sf
Pre}(T^{\prime})$, thus also in $T^{\prime}$ (but, in at least $1$ step).
Intuitively, by successively halving the value of $\varepsilon$ one can
construct a strategy that ensures almost all the probability mass loops
through $T^{\prime}$, thus a limit-sure weakly synchronizing strategy (which
is equivalent to the existence of an almost-sure weakly synchronizing
strategy).

If $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{weakly}}(T)$ is not almost-sure
weakly synchronizing, we use Lemma 5 to show that for all sets
$T^{\prime}\subseteq T$, if $d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T^{\prime})$ is limit-
sure eventually synchronizing in $T^{\prime}$, then $T^{\prime}$ is not limit-
sure eventually synchronizing in ${\sf Pre}(T^{\prime})$ (i.e.,
$T^{\prime}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}({\sf Pre}(T^{\prime}))$).
This implies that a bounded number of distributions in the sequence ${\cal
M}^{\sigma}$ can be $(1-\varepsilon)$-synchronized in $T$ (for sufficiently
small $\varepsilon$). We now state the main result of this section.

###### Theorem 4.1

Given an initial distribution $d_{0}$, let $\alpha_{0}$ be the smallest
positive probability in $d_{0}$, and let
$\varepsilon_{w}=\alpha_{0}\cdot\frac{\alpha^{(n+2)\cdot
4^{n}}}{{n}^{2^{n}+1}}$ and $N_{w}=2^{n}$.

If $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{weakly}}(T)$ is not almost-sure
weakly synchronizing in $T$, then for all strategies $\sigma$, in the sequence
${\cal M}^{\sigma}$ at most $N_{w}$ distributions are strictly
$(1-\varepsilon_{w})$-synchronized in $T$, that is ${\cal
M}^{\sigma}_{i}(T)>1-\varepsilon_{w}$ for at most $N_{w}$ values of $i$.

###### Proof

Given the assumption of the lemma, we show the following statement by
induction on $k=0,1,\dots,2^{n}$: if there are $k$ distributions in ${\cal
M}^{\sigma}$ that are strictly $(1-\varepsilon_{w})$-synchronized in $T$, then
there exist $k$ _distinct_ nonempty sets $T_{1},\dots,T_{k}\subseteq T$ such
that no distribution after those $k$ distributions in ${\cal M}^{\sigma}$ is
strictly $(1-\varepsilon_{w})$-synchronized in $T_{j}$ (for all $1\leq j\leq
k$).

For $k=2^{n}$, one of the sets $T_{j}$ is equal to $T$ and it follows that at
most $2^{n}$ distributions in ${\cal M}^{\sigma}$ can be
$(1-\varepsilon_{w})$-synchronized in $T$, which concludes the base case. For
the proof by induction, we use the bound $\varepsilon_{e}$ of Theorem 3.1. Let
$F=(n+1)\cdot 2^{n}$ (thus $\varepsilon_{e}=\alpha_{0}\cdot\alpha^{F}$) and
for $k=0,1,\dots$ define
$z_{k}=\frac{\alpha_{0}}{n}\cdot\left(\frac{\alpha^{F+1}}{n}\right)^{k}$. We
prove a slightly stronger statement: for $k=0,1,\dots,2^{n}$, if there are $k$
positions $i_{1}<i_{2}<\ldots<i_{k}$ such that the distributions ${\cal
M}^{\sigma}_{i_{j}}$ ($j=1,\dots,k$) are strictly
$(1-\varepsilon_{w})$-synchronized in $T$, then there exist $k$ distinct
nonempty sets $T_{1},\dots,T_{k}\subseteq T$ such that no distribution after
position $i_{j}$ in ${\cal M}^{\sigma}$ is strictly
$(1-z_{j}\cdot\alpha^{F+1})$-synchronized in $T_{j}$ (for all $1\leq j\leq
k$).

This statement is indeed stronger since the sequence $z_{k}$ is decreasing,
and $\varepsilon_{w}$ was chosen such that $\varepsilon_{w}\leq z_{2^{n}}$,
from which it follows that $1-\varepsilon_{w}\geq 1-z_{k}$ for all $k\leq
2^{n}$.

The base case for $k=0$ holds trivially. For the induction case, assume that
the statement holds for a given $k<2^{n}$, and show that it holds for $k+1$ as
follows. If there are $k+1$ positions $i_{1}<i_{2}<\ldots<i_{k+1}$ such that
all distributions $d_{j}={\cal M}^{\sigma}_{i_{j}}$ ($j=1,\dots,k+1$) are
strictly $(1-\varepsilon_{w})$-synchronized in $T$, then by the induction
hypothesis, no distribution after position $i_{j}$ in ${\cal M}^{\sigma}$ is
strictly $(1-z_{j}\cdot\alpha^{F+1})$-synchronized in $T_{j}$ (for all $1\leq
j\leq k$).

Now consider the distribution $d_{k+1}$ at position $i_{k+1}$, which is
$(1-\varepsilon_{w})$-synchronized in $T$ and appears after position $i_{k}$
in ${\cal M}^{\sigma}$. We construct the set $T_{k+1}=\\{q\in T\cap{\sf
Supp}(d_{k+1})\mid d_{k+1}(q)>z_{k+1}\\}$, which contains the states in $T$
that carry enough probability mass (namely $z_{k+1}$) according to $d_{k+1}$.

Note that not all states in $T\cap{\sf Supp}(d_{k+1})$ carry a probability
mass less than $z_{k+1}$: otherwise, the total mass of $T$ in $d_{k+1}$ would
be at most $n\cdot z_{k+1}\leq 1-\varepsilon_{w}$ (this inequality holds
thanks to $n\geq 2$), in contradiction with $d_{k+1}$ being
$(1-\varepsilon_{w})$-synchronized in $T$. Therefore $T_{k+1}$ is nonempty.
Hence the set $T_{k+1}$ can be obtained from $T$ by removing at most $n-1$
states and we have

$\begin{cases}d_{k+1}(T_{k+1})>1-\varepsilon_{w}-(n-1)\cdot z_{k+1}\geq
1-n\cdot z_{k+1}=1-z_{k}\cdot\alpha^{F+1}&\\\ d_{k+1}(q)>z_{k+1}\text{ for all
}q\in T_{k+1}&\\\ \end{cases}$

So $d_{k+1}$ is strictly $(1-z_{k}\cdot\alpha^{F+1})$-synchronized in
$T_{k+1}$, and therefore also strictly
$(1-z_{j}\cdot\alpha^{F+1})$-synchronized in $T_{k+1}$ (for all $1\leq j\leq
k$). Then, the induction hypothesis implies that the set $T_{k+1}$ is distinct
from $T_{1},\dots,T_{k}$. Since $1-z_{k}\cdot\alpha^{F+1}\geq
1-z_{0}\cdot\alpha^{F+1}>1-\varepsilon_{e}$, it follows that $d_{k+1}={\cal
M}^{\sigma}_{i_{k+1}}$ is strictly $(1-\varepsilon_{e})$-synchronized in
$T_{k+1}$, and by Theorem 3.1, that the initial distribution $d_{0}$ is limit-
sure eventually synchronizing in $T_{k+1}$, that is $d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}(T_{k+1})$.

By Lemma 5, this entails that $T_{k+1}$ is not limit-sure eventually
synchronizing in ${\sf Pre}(T_{k+1})$ (i.e., $T_{k+1}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{event}}({\sf Pre}(T_{k+1}))$),
and by Theorem 3.1, for all distributions $d$ in ${\cal M}^{\sigma}$ that
occur at or after position $i_{k+1}$, we have $d({\sf Pre}(T_{k+1}))\leq
1-z_{k+1}\cdot\alpha^{F}$ where $z_{k+1}<\min\\{d_{k+1}(q)\mid q\in
T_{k+1}\cap{\sf Supp}(d_{k+1})\\}$ is a lower bound on the smallest positive
probability of a state of $T_{k+1}$ in the distribution $d_{k+1}$, taken as
the initial distribution (see Remark 2). It follows that for all distributions
$d$ in ${\cal M}^{\sigma}$ that occur (strictly) after position $i_{k+1}$, we
have $d(T_{k+1})\leq 1-z_{k+1}\cdot\alpha^{F+1}$. Hence no distribution in
${\cal M}^{\sigma}$ after $d_{k+1}$ is strictly
$(1-z_{k+1}\cdot\alpha^{F+1})$-synchronized, which concludes the proof of the
induction case. ∎

##  5 Always and Strongly Synchronizing

We summarize the key insights for always and strongly synchronizing (i.e.,
synchronizing always from some point on), and give the bounds in Theorem 5.1.

#### Always synchronizing.

For always synchronizing, all winning modes coincide $\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{always}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{always}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{limit}}^{\mathit{always}}(T)$ and it is easy to
see that sure winning for always synchronizing is equivalent to sure winning
for the safety objective $\Box T$ [14, Lemma 2]. A standard analysis of MDPs
shows that if a sure safety objective $\Box T$ is violated, then for all
_pure_ strategies $\sigma$ there exists a path compatible with $\sigma$ from
some state in the support of the initial distribution to a state in
$Q\setminus T$, of length at most $\lvert Q\rvert$ and thus of probability at
least $\alpha_{0}\cdot\alpha^{n}$ where $\alpha_{0}$ is the smallest positive
probability in the initial distribution, and $\alpha$ is the smallest positive
probability in the transitions of ${\cal M}$. Under a _randomized_ strategy
$\sigma$, a probability mass $\alpha_{0}\cdot\alpha^{n}$ also reaches
$Q\setminus T$ within $n$ steps, but possibly along paths of different
lengths. By a pigeonhole principle, at some length (smaller than $n$) the
probability mass must be at least $\frac{\alpha_{0}}{n}\cdot\alpha^{n}$ in
$Q\setminus T$.

#### Strongly synchronizing.

For strongly synchronizing, the almost-sure and limit-sure winning modes
coincide [14, Corollary 28]. On the other hand, the sure and almost-sure
winning modes are equivalent to, respectively, sure, and almost-sure winning
for the reachability objective $\Diamond S$ where $S$ is the sure-winning
region for the safety objective $\Box T$ [14, Lemma 27]. It follows that:

  * •

if $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{strongly}}(T)$ is not sure winning
for strongly synchronizing in $T$, then for all _pure_ strategies $\sigma$
there exists an infinite path $q_{0}a_{0}q_{1}a_{1}\dots$ compatible with
$\sigma$ from some state $q_{0}$ in the support of $d_{0}$ that remains
outside $S$, that is $q_{i}\in Q\setminus S$ for all $i\geq 0$. The
corresponding probability mass is at least $\alpha_{0}\cdot\alpha^{i}$, and
hence for all _randomized_ strategies $\sigma$, a probability mass at least
$\alpha_{0}\cdot\alpha^{i}$ is also in $Q\setminus S$ at step $i$ (but not
necessarily in a single state).

By definition of $S$, and using an argument similar to the case of always
synchronizing, for all $i\geq 0$, there exists a length $\ell_{i}\leq n$ such
that a probability mass at least
$\alpha_{0}\cdot\alpha^{i}\cdot\frac{\alpha^{n}}{n}$ is in $Q\setminus T$ at
step $i+\ell_{i}$. We construct the indices $i_{0},i_{1},\dots$ inductively as
follows. Let $i_{0}=\ell_{0}$ and for all $j\geq 0$ let
$i_{j+1}=i_{j}+1+\ell_{i_{j}+1}$. Then ${\cal M}^{\sigma}_{i_{j}}(T)<1$ is not
$1$-synchronized in $T$ (in fact ${\cal M}^{\sigma}_{i_{j}}(T)\leq
1-\alpha_{0}\cdot\alpha^{i_{j-1}+n}$) for all $j\geq 0$. Note that $i_{0}\leq
n$ and $0<i_{j+1}-i_{j}\leq n$ for all $j\geq 0$.

  * •

if $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{strongly}}(T)$, then $d_{0}$ is
not almost-sure winning for the reachability objective $\Diamond S$, and by
Lemma 1 for all (randomized) strategies $\sigma$ and all $i\geq 0$, there
exists a state $q_{i}\in Q\setminus S$ such that
$\Pr^{\sigma}_{d_{0}}(\Diamond^{i}\\{q_{i}\\})\geq\alpha_{0}\cdot\frac{\alpha^{n}}{n}$.
Since $q_{i}\not\in S$ is not in the winning region for sure safety $\Box T$,
there is a length $\ell_{i}\leq n$ as above, such that the probability mass in
$Q\setminus T$ at length $i+\ell_{i}$ is at least
$\alpha_{0}\cdot\frac{\alpha^{2n}}{n^{2}}$. For the indices $i_{0}=\ell_{0}$
and $i_{j+1}=i_{j}+1+\ell_{i_{j}+1}$ for all $j\geq 0$, we get ${\cal
M}^{\sigma}_{i_{j}}(T)\leq 1-\alpha_{0}\cdot\frac{\alpha^{2n}}{n^{2}}$.

###### Theorem 5.1

Given an initial distribution $d_{0}$, let $\alpha_{0}$ be the smallest
positive probability in $d_{0}$, and let
$\varepsilon_{a}=\alpha_{0}\cdot\frac{\alpha^{n}}{n}$ and
$\varepsilon_{s}=\alpha_{0}\cdot\frac{\alpha^{2n}}{n^{2}}$.

  * •

if $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{always}}(T)$ is not sure always
synchronizing in $T$, then for all strategies $\sigma$, in the sequence ${\cal
M}^{\sigma}$ there exists a position $i\leq n$ such that ${\cal
M}^{\sigma}_{i}$ is not $(1-\varepsilon_{a})$-synchronized in $T$,

  * •

if $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{sure}}^{\mathit{strongly}}(T)$ is not sure
strongly synchronizing in $T$, then for all strategies $\sigma$, in the
sequence ${\cal M}^{\sigma}$ there exist infinitely many positions
$i_{0}<i_{1}<i_{2}<\dots$ where $i_{0}\leq n$ and $i_{j+1}-i_{j}\leq n$ for
all $j\geq 0$ such that ${\cal M}^{\sigma}_{i_{j}}$ is not $1$-synchronized in
$T$.

  * •

if $d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{almost}}^{\mathit{strongly}}(T)$ is not almost-
sure strongly synchronizing in $T$, then for all strategies $\sigma$, in the
sequence ${\cal M}^{\sigma}$ there exist infinitely many positions
$i_{0}<i_{1}<i_{2}<\dots$ where $i_{0}\leq n$ and $i_{j+1}-i_{j}\leq n$ for
all $j\geq 0$ such that ${\cal M}^{\sigma}_{i_{j}}$ is not
$(1-\varepsilon_{s})$-synchronized in $T$.

##  6 Adversarial Synchronizing Objectives

In an adversarial MDP the strategies are universally quantified, which
corresponds to satisfying an objective regardless of the choice of strategies
by an adversary. Replacing $\exists\sigma$ by $\forall\sigma$ in the
definition of the three winning modes gives, after taking the negation to get
existentially quantified strategies, the following new winning modes.

Given a set $T\subseteq Q$, we say that a sequence $d_{0}d_{1}\dots$ of
probability distributions is:

  * •

_positively_ {always, eventually, weakly, strongly} winning if $d_{i}(T)>0$
for, respectively, all $i\geq 0$, some $i\geq 0$, infinitely many $i$’s, all
but finitely many $i$’s.

  * •

_boundedly_ {always, eventually, weakly, strongly} winning if there exists
$\varepsilon>0$ such that $d_{i}(T)>\varepsilon$ for, respectively, all $i\geq
0$, some $i\geq 0$, infinitely many $i$’s, all but finitely many $i$’s.

For $\lambda\in\\{always,event,weakly,strongly\\}$, we denote by
$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{positive}}^{\mathit{\lambda}}(T)$ (resp.,
$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{\lambda}}(T)$) the set of
initial distributions $d_{0}$ from which there exists a strategy $\sigma$ such
that the sequence ${\cal M}^{\sigma}$ is positively (resp., boundedly)
$\lambda$-synchronizing in $T$, and we say that $\sigma$ is positively (resp.,
boundedly) $\lambda$-synchronizing in $T$ from $d_{0}$.

Table 1 summarizes the new definitions. Note that replacing the existential
quantification on strategies in boundedly winning mode by a supremum gives the
same question, since $\exists\sigma:f(\sigma)>0$ is equivalent to
$\sup_{\sigma}f(\sigma)>0$. For the same reason, we have the identity
$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{positive}}^{\mathit{event}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{event}}(T)$. It is easy to show
that the definitions imply the identity $\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{always}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{positive}}^{\mathit{always}}(T)\cap\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{strongly}}(T)$, which we also
obtain as a corollary of Lemma 6 below.

###### Remark 3

It immediately follows from the definitions that for all synchronizing modes
$\lambda\in\\{always,event,weakly,strongly\\}$, and
$\mu\in\\{positive,bounded\\}$:

  * •

$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{always}}(T)\subseteq\langle\\!\langle
1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{strongly}}(T)\subseteq\langle\\!\langle
1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{weakly}}(T)\subseteq\langle\\!\langle
1\rangle\\!\rangle_{\mathit{\mu}}^{\mathit{event}}(T)$,

  * •

$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{\lambda}}(T)\subseteq\langle\\!\langle
1\rangle\\!\rangle_{\mathit{positive}}^{\mathit{\lambda}}(T)$,

and moreover,

  * •

$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{positive}}^{\mathit{event}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{event}}(T)$, and

  * •

$\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{always}}(T)=\langle\\!\langle
1\rangle\\!\rangle_{\mathit{positive}}^{\mathit{always}}(T)\cap\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{strongly}}(T)$.

It is easy to see that if there exists a strategy $\sigma$ that is positively
$\lambda$-synchronizing in $T$, then the strategy $\sigma_{{\sf u}}$ that
plays at every round all actions uniformly at random is also positively
$\lambda$-synchronizing in $T$, because the condition $d_{i}(T)>0$ is
equivalent to ${\sf Supp}(d_{i})\cap T\neq\varnothing$, and because we have
$\sigma\subseteq\sigma_{{\sf u}}$, which implies that ${\sf Supp}({\cal
M}_{i}^{\sigma})\subseteq{\sf Supp}({\cal M}_{i}^{\sigma_{{\sf u}}})$ for all
$i\geq 0$.

Hence, in all four synchronization modes, the question is equivalent to the
same question in Markov chains (obtained from the given MDP by fixing the
strategy $\sigma_{{\sf u}}$) which can be solved as follows. Given a Markov
chain, consider the underlying directed graph $\langle Q,E\rangle$ where
$(q,q^{\prime})\in E$ if $\delta(q,a)(q^{\prime})>0$ (where ${\sf
A}=\\{a\\}$). For positive eventually synchronizing, it suffices to find a
state in $T$ that is reachable in that graph, and for positive weakly
synchronizing, it suffices to find a state in $T$ that is both reachable and
can reach itself. These questions are NL-complete. For positive always and
strongly synchronizing, the question is equivalent to the model-checking
problem for the formulas $G\exists T$ and $FG\exists T$ in the logic CTL+Sync,
which are both coNP-complete [8, Lemma 2 & Section 3].

For boundedly winning, we show that one strategy is good enough in all four
synchronization modes, like for positive winning. The strategy plays like
$\sigma_{{\sf u}}$ for the first $2^{n}$ rounds, and then switches to a
strategy $\sigma_{{\cal E}}$ that, in the states $q\in{\cal E}$, plays
uniformly at random all actions that stay in the end-component ${\cal E}(q)$
of $q$ (thus all actions in ${\sf A}_{{\cal E}(q)}$), and in the transient
states $q\not\in{\cal E}$, plays all actions uniformly at random. We call this
strategy the _freezing_ strategy. Intuitively we use $\sigma_{{\sf u}}$ to
scatter the probability mass in all end-components of the MDP, and then
$\sigma_{{\cal E}}$ to maintain a bounded probability in each end-component.

###### Lemma 6

Let ${\cal M}$ be an MDP with $n$ states and initial distribution $d_{0}$, and
let $T$ be a target set. Consider the following conditions:

  * (1)

$\forall i\geq 0:{\cal M}^{\sigma_{{\sf u}}}_{i}(T)>0$ (2) $\forall i\geq
2^{n}:{\cal M}^{\sigma_{{\sf u}}}_{i}({\cal E}\cap T)>0$

Then, the following equivalences hold:

  * (a)

$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{positive}}^{\mathit{always}}(T)$ if and only if
Condition $(1)$ holds;

  * (b)

$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{strongly}}(T)$ if and only if
Condition $(2)$ holds;

  * (c)

$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{always}}(T)$ if and only if
Conditions $(1)$ and $(2)$ hold;

###### Proof

Equivalence $(a)$ follows from the definition of positive always
synchronizing, and from the fact that the uniform strategy $\sigma_{{\sf u}}$
is sufficient for positive winning.

We show Equivalence $(b)$ as follows. First, if Condition $(2)$ does not hold,
then ${\cal M}^{\sigma_{{\sf u}}}_{i}({\cal E}\cap T)=0$ for some $i\geq
2^{n}$, and thus also for infinitely many $i$’s (since the sequence ${\sf
Supp}({\cal M}^{\sigma_{{\sf u}}}_{i})$ is ultimately periodic, after at most
$2^{n}$ steps). For arbitrary strategy $\sigma$, we have ${\sf Supp}({\cal
M}^{\sigma}_{i})\subseteq{\sf Supp}({\cal M}^{\sigma_{{\sf u}}}_{i})$ for all
$i\geq 0$, therefore ${\cal M}^{\sigma}_{i}({\cal E}\cap T)=0$ for infinitely
many $i$’s. By Lemma 2, we have $\liminf_{i\to\infty}{\cal
M}^{\sigma}_{i}({\cal E})=1$ which entails that $\limsup{\cal
M}^{\sigma}_{i}({\cal E}\setminus T)=1$ and $\limsup{\cal
M}^{\sigma}_{i}(Q\setminus T)=1$, that is $\liminf{\cal M}^{\sigma}_{i}(T)=0$.
Since this holds for arbitrary strategy $\sigma$, it follows that
$d_{0}\not\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{strongly}}(T)$.

For the converse direction, assuming Condition $(2)$ holds, we show that
$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{strongly}}(T)$, witnessed by
the freezing strategy $\sigma_{f}$ (which plays like $\sigma_{{\sf u}}$ for
the first $2^{n}$ rounds, and then switches to the strategy $\sigma_{{\cal
E}}$).

We show the key property that

${\sf Supp}({\cal M}^{\sigma_{{\sf u}}}_{i})\cap{\cal E}={\sf Supp}({\cal
M}^{\sigma_{f}}_{i})\cap{\cal E}\text{ for all }i\geq 2^{n}.$

Fix an arbitrary $i\geq 2^{n}$ and let $p$ be a period of the sequence ${\sf
Supp}({\cal M}^{\sigma_{{\sf u}}})$ such that $i-p\leq 2^{n}$ and ${\sf
Supp}({\cal M}^{\sigma_{{\sf u}}}_{i})={\sf Supp}({\cal M}^{\sigma_{{\sf
u}}}_{i-p})$. Consider the Markov chain ${\cal M}_{{\cal E}}$ obtained by
fixing the strategy $\sigma_{{\cal E}}$ in ${\cal M}$. From the basic theory
of Markov chains, each end-component $C$ in ${\cal M}$ is a recurrent class in
${\cal M}_{{\cal E}}$. For each $i\geq 2^{n}$, either all or none of the
states in a periodic class of $C$ are in the support of ${\cal
M}^{\sigma_{{\sf u}}}_{i}$.

To show the key property, first consider a state $q\in{\sf Supp}({\cal
M}^{\sigma_{{\sf u}}}_{i})\cap{\cal E}$ for $i\geq 2^{n}$, and show that
$q\in{\sf Supp}({\cal M}^{\sigma_{f}}_{i})\cap{\cal E}$. Let $S$ be the
periodic class of ${\cal E}(q)$ containing $q$ (in ${\cal M}_{{\cal E}}$), and
thus

$S\subseteq{\sf Supp}({\cal M}^{\sigma_{{\sf u}}}_{i})\cap{\cal E},\text{ and
thus }S\subseteq{\sf Supp}({\cal M}^{\sigma_{{\sf u}}}_{i-p})\cap{\cal E}.$

Since $\sigma_{{\sf u}}$ and $\sigma_{f}$ coincide on the first $2^{n}$
rounds, we have

$S\subseteq{\sf Supp}({\cal M}^{\sigma_{f}}_{i-p})\cap{\cal E}.$

Now consider the strategy $\sigma_{{\cal E}}$ and an initial distribution with
support $S$, and denote by $S+j$ the support of the probability distribution
after playing $\sigma_{{\cal E}}$ for $j$ steps. Then, since $\sigma_{{\cal
E}}\subseteq\sigma_{f}\subseteq\sigma_{u}$,

$S+p\subseteq{\sf Supp}({\cal M}^{\sigma_{f}}_{i})\cap{\cal E},\text{ and
}S+p\subseteq{\sf Supp}({\cal M}^{\sigma_{u}}_{i})\cap{\cal E}.$

We can repeat the same argument with $S+p$ instead of $S$, and show by
induction that $S+j\cdot p\subseteq{\sf Supp}({\cal
M}^{\sigma_{f}}_{i})\cap{\cal E}$ for all $j\geq 1$. In particular, by taking
$j$ the period of the end-component containing $q$, we get $S+j\cdot p=S$ and
thus $S\subseteq{\sf Supp}({\cal M}^{\sigma_{f}}_{i})\cap{\cal E}$, which
establishes one direction of the key property (the converse direction follows
from $\sigma_{f}\subseteq\sigma_{{\sf u}}$).

From the theory of Markov chains, in every end-component state $q\in{\cal E}$,
the positive probability mass is bounded away from $0$ in ${\cal M}^{{\cal
E}}$, that is there exists a bound $\varepsilon>0$ such that for all $i\geq
2^{n}$, for all $q\in{\cal E}$, if ${\cal M}^{\sigma_{f}}_{i}(q)\neq 0$, then
${\cal M}^{\sigma_{f}}_{i}(q)\geq\varepsilon$. By the key property and
Condition $(2)$, for all $i\geq 2^{n}$, there exists $q\in{\cal E}\cap T$ such
that ${\cal M}^{\sigma_{f}}_{i}(q)\neq 0$, which implies that
$\liminf_{i\to\infty}M^{\sigma_{f}}_{i}(T)\geq\varepsilon>0$ and thus
$d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{strongly}}(T)$.

Finally, the proof for Equivalence $(c)$ follows the same steps as above to
show that Conditions $(1)$ and $(2)$ imply $d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{always}}(T)$, where Condition
$(1)$ is used to bound $M^{\sigma_{f}}_{i}(T)$ for the first $2^{n}$ rounds,
and thus to ensure that $M^{\sigma_{f}}_{i}(T)\geq B>0$ for all $i\geq 0$,
hence $d_{0}\in\langle\\!\langle
1\rangle\\!\rangle_{\mathit{bounded}}^{\mathit{always}}(T)$. The converse
direction immediately follows from the first part of Remark 3 and Equivalences
$(a)$ and $(b)$. ∎

We extract explicit bounds from the proof of Lemma 6. All end-components are
reached within a most $n$ steps (under $\sigma_{{\sf u}}$), and further all
states in (a periodic class of) a recurrent class are reached (synchronously)
within a most $n^{2}$ steps [16, Theorem 4.2.11], thus all states in the
periodic class have probability mass at least
$\varepsilon_{a}=\alpha_{0}\cdot\left(\frac{\alpha}{\lvert{\sf
A}\rvert}\right)^{n+n^{2}}$ where $\alpha_{0}$ is the smallest positive
probability in the initial distribution $d_{0}$ (note that $\alpha/\lvert{\sf
A}\rvert$ is the smallest probability in the Markov chain ${\cal M}_{{\cal
E}}$). It follows that the freezing strategy ensures probability at least
$\varepsilon_{a}$ in $T$ at every step (if ${\cal M}$ is boundedly always
synchronizing), and probability at least $\varepsilon_{a}$ in $T$ at every
step after $N=n+n^{2}$.

The conditions $(1)$ and $(2)$ in Lemma 6 can be decided in coNP as follows.
For Condition $(1)$ we guess an index $i\leq 2^{n}$ (in binary) and compute
the $i$-th power of the Boolean transition matrix $M\in\\{0,1\\}^{n^{2}}$
where $M(q,q^{\prime})=1$ if there is a transition from state $q$ to state
$q^{\prime}$ in the Markov chain obtained from the given MDP ${\cal M}$ by
fixing the strategy $\sigma_{{\sf u}}$. The matrix $M^{i}$ can be computed in
polynomial time by successive squaring of $M$. Then it suffices to check
whether $M^{i}(q_{0},q)=0$ for all $q_{0}\in{\sf Supp}(d_{0})$ and $q\in T$.
For Condition $(2)$, since the sequence ${\sf Supp}({\cal M}^{\sigma_{{\sf
u}}}_{i})$ is ultimately periodic, we guess two indices $i,p\leq 2^{n}$
($p\geq 1$) and check that ${\sf Supp}({\cal M}^{\sigma_{{\sf u}}}_{i})={\sf
Supp}({\cal M}^{\sigma_{{\sf u}}}_{i+p})$ and ${\sf Supp}({\cal
M}^{\sigma_{{\sf u}}}_{i})\cap{\cal E}\cap T=\varnothing$, using the same
approach by successive squaring. Note that the union ${\cal E}$ of all end-
components can be computed in polynomial time [11, 12].

Conditions $(1)$ and $(2)$ are also coNP-hard, using the same reduction that
established coNP-hardness of the positive always and positive bounded
synchronizing [8, Lemma 2 & Section 3], in which positive and bounded winning
mode coincide. It follows that the membership problem for bounded always and
bounded strongly synchronizing is coNP-complete.

We now show the solution for bounded weakly synchronizing. It suffices to find
a state in $T\cap{\cal E}$ that is reachable in the underlying graph of the
Markov chain ${\cal M}_{\sigma_{{\sf u}}}$, which is a NL-complete problem
(like for positive weakly synchronizing, except we require a reachable state
in $T\cap{\cal E}$, not just in $T$). Indeed, if all reachable end-components
are contained in $Q\setminus T$, then by Lemma 2 we have
$\liminf_{i\to\infty}{\cal M}^{\sigma}_{i}(Q\setminus T)=1$, that is
$\limsup_{i\to\infty}{\cal M}^{\sigma}_{i}(T)=0$. For the converse direction,
if a state $\hat{q}\in T\cap{\cal E}$ is reachable, then by a similar argument
as above based on the theory of Markov chains, as the probability mass in the
states of the periodic classes (that contain some probability mass) is bounded
away from $0$ in ${\cal M}^{\sigma_{{\cal E}}}$, it follows that within every
$p$ steps, where $p$ is the period of the recurrent class ${\cal E}(\hat{q})$
the probability mass in $\hat{q}$ is at least
$\alpha_{0}\cdot(\alpha/\lvert{\sf A}\rvert)^{n+n^{2}}$. Therefore, ${\cal M}$
is boundedly weakly synchronizing in $T$. For the sake of completeness, note
that for eventually synchronizing MDPs, the probability mass
$\varepsilon_{e}=\alpha_{0}\cdot(\alpha/\lvert{\sf A}\rvert)^{n}$ in $T$ can
be ensured within $n$ steps (using $\sigma_{{\sf u}}$).

###### Theorem 6.1

The complexity of the membership problem for positive and bounded
synchronizing objectives is summarized in Table 2.

In Table 2, the merged cells for eventually synchronizing reflect the fact
that the winning regions coincide (see Remark 3). The winning regions for the
other synchronizing modes do not coincide, already in Markov chains (see
Figure 1).

#### Acknowledgment.

The authors are grateful to Jean-François Raskin for logistical support, and
to Mahsa Shirmohammadi for interesting discussions about adversarial
objectives.

## References

  * [1] S. Akshay, B. Genest, and N. Vyas.  Distribution-based objectives for Markov decision processes.  In Proc. of LICS: Logic in Computer Science, pages 36–45. ACM, 2018.
  * [2] C. Baier and J.-P. Katoen.  Principles of Model Checking.  MIT, 2008.
  * [3] D. Beauquier, A. M. Rabinovich, and A. Slissenko.  A logic of probability with decidable model-checking.  In Proc. of CSL: Computer Science Logic, LNCS 2471, pages 306–321. Springer, 2002.
  * [4] P. C. Bell and P. Semukhin.  Decidability of cutpoint isolation for probabilistic finite automata on letter-bounded inputs.  In Proc. of CONCUR: Concurrency Theory, volume 171 of LIPIcs, pages 22:1–22:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [5] N. Bertrand, M. Dewaskar, B. Genest, and H. Gimbert.  Controlling a population.  In Proc. of CONCUR: Concurrency Theory, volume 85 of LIPIcs, pages 12:1–12:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
  * [6] J. C. Bradfield and C. Stirling.  Modal mu-calculi.  In Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721–756. North-Holland, 2007.
  * [7] J. C. Bradfield and I. Walukiewicz.  The mu-calculus and model checking.  In Handbook of Model Checking, pages 871–919. Springer, 2018.
  * [8] K. Chatterjee and L. Doyen.  Computation tree logic for synchronization properties.  In Proc. of ICALP: Automata, Languages, and Programming, volume 55 of LIPIcs, pages 98:1–98:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
  * [9] K. Chatterjee and T. A. Henzinger.  A survey of stochastic $\omega$-regular games.  J. Comput. Syst. Sci., 78(2):394–413, 2012.
  * [10] T. Colcombet, N. Fijalkow, and P. Ohlmann.  Controlling a random population.  In Proc. of FoSSaCS: Foundations of Software Science and Computation Structures, LNCS 12077, pages 119–135. Springer, 2020.
  * [11] C. Courcoubetis and M. Yannakakis.  The complexity of probabilistic verification.  Journal of the ACM, 42(4):857–907, 1995.
  * [12] L. de Alfaro.  Formal Verification of Probabilistic Systems.  PhD thesis, Stanford University, 1997.
  * [13] L. de Alfaro and T. A. Henzinger.  Concurrent omega-regular games.  In Proc. of LICS: Logic in Computer Science, pages 141–154. IEEE, 2000.
  * [14] L. Doyen, T. Massart, and M. Shirmohammadi.  The complexity of synchronizing Markov decision processes.  Journal of Computer and System Sciences, 100:96–129, 2019.
  * [15] E. Feinberg and A. Shwartz, editors.  Handbook of Markov Decision Processes - Methods and Applications.  Kluwer, 2002.
  * [16] R. G. Gallager.  Stochastic processes: theory for applications.  Cambridge University Press, 2013.
  * [17] H. Hermanns, J. Krcál, and J. Kretínský.  Probabilistic bisimulation: Naturally on distributions.  In Proc. of CONCUR: Concurrency Theory, LNCS 8704, pages 249–265. Springer, 2014.
  * [18] P. Jancar and Z. Sawa.  A note on emptiness for alternating finite automata with a one-letter alphabet.  Inf. Process. Lett., 104(5):164–167, 2007.
  * [19] V. A. Korthikanti, M. Viswanathan, G. Agha, and Y. Kwon.  Reasoning about MDPs as transformers of probability distributions.  In Proc. of QEST: Quantitative Evaluation of Systems, pages 199–208. IEEE Computer Society, 2010.
  * [20] M. L. Puterman.  Markov Decision Processes.  John Wiley and Sons, 1994.
  * [21] M. O. Rabin.  Probabilistic automata.  Information and Control, 6:230–245, 1963.
  * [22] M. Shirmohammadi.  Qualitative analysis of probabilistic synchronizing systems.  PhD thesis, Université Libre de Bruxelles & École Normale Supérieure de Cachan, 2014.
  * [23] M. Y. Vardi.  Automatic verification of probabilistic concurrent finite-state programs.  In Proc. of FOCS: Foundations of Computer Science, pages 327–338. IEEE Computer Society, 1985.