--- abstract: | We consider Markov decision processes (MDP) as generators of sequences of probability distributions over states. A probability distribution is $p$-synchronizing if the probability mass is at least $p$ in a single state, or in a given set of states. We consider four temporal synchronizing modes: a sequence of probability distributions is always $p$-synchronizing, eventually , weakly $p$-synchronizing, or strongly $p$-synchronizing if, respectively, all, some, infinitely many, or all but finitely many distributions in the sequence are $p$-synchronizing. For each synchronizing mode, an MDP can be $(i)$ *sure* winning if there is a strategy that produces a $1$-synchronizing sequence; $(ii)$ *almost-sure* winning if there is a strategy that produces a sequence that is, for all $\epsilon > 0$, a (1-$\epsilon$)-synchronizing sequence; $(iii)$ *limit-sure* winning if for all $\epsilon > 0$, there is a strategy that produces a (1-$\epsilon$)-synchronizing sequence. We provide fundamental results on the expressiveness, decidability, and complexity of synchronizing properties for MDPs. For each synchronizing mode, we consider the problem of deciding whether an MDP is sure, almost-sure, or limit-sure winning, and we establish matching upper and lower complexity bounds of the problems: for all winning modes, we show that the problems are PSPACE-complete for eventually and weakly synchronizing, and PTIME-complete for always and strongly synchronizing. We establish the memory requirement for winning strategies, and we show that all winning modes coincide for always synchronizing, and that the almost-sure and limit-sure winning modes coincide for weakly and strongly synchronizing. address: - 'LSV, ENS Cachan & CNRS, France' - 'Université Libre de Bruxelles, Belgium' author: - Laurent Doyen - Thierry Massart - Mahsa Shirmohammadi bibliography: - 'biblio.bib' title: | <span>**The Complexity of Synchronizing\ Markov Decision Processes**</span> --- Introduction {#sec:intro} ============ Markov decision processes (MDP) are finite-state stochastic models of dynamic systems studied in many applications such as planning @MHC03, randomized algorithms @AspnesH90 [@PSL00], communication protocols @FokkinkP06, and in many problems related to reactive system design and verification @FV97 [@BBS06; @EKVY08]. MDPs exhibit both stochastic and nondeterministic behavior, as in the control problem for reactive systems: nondeterminism represents the possible choice of actions of the controller, and stochasticity represents the uncertainties about the system response (see \[fig:almost-limit-eventually-differ\]). The controller synthesis problem is to compute the largest probability with which a control strategy can ensure that the system satisfies a given specification, and to construct an optimal strategy @BA95 [@FV97]. The qualitative variant of the problem is to decide if the system can satisfy the specification with probability $1$. Fundamental well-studied specifications are state-based and describe correct behaviors as infinite sequences of states of the MDP, including safety and liveness properties such as reachability, Büchi, and co-Büchi conditions, which require the system to visit a set of target states once, infinitely often, and ultimately always, respectively @automata [@AHK07]. In contrast to this traditional approach, we consider a distribution-based semantics where the specification describes correct behaviors of MDPs as infinite sequences of probability distributions $d_i : Q \to [0,1]$ over the finite state space $Q$ of the system, where $d_i(q)$ is the probability that the MDP is in state $q \in Q$ after $i$ execution steps. The distribution-based semantics is adequate in large-population models, such as systems biology @HMW09, robot planning @BBMR08, distributed systems @GGB12, etc. where the system consists of several copies of the same process (molecules, robots, sensors, etc.), and the relevant information along the execution of the system is the number of processes in each state, or the relative frequency (i.e., the probability) of each state. In the context of several identical processes, the same control strategy is used in every process, but the internal state of each process need not be the same along the execution, since probabilistic transitions may have a different outcome in each process. Therefore, the global execution of the system (consisting of all the processes) is better described by the sequence of probability distributions over states along the execution. However, the control strategy is local to each process and can select control actions depending on the full history of the process execution, which corresponds to general perfect-information strategies that we consider in this work. Previously, the special case of blind strategies has been considered, which in each step select the same control action at all states, and thus only depend on the number of execution steps of the system. In automata theory, a blind strategy corresponds simply to an input word. In MDPs with blind strategies, also known as probabilistic automata @Rabin63 [@PAZBook], several basic problems are undecidable such as deciding if there exists a blind strategy that ensures a coBüchi condition with probability $1$ @BGB12, or deciding if a reachability condition can be ensured with probability arbitrarily close to $1$ @GO10. The main contribution of this article is to establish the decidability and optimal complexity of deciding *synchronizing* properties for the distribution-based semantics of MDPs under general strategies. Synchronizing properties require that the sequence of probability distributions accumulate all the probability mass in a single state, or in a given set of states. They generalize synchronizing properties of finite automata @Volkov08 [@DMS11b]. Formally, for $0 \leq p \leq 1$ let a probability distribution $d : Q \to [0,1]$ be $p$-synchronized if it assigns probability at least $p$ to some state. A sequence $\bar{d} = d_0 d_1 \dots$ of probability distributions is - *always $p$-synchronizing* if $d_i$ is $p$-synchronized for all $i$; - *eventually $p$-synchronizing* if $d_i$ is $p$-synchronized for some $i$; - *weakly $p$-synchronizing* if $d_i$ is $p$-synchronized for infinitely many $i$'s; - *strongly $p$-synchronizing* if $d_i$ is $p$-synchronized for all but finitely many $i$'s. We present a consistent and comprehensive theory of the qualitative synchronizing properties, corresponding to the case where either $p=1$, or $p$ tends to $1$, which are analogous to the traditional safety, reachability, Büchi, and coBüchi conditions @ConcOmRegGames. <span>|l@<span> </span> |\*<span>2</span><span>c@c@c@|</span></span> & &\ Sure & $\exists \alpha$ & $\forall n$ & ${{\cal M}}^{\alpha}_n(T)=1$ & $\exists \alpha$ & $\exists N \: \forall n \geq N$ & ${{\cal M}}^{\alpha}_n(T)=1$\ Almost-sure & $\exists \alpha$ & $\inf_{n}$ & ${{\cal M}}^{\alpha}_n(T)=1$ & $\exists \alpha$& $\liminf_{n\to\infty}$ & ${{\cal M}}^{\alpha}_n(T)=1$\ Limit-sure & $\sup_{\alpha}$ & $\inf_{n}$ & ${{\cal M}}^{\alpha}_n(T)=1$ & $\sup_{\alpha}$& $\liminf_{n\to\infty}$ & ${{\cal M}}^{\alpha}_n(T)=1$\ & &\ Sure & $\exists \alpha$ & $\forall N \: \exists n \geq N$ & ${{\cal M}}^{\alpha}_n(T)=1$ & $\exists \alpha$ & $\exists n$ & ${{\cal M}}^{\alpha}_n(T)=1$\ Almost-sure & $\exists \alpha$& $\limsup_{n\to\infty}$ & ${{\cal M}}^{\alpha}_n(T)=1$ & $\exists \alpha$ & $\sup_{n}$ & ${{\cal M}}^{\alpha}_n(T)=1$\ Limit-sure & $\sup_{\alpha}$& $\limsup_{n\to\infty}$ & ${{\cal M}}^{\alpha}_n(T)=1$ & $\sup_{\alpha}$ & $\sup_{n}$ & ${{\cal M}}^{\alpha}_n(T)=1$\ #### Applications A typical application scenario of synchronizing properties is the design of a control program for a group of mobile robots running in a stochastic environment @MSG10. The possible behaviors of the robots and the stochastic response of the environment (such as obstacle encounters) are represented by an MDP, and a synchronizing strategy corresponds to a control program that can be embedded in every robot to ensure that they meet (or synchronize) all the time, eventually once, infinitely often, or eventually forever. Synchronization properties are central in large-population models in biology, such as yeast, where experimental synchronization methods have been developed to get a population of yeast in the same cell cycle stage @BDGG17 [@Futcher99]. A simple abstraction of large populations of identical finite-state stochastic agents is to consider a continuum of agents, described by the relative fraction of agents in each possible state, i.e. by a distribution. For example, consider a model of cells where at each time instant half of the cells get activated, and once activated we can block them for a while, or release them to reach a fluorescent state. In the MDP of \[fig:almost-limit-eventually-differ\], the state $q_{1}$ corresponds to activation, action $a$ is blocking, and action $b$ is releasing. The fluorescent state is $q_2$. Probability mass arbitrarily close to $1$ can be accumulated in $q_2$, thus for all $\epsilon > 0$ we can generate an eventually $(1-\epsilon)$-synchronizing sequence in $q_2$, but not an eventually $1$-synchronizing sequence. If it was possible to reset the cell state after fluorescence, such as in the MDP of \[fig:inf-mem\], then we can obtain a sequence of distribution that is weakly $(1-\epsilon)$-synchronizing, for all $\epsilon > 0$. We consider the following qualitative winning modes, summarized in Table \[tab:def-modes\]: $(i)$ *sure* winning, if there is a strategy that generates an {always, eventually, weakly, strongly} $1$-synchronizing sequence; $(ii)$ *almost-sure* winning, if there is a strategy that generates a sequence that is, for all $\epsilon>0$, {always, eventually, weakly, strongly} $(1-\epsilon)$-synchronizing; $(iii)$ *limit-sure* winning, if for all $\epsilon>0$, there is a strategy that generates an {always, eventually, weakly, strongly} $(1-\epsilon)$-synchronizing sequence. *Contribution.* The contributions of this article are summarized as follows: - *Expressiveness.* We show that the three winning modes form a strict hierarchy for eventually synchronizing: there are limit-sure winning MDPs that are not almost-sure winning, and there are almost-sure winning MDPs that are not sure winning. This is in contrast with the traditional state-based reachability objectives for which the notions of almost-sure and limit-sure winning coincide in MDPs. In this context, a more unexpected and difficult result is that the almost-sure and limit-sure modes coincide for weakly and strongly synchronizing. Thus those two synchronizing modes are more robust than eventually synchronizing, although we show that almost-sure weakly synchronizing strategies can be constructed from the analysis of eventually synchronizing (in limit-sure winning mode). Finally, for always synchronizing the three winning modes coincide, and we show that they coincide with a traditional safety objective. - *Complexity.* For each synchronizing and winning mode, we consider the problem of deciding if a given initial distribution is winning. The complexity results are shown in Table \[tab:complexity\] (p. ). We establish the decidability and optimal complexity bounds for all winning modes. Under general strategies, the decision problems have much lower complexity than with blind strategies. We show that all decision problems are decidable, in polynomial time for always and strongly synchronizing, and PSPACE-complete for eventually and weakly synchronizing. This is also in contrast with almost-sure winning in the traditional semantics of MDPs, which is solvable in polynomial time for both safety and reachability @deAlfaro97. - *Memory bounds.* We complete the picture by proving optimal memory bounds for winning strategies, summarized in Table \[tab:memory\] (p. ). Memoryless strategies are sufficient for always synchronizing (like for safety objectives). We show that linear memory is sufficient for strongly synchronizing, and we identify a variant of strongly synchronizing for which memoryless strategies are sufficient. For eventually and weakly synchronizing, exponential memory is sufficient and may be necessary for sure winning strategies, and in general infinite memory is necessary for almost-sure winning. Some results in this article rely on insights about games and alternating automata that are of independent interest. Firstly, the sure-winning problem for eventually synchronizing is equivalent to a two-player game with a synchronized reachability objective, where the goal for the first player is to ensure that a target state is reached after a number of steps that is independent of the strategy of the opponent (and thus this number can be fixed in advance by the first player). This condition is stronger than plain reachability, and while the winner in two-player reachability games can be decided in polynomial time, deciding the winner for synchronized reachability is PSPACE-complete. This result is obtained by turning the synchronized reachability game into a one-letter alternating automaton for which the emptiness problem (i.e., deciding if there exists a word accepted by the automaton) is PSPACE-complete @Holzer95 [@AFA1]. Secondly, our PSPACE lower bound for the limit-sure winning problem in eventually synchronizing uses a PSPACE-completeness result that we establish for the *universal finiteness problem*, which is to decide, given a one-letter alternating automata, whether from every state the accepted language is finite. #### Related Works The traditional state-based semantics of MDPs has been studied extensively @Puterman [@CY95; @FV97] and plays a central role in recent developments of system verification and controller synthesis, including expressiveness and complexity analysis of various classes of properties @FKNP11, using techniques such as symbolic algorithms for Büchi objectives @CHJS11, game-based abstraction techniques @KKNP10, and multi-objective analysis for assume-guarantee model-checking @EKVY08. On the other hand, the distribution-based semantics has received a greater interest only recently, as it is shown that relevant key properties of MDPs can only be expressed in a distribution-based logical framework @BRS02 [@KVAK10] and that a new useful notion of probabilistic bisimulation can be obtained in the distribution-based semantics @HKK14. Several recent works have investigated this new approach showing that the verification of quantitative properties of the distribution-based semantics is undecidable @KVAK10 [@FKS16], and decidability can be obtained for special subclasses of systems @CKVAK11, or through approximations @AAGT12. In this context, a challenging goal is to identify useful decidable properties for the distribution-based semantics. Synchronization problems were first considered for deterministic finite automata (DFA) where a *synchronizing word* is a finite sequence of control actions that can be executed from any state of an automaton and leads to the same state (see @Volkov08 for a survey of results and applications). While the existence of a synchronizing word can be decided in NLOGSPACE for DFA, extensive research effort is devoted to establishing a tight bound on the length of the shortest synchronizing word @Ber16 [@Nic16; @Szy18], which is conjectured to be $(n-1)^2$ for automata with $n$ states @Cer64. Various extensions of the notion of synchronizing word have been proposed for non-deterministic and probabilistic automata @Burkhard76a [@IS99; @Kfo70; @Shi14], leading to results of PSPACE-completeness @Martyugin14, or even undecidability @Kfo70. For probabilistic systems, it is natural to consider infinite input words (i.e., blind strategies) in order to study synchronization at the limit. In particular, almost-sure weakly and strongly synchronizing with blind strategies has been studied @DMS11a and the main result is that the problem of deciding the existence of a blind almost-sure winning strategy is undecidable for weakly synchronizing, and PSPACE-complete for strongly synchronizing @DMS11b [@DMS11Err]. In contrast in this article, for general strategies, we establish the PSPACE-completeness and PTIME-completeness of deciding almost-sure weakly and strongly synchronizing respectively. Synchronization has been studied recently in a variety of classical computation models that extend finite automata, such as timed automata @DJLMS14, weighted automata @Iva14 [@DJLMS14], visibly pushdown automata @CMS16, and register automata @BQS16. Automata with partial observability have been considered to model systems that disclose information along their execution, which can help the synchronizing strategy @LLS14 [@KLLS15]. An elegant extension of the computation tree logic (CTL) has been proposed to express synchronizing properties @CD16. Markov Decision Processes and Synchronizing Properties {#sec:def} ====================================================== A *probability distribution* over a finite set $S$ is a function $d : S \to [0, 1]$ such that $\sum_{s \in S} d(s)= 1$. The *support* of $d$ is the set ${{\sf Supp}}(d) = \{s \in S \mid d(s) > 0\}$. We denote by ${{\cal D}}(S)$ the set of all probability distributions over $S$. Given a set $T\subseteq S$, let $$d(T)=\sum_{s\in T}d(s) \quad\text{ and }\quad \norm{d}_T = {\mathit{max}}_{s\in T} d(s).$$ For $T \neq \emptyset$, the *uniform distribution* on $T$ assigns probability $\frac{1}{\abs{T}}$ to every state in $T$. Given $s \in S$, we denote by $\xi^s$ the *Dirac distribution* on $s$ that assigns probability $1$ to $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 actions, and $\delta: Q \times {{\sf A}}\to {{\cal D}}(Q)$ is a probabilistic transition function. A state $q$ is *absorbing* if $\delta(q,a)$ is the Dirac distribution on $q$ for all actions $a \in {{\sf A}}$. Given state $q\in Q$ and action $a \in {{\sf A}}$, the successor state of $q$ under action $a$ is $q'$ with probability $\delta(q,a)(q')$. Denote by ${{\sf post}}(q,a)$ the set ${{\sf Supp}}(\delta(q,a))$, and given $T \subseteq Q$ let $${{\sf Pre}}(T)= \{q \in Q \mid \exists a \in {{\sf A}}: {{\sf post}}(q, a) \subseteq T\}$$ be the set of states from which there is an action to ensure that the successor state is in $T$. For $k>0$, let ${{\sf Pre}}^k(T) = {{\sf Pre}}({{\sf Pre}}^{k-1}(T))$ with ${{\sf Pre}}^0(T)=T$. Note that the sequence ${{\sf Pre}}^k(T)$ of iterated predecessors is ultimately periodic, precisely there exist $k < k' < 2^{\abs{Q}}$ such that ${{\sf Pre}}^k(T) = {{\sf Pre}}^{k'}(T)$. A *path* in ${{\cal M}}$ is an infinite sequence $\pi = q_0 a_0 q_1 a_1 \dots$ such that $q_{i+1} \in {{\sf post}}(q_{i},a_{i})$ for all $i \geq 0$. A finite prefix $\rho = q_0 a_0 q_1 a_1 \dots q_n$ of a path (or simply a finite path) has length $\abs{\rho}=n$ and last state ${{\sf Last}}(\rho)=q_{n}$. We denote by ${{\sf Path}}({{\cal M}})$ and ${{\sf Pref}}({{\cal M}})$ the set of all paths and finite paths in ${{\cal M}}$ respectively. For the decision problems considered in this article, only the support of the probability distributions in the transition function is relevant (i.e., the exact value of the positive probabilities does not matter); therefore, we can assume that MDPs are encoded as ${{\sf A}}$-labelled transition systems $(Q,R)$ with $R \subseteq Q \times {{\sf A}}\times Q$ such that $(q,a,q') \in R$ is a transition if $q' \in {{\sf post}}(q,a)$. #### Strategies A *randomized strategy* for ${{\cal M}}$ (or simply a strategy) is a function $$\alpha: {{\sf Pref}}({{\cal M}}) \to {{\cal D}}({{\sf A}})$$ that, given a finite path $\rho$, returns a probability distribution $\alpha(\rho)$ over the action set, used to select a successor state $q'$ of $\rho$ with probability $\sum_{a \in {{\sf A}}} \alpha(\rho)(a) \cdot \delta(q,a)(q')$ where $q={{\sf Last}}(\rho)$. A strategy $\alpha$ is *pure* if for all $\rho \in {{\sf Pref}}({{\cal M}})$, there exists an action $a \in {{\sf A}}$ such that $\alpha(\rho)(a)=1$; and *memoryless* if $\alpha(\rho) = \alpha(\rho')$ for all $\rho, \rho'$ such that ${{\sf Last}}(\rho) = {{\sf Last}}(\rho')$. We view pure strategies as functions $\alpha: {{\sf Pref}}({{\cal M}})\to {{\sf A}}$, and memoryless strategies as functions $\alpha: Q \to {{\cal D}}({{\sf A}})$. Finally, a strategy $\alpha$ uses *finite-memory* if it can be represented by a finite-state transducer $T = {\langle {{\sf Mem}},m_0, \alpha_u, \alpha_n \rangle}$ where ${{\sf Mem}}$ is a finite set of modes (the memory of the strategy), $m_0 \in {{\sf Mem}}$ is the initial mode, $\alpha_u: {{\sf Mem}}\times ({{\sf A}}\times Q) \to {{\sf Mem}}$ is an update function that, given the current memory, last action, and state updates the memory, and $\alpha_n: {{\sf Mem}}\times Q \to {{\cal D}}({{\sf A}})$ is a next-move function that selects the probability distribution $\alpha_n(m,q)$ over actions when the current mode is $m$ and the current state of ${{\cal M}}$ is $q$. For pure strategies, we assume that $\alpha_n: {{\sf Mem}}\times Q \to {{\sf A}}$. The *memory size* of the strategy is the number $\abs{{{\sf Mem}}}$ of modes. For a finite-memory strategy $\alpha$, let ${{\cal M}}(\alpha)$ be the Markov chain obtained as the product of ${{\cal M}}$ with the transducer defining $\alpha$. State-based semantics --------------------- In the traditional state-based semantics, given an initial distribution $d_0 \in {{\cal D}}(Q)$ and a strategy $\alpha$ in an MDP ${{\cal M}}$, a *path-outcome* is a path $\pi = q_0 a_0 q_1 a_1 \dots$ in ${{\cal M}}$ such that $q_0 \in {{\sf Supp}}(d_0)$ and $a_i \in {{\sf Supp}}(\alpha(q_0 a_0 \dots q_i))$ for all $i \geq 0$. The probability of a finite prefix $\rho = q_0 a_0 q_1 a_1 \dots q_n$ of $\pi$ is $$d_0(q_0) \cdot \prod_{j=0}^{n-1} \alpha(q_0 a_0\dots q_j)(a_j) \cdot \delta(q_j,a_j)(q_{j+1}).$$ We denote by ${\mathit{Outcome}}(d_0,\alpha)$ the set of all path-outcomes from $d_0$ under strategy $\alpha$. An *event* $\Omega \subseteq {{\sf Path}}({{\cal M}})$ is a measurable set of paths, and given an initial distribution $d_0$ and a strategy $\alpha$, the probability $Pr^{\alpha}(\Omega)$ of $\Omega$ is uniquely defined @Vardi-focs85. We consider the following classical winning modes. Given an initial distribution $d_0$ and an event $\Omega$, we say that ${{\cal M}}$ is: *sure winning* if there exists a strategy $\alpha$ such that ${\mathit{Outcome}}(d_0,\alpha) \subseteq \Omega$; *almost-sure winning* if there exists a strategy $\alpha$ such that $\Pr^{\alpha}(\Omega) = 1$; *limit-sure winning* if $\sup_{\alpha} \Pr^{\alpha}(\Omega) = 1$, that is the event $\Omega$ can be realized with probability arbitrarily close to $1$. Given a set $T \subseteq Q$ of target states, and $k \in {\mathbb N}$, we define the following events: - $\Box T = \{q_0 a_0 q_1 \dots \in {{\sf Path}}({{\cal M}}) \mid \forall i: q_i \in T\}$ the safety event of always staying in $T$; - $\Diamond T = \{q_0 a_0 q_1 \dots \in {{\sf Path}}({{\cal M}}) \mid \exists i: q_i \in T\}$ the event of reaching $T$; - $\Diamond^{k}\, T = \{q_0 a_0 q_1 \dots \in {{\sf Path}}({{\cal M}}) \mid q_k \in T \}$ the event of reaching $T$ after exactly $k$ steps; - $\Diamond^{\leq k}\, T = \bigcup_{j \leq k} \Diamond^{j}\, T$ the event of reaching $T$ within at most $k$ steps. For example, if $\Pr^{\alpha}(\Diamond T)=1$ then almost-surely a state in $T$ is reached under strategy $\alpha$. It is known for reachability objectives $\Diamond T$, that an MDP is almost-sure winning if and only if it is limit-sure winning, and the set of initial distributions for which an MDP is sure (resp., almost-sure or limit-sure) winning can be computed in polynomial time @deAlfaro97. Distribution-based semantics {#sec:distribution-based-semantice} ---------------------------- In contrast to the state-based semantics, we consider a symbolic outcome of MDPs viewed as generators of sequences of probability distributions over states @KVAK10. Given an initial distribution $d_0 \in {{\cal D}}(Q)$ and a strategy $\alpha$ in ${{\cal M}}$, the *symbolic outcome* of ${{\cal M}}$ from $d_0$ is the sequence $({{\cal M}}^{\alpha}_n)_{n\in {\mathbb N}}$ of probability distributions defined by ${{\cal M}}^{\alpha}_k(q) = Pr^{\alpha}(\Diamond^{k}\, \{q\})$ for all $k \geq 0$ and $q \in Q$. Hence, ${{\cal M}}^{\alpha}_k$ is the probability distribution over states after $k$ steps under strategy $\alpha$. Note that ${{\cal M}}^{\alpha}_0 = d_0$ and the symbolic outcome is a deterministic sequence of distributions: each distribution ${{\cal M}}^{\alpha}_k$ has a unique (deterministic) successor. Informally, synchronizing objectives require that the probability of some state (or some group of states) tends to $1$ in the sequence $({{\cal M}}^{\alpha}_n)_{n\in {\mathbb N}}$, either always, once, infinitely often, or always after some point. Given a set $T \subseteq Q$, consider the functions $$\begin{array}{l} {\mathit{sum}}_T: {{\cal D}}(Q) \to [0,1] \ \text{ defined by } {\mathit{sum}}_T(d) = \sum_{q \in T} d(q), \text{ and} \\[3pt] {\mathit{max}}_T: {{\cal D}}(Q) \to [0,1] \ \text{ defined by } {\mathit{max}}_T(d) = \max_{q \in T} d(q).\\ \end{array}$$ For $f \in \{{\mathit{sum}}_T,{\mathit{max}}_T\}$ and $p \in [0,1]$, we say that a probability distribution $d$ is $p$-synchronized according to $f$ if $f(d) \geq p$, and that a sequence $\bar{d} = d_0 d_1 \dots$ of probability distributions is: - *always $p$-synchronizing* if $d_i$ is $p$-synchronized for all $i \geq 0$; - *event* (or *eventually*) *$p$-synchronizing* if $d_i$ is $p$-synchronized for some $i \geq 0$; - *weakly $p$-synchronizing* if $d_i$ is $p$-synchronized for infinitely many $i$'s; - *strongly $p$-synchronizing* if $d_i$ is $p$-synchronized for all but finitely many $i$'s. For $p=1$, these definitions are analogous to the traditional safety, reachability, Büchi, and coBüchi conditions @ConcOmRegGames. In this article, we consider the following winning modes where either $p=1$, or $p$ tends to $1$ (we do not consider $p < 1$, see the discussion in Section \[sec:conclusion\]). Given an initial distribution $d_0$ and a function $f \in \{{\mathit{sum}}_T,{\mathit{max}}_T\}$, 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 $\alpha$ such that the symbolic outcome of $\alpha$ from $d_0$ is {always, eventually, weakly, strongly} $1$-synchronizing according to $f$; - *almost-sure winning* if there exists a strategy $\alpha$ such that for all $\epsilon>0$ the symbolic outcome of $\alpha$ from $d_0$ is {always, eventually, weakly, strongly} $(1-\epsilon)$-synchronizing according to $f$; - *limit-sure winning* if for all $\epsilon>0$, there exists a strategy $\alpha$ such that the symbolic outcome of $\alpha$ from $d_0$ is {always, eventually, weakly, strongly} $(1-\epsilon)$-synchronizing according to $f$; Note that the winning modes for synchronizing objectives differ from the traditional winning modes in MDPs: synchronizing objectives specify sequences of distributions, in a deterministic transition system with infinite state space (the states are the probability distributions). Since the transitions are deterministic and the probabilities are embedded in the state space, the behavior of the system is non-stochastic and the specification is simply a set of sequences (of distributions). In contrast, the traditional almost-sure and limit-sure winning modes of MDPs specify probability measures over sequences of states (called paths) in a probabilistic system with finite state space. Since the probabilities influence the transitions, the behavior of the system is stochastic and the specification is a set of probability measures over paths. For instance almost-sure reachability requires that the probability measure of *all* paths that visit a target state is $1$, while almost-sure eventually synchronizing requires that the *single* symbolic outcome belongs to the set of sequences of distributions that are $(1-\epsilon)$-synchronizing for all $\epsilon>0$. We often write $\norm{d}_T$ instead of ${\mathit{max}}_T(d)$ (and we omit the subscript when $T=Q$) and $d(T)$ instead of ${\mathit{sum}}_T(d)$, as in Table \[tab:def-modes\] where the definitions of the various winning modes and synchronizing objectives for $f={\mathit{sum}}_T$ are summarized. Membership problem ------------------ For $f \in \{{\mathit{sum}}_T,{\mathit{max}}_T\}$ and $\lambda \in \{always, event, weakly, strongly\}$, the *winning region* ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{\lambda}}}(f)$ is the set of initial distributions such that ${{\cal M}}$ is sure winning for $\lambda$-synchronizing (we assume that ${{\cal M}}$ is clear from the context). We define analogously the sets ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{\lambda}}}(f)$ and ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{limit}}^{\mathit{\lambda}}}(f)$ of almost-sure and limit-sure winning distributions. By an abuse of notation, if a Dirac distribution $\xi^q$ belongs to ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}(f)$, we often write $q \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}(f)$ instead of $\xi^q \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}(f)$. For a singleton $T = \{q\}$ we have ${\mathit{sum}}_{T} = {\mathit{max}}_{T}$, and we simply write ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}(q)$ (where $\mu \in \{sure, almost, limit\}$). We are interested in the algorithmic complexity of the *membership problem*, which is to decide, given a probability distribution $d_0$ and a function $f$, whether $d_0 \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}(f)$. We show that the winning region is identical for always synchronizing in the three winning modes (Lemma \[lem:always\]), whereas for eventually synchronizing, the winning regions of the three winning modes are in general different (Lemma \[lem:dif-in-def\]). \[rem:expressiveness\] First, note that it follows from the definitions that for all $f \in \{{\mathit{sum}}_T,{\mathit{max}}_T\}$, for all $\lambda \in \{always, event, weakly, strongly\}$, and all $\mu \in \{sure, almost, limit\}$: - ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{always}}}(f) \subseteq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{strongly}}}(f) \subseteq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{weakly}}}(f) \subseteq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{event}}}(f)$, and - ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{\lambda}}}(f) \subseteq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{\lambda}}}(f) \subseteq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{limit}}^{\mathit{\lambda}}}(f)$. \[lem:always\] Let $T$ be a set of states. For all functions $f \in \{{\mathit{max}}_T, {\mathit{sum}}_T\}$, we have ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{always}}}(f) = {\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{always}}}(f) = {\langle \! \langle 1 \rangle \! \rangle_{\mathit{limit}}^{\mathit{always}}}(f)$. By Remark \[rem:expressiveness\], we obtain a cyclic chain of inclusions (thus an overall equality) if we show that $${\langle \! \langle 1 \rangle \! \rangle_{\mathit{limit}}^{\mathit{always}}}(f) \subseteq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{always}}}(f),$$ that is for all distributions $d_0$, if ${{\cal M}}$ is limit-sure always synchronizing from $d_0$, then ${{\cal M}}$ is sure always synchronizing from $d_0$. For $f={\mathit{max}}_T$, consider $\epsilon$ smaller than the smallest positive probability in the initial distribution $d_0$ and in the transitions of the MDP ${{\cal M}}= {\langle Q,{{\sf A}},\delta \rangle}$. If ${{\cal M}}$ is limit-sure always synchronizing, then by definition there exists an always $(1-\epsilon)$-synchronizing strategy $\alpha$, and it is easy to show by induction on $k$ that the distributions ${{\cal M}}^{\alpha}_k$ are Dirac for all $k \geq 0$. In particular $d_0$ is Dirac, and let $q_{{{\sf init}}} \in T$ be such that $d_0(q_{{{\sf init}}})=1$. It follows that there is an infinite path from $q_{{{\sf init}}}$ in the graph ${\langle T,E \rangle}$ where $(q,q') \in E$ if there exists an action $a \in {{\sf A}}$ such that $\delta(q,a)(q') = 1$. The existence of this path entails that there is a loop reachable from $q_{{{\sf init}}}$ in the graph ${\langle T,E \rangle}$, and this naturally defines a sure-winning always synchronizing strategy in ${{\cal M}}$. A similar argument for $f={\mathit{sum}}_T$ shows that for sufficiently small $\epsilon$, an always $(1-\epsilon)$-synchronizing strategy $\alpha$ must produce a sequence of distributions with support contained in $T$, until some support repeats in the sequence. This naturally induces an always $1$-synchronizing strategy. The results established in this article will entail that the almost-sure and limit-sure modes coincide for weakly and strongly synchronizing (see Theorem \[theo:weakly-ls-is-as\], Corollary \[col: almost-limit-strong\], and Corollary \[col: almost-limit-strong-sum\]). The other winning regions are distinct, as shown in the following lemma. \[lem:dif-in-def\] There exists an MDP ${{\cal M}}$ and states $q_1,q_2$ such that: --------- -------- ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- $(i)$ ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{\lambda}}}(q_1) \subsetneq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{\lambda}}}(q_1)$ for all $\lambda \in \{event, weakly, strongly\}$, and \[4pt\] $(ii)$ ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{event}}}(q_2) \subsetneq {\langle \! \langle 1 \rangle \! \rangle_{\mathit{limit}}^{\mathit{event}}}(q_2)$. --------- -------- ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Consider the MDP ${{\cal M}}$ with states $q_{{{\sf init}}}, q_1, q_2, q_3$ and actions $a,b$ as shown in \[fig:almost-limit-eventually-differ\]. All transitions are deterministic except from $q_{{{\sf init}}}$ where on all actions, the successors are $q_{{{\sf init}}}$ and $q_1$ with probability $\frac{1}{2}$. To establish $(i)$, it is sufficient to prove that $$q_{{{\sf init}}} \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{strongly}}}(q_1) \ \text{ and }\ q_{{{\sf init}}} \not \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{event}}}(q_1),$$ because, by Remark \[rem:expressiveness\], it implies that $$q_{{{\sf init}}} \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{\lambda}}}(q_1) \ \text{ and }\ q_{{{\sf init}}} \not \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{\lambda}}}(q_1) \text{ for all } \lambda \in \{event, weakly, strongly\},$$ establishing all strict mcollins@example.org. To prove that $q_{{{\sf init}}} \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{almost}}^{\mathit{strongly}}}(q_1)$, consider the pure strategy that always plays $a$. The outcome is such that the probability to be in $q_1$ after $k$ steps is $1-\frac{1}{2^k}$, showing that ${{\cal M}}$ is almost-sure winning for the strongly synchronizing objective in $q_1$ (from $q_{{{\sf init}}}$). On the other hand, $q_{{{\sf init}}} \not \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{sure}}^{\mathit{event}}}(q_1)$ because for all strategies $\alpha$, the probability in $q_{{{\sf init}}}$ remains always positive, and thus in $q_1$ we have ${{\cal M}}^{\alpha}_n(q_1) < 1$ for all $n \geq 0$, showing that ${{\cal M}}$ is not sure winning for the eventually synchronizing objective in $q_1$ (from $q_{{{\sf init}}}$). To establish $(ii)$, we first show that ${{\cal M}}$ is limit-sure winning for the eventually synchronizing objective in $q_2$ (from $q_{{{\sf init}}}$): for $k \geq 0$ consider a strategy that plays $a$ for $k$ steps, and then plays $b$. Then the probability to be in $q_2$ after $k+1$ steps is $1-\frac{1}{2^k}$, showing that this strategy is eventually $(1-\frac{1}{2^k})$-synchronizing in $q_2$. Second, we show that almost-sure eventually synchronizing is impossible because, to get probability $1-\epsilon$ in $q_2$, the probability mass needs to accumulate for more and more steps in $q_1$ as $\epsilon$ gets smaller, which cannot be achieved by a single strategy. Formally, for all strategies, since the probability in $q_{{{\sf init}}}$ remains always positive, the probability in $q_2$ is always smaller than $1$. Moreover, if the probability $p$ in $q_2$ is positive after $n$ steps ($p>0$), then after any number $m > n$ of steps, the probability in $q_2$ is bounded by $1-p < 1$. It follows that the probability in $q_2$ is never equal to $1$ and cannot tend to $1$ for $m \to \infty$, showing that ${{\cal M}}$ is not almost-sure winning for the eventually synchronizing objective in $q_2$ (from $q_{{{\sf init}}}$). Finally, for eventually and weakly synchronizing we present in Lemma \[lem:weakly-max-sum\] a reduction of the membership problem with function ${\mathit{max}}_T$ to the membership problem with function ${\mathit{sum}}_{T'}$ for a singleton ${T'}$. It follows that the complexity results established in this article for eventually and weakly synchronizing with function ${\mathit{sum}}_{T}$ also hold with function ${\mathit{max}}_{T}$ (this is trivial for the upper bounds, and for the lower bounds it follows from the fact that our hardness results hold for ${\mathit{sum}}_{T}$ with singleton $T$, and thus for ${\mathit{max}}_{T}$ as well since in this case ${\mathit{sum}}_{T} = {\mathit{max}}_{T}$). \[lem:weakly-max-sum\] For eventually and weakly synchronizing, in each winning mode the following problems are polynomial-time equivalent: - the membership problem with a function ${\mathit{max}}_T$ where $T$ is an arbitrary subset of the state space, and - the membership problem with a function ${\mathit{sum}}_{T'}$ where $T'$ is a singleton. Let $\mu \in \{sure, almost, limit\}$ and $\lambda \in \{event, weakly\}$. First we have ${\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}({\mathit{max}}_T) = \bigcup_{q \in T} {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}(q)$, showing that the membership problems for ${\mathit{max}}$ and ${\mathit{max}}_T$ are polynomial-time reducible to the corresponding membership problem for ${\mathit{sum}}_{T'}$ with singleton $T'$. The reverse reduction is as follows. Given an MDP ${{\cal M}}$, a state $q$ and an initial distribution $d_0$, we can construct an MDP ${{\cal M}}'$ and initial distribution $d'_0$ such that $d_0 \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}(q)$ iff $d'_0 \in {\langle \! \langle 1 \rangle \! \rangle_{\mathit{\mu}}^{\mathit{\lambda}}}({\mathit{max}}_{Q'})$ where $Q'$ is the state space of ${{\cal M}}'$ (thus ${\mathit{max}}_{Q'}$ is simply the function $\max$). The idea is to construct ${{\cal M}}'$ and $d'_0$ as a copy of ${{\cal M}}$ and $d_0$ where all states except $q$ are duplicated, and the initial and transition probabilities are equally distributed between the copies (see \[fig:twin\]). Therefore, if the probability tends to $1$ in some state, it has to be in $q$ (since the probability in any other state of ${{\cal M}}'$ can be at most $1/2$). The rest of this article is devoted to the solution of the membership problem. By definition, a sequence of probability distribution is sure always synchronizing according to ${\mathit{sum}}_T$ if all supports are contained in $T$, i.e., all states in all path-outcomes are in $T$, that is all path-outcomes are contained in $\Box T$. Hence, it follows from the proof of Lemma \[lem:always\] that the winning region for always synchronizing according to ${\mathit{sum}}_T$ coincides with the set of winning initial distributions for the safety objective $\Box T$ in the traditional semantics, which can be computed in polynomial time @CH12. Moreover, always synchronizing according to ${\mathit{max}}_T$ is equivalent to the existence of an infinite path staying in $T$ in the transition system ${\langle Q,R \rangle}$ of the MDP restricted to transitions $(q,a,q') \in R$ such that $\delta(q,a)(q')=1$, which can also be decided in polynomial time. In both cases, pure memoryless strategies are sufficient. \[theo:always\] The membership problem for always synchronizing can be solved in polynomial time, and pure memoryless strategies are sufficient. \[rmk:Dirac-initial-suffices\] For the other synchronizing modes (eventually, weakly, and strongly synchronizing), it is sufficient to consider Dirac initial distributions (i.e., assuming that MDPs have a single initial state) because the answer to the general membership problem for an MDP ${{\cal M}}$ with initial distribution $d_0$ can be obtained by solving the membership problem for a copy of ${{\cal M}}$ with a new initial state from which the successor distribution on all actions is $d_0$. Always Eventually Weakly Strongly ------------- --------- ------------ ---------- ---------- Sure PSPACE-C PSPACE-C PTIME-C Almost-sure PTIME-C PSPACE-C Limit-sure PSPACE-C : Computational complexity of the membership problem.\[tab:complexity\] In the rest of the article, we present algorithms to decide the membership problem and we establish matching upper and lower bounds for the complexity of the problem: we show that eventually and weakly synchronizing are PSPACE-complete, whereas strongly synchronizing is PTIME-complete (like always synchronizing). We also establish optimal memory bounds for the memory needed by strategies to win. Our results will show that pure strategies are sufficient in all modes. The complexity results are summarized in Table \[tab:complexity\], and we present the memory requirement for winning strategies in Table \[tab:memory\]. <span> </span> One-Letter Alternating Automata {#sec:1L-AFA} ------------------------------- In this section, we consider one-letter alternating automata (1L-AFA) and show a tight connection with MDP. We present complexity results for 1L-AFA that are useful to establish the PSPACE lower bounds for eventually and weakly synchronizing in MDPs (in Theorem \[theo:sure-eventually-pspace-c\], Lemma \[lem:as-event-pspace-hard\], \[lem:limit-event-pspace-hard\], and \[lem: sure-weakly-psapce-hradness\]). In 1L-AFA, the alphabet is a singleton, and thus only the length of a word is relevant. The transitions of an alternating automaton are described by Boolean formulas over the set of automaton states using only $\land$ and $\lor$ (but no negation). For example, if the formula $(q_2 \land q_3) \lor q_4$ describes the transitions from a state $q_1$, then the word of length $n$ is accepted from $q_1$ if the word of length $n-1$ is accepted either from both $q_2$ and $q_3$, or from $q_4$. #### One-letter alternating automata {#one-letter-alternating-automata} Let ${{\sf B}^+}(Q)$ be the set of positive Boolean formulas over a set $Q$, i.e. Boolean formulas built from elements in $Q$ using $\land$ and $\lor$ (but no negation). A set $S \subseteq Q$ *satisfies* a formula $\varphi \in {{\sf B}^+}(Q)$ (denoted $S \models \varphi$) if $\varphi$ is satisfied when replacing in $\varphi$ the elements in $S$ by <span><span>true</span></span>, and the elements in $Q \setminus S$ by <span><span>false</span></span>. A *one-letter alternating finite automaton* is a tuple ${{\cal A}}={\langle Q,\delta_{{{\cal A}}},{{\cal F}}\rangle}$ where $Q$ is a finite set of states, $\delta_{{{\cal A}}}: Q \to {{\sf B}^+}(Q)$ is the transition function, and ${{\cal F}}\subseteq Q$ is the set of accepting states. We assume that the formulas in transition function are in disjunctive normal form. Note that the alphabet of the automaton is omitted, as it consists of a single letter. As in the language of a 1L-AFA, only the length of words is relevant, define for all $n\geq 0$, the set $Acc_{{{\cal A}}}(n,{{\cal F}}) \subseteq Q$ of states from which the word of length $n$ is accepted by ${{\cal A}}$ as follows: - $Acc_{{{\cal A}}}(0,{{\cal F}}) = {{\cal F}}$; - $Acc_{{{\cal A}}}(n,{{\cal F}}) = \{q \in Q \mid Acc_{{{\cal A}}}(n-1,{{\cal F}}) \models \delta(q) \}$ for all $n > 0$. The set ${{\cal L}}({{\cal A}}_q) = \{n \in {\mathbb N}\mid q \in Acc_{{{\cal A}}}(n,{{\cal F}})\}$ is the *language* accepted by ${{\cal A}}$ from state $q$ (called *initial* state in this context). \[b\]<span>0.46</span> ------------------------------------------------------------------------ ------------------------------------------------------------------------ \[b\]<span>0.53</span> ------------------------------------------------------------------------ ------------------------------------------------------------------------ #### Example Consider the 1L-AFA ${{\cal A}}$ in \[fig:afa-AFA\] with initial state $q_{{{\sf init}}}$. Transition function is defined by $\delta_{{{\cal A}}}(q_{{{\sf init}}}) = q_1 \land q_2$ and $\delta_{{{\cal A}}}(q_{1}) = (q_{{{\sf init}}} \land q_2) \lor (q_2 \land q_3)$, etc. The word of length $3$ is accepted by ${{\cal A}}$, as witnessed by the execution tree in \[fig:afa-tree\]: for every node of the tree (let $q$ be its label), the labels of the successor nodes form a set that satisfies the transition function at $q$. The root of the tree is labeled by $q_{{{\sf init}}}$ and all leaves are accepting. Note that all branches are of the same length, namely $3$, the length of the input word. For every 1L-AFA with $n$ states, there is an equivalent deterministic automaton with at most $2^n$ states (that accepts the same language), which can be constructed as follows @CKS81. It is easier to think that the deterministic automaton accepts the *reverse* image of the words in the language of ${{\cal A}}$, which is the same as the language of ${{\cal A}}$. For all $n \geq 1$, we view $Acc_{{{\cal A}}}(n,\cdot)$ as an operator on $2^Q$ that, given a set ${{\cal F}}\subseteq Q$ computes the set $Acc_{{{\cal A}}}(n,{{\cal F}})$. Note that $Acc_{{{\cal A}}}(n,{{\cal F}}) = Acc_{{{\cal A}}}(1,Acc_{{{\cal A}}}(n-1,{{\cal F}}))$ for all $n \geq 1$. Call $Acc_{{{\cal A}}}(1,s)$ the *predecessor* of $s$. The deterministic automaton has state space $\{s_0,\dots,s_{2^n} \}$ where $s_i = Acc_{{{\cal A}}}(i,{{\cal F}})$, and a deterministic transition from $s_i$ to its predecessor $Acc_{{{\cal A}}}(1,s_i)$. The sequence of predecessors for the 1L-AFA of \[fig:afa-AFA\] is shown in \[fig:afa-pred\]. It is easy to see that this sequence is always ultimately periodic (for all $k > 2^n$ there exists $k' \leq 2^n$ such that $s_k = s_{k'}$), and therefore the transitions of the deterministic automaton are well defined. Let $s_0 = {{\cal F}}$ be the initial state, and let all $s_i$ such that $q_{{{\sf init}}} \in s_i$ be the accepting states, then its language is ${{\cal L}}({{\cal A}}_{q_{{{\sf init}}}})$. Considering the sequence of predecessors in \[fig:afa-pred\] it is easy to see that the language of ${{\cal A}}$ is the set $\{n > 1 \mid n \text{ is odd}\}$ of odd numbers greater than $1$. Note that the language of ${{\cal A}}$ is nonempty because in the sequence of predecessors there is a state $s$ such that $q_{{{\sf init}}} \in s$, and the language of ${{\cal A}}$ is infinite because there is such a state $s$ in the periodic part of the sequence. #### Relation with MDPs Consider the MDP ${{\cal M}}$ in \[fig:afa-mdp\], obtained from ${{\cal A}}$ by transforming the transition function, which is a disjunction of conjunctions of states as follows: each conjunction is replaced by a uniform probability distribution over its elements, and the elements of the disjunction are labeled by a letter from the alphabet of ${{\cal M}}$. The correspondence between 1L-AFA and MDPs is based on the observation that they have the same underlying structure of alternating graph (or AND-OR graph): - the combinatorial structure of an MDP ${\langle Q,{{\sf A}},\delta \rangle}$ can be described as an alternating graph, with *existential* vertices $q \in Q$ with successors $(q,a)$ for all actions $a \in {{\sf A}}$, and *universal* vertices $(q,a) \in Q \times {{\sf A}}$ with successors $q' \in {{\sf Supp}}(\delta(q,a))$; - the structure of a 1L-AFA ${\langle Q,\delta_{{{\cal A}}},{{\cal F}}\rangle}$ is also an alternating graph, where states $q \in Q$ are *existential* vertices with successors the clauses $c_1,\dots,c_m$ such that $\delta_{{{\cal A}}}(q) = c_1 \lor \dots \lor c_m$ where each $c_i$ is a conjunctive clause, and the conjunctive clauses $c_i$ are *universal* vertices with successors the states that belong to $c_i$. The common structure of 1L-AFA and MDP is illustrated in \[fig:AFA\] where we show only the existential vertices. The correspondence is defined formally as follows. Given a 1L-AFA ${{\cal A}}= {\langle Q, \delta_{{{\cal A}}}, {{\cal F}}\rangle}$, assume without loss of generality that the transition function $\delta_{{{\cal A}}}$ is such that $\delta_{{{\cal A}}}(q) = c_1 \lor \dots \lor c_m$ has the same number $m$ of conjunctive clauses for all $q \in Q$ (we can duplicate clauses if necessary). From ${{\cal A}}$, construct the MDP ${{\cal M}}_{{{\cal A}}} = {\langle Q, {{\sf A}}, \delta_{{{\cal M}}} \rangle}$ where ${{\sf A}}= \{a_1, \dots, a_m\}$ and $\delta_{{{\cal M}}}(q,a_k)$ is the uniform distribution over the states occurring in the $k$-th clause $c_k$ in $\delta_{{{\cal A}}}(q)$, for all $q \in Q$ and $a_k \in {{\sf A}}$. Then, we have $Acc_{{{\cal A}}}(n,{{\cal F}}) = {{\sf Pre}}_{{{\cal M}}}^n({{\cal F}})$ for all $n \geq 0$. Similarly, from an MDP ${{\cal M}}$ and a set $T$ of states, we can construct a 1L-AFA ${{\cal A}}= {\langle Q, \delta_{{{\cal A}}}, {{\cal F}}\rangle}$ with ${{\cal F}}= T$ such that $Acc_{{{\cal A}}}(n,{{\cal F}}) = {{\sf Pre}}_{{{\cal M}}}^n(T)$ for all $n \geq 0$: let $\delta_{{{\cal A}}}(q) = \bigvee_{a \in {{\sf A}}} \bigwedge_{q' \in {{\sf post}}(q,a)} q'$ for all $q \in Q$. For example, for ${{\sf A}}= \{a,b\}$ if $\delta_{{{\cal M}}}(q_3,a)(q_1) = \delta_{{{\cal M}}}(q_3,a)(q_4) = \frac{1}{2}$ and $\delta_{{{\cal M}}}(q_3,b)(q_5) = 1$, then $\delta_{{{\cal A}}}(q_3) = (q_1 \land q_4) \lor q_5$ (see \[fig:AFA\]). It follows that, up to the correspondence between 1L-AFA and MDPs established above, $Acc_{{{\cal A}}}(n,T) = {{\sf Pre}}_{{{\cal M}}}^n(T)$. In the sequel we denote the operator $Acc_{{{\cal A}}}(1,\cdot)$ by ${{\sf Pre}}_{{{\cal A}}}(\cdot)$ (note the subscript). Then for all $n \geq 0$ the operator $Acc_{{{\cal A}}}(n,\cdot)$ coincides with ${{\sf Pre}}^n_{{{\cal A}}}(\cdot)$, the $n$-th iterate of ${{\sf Pre}}_{{{\cal A}}}(\cdot)$. #### Decision problems Questions related to MDPs have a corresponding formulation in terms of alternating automata. We show that such connections exist between synchronizing problems for MDPs and language-theoretic questions for alternating automata. Several decision problems for 1L-AFA can be solved by computing the sequence $Acc_{{{\cal A}}}(n,{{\cal F}})$ (i.e., ${{\sf Pre}}_{{{\cal A}}}^n({{\cal F}})$), and analogously we show that synchronizing problems for MDPs can also be solved by computing the sequence ${{\sf Pre}}_{{{\cal M}}}^n({{\cal F}})$. Therefore, the above relationship between 1L-AFA and MDPs provides a tight connection that we use in Section \[sec:eventually\] to transfer complexity results between 1L-AFA and MDPs. We review classical decision problems for 1L-AFA, namely the emptiness and finiteness problems, and establish the complexity of a new problem, the *universal finiteness problem* which is to decide if from every initial state the language of a given 1L-AFA is finite. These results of independent interest are useful to establish the PSPACE lower bounds for eventually and weakly synchronizing in MDPs. - The *emptiness problem* for 1L-AFA is to decide, given a 1L-AFA ${{\cal A}}$ and an initial state $q$, whether ${{\cal L}}({{\cal A}}_q)=\emptyset$. The emptiness problem can be solved by checking whether $q \in {{\sf Pre}}^n_{{{\cal A}}}({{\cal F}})$ for some $n \geq 0$. It is known that the emptiness problem is PSPACE-complete, even for transition functions in disjunctive normal form @Holzer95 [@AFA1]. - The *finiteness problem* is to decide, given a 1L-AFA ${{\cal A}}$ and an initial state $q$, whether ${{\cal L}}({{\cal A}}_q)$ is finite. The finiteness problem can be solved in (N)PSPACE by guessing $n,k \leq 2^{\abs{Q}}$ such that ${{\sf Pre}}^{n+k}_{{{\cal A}}}({{\cal F}}) = {{\sf Pre}}^n_{{{\cal A}}}({{\cal F}})$ and $q \in {{\sf Pre}}^n_{{{\cal A}}}({{\cal F}})$. The finiteness problem is PSPACE-complete by a simple reduction from the emptiness problem: from an instance $({{\cal A}},q)$ of the emptiness problem, construct $({{\cal A}}',q')$ where $q'=q$ and ${{\cal A}}' = {\langle Q,\delta',{{\cal F}}\rangle}$ is a copy of ${{\cal A}}= {\langle Q,\delta,{{\cal F}}\rangle}$ with a self-loop on $q$ (formally, $\delta'(q) = q \lor \delta(q)$ and $\delta'(r) = \delta(r)$ for all $r \in Q \setminus \{q\}$). It is easy to see that ${{\cal L}}({{\cal A}}_q)=\emptyset$ iff ${{\cal L}}({{\cal A}}'_{q'})$ is finite. - The *universal finiteness problem* is to decide, given a 1L-AFA ${{\cal A}}$, whether ${{\cal L}}({{\cal A}}_q)$ is finite for all states $q$. This problem can be solved by checking whether ${{\sf Pre}}^n_{{{\cal A}}}({{\cal F}}) = \emptyset$ for some $n \leq 2^{\abs{Q}}$, and thus it is in PSPACE. Note that if ${{\sf Pre}}^n_{{{\cal A}}}({{\cal F}}) = \emptyset$, then ${{\sf Pre}}^m_{{{\cal A}}}({{\cal F}}) = \emptyset$ for all $m \geq n$. Given the PSPACE-hardness proofs of the emptiness and finiteness problems, it is not easy to see that the universal finiteness problem is PSPACE-hard. \[lem:universal-finiteness-pspace-hard\] The universal finiteness problem for 1L-AFA is PSPACE-hard. We show the result by a reduction from the emptiness problem for 1L-AFA, which is PSPACE-complete @Holzer95 [@AFA1]. We first present a basic fact about 1L-AFA, then an overview of the reduction, and a detailed description of the reduction and the correctness argument. <span>*Basic result.*</span> The language of a 1L-AFA ${{\cal A}}= {\langle Q, \delta, {{\cal F}}\rangle}$ from initial state $q_0$ is non-empty if $q_0 \in {{\sf Pre}}_{{{\cal A}}}^i({{\cal F}})$ for some $i\geq 0$. Since the sequence ${{\sf Pre}}_{{{\cal A}}}^i({{\cal F}})$ is ultimately periodic, it is sufficient to compute ${{\sf Pre}}_{{{\cal A}}}^i({{\cal F}})$ for every $i\leq 2^{\abs{Q}}$ to decide emptiness. <span>*Overview of the reduction.*</span> From ${{\cal A}}$, we construct a 1L-AFA $B = {\langle Q', \delta', {{\cal F}}' \rangle}$ with set ${{\cal F}}'$ of accepting states such that the sequence ${{\sf Pre}}_B^i({{\cal F}}')$ in $B$ mimics the sequence ${{\sf Pre}}_{{{\cal A}}}^i({{\cal F}})$ in ${{\cal A}}$ for $2^{\abs{Q}}$ steps. The automaton $B$ contains the state space of ${{\cal A}}$, i.e. $Q \subseteq Q'$. The goal is to have $${{\sf Pre}}_B^i({{\cal F}}') \cap Q = {{\sf Pre}}_{{{\cal A}}}^i({{\cal F}}) \text{ for all } i \leq 2^{\abs{Q}}, \text{ as long as } q_0 \not\in {{\sf Pre}}_{{{\cal A}}}^i({{\cal F}}).$$ Moreover, if $q_0 \in {{\sf Pre}}_{{{\cal A}}}^i({{\cal F}})$ for some $i\geq 0$, then ${{\sf Pre}}_B^j({{\cal F}}')$ will contain $q_0$ for all $j\geq i$ (the state $q_0$ has a self-loop in $B$), and if $q_0 \not\in {{\sf Pre}}{{{\cal A}}}^i({{\cal F}})$ for all $i\geq 0$, then $B$ is constructed such that ${{\sf Pre}}_B^j({{\cal F}}') = \emptyset$ for sufficiently large $j$ (roughly for $j > 2^{\abs{Q}}$). Hence, the language of ${{\cal A}}$ is non-empty if and only if the sequence ${{\sf Pre}}_B^j({{\cal F}}')$ is not ultimately empty, that is if and only if the language of $B$ is infinite from some state (namely $q_0$). <span>*Detailed reduction.*</span> The key is to let $B$ simulate ${{\cal A}}$ for exponentially many steps, and to ensure that the simulation stops if and only if $q_0$ is not reached within $2^{\abs{Q}}$ steps. We achieve this by defining $B$ as the gadget in \[fig:pre-empty-reduction2\] connected to a modified copy ${{\cal A}}'$ of ${{\cal A}}$ with the same state space. The transitions in ${{\cal A}}'$ are defined as follows, where $x$ is the entry state of the gadget (see \[fig:pre-empty-reduction\]): for all $q \in Q$ let $(i)$ $\delta_{B}(q) = x \land \delta_{{{\cal A}}}(q)$ if $q \neq q_0$, and $(ii)$ $\delta_{B}(q_0) = q_0 \lor (x \land \delta_{{{\cal A}}}(q_0))$. Thus, $q_0$ has a self-loop, and given a set $S \subseteq Q$ in the automaton ${{\cal A}}$, if $q_0 \not\in S$, then ${{\sf Pre}}_{{{\cal A}}}(S) = {{\sf Pre}}_B(S \cup \{x\})$ that is ${{\sf Pre}}_B$ mimics ${{\sf Pre}}_{{{\cal A}}}$ when $x$ is in the argument (and $q_0$ has not been reached yet). Note that if $x \not\in S$ (and $q_0 \not\in S$), then ${{\sf Pre}}_B(S) = \emptyset$, that is unless $q_0$ has been reached, the simulation of ${{\cal A}}$ by $B$ stops. Since we need that $B$ mimics ${{\cal A}}$ for $2^{\abs{Q}}$ steps, we define the
{'source': 'arXiv_out/1604'}