Optimally Controlling a Random Population

Gimbert, Hugo; Mascle, Corto; Totzke, Patrick

doi:10.4230/LIPIcs.ICALP.2026.180

Optimally Controlling a Random Population

Hugo Gimbert

CNRS, LaBRI, Université de Bordeaux, Talence, France Corto Mascle

Max Planck Institute for Software Systems, Kaiserslautern, Germany Patrick Totzke

University of Liverpool, UK

Abstract

The population control problem is a parameterised problem where a controller sends messages to a whole population of identical finite-state agents, aiming to eventually move them all into a target state. The decision problem asks whether this can be achieved for arbitrarily large finite populations. We focus on the randomised version of this problem, where every agent is a copy of the same finite Markov Decision Process and non-determinism in the global action chosen by the controller is resolved independently and uniformly at random. Colcombet, Fijalkow and Ohlmann [6] showed that this problem is decidable, but without any complexity upper bound. We show that the random population control problem is in fact ExpTime-complete.

Keywords and phrases:

Controller synthesis, Parameterized verification

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Funding:

Patrick Totzke: EPSRC, grant no.: EP/X042596/1.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Formal languages and automata theory

Editors:

Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

We place $N$ tokens on the initial state of a non-deterministic finite automaton and update their positions in rounds, in each of which a Controller selects a letter $a$ and then every token moves along an $a$ -labelled edge out of its current state. The goal for the Controller is to eventually synchronise all tokens, gathering them into accepting states at the same time. Naturally, increasing $N$ can only make this task more difficult. The decision question we study asks whether, for a given automaton, can the Controller succeed for all values of $N$ ?

This population control problem has been studied both in the adversarial and random settings, which differ in how agents resolve choices and what guarantees the Controller is after. In the adversarial setting, an antagonistic environment resolves all agents’ choices, trying to frustrate Controller and avoid synchronisation. Bertrand et al. [3, 4] showed that the adversarial population control problem is decidable and ExpTime-complete.

In the random setting, all agents’ choices are made uniformly at random and the Controller aims to synchronise the agents almost surely, with probability one.

Figure 1: An automaton for which Controller wins against a random environment but not an adversarial one. The initial and target states are

s_{0}

and

s_{4}

, respectively. Not shown, but implicitly present is a sink state, to which all states move on actions not shown (

b

from

s_{2}

and

a

from

s_{3}

).

Example 1.

Controller loses the adversarial population control game from Figure 1. For example, the opponent can win by keeping all tokens in the initial state in every round.

However, Controller does have a winning strategy for the corresponding random population control game: Regardless of the size $N$ of the population, she plays the action $a$ until exactly one token is in $s_{1}$ , which happens eventually with probability $1$ . She then plays $b$ followed by either $a$ (if the isolated token moved to $s_{2}$ ) or $b$ (if the token moved to $s_{3}$ ) to send that token to the final state. She can repeat this procedure until all tokens are in the target. Note that if instead she plays $b$ while more than one token is in $s_{1}$ then some of them may spread simultaneously to $s_{2}$ and $s_{3}$ and she is stuck: whatever action she plays, at least one token will move to the (invisible) sink state and cannot be recovered.

The random population control problem is ExpTime-hard [14] and decidable [6]. Colcombet et al.’s decision procedure is based on two ingredients [6]:

$\blacksquare$

First, winning regions are downward-closed with respect to the natural product order on $\mathbb{N}^{S}$ and can therefore be finitely represented and manipulated as a union of ideals.
$\blacksquare$

The second ingredient is solving the sequential flow problem, which asks whether an unbounded number of tokens can be moved from one set of states to another, while respecting capacity constraints on the number of tokens occupying each transition. They show that one can compute the full corresponding pre-set of a given downward-closed set of target configurations, by a reduction to the boundedness problem of nested distance-desert automata [13].

Ultimately, this allows one to compute a representation of the winning region by iterative refinement. The main limitation of this approach is that the bounds on the representation of intermediate sets, and termination of the resulting algorithm rely on well-quasi-orders and therefore only provide a non-elementary upper bound.

Our Contribution.

We show that the random population control problem is ExpTime-complete. As in [6], our upper bound relies on symbolic representations. However, instead of computing the whole winning region, we show that one can witness positive instances already with a potentially smaller, more compactly representable subset (Theorem 7). Computing this in exponential time requires solving what we call the Dynamic flow problem, which asks whether we can transfer arbitrarily many tokens, with positive probability, from an initial configuration to the set of final configurations while staying in a given set of safe configurations. It is closely related to the sequential flow problem defined in [6]. For this we rely on a recent result showing that a closely-related problem is decidable in PSPACE [10], which we adapt to our setting.

We also include the original, previously unpublished lower bound [14] (Theorem 21).

Related work.

Models for biological, chemical, or computational systems with large crowds of simple finite-state components include Petri nets [16], population protocols [2], or chemical reaction networks [21].

Population control problems provide a formal framework for the design of strategies to control a large number of identical agents. This formalisation was introduced in [4], as a model for the synchronization of large populations of yeasts [23]. It fits into parameterized verification, a line of research that aims to verify distributed protocols over arbitrarily large networks [20, 8]. While we take a discrete approach, in the sense that we have an integral number of agents, other models have been studied where the number is considered so large that it can be abstracted by a continuous probability distribution [1, 7].

Another model close to our setting is explorable automata [11], which generalise both (adversarial) population control problems and history-deterministic automata on infinite words. Closer to our setting, other models of games parameterized by the number of agents exist, typically aiming to synthesize distributed protocols for arbitrarily large networks [5, 22]. Finally, recent works bridge the adversarial setting for population control to the modern study of history-deterministic automata: They introduce explorability games, played on automata on infinite words. A player gives an input letter by letter, while the other player has to move tokens in the state space of the automaton so that one of them finds an accepting run whenever the input word is in the language of the automaton [11].

We omit part of the proofs due to space constraints; missing proofs can be found in the full version of the paper.

2 Preliminaries

We assume familiarity with automata theory [18] and Markov Decision Processes [17], and proceed to recall some necessary notations.

Markov decision processes.

A Markov decision process (MDP) $\mathcal{M}=(S,\Sigma,\Delta)$ consists of a set $S$ of states, $\Sigma$ a set of actions, and a transition function $\Delta:S\times\Sigma\to{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.1875,0.3125}\mathpzc{Dist}}(S)$ , where $\immediate\immediate\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}% \definecolor[named]{pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}\mathpzc% {Dist}}(S)$ denotes the set of probability distributions over $S$ .

We consider almost-sure reachability objectives, given by a set $F\subseteq S$ of target states that Controller aims to visit. A strategy is a function $\sigma:S\to{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\mathpzc{Dist}}(\Sigma)$ . Fixing such a strategy $\sigma$ and an initial state $s\in S$ results in a Markov Chain with probability measure $\mathbb{P}_{\sigma,s}$ (see [17] for details). We call $\sigma$ winning from state $s$ if $F$ is reached $\mathbb{P}_{\sigma,s}$ -almost surely.

The winning region is the subset $W\subseteq S$ of states from which a winning strategy exists.

Random walks in winning regions.

In an MDP with finitely many states, if there is an almost surely winning strategy for Controller, then there is a canonical one: play at random any action that guarantees staying in the winning region. This is formalized using arenas and safe random walks, as follows.

We call an MDP simple if for all $s\in S$ , the set of states reachable from $s$ is finite. A commit is an element of $S\times\Sigma$ . An arena is a set $\Gamma\subseteq S\times\Sigma$ of commits such that for all $(s,a)\in\Gamma$ and $t\in S$ , if $\Delta(s,a)(t)>0$ then there exists $b\in\Sigma$ such that $(t,b)\in\Gamma$ . For brevity we will write $s\in\Gamma$ instead of $\exists b\in\Sigma,(s,b)\in\Gamma$ . A path in arena $\Gamma$ is a sequence $s_{0}\xrightarrow{a_{1}}s_{1}\xrightarrow{a_{2}}\ldots\xrightarrow{a_{k}}s_{k}% \in S(\Sigma S)^{*}$ such that $(s_{j-1},a_{j})\in\Gamma$ and $\Delta(s_{j-1},a_{j})(s_{j})>0$ for all $j>0$ . A safe random walk in the arena $\Gamma$ is a strategy $\sigma$ defined such that $\sigma(s)$ is the uniform distribution on $\{a\in\Sigma\mid(s,a)\in\Gamma\}$ . An arena is winning (with respect to $F$ ) if from every $s\in\Gamma$ there is a path in $\Gamma$ to $F$ . This is closely linked with winning regions, as shown in the next lemma.

Lemma 2 (Winning arenas).

Given a simple MDP and a set of target states $F$ ,

1.

A union of winning arenas is a winning arena, and the winning region is the projection onto $S$ of the largest winning arena.
2.

In a winning arena, a safe random walk is a winning strategy from every state.

Random Populations.

We consider populations of agents (or tokens), described by a common finite MDP $\mathcal{M}=(S,\Sigma,\Delta)$ .

Our arguments require tracking the trajectory of selected (sets of) tokens along paths and the following definitions will be convenient for this purpose.

Write $T_{\infty}$ for the countably infinite set of tokens. For any finite subset $T\subseteq T_{\infty}$ , let $\mathcal{M}^{T}=(S^{T},\Sigma,\Delta^{T})$ denote the MDP whose states (called configurations) are functions mapping each token of $T$ to a state of $S$ , and $\Delta$ is naturally lifted to $S^{T}$ : $\Delta^{T}(\gamma,a)(\gamma^{\prime})=\prod_{t\in T}\Delta(\gamma(t),a)(\gamma% ^{\prime}(t))$ for all $\gamma,\gamma^{\prime}\in S^{T}$ and $a\in\Sigma$ . For a subset $R\subseteq S$ , $R^{T}$ contains those configurations where all tokens are mapped to states in $R$ . In particular, $\{s\}^{T}$ contains only the configuration mapping all tokens to $s\in S$ , and $F^{T}$ is the set of final configurations, mapping all tokens to some state of $F$ .

We study the following decision problem, which asks whether for every finite population $T$ , Controller can almost surely ensure that all tokens simultaneously¹¹1Requiring all tokens to visit a final state simultaneously or possibly at different times is irrelevant for our purposes: The two variants are logspace inter-reducible (see the full version for a proof). reach a final state.

The Random population control problem
Given: an MDP $\mathcal{M}=(S,\Sigma,\Delta)$ , initial state $i\in S$ and target set $F\subseteq S$ .

Question: Is there a winning strategy to reach $F^{T}$ from $\{i\}^{T}$ , for all finite $T\subseteq T_{\infty}$ ?

We define $\mathcal{M}^{*}=\bigcup_{T\subseteq_{f}T_{\infty}}\mathcal{M}^{T}$ as the disjoint union of all finite $\mathcal{M}^{T}$ . Notice that, while the state space $S^{*}=\bigcup_{T\subseteq_{f}T_{\infty}}S^{T}$ is infinite, each $S^{T}$ is finite and therefore $\mathcal{M}^{*}$ is simple.

According to Lemma 2, a given MDP $\mathcal{M}$ is a positive instance if, and only if, there is a winning arena $A\subseteq S^{*}\times\Sigma$ with $\{i\}^{T}\subseteq A$ for all $T\subseteq_{f}T_{\infty}$ . Our main decidability result relies on identifying such a witness $A$ . By Lemma 2, the existence of such a witness $A$ does not depend on the precise probabilities in $\Delta$ . We will omit them in all examples and just assume without loss of generality that all probability distributions are uniform.

$\blacktriangleright$ Remark 3.

At this point one might wonder why we choose to define configurations as mappings from a set of tokens to states, and not simply as vectors counting the number of tokens in each state. This is due to the nature of our main proof: we use strategies in which tokens are split between a cohort of many tokens and small groups of tokens, isolated from each other. This isolation requirement is difficult to formulate without referring to specific token identities, and dropping those identities would make some proofs extremely hard to write (and read), especially for Lemma 16 and Theorem 7.

3 Symbolic Configurations

We first observe that the maximal winning arena $W$ of $\mathcal{M}^{(*)}$ must be closed under renaming of tokens. That is, for any bijective $\tau:T\to T^{\prime}$ and configurations $\gamma\in S^{T}$ and $\gamma^{\prime}\in S^{T^{\prime}}$ , if $\gamma=\gamma^{\prime}\circ\tau$ then either both $\gamma$ and $\gamma^{\prime}$ , or neither is in $W$ . Furthermore, $W$ must be closed under removal of tokens: if $W$ contains $\gamma\in S^{T}$ and $T^{\prime}\subseteq T$ then $W$ must also contain the restriction of $\gamma$ to $T^{\prime}$ . Both these can be seen by simple transfers of winning strategies.

The winning region can therefore conveniently be represented as a downward-closed set of $\lvert S\rvert$ -dimensional vectors of integers, each of which just reflects how many tokens occupy each state. Given a configuration $\gamma\in S^{T}$ , we write $\immediate\immediate\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}% \definecolor[named]{pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}|\gamma|}$ for the vector of $\mathbb{N}^{S}$ such that ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}|\gamma|}(s)$ is the number of tokens in $s$ in $\gamma$ , for all $s\in S$ .

Take $\overline{\mathbb{N}}=\{0<1<2<3<\ldots<\omega\}$ , the non-negative integers with natural ordering extended by a maximal element $\omega$ . This ordering is lifted pointwise to $\overline{\mathbb{N}}^{S}$ , whereby $\mathbf{v}\leq\mathbf{v}^{\prime}$ if and only if $\mathbf{v}(s)\leq\mathbf{v}^{\prime}(s)$ for all $s\in S$ , and $(\mathbf{v},a)\leq(\mathbf{v}^{\prime},a^{\prime})$ if and only if $\mathbf{v}\leq\mathbf{v}^{\prime}$ and $a=a^{\prime}$ .

Definition 4 (Symbolic representations).

A symbolic configuration is a vector $\mathbf{v}\in\overline{\mathbb{N}}^{S}$ . Given a symbolic configuration, the ideal ${\mathbf{v}\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}\definecolor[% named]{pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}\hskip 0.0pt% \downarrow}}$ is the set of all configurations $\gamma$ such that ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}|\gamma|}\leq\mathbf{v}.$ For a set of symbolic configurations $\mathbf{V}$ , we write ${\mathbf{V}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ for the set $\bigcup_{\mathbf{v}\in\mathbf{V}}{\mathbf{v}{\color[rgb]{0,0.1875,0.3125}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}\hskip 0.0pt% \downarrow}}$ .

Similarly, a symbolic commit $(\mathbf{v},a)$ is a symbolic configuration $\mathbf{v}\in\overline{\mathbb{N}}^{S}$ together with an action $a\in\Sigma$ . The commit ideal ${(\mathbf{v},a){\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor% }{rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ is the set $\{(\gamma,a)\mid\gamma\in{\mathbf{v}{\color[rgb]{0,0.1875,0.3125}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}\}$ .

We recall that the product ordering on commit ideals is a well-quasi-order. Every downward-closed set $A\subseteq\overline{\mathbb{N}}^{S}\times\Sigma$ , including our maximal winning arena, can therefore be written as a union $A=\bigcup_{0<i<m}{({\mathbf{v}}_{i},a_{i}){\color[rgb]{0,0.1875,0.3125}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}\hskip 0.0pt% \downarrow}}$ of finitely many incomparable ideals [19]. We call such a finite union of commit ideals a population arena, or simply an arena when clear from the context. Throughout this work we will make use of the notion of $K$ -definability, that bounds the maximal finite constants in such ideal representations of population arenas.

Definition 5 ( $K$ -definability).

Let $K\in\mathbb{N}$ . A set $\Gamma$ of commits is $K$ -definable if it is a finite union of commit ideals of the form $({\mathbf{v}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}},a)$ with $\mathbf{v}\in\{0,\ldots,K,\omega\}^{S}$ . The maximal $K$ -definable subset of $\Gamma$ is denoted by $\immediate\immediate\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}% \definecolor[named]{pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}\Gamma_{% K}}.$

Example 6.

In the MDP from Example 1, the maximal winning arena is

W={((\omega,\omega,\omega,0,\omega),a){\color[rgb]{0,0.1875,0.3125}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}\hskip 0.0pt% \downarrow}}\nobreak\ \cup\nobreak\ {((\omega,1,0,\omega,\omega),b){\color[rgb% ]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}% \hskip 0.0pt\downarrow}}

with states enumerated as $(s_{0},\dots,s_{4})$ . A safe random walk in $W$ instructs to play, with positive probability, the action $a$ in any configuration where no tokens are on $s_{3}$ . Further, to play $b$ with positive probability if at most one token is on $s_{1}$ and none on $s_{2}$ . This set is clearly $1$ -definable and therefore, $W={\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{1}}$ . Its maximal $0$ -definable subset is

{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{0}}={((\omega,\omega,\omega,0,\omega),a){\color[rgb]{% 0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}% \hskip 0.0pt\downarrow}}\nobreak\ \cup\nobreak\ {((\omega,0,0,\omega,\omega),b% ){\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\hskip 0.0pt\downarrow}}

While ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{0}}$ is still an arena (it is a forward invariant), it is not winning because there is no path in it from initial to target configurations. This is because the action $b$ that takes tokens to $s_{2}$ or $s_{3}$ is never played when there are tokens on $s_{1}$ .

4 Solving the Random Population Control Problem

We present our main result: the Random population control problem is solvable in exponential time. According to Lemma 2, there is a maximal winning arena containing all configurations from which there is a winning strategy. As a consequence, there is a winning strategy from all initial configurations if and only if there is a winning arena which contains them all.

Thus, all positive instances are witnessed by a set of commits that is 1) an arena (forward-closed), 2) winning (every included configuration can reach a target configuration without leaving this set), and finally, 3) includes all initial configurations.

We will symbolically represent candidate sets as per Definition 4, as finite unions of commit ideals $Y=\bigcup_{0<i<m}{({\mathbf{v}}_{i},a_{i}){\color[rgb]{0,0.1875,0.3125}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}\hskip 0.0pt% \downarrow}}$ . This makes it straightforward to check conditions 1) and 3) syntactically. The two main remaining ingredients for our approach are Theorem 7, that positive instances admit polynomially-definable winning arenas; and Theorem 8, that one can check condition 2) in exponential time (and even polynomial space). We formally state these theorems below and derive an algorithm to solve the Random population control problem in exponential time. The following sections contain proofs.

In what follows, fix an MDP $\mathcal{M}=(S,\Sigma,\Delta)$ , initial state $i\in S$ and target set $F\subseteq S$ . Let $W$ denote the winning arena in $\mathcal{M}^{(*)}$ , and recall that for every $K\in\mathbb{N}$ , ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{K}}$ is its maximal $K$ -definable subset. Let $\textbf{i},{\mathbf{f}}\in\overline{\mathbb{N}}^{S}$ be the symbolic configurations mapping the state $i$ (resp. all states in $F$ ) to $\omega$ and other states to $0$ . Then in particular, ${{\mathbf{f}}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ is the set of configurations whose tokens are all in $F$ . Observe that, since all those configurations are in the winning region by definition, we have ${\textbf{f}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}\subseteq{\color[rgb]{% 0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}W_{0}}$ and the answer to the Random population control problem is positive if and only if ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{0}}$ contains all configurations with all tokens on the initial state, i.e., ${\textbf{i}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}\subseteq{\color[rgb]{% 0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}W_{0}}$ .

Theorem 7.

Let $W$ be the maximal winning arena. There is a winning arena $Y\subseteq W$ with

$\blacksquare$

$Y$ contains ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{0}}$ ; and
$\blacksquare$

$Y$ is $|S|$ -definable.

$\blacktriangleright$ Remark.

Theorem 7 implies that, if we can control arbitrarily many tokens then we can do so with a safe random walk in some $\lvert S\rvert$ -definable arena. This has no immediate consequences for the shape of the winning region $W$ . In fact, $W$ may not be $|S|$ -definable and its ideal representation may require doubly exponentially large constants (cf. Section 7.2). Therefore, in general, $Y$ is strictly contained in $W$ .

Moreover, despite there existing memoryless and deterministic strategies from every configuration in the winning region [15], the $\lvert S\rvert$ -definable winning strategies guaranteed by Theorem 7 may still require randomisation (cf. Section 7.3).

To verify that a candidate arena is winning, we need to be able to check that all configurations in it can reach a final one while staying in the arena. We show (in Section 6), how to solve the following problem²²2This is a slightly different presentation of the “sequential flow problem” in [6]. They presented a solution in exponential space, which was recently improved to polynomial space [10]. .

The Dynamic flow problem
Given: an MDP $\mathcal{M}=(S,\Sigma,\Delta)$ , a finite set of symbolic commits $\mathbf{V}$ , a symbolic configuration $\mathbf{v}_{0}\in\mathbf{V}$ and a set of symbolic configurations $\mathbf{F}$ .

Question: Does every configuration in ${\mathbf{v}_{0}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor% }{rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ , admit a path to ${\mathbf{F}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ inside ${\mathbf{V}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ ?

Theorem 8.

The Dynamic flow problem can be solved in polynomial space in $\log(K)$ and $|S|$ , where $K$ is the largest integer appearing in the input.

Together, Theorems 7 and 8 suggest a simple algorithm to compute a suitable winning arena $Y$ by refining a candidate set $\mathbf{V}$ of symbolic commits until the corresponding union of ideals is a winning arena. Recall that given a set of commits $\Gamma$ we use the notation $\gamma\in\Gamma$ for $\exists b\in\Sigma,(\gamma,b)\in\Gamma$ . Similarly, given a set of configurations $C$ and a set of commits $\Gamma$ , we write $C\subseteq\Gamma$ instead of $\forall\gamma\in C,\exists a\in\Sigma,(\gamma,a)\in\Gamma$ .

Algorithm 1 Algorithm for the Random population control problem.

The idea is to compute a $\lvert S\rvert$ -definable winning arena $Y$ as guaranteed by Theorem 7 by refinement. Start with the largest such candidate set (line 1), and reduce it if it is not an arena (lines 3 and 4) or if it is not a winning one (lines 5 and 6). Computing ideal representations for reduced candidate sets, and the check in line 3, are syntactic and therefore simple. The check in line 5 is an instance of the Dynamic flow problem. Once the procedure stabilizes, ${{\mathbf{V}}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ is a winning arena that satisfies the conditions of Theorem 7. In particular, it contains all of ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\Gamma_{0}}$ . The input therefore describes a positive instance if and only if ${\mathbf{i}}\in{\mathbf{V}}$ , the output of the algorithm in line 8.

Observe that $\mathbf{V}$ is deliberately initialised as the set of all symbolic configurations that may appear in the decomposition of $Y$ , and therefore only reduces during the computation.

Theorem 9.

The Random population control problem is ExpTime-complete.

Proof.

ExpTime-hardness is shown as Theorem 21. The matching upper bound is provided by Algorithm 1: It remains to argue that it takes at most exponential time.

$\blacksquare$

$\mathbf{V}$ has $(|S|+2)^{|S|}|\Sigma|$ elements at the start, and every iteration removes at least one.
$\blacksquare$

The first condition (line 3) can be checked simply by computing the set of successors of each symbolic commit in $\mathbf{V}$ . This can be straightforwardly done in exponential time in the number of states.
$\blacksquare$

Checking the second condition (line 5) is solving an instance of the Dynamic flow problem with largest constant $\leq|S|$ , for each $(\mathbf{v},a)$ in $\mathbf{V}$ . This problem is solvable in polynomial space (and thus exponential time) in $|S|$ (Section 6).

Therefore, Algorithm 1 takes exponential time in the size of the input. $\hfill\blacktriangleleft$

5 Theorem 6: Small Winning Arenas

Consider now a positive instance of the Random population control problem with maximal winning arena $W$ .

Towards proving Theorem 7, we now describe a winning strategy for Controller that remains in (and thus defines) a suitable winning sub-arena $Y\subseteq W$ which satisfies the claim of the theorem. As discussed previously, the inclusion $Y\subseteq W$ might be strict.

We consider the tokens of any configuration to be split between those that are part of the large cohort and a few individuals that are tracked separately. Increasing the number of tokens in states occupied by the cohort cannot result in configurations outside the winning region (see Definition 15). By contrast, increasing the number of individuals on a state may turn a winning configuration into a losing one.

The strategy operates in two modes. The first mode attempts to follow a “lucky” path in $W$ that leads to a final configuration: one where at any step only a few tokens leave the cohort and those that do, subsequently never meet until they rejoin the cohort. For instance, in Example 1 we would try sending tokens one by one via $s_{0}\to s_{1}\to s_{2}\to s_{4}$ , while keeping all others in their current states. Formally, this means that the path stays within ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{1}}$ , and therefore introduces at most $|S|$ individual tokens. The existence of such paths is guaranteed by Lemma 11. Successfully following such a path to the end has a positive probability that is bounded away from zero (for a given number of tokens).

In case the “lucky” path is exited prematurely, our strategy enters a second, recovery mode that, almost surely, brings the individual tokens back into the large cohort (reaches ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{0}}$ ) in order to attempt a new “lucky” path to a final configuration again. See Figure 2 for an illustration.

This must be possible because we have not left the maximal winning arena $W$ , and therefore can still almost surely reach a final configuration in ${{\mathbf{F}}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}\subseteq{\color[rgb]{% 0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}W_{0}}$ . We again attempt to follow another “lucky” path towards this new target, using Lemma 11, thereby creating up to $|S|$ additional individuals along the way. Again, following this path succeeds with probability bounded away from zero.

The issue with this approach is that we may continue to be unlucky and track ever more individual tokens. However, as we show in Lemma 16, one can play as described above while ensuring that individuals introduced at different steps never meet before they are brought back to the cohort. As each step produces at most $|S|$ new individual tokens (necessarily on distinct states), we can see at most $|S|$ individual tokens in each state overall.

Figure 2: Controller tries to follow the black path from

{{\mathbf{i}}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}

to

{{\mathbf{F}}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}

, along which individual tokens (in blue) may be produced temporarily yet never meet in the same state. If this path is exited (red arrow) those individuals can meet, in which case we leave

{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{1}}

as here. We then attempt to recover by following a new black path towards

{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}W_{0}}

which can spawn new individual tokens (as here, in blue-green) and so on. Lemma 16 guarantees that tokens of different colors never meet and therefore that there are no more than

|S|

layers. We define

Y

as the union of all those layers.

We will need some notation to formalize our argument. In particular, we extend all previous definitions to (symbolic) configurations that explicitly track finitely many individual tokens. We thus extend the symbolic representations in Definition 4 accordingly.

Definition 10.

Let $T_{f}$ be a finite set of tokens, called individuals, whereas other tokens in $T_{\infty}\setminus T_{f}$ are called the cohort tokens. Given a symbolic configuration $\mathbf{v}\in\overline{\mathbb{N}}^{S}$ and a configuration $\gamma_{f}:T_{f}\to S$ , the ideal tracking $T_{f}$ generated by $\mathbf{v}$ and $\gamma_{f}$ is written $\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}\definecolor[named]{% pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}(\gamma_{f}\otimes\mathbf{v}% )\downarrow}$ and defined as the set of configurations $\gamma:T\to S$ such that:

$\blacksquare$

individuals are placed on states according to $\gamma_{f}$ , i.e. $T_{f}\subseteq T$ and $\forall t\in T_{f},\gamma(t)=\gamma_{f}(t)$ .
$\blacksquare$

the number of cohort tokens on a state is bounded from above by $\mathbf{v}$ , i.e.

$\forall s\in S,|\{t\in T\setminus T_{f},\gamma(t)=s\}|\leq\mathbf{v}(s).$

Similarly, given an action $a\in\Sigma$ , the commit ideal tracking $T_{f}$ associated with $\mathbf{v}$ , $\gamma_{f}$ and $a$ is denoted $\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}\definecolor[named]{% pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}(\gamma_{f}\otimes\mathbf{v}% ,a)\downarrow}$ , and is the set of commits $(\gamma,a)$ with $\gamma\in{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}% {0,0.1875,0.3125}(\gamma_{f}\otimes\mathbf{v})\downarrow}$ . A population arena tracking $T_{f}$ is a finite union of commit ideals tracking $T_{f}$ .

Let $\Gamma$ be an arena and $K\in\mathbb{N}$ . Then $\immediate\immediate\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}% \definecolor[named]{pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}\Gamma_{% K,T_{f}}}$ denotes the union of all ideals tracking $T_{f}$ of the form ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}(\gamma_{f}\otimes\mathbf{v})\downarrow}$ with $\mathbf{v}\in\{0,\ldots,K,\omega\}^{S}$ that are included in $\Gamma$ .

5.1 The Existence of Lucky Paths

We start from a fairly simple idea: Suppose that we are able to transfer arbitrarily many tokens from one state to another along paths that remain in the winning region. It may be necessary to transfer those tokens in small groups, as they have to go through a bottleneck. In this case, we might as well transfer them one by one.

Lemma 11.

Let $T_{f}$ be a finite set of tokens, $\mathbf{F}$ an ideal tracking $T_{f}$ and $\Gamma$ a population arena tracking $T_{f}$ . If $\Gamma$ is a winning arena with respect to $\mathbf{F}$ , then for every configuration $\gamma_{0}\in{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\Gamma_{0,T_{f}}}$ there is a path in ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\Gamma_{1,T_{f}}}$ from $\gamma_{0}$ to $\mathbf{F}$ .

The rest of Section 5.1 is dedicated to the proof of Lemma 11. Let us start by defining the necessary terminology on flows and cuts. Let $\overline{\mathbb{R}^{+}}$ be the set of non-negative real numbers, with an additional maximum element $\omega$ . We extend the addition by setting $\omega+r=r+\omega$ for all $r\in\overline{\mathbb{R}^{+}}$ .

Given a finite directed graph $G=(V,E)$ , a capacity function $c:V\to\overline{\mathbb{R}^{+}}$ , and two vertices $s r c$ and $t g t$ (a source and a target), we define a flow from $s r c$ to $t g t$ as follows. It is a function $f:E\to\overline{\mathbb{R}^{+}}$ such that for all $v\in V\setminus\{src,tgt\}$ , we have

\sum_{(v_{-},v)\in E}f(v_{-},v)=\sum_{(v,v_{+})\in E}f(v,v_{+})\leq c(v).

The value of the flow is defined as $\mathbf{val}_{G,c}(f)=\sum_{(src,v)\in E}f(src,v)$ .

A cut is a set $M$ of vertices such that every path from $s r c$ to $t g t$ contains a vertex of $M$ . Its weight is defined as $\mathbf{weight}_{G,c}(M)=\sum_{v\in M}c(v)$ .

Theorem 12 (Max flow-min cut [9]).

For every graph $G=(V,E)$ , capacity function $c:V\to\overline{\mathbb{R}^{+}}$ and vertices $src,tgt\in V$ ,

\max_{f\text{flow}}\mathbf{val}_{G,c}(f)=\min_{M\text{cut}}\mathbf{weight}_{G,% c}(M)

$\blacktriangleright$ Remark 13.

We state this theorem with the capacities on the vertices, as it is convenient for the next proof. It is more commonly stated with capacities on the edges $c:E\to\overline{\mathbb{R}^{+}}$ . The constraints on the flow is then $\sum_{(v_{-},v)\in E}f(v_{-},v)=\sum_{(v_{-},v)\in E}f(v_{-},v)$ for all $v\in V$ and $f(e)\leq c(e)$ for all $e\in E$ . A cut is then defined as a set of edges, and the theorem is stated analogously.

Another classic result is the integer flow theorem. It says that if all capacities in the graph are integers, then there is an integer maximal flow $f:E\to\overline{\mathbb{N}}$ . This is a by-product of the Ford-Fulkerson algorithm.

Theorem 14 (Integer flow theorem [9]).

For every graph $G=(V,E)$ , capacity function $c:V\to\overline{\mathbb{N}}$ and vertices $src,tgt\in V$ , there exists a flow $f:E\to\overline{\mathbb{R}^{+}}$ of maximal value such that $f(u,v)\in\overline{\mathbb{N}}$ for all $(u,v)\in E$ .

With those two results in mind, we can establish Lemma 11.

Proof.

As $\Gamma$ is a population arena tracking $T_{f}$ , by definition it is a finite union of commit ideals tracking $T_{f}$ , hence we can decompose it as

\Gamma=\bigcup_{j=1}^{k}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.1875,0.3125}(\gamma_{j}\otimes\mathbf{v}_{j},a_{j})% \downarrow}.

Let $B<\omega$ be the largest constant used to define those commit ideals. That is, $B=\max(\{\mathbf{v}_{j}(s)\mid 1\leq j\leq k,s\in S,\mathbf{v}_{j}<\omega\})$ .

By definition, ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\Gamma_{0,T_{f}}}$ is also a finite union of commit ideals tracking $T_{f}$ . Let ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}(\gamma_{f}\otimes\mathbf{v},a)\downarrow}$ with $\mathbf{v}\in\{0,\omega\}^{S}$ be one of them. Let $S_{\omega}$ be the set of states $s$ such that $\mathbf{v}(s)=\omega$ and let $d=\lvert S_{\omega}\rvert$ . For all $N\in\mathbb{N}$ , define $\gamma_{f}\otimes\mathbf{v}[N]$ as a configuration obtained by taking $\gamma_{f}$ and adding $N$ tokens on each state of $S_{\omega}$ . The set of configurations $\gamma_{0}$ which satisfy the conclusion of the theorem is clearly stable by token renaming and token removal (because the set of paths in ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\Gamma_{1,T_{f}}}$ is stable by token deletion). Thus, it is enough to prove it for configurations $\gamma_{0}$ of the specific form $\gamma_{f}\otimes\mathbf{v}[N],N\in\mathbb{N}$ .

Fix $N\in\mathbb{N}$ , we show that a path from $\gamma_{f}\otimes\mathbf{v}[N]$ to $\mathbf{F}$ in ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\Gamma_{1,T_{f}}}$ exists.

The configuration $\gamma_{f}\otimes\mathbf{v}[B\cdot N]$ belongs to the ideal tracking $T_{f}$ ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}(\gamma_{f}\otimes\mathbf{v})\downarrow}$ , which is a subset of $\Gamma$ , hence there is a path $y_{0}\xrightarrow{a_{1}}y_{1}\xrightarrow{a_{2}}\cdots y_{n}$ within $\Gamma$ with $y_{0}=\gamma_{f}\otimes\mathbf{v}[B\cdot N]$ and $y_{n}\in\mathbf{F}$ . Let $T$ be the set of tokens used in $y_{0}$ .

Figure 3: An illustration of the proof of Lemma 11. We do not describe

\Gamma

in full, only the two relevant ideals (which by themselves, do not form an arena). We have two actions,

a

and

b

. We can play

a

when there are no tokens in

q_{2}

,

b

when there are at most

3

, and they let us transfer tokens along the indicated transitions. Those two actions let us transfer arbitrarily many tokens from

q_{1}

and

q_{3}

to

q_{4}

. With the notations of the proof, we have

d=2

,

B=3

and

T_{f}=\emptyset

. Let

N=2

. The graph

G

and flow given below represents the path transferring

BN=6

tokens from

q_{1}

and

q_{3}

to

q_{4}

. The corresponding flow has value

dBN=12

. On the top right are restricted versions of our ideals, where finite positive numbers have been replaced by

1

: in order to play

b

, we must have at most one token on

q_{2}

. By applying those constraints in

G

, we get a graph where the maximal flow has been divided by at most

3

: by the max flow-min cut theorem and because all capacities have been divided by at most

B=3

. We are thus guaranteed that there is a flow of value

\geq 4

in this graph (such as the one on the bottom graph), which corresponds to the transfer of

N=2

tokens from

q_{1}

and

q_{3}

.

Consider the following directed graph $G=(V,E)$ and capacity function $c:V\to\overline{\mathbb{N}}$ . The set of vertices is $V=S\times\{0,\ldots,n\}\cup\{src,tgt\}\cup\{r_{s}\mid s\in S\}$ , i.e., one vertex for each state and configuration in the path, plus a source, a target, and one intermediate vertex $r_{s}$ between $s r c$ and each $(s,0)$ .

We define the set of edges $E$ and the capacity function $c$ on vertices of $G$ as follows: for all $j\in\{0,\ldots,n-1\}$ , we pick a commit ideal tracking $T_{f}$ ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}(\gamma_{j}\otimes\mathbf{v}_{j},a_{j+1})\downarrow}$ in the ideal decomposition of $\Gamma$ such that $(\gamma_{j},a_{j+1})$ is in it. We also define $\gamma_{n},\mathbf{v}_{n}$ such that $\mathbf{F}={\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}(\gamma_{n}\otimes\mathbf{v}_{n})\downarrow}$ (they are well-defined since $\mathbf{F}$ is an ideal tracking $T_{f}$ ). For all $j<n$ and states $s,s^{\prime}$ , there is an edge from $(s,j)$ to $(s^{\prime},j+1)$ if and only if $\Delta(s,a_{j+1})(s^{\prime})>0$ . We also have edges from $s r c$ to $r_{s}$ , $r_{s}$ to $(s,0)$ and from $(s,n)$ to $t g t$ for all $s\in S$ .

For every state $s$ and index $j$ , the vertex $(s,j)$ is assigned capacity $c(s,j)=\mathbf{v}_{j}(s)$ . Furthermore, for all $s\in S$ , $r_{s}$ has capacity $c(r_{s})=B\cdot N$ if $\mathbf{v}(s)=\omega$ and $0$ otherwise. Observe that by definition of $B$ , we only assigned capacities in $\{0,\dots,B,\omega\}$ to vertices $(s,j)$ .

The trajectories of tokens outside of $T_{f}$ in the path $y_{0}\xrightarrow{a_{1}}y_{1}\xrightarrow{a_{2}}\cdots\xrightarrow{a_{n}}y_{n}$ define a flow $\phi:E\to\mathbb{N}$ from $s r c$ to $t g t$ in $G$ of value $d B N$ : for each edge $e=((s,j-1),(s^{\prime},j))$ we define $\phi(e)$ as the number of tokens of $T\setminus T_{f}$ going from $s$ to $s^{\prime}$ at the $j$ th step. We also define $\phi((src,r_{s}))=\phi(r_{s},(s,0))=BN$ for all $s\in S_{\omega}$ and $0$ otherwise. For all $s\in S$ , $\phi(((s,n),tgt))$ is the number of tokens of $T\setminus T_{f}$ in $s$ at the end of the path. This flow satisfies the capacity constraints of $G$ by definition of $(\mathbf{v}_{j})_{0\leq j\leq n}$ .

Let us now define a new capacity function $c^{1}$ on $G$ , as follows.

$\blacksquare$

For all $s\in S$ we set $c^{1}(r_{s})=N$ if $s\in S_{\omega}$ and $0$ otherwise.
$\blacksquare$

For all other vertices $v\in V\setminus\{r_{s}\mid s\in S\}$ , we set $c^{1}(v)=1$ if $c(v)\in\{1,\dots,B\}$ and $c^{1}(v)=c(v)$ if $c(v)\in\{0,\omega\}$ .

We claim that $G$ has an integer flow of value $d N$ satisfying the capacity constraint $c^{1}$ . Indeed, suppose the contrary, then by the integer flow theorem all flows have value $<dN$ . Therefore, by the max-flow min-cut theorem there is a cut $M$ in $G$ such that $\mathbf{weight}_{G,c^{1}}(M)<dN$ . As $c(v)\leq B\cdot c^{1}(v)$ for all $v\in V$ , that same cut has capacity $\mathbf{weight}_{G,c}(M)<dBN$ in $G$ . By the max-flow min-cut theorem, this contradicts the existence of a flow of value $d B N$ in $(G,c)$ . We obtain that $(G,c^{1})$ has a flow of value $d N$ , which is optimal as $\{r_{s}\mid s\in S\}$ is a cut of value $d N$ .

As all capacities defined by $c^{1}$ are integers, the integer flow theorem guarantees the existence of an optimal integer flow $\phi^{1}:E\to\mathbb{N}$ of value $d N$ , which in turn defines a path of length $n$ from $\gamma_{f}\otimes\mathbf{v}[N]$ to $\mathbf{F}$ : at step $j$ , the tokens of $T_{f}$ move in the same way as in the step $y_{j-1}\xrightarrow{a_{j}}y_{j}$ , and the number of other tokens sent from state $s$ to $s^{\prime}$ is $\phi^{1}((s,j-1),(s^{\prime},j))$ . Note that by definition of $E$ tokens can only move from state $s$ to $s^{\prime}$ if $\Delta(s,a_{j})(s^{\prime})>0$ .

Observe that the $j$ th commit along this path belongs to the ideal ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}(\gamma_{j-1}\otimes\mathbf{v}_{j-1},a_{j})\downarrow}$ because the flow $f$ must respect the capacities of vertices $G^{1}$ , which were derived from $\mathbf{v}_{j-1}$ . The path therefore stays in $\Gamma$ . In fact, by definition of $c^{1}$ , the $j$ th commit belongs to the smaller ideal ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}(\gamma_{j-1}\otimes\mathbf{v}_{j-1},a_{j})\downarrow}$ , where $\mathbf{v}^{1}_{j-1}$ is $\mathbf{v}_{j-1}$ where all finite positive coefficients have been replaced by $1$ . Consequently, it belongs to ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\Gamma_{1,T_{f}}}$ . Since all $(r_{s})_{s\in S_{\omega}}$ have capacity $N$ , the resulting path starts with $N$ tokens outside $T_{f}$ in each state of $S_{\omega}$ . The path ends in $\mathbf{F}$ as the capacities of $(s,n)_{s\in S}$ constrain the final configuration to be in ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}(\gamma_{n}\otimes\mathbf{v}_{n})\downarrow}\subseteq\mathbf{F}$ . This concludes the proof. $\hfill\blacktriangleleft$

5.2 The Isolation Lemma

In a configuration, we say that a set of states is an $\omega$ -base if an arbitrary amount of extra tokens could be placed on these states without exiting the arena $\Gamma$ . This is formally defined as follows.

Definition 15 ( $\omega$ -base and finite base).

Fix an arena $\Gamma$ and $\gamma:T\to S$ a configuration in $\Gamma$ over a set of tokens $T$ . A set of states $S_{\omega}$ is an $\omega$ -base of $\gamma$ in $\Gamma$ if

{\gamma[{S_{\omega}*\omega}]{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}\subseteq\Gamma\enspace.

with $\gamma[{S_{\omega}*\omega}]$ the symbolic configuration obtained from ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}|\gamma|}$ by mapping states of $S_{\omega}$ to $\omega$ .

By extension, a set of tokens $T_{\omega}\subseteq T$ is an $\omega$ -base of $\gamma$ in $\Gamma$ if the set of states occupied by those tokens in $\gamma$ is. Dually, a set of tokens $T_{f}\subseteq T$ is a finite base of $\gamma$ in $\Gamma$ iff $T\setminus T_{f}$ is an $\omega$ -base of $\gamma$ in $\Gamma$ .

Note that a configuration $\gamma$ may have several $\omega$ -bases and finite bases: for instance, say we have two states $s_{1},s_{2}$ and the arena $\Gamma$ is ${(\omega,1){\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}\cup{(1,\omega){\color[rgb]{% 0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}% \hskip 0.0pt\downarrow}}$ , then the configuration $[t_{1}\mapsto s_{1},t_{2}\mapsto s_{2}]$ has $\{t_{1}\}$ and $\{t_{2}\}$ as $\omega$ -bases, but not $\{t_{1},t_{2}\}$ .

We say that two tokens $t_{1},t_{2}$ meet in a configuration $\gamma$ if they share the same state i.e. if $\gamma(t_{1})=\gamma(t_{2})$ . The following lemma says that if starting from a configuration with a finite base $T_{f}$ we can reduce the size of the finite base (bring back an individual token into the cohort) with a strategy that treats tokens symmetrically, then we can do so while making sure that the tokens of $T_{f}$ never meet the tokens outside $T_{f}$ before this goal is achieved.

Intuitively, while the tokens of $T_{f}$ are all in bounded places, it means that they only meet boundedly many other tokens. Since this strategy works with an arbitrarily large cohort, we can show that in fact we can strengthen it to make sure that no token meets the ones in $T_{f}$ .

Lemma 16 (Isolation Lemma).

Fix a population arena $\Gamma$ and $k\in\mathbb{N}$ , and assume that from all $\gamma\in\Gamma$ there is a strategy to almost surely reach a configuration with a finite base of size $<k$ , without leaving $\Gamma$ .

Then for all $\gamma^{\prime}\in\Gamma$ with a finite base $T_{f}$ of size $k$ , there is a strategy $\sigma$ which, when starting from $\gamma^{\prime}$ :

$\blacksquare$

surely remains in $\Gamma$ ;
$\blacksquare$

almost surely reaches a configuration with a finite base strictly included in $T_{f}$ , and
$\blacksquare$

guarantees that in every configuration before that, every state contains either only tokens of $T_{f}$ or no token of $T_{f}$ .

Sketch of proof.

This lemma is central to the proof of Theorem 7. Unfortunately we cannot include the full proof due to space constraints. The proof can be found in the full version, we sketch it here.

A crucial element in the assumption is that $\Gamma$ is a population arena, i.e., it does not distinguish tokens. Since we have a winning strategy to reach a configuration with finite base of size $<k$ from everywhere in $\Gamma$ , a safe random walk in $\Gamma$ is a winning strategy, from all configurations of $\Gamma$ . Again, this random walk treats tokens symmetrically.

Now consider an initial configuration $\gamma^{\prime}$ in $\Gamma$ , with $N$ tokens. On states of the $\omega$ -base, we can add many more tokens and still have a winning strategy. We add many imaginary tokens on all states of the $\omega$ -base. Then we make the following observation: as long as tokens in $T_{f}$ remain outside the cohort, no token of the initial finite base $T_{f}$ meets the cohort; they can only meet a few tokens at a time. If a token $t$ of $T_{f}$ meets sufficiently many tokens along a path, then some of them must have re-entered the cohort since they met. Since the random walk treats all tokens symmetrically, $t$ also had a chance of reaching the cohort. This lets us bound the expected number of tokens $t$ meets before reaching the cohort, independently of the number of tokens in total. As we add more imaginary tokens, the probability that one of the tokens $t$ meets one of the real ones converges to $0$ .

We use these observations to show that we can obtain a probability as small as we want that any of the tokens of $T_{f}$ meets tokens outside $T_{f}$ before reaching the cohort. Since the set of configurations reachable from $\gamma^{\prime}$ is finite, this implies that this probability can be brought down to $0$ . As a consequence, we can make sure that a token of $T_{f}$ reaches the cohort while no token of $T_{f}$ meets one outside $T_{f}$ beforehand. $\hfill\blacktriangleleft$

5.3 Proof of Theorem 7

The proof of Theorem 7 uses a partition $T_{1},\ldots,T_{d}$ of the individuals $T_{f}$ into non-empty groups with at most $|S|$ tokens per group. Moreover, the induction hypothesis assumes that

$\blacksquare$

individuals of different groups never meet in the arena, other than in final configurations.
$\blacksquare$

$T_{f}$ is a finite base, i.e., the set of states occupied by the cohort is an $\omega$ -base.

Since every group occupies at least one state then $d\leq|S|$ . The induction step is done by induction on $|S|-d$ . The base case $|S|=d$ is trivial, because in that case all tokens are individuals: the cohort is empty, and $|S|$ -definability follows from the hypothesis that tokens of different groups never meet unless on $F$ . The value of $F$ is not fixed; the induction step uses the inductive hypothesis for $F=W_{0}$ . The induction step is done as follows, details are in the full version.

$\blacksquare$

We try to follow a path to the target set ${{\mathbf{F}}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ . We can choose this path so that we create at most $|S|$ individual tokens, by Lemma 11. These $|S|$ isolated tokens constitute a new group of individuals, denoted $T_{d+1}$ .
$\blacksquare$

If we deviate from that path, we use Lemma 16 to define a sub-arena that lets us recover all individual tokens (i.e. bring them into the cohort) while making sure that none of them meets any token from outside their group. We then apply the induction hypothesis (for $d+1$ and $F$ the set of configurations where tokens of $T_{d+1}$ have been recovered) to recover those individual tokens within an $|S|$ -definable sub-arena.
$\blacksquare$

Once all individuals are recovered, we apply the first step again, until we successfully follow the path to the end.

We define the desired sub-arena $Y$ as the union of those paths and sub-arenas. Since, in any included configuration, the number of individuals residing on any one state is at most $\lvert S\rvert$ , this arena must be $\lvert S\rvert$ -definable. Clearly, Controller wins from any included configuration by following the strategy outlined above. Therefore, $Y$ is a winning arena.

6 Theorem 7: The Dynamic Flow Problem

To prove Theorem 8, we rely on a result by Gimbert, Mascle and Totzke [10] about maximising the flow through directed graphs, where edge capacities are dynamically chosen by the maximiser. We recall the notation and statement of the relevant theorem.

A capacity is a function $\alpha:S^{2}\to\mathbb{N}\cup\{\omega\}$ mapping each pair of states $(s_{1},s_{2})$ to a maximal number of tokens that can be transferred from $s_{1}$ to $s_{2}$ . Let $A\subseteq(\mathbb{N}\cup\{\omega\})^{S^{2}}$ be a finite alphabet of capacities, and $E\subseteq S^{2}$ a set of pairs of states. Given a word $w=\alpha_{1}\dots\alpha_{k}\in A^{*}$ and a set of tokens $T$ , a token flow over $w$ is a sequence of configurations $\tau=\gamma_{0}\to\cdots\to\gamma_{k}\in(S^{T})^{*}$ such that, for every $i\in[1,k]$ and $s,s^{\prime}\in S$ , $|\{t\in T\mid\gamma_{i-1}(t)=s\land\gamma_{i}(t)=s^{\prime}\}|\leq\alpha_{i}(s% ,s^{\prime})$ . Define the global flow of $\tau$ as the function $\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}\definecolor[named]{% pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}g(\tau)}:S^{2}\to\mathbb{N}$ counting the number of tokens moving between each pair of states: formally, for all $s,s^{\prime}\in S$ ,

{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}g(\tau)}(s,s^{\prime})=\lvert\{t\in T:\gamma_{0}(t)=s\land% \gamma_{k}(t)=s^{\prime}\}\rvert.

Now let $L\subseteq A^{*}$ be a language over $A$ . The maximal sequential multi-flow on $E$ satisfying $L$ , denoted $\immediate{\color[rgb]{0.609375,0.1328125,0.1484375}\definecolor[named]{% pgfstrokecolor}{rgb}{0.609375,0.1328125,0.1484375}\xi}(E,L)$ , is the maximum number of tokens that can be simultaneously transferred between every pair of states in $E$ by a path over some word of $L$ .

{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\xi}(E,L)=\sup_{w\in L}\quad\sup_{\pi\text{ over }w}\quad\min_% {(s,s^{\prime})\in E}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.1875,0.3125}g(\pi)}(s,s^{\prime}).

Example 17.

Consider the capacities from Figure 4, and set of edges $E=\{(s_{1},s_{4}),(s_{3},s_{4})\}$ . For the language $L=\{abba\}$ containing only the capacity word $a b b a$ , we get ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\xi}(E,L)=1$ , witnessed by the token flow $\tau$ with global flow ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}g(\tau)}(s_{1},s_{4})={\color[rgb]{0,0.1875,0.3125}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}g(\tau)}(s_{3},s_{4})=1$ . Note that the maximal flow from $s_{2}$ to $s_{3}$ for the intermediate word $b b$ cannot exceed $2$ . However letting $L=\{ab^{n}a\}$ , we have ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\xi}(E,L)=\infty$ , because for every $n$ there is a token flow $\tau_{n}$ over $ab^{2n}a$ so that ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}g(\tau_{n})}(s_{1},s_{4})={\color[rgb]{0,0.1875,0.3125}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.1875,0.3125}g(\tau_{n})}(s_{3},s_% {4})=n$ .

As Gimbert et al. show, one can determine if such flows are unbounded, and otherwise precisely compute their finite value, in polynomial space.

capacity

a

capacity

b

capacity word

a b b a

token flow

\tau

over

a b b a

Figure 4: Two capacity constraints

a,b:S\to\mathbb{N}\cup\{\omega\}

, a capacity word, and a token flow over it.

Theorem 18 (Theorem 37 in [10]).

Let $A$ be a set of capacities over a set of states $S$ , with coefficients in $\{0,\dots,K,\omega\}$ , and $L\subseteq A^{*}$ a regular language recognised by an NFA with $m$ states. Then, either ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\xi}(E,L)=+\infty$ , or ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\xi}(E,L)\leq K(2|S|)^{(170\log_{2}(m)+835)|S|^{12}}$ .

This is almost what we need for deciding the Dynamic flow problem, except for two things. First, our constraints are on vertices while theirs are on edges. Second, in our initial ideal we may have both states marked $\omega$ and states bounded by finite numbers. We will translate the constraints given by ideals over configurations into capacities, thereby reinterpreting paths as token flows. This way one can use Theorem 18 to check that we can transfer arbitrarily many tokens from the states marked $\omega$ , while using the regular constraint to track the finite number of extra tokens and make sure that all token end up in $F$ .

Let $\mathcal{M}=(S,\Sigma,\Delta)$ , $\mathbf{V}$ , $\mathbf{v}_{0}$ , $\mathbf{F}$ be an instance of the Dynamic flow problem. We split $\mathbf{v}_{0}$ in two parts $\mathbf{v}_{0}=\mathbf{v}_{f}+\mathbf{v}_{\omega}$ , so that $\mathbf{v}_{f}\in\mathbb{N}^{S}$ and $\mathbf{v}_{\omega}\in\{0,\omega\}^{S}$ . Vector $\mathbf{v}_{\omega}$ describes the set of states with arbitrarily many tokens at the start, while $\mathbf{v}_{f}$ describes the remaining tokens in other states. Intuitively, the Dynamic flow problem comes down to checking that we can simultaneously transfer tokens of $\mathbf{v}_{f}$ and arbitrarily many tokens from every state marked $\omega$ in $\mathbf{v}_{0}$ to ${\mathbf{F}{\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.1875,0.3125}\hskip 0.0pt\downarrow}}$ . We will construct a finite alphabet of capacities and a finite automaton $\mathcal{A}$ which guesses the movement of the remaining tokens. Its language is the set of sequences of capacities which can be used while making sure that both the cohort of tokens from unbounded states and those remaining tokens are brought safely to $\mathbf{F}$ . The largest finite number appearing in the capacities is the same as in $\mathbf{V}$ , and $\mathcal{A}$ has exponential size in in $S$ and the logarithm of the largest finite number appearing in $\mathbf{V}$ .

Lemma 19.

$\mathcal{M}$ , $\mathbf{V}$ , $\mathbf{v}_{0}$ , $\mathbf{F}$ is a positive instance of the Dynamic flow problem if and only if there exists $E\subseteq S^{2}$ such that

1.

${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\xi}(E,L(\mathcal{A}))=+\infty$
2.

$\mathbf{v}_{0}^{-1}(\omega)\subseteq\{s\in S\mid\exists s^{\prime}\in S,(s,s^{% \prime})\in E\}$ .

Proof of Theorem 8.

By Lemma 19, in order to check if $\mathcal{M}$ , $\mathbf{V}$ , $\mathbf{v}_{0}$ , $\mathbf{F}$ is a positive instance of the Dynamic flow problem, we can enumerate sets $E\subseteq S^{2}$ and for each such $E$ , check the two conditions from Lemma 19. Condition 2 can be checked easily in polynomial time (and space). For condition 1, we can rely on Theorem 18: Note that the automaton $\mathcal{A}$ as constructed above is singly exponential in the input. Consequently, the same holds for $m$ and the quantity $M=K(2|S|)^{(170\log_{2}(m)+835)|S|^{12}}$ . This means that in order to check whether ${\color[rgb]{0,0.1875,0.3125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.1875,0.3125}\xi}(E,L(\mathcal{A}))=+\infty$ , it suffices to check that there is a word $w\in L(\mathcal{A})$ and a path $\pi$ over $w$ carrying $M+1$ tokens from $s$ to $s^{\prime}$ for all $(s,s^{\prime})\in E$ . These can be guessed on the fly: it suffices to memorise the current state in the automaton and the number of tokens in each state, in binary. This only requires polynomial space in $\log(K)$ and $|S|$ . $\hfill\blacktriangleleft$

7 Lower bounds an a hard case

7.1 Complexity lower bound

An exponential-time lower bound for the Random population control problem can be established by reduction from countdown games, as shown by Mascle, Shirmohammadi, and Totzke in [14].

Definition 20.

A Countdown Game is given by a directed graph $\mathcal{G}=(V,E)$ , where edges carry positive integer weights, $E\subseteq(V\times\mathbb{N}_{>0}\times V)$ . For an initial pair $(v,c_{0})\in V\times\mathbb{N}$ of a vertex and a number, two opposing players (Player 1 and 2) alternatingly determine a sequence of such pairs as follows. In each round, from $(v,c)$ , Player 1 picks a number $d\leq c$ such that $E$ contains at least one edge $(v,d,v^{\prime})$ ; then Player 2 picks one such edge and the game continues from $(v^{\prime},c-d)$ . Player 1 wins the game iff the play reaches a pair in $V\times\{0\}$ .

Determining the winner of a Countdown Game, where all constants are given in binary, is ExpTime-complete [12]. We state the lower bound and a sketch of the construction.

Theorem 21.

The Random population control problem is ExpTime-hard.

Proof sketch.

The number of turns in a Countdown Game cannot exceed the initial value of the counter, as the initial counter value decreases at each turn. Thus, if Player 2 has a winning strategy, choosing actions at random yields a positive probability of applying that strategy, hence a positive probability of winning. Therefore, Player 1 wins the initial game if and only if she wins with probability one against a randomised adversary.

The main idea for the further construction is to require Controller, who impersonates Player 1, to move tokens one-by-one from a waiting state, first into the control graph of the Countdown game, and ultimately into the target. To avoid a loss in the intermediate phase, she must win an instance of the game against a randomising opponent. This is enforced using a combination of gadgets, including two binary counters (encoded using two states per bit) that can effectively test for zero, be set to specific numbers, and that are set up so that they can decrement at the same rate. These are used to hold the global integral value $n$ , and an auxiliary counter holding the value $d$ chosen by Player 1. Controller is compelled to reduce them both and can only continue once the auxiliary counter is exhausted. She can only afford to safely end the simulation of the game if the first counter holds value $0$ . As a result, Player 1 has a winning strategy for the two-player Countdown Game if, and only if, Controller can synchronise the $n$ -fold product of the constructed MDP for all $n$ . $\hfill\blacktriangleleft$

7.2 A Double-exponential Cut-off

We use the following vocabulary: a state $s$ is marked in a configuration $\gamma$ if at least one token occupies it: $\exists t.\gamma(t)>0$ . Whenever an action $a$ takes state $s$ only back to itself we say that $s$ ignores $a$ . There are states Heaven (the target) and Hell which ignore all actions. For a given state $s$ , an action $a$ is angelic if it takes $s$ only to Heaven, and daemonic if it takes $s$ to Hell. An action $a$ is safe in a configuration if it is not daemonic for any marked state (in any gadget).

Figure 5: A (4-bit) Binary Counter. Not displayed are edges labelled by (deci) that make the respective actions daemonic for state (i:0), and error actions errori, which are daemonic for (i:0) and (i:1), for all bits

i\in\{0,1,2,3\}

.

The cut-off of an MDP is the minimal number of tokens against which Controller does not have an almost-sure winning strategy, In this section we show that there are MDPs whose cut-off is finite but doubly-exponential in the number of states. We reuse a construction from [3]. We simply replace the adversary with randomisation. Let us summarise it here.

Let $N\in\mathbb{N}$ . We build an MDP $\mathcal{M}_{N}$ as follows: We have an initial state $i$ and a final state $f$ , plus a sink state $\mathtt{sink}$ .

$\blacksquare$

First of all we have a splitting gadget, as shown in Figure 6. This gadget forces Controller to play a word of $((\Sigma_{N}\setminus\{l,r\})\{l,r\})^{*}$ until all three states are empty. We call a sequence of two actions of $(\Sigma_{N}\setminus\{l,r\})\{l,r\}$ a round. Say there are $2^{K}$ tokens in $\mathtt{s}$ at the start, then there is a positive probability that they distribute evenly between $\mathtt{left}$ and $\mathtt{right}$ whenever they split from $\mathtt{s}$ . Therefore, for any strategy of Controller, there is a positive probability that after $K$ rounds there is still at least one token in $\mathtt{s}$ .
$\blacksquare$

Second, we have a counter gadget, as shown in Figure 5. This one consists of $2N$ states, representing $N$ bits, $\{(i:0),(i:1)\mid 0\leq i\leq N-1\}$ . For all $0\leq j\leq N-1$ there is an action $\mathtt{dec}_{j}$ that fixes all states $(k:0),(k:1)$ with $k>j$ , sends $(j:1)$ to $(j:0)$ , and sends each $(k:0)$ with $k<j$ to $(k:1)$ . The tokens in states $(k:1)$ with $k<j$ and $(j:0)$ are all sent to $\mathtt{sink}$ . Action $\mathtt{stop}$ sends all tokens in $(i:0)_{1\leq i\leq N}$ to $f$ and all tokens in $(i:1)_{1\leq i\leq N}$ to $\mathtt{sink}$ . Actions $l, r$ leave the tokens in those states idle. This gadget implements a binary counter over $N$ bits. Let $\mathtt{Dec}=\{\mathtt{dec}_{j}\mid 1\leq j\leq N\}$ . If we start with tokens in states $(i:0)_{1\leq i\leq N}$ and not in states $(i:1)_{1\leq i\leq N}$ , then at all times Controller has only one action from $\mathtt{Dec}$ available, which increments the counter. Once every bit is $1$ , the only possible action apart from $\{l,r\}$ is $\mathtt{stop}$ . She is forced to play a sequence of actions of $\mathtt{Dec}^{2^{N}-1}\mathtt{stop}$ , interleaved with some $l$ and $r$ .
$\blacksquare$

We add an action $\mathtt{start}$ which sends tokens from $i$ to $\{\mathtt{s}\}\cup\{0_{i}\mid 1\leq i\leq N\}$ , and leaves all other tokens idle. All other actions map $i$ to $\mathtt{sink}$ .

Figure 6: The splitting gadget. The action

\mathtt{stop}

sends all tokens in

s

,

\mathtt{left}

and

\mathtt{right}

to a sink state.

If there are more than $2^{2^{N}}+N$ tokens, then, with positive probability, when playing $\mathtt{start}$ one goes to each of the $(i:0)_{1\leq i\leq N}$ and the rest to $\mathtt{s}$ . Then, as observed above, with positive probability the first gadget forces Controller to play at least $2^{N}$ actions from $\Sigma_{N}\setminus\{l,r\}$ before being able to play $\mathtt{stop}$ . However, the second gadget forces Controller to play $\mathtt{stop}$ after playing $2^{N}$ actions from $\Sigma\setminus\{l,r,\mathtt{stop}\}$ . Hence Controller cannot win almost surely.

If there are fewer than $2^{2^{N}}$ tokens, then Controller can play as follows: Play $\mathtt{start}$ , then alternate between playing the available $\mathtt{dec}_{j}$ (it may be that several actions are available because some $(i:0)$ did not receive any tokens in the first step; in that case, choose the minimal $j$ ) and playing either $l$ or $r$ (whichever sends the most tokens to $f$ ). After $2^{N}$ steps, all tokens in the counter gadget are in the states $(i:1)_{1\leq i\leq N}$ . Since at every round we send at least half of the tokens in the splitting gadget to $f$ , after $2^{N}$ rounds the gadget is empty. Controller can then play $\mathtt{stop}$ safely, and send all tokens in the counter gadget to $f$ .

We obtain an MDP with $2N+6$ states whose cut-off is between $2^{2^{N}}$ and $2^{2^{N}}+N$ .

7.3 A Butterfly

Figure 7: An automaton where Controller can synchronise any finite number of tokens but no deterministic,

k

-definable winning strategy exists.

Consider now the example in Figure 7. We will set it up so that initially, all tokens are randomly distributed onto states $L$ and $R$ , and Controller must eventually place all of them on only one side of the graph. To do so,

$\blacksquare$

add an initial action which moves tokens from an initial state to $L$ and $R$ and is daemonic everywhere else;
$\blacksquare$

add a fresh winning action that is angelic for all red states and daemonic for all green states; and
$\blacksquare$

add a fresh winning action that is angelic for all green states and daemonic for all red states.

Idea.

Each round starts with all tokens on $L$ and $R$ . Controller stepwise proposes a sequence of actions, either in $l^{+}l_{1}[l_{2}l_{3}]$ or $r^{+}r_{1}[r_{2}r_{3}]$ . Notice that until one side is empty, these are the only safe sequences to play. At the end of each round, all tokens (except possibly one) will switch sides. Controller can choose to isolate one token and keep it on its side, thereby getting closer to her goal of moving everyone to one side. The relevant decisions to make are

1.

whether to go left or right at the start of a round
2.

when to stop playing $l$ (or $r$ , resp.)

We say that two configurations $\gamma_{1},\gamma_{2}$ are $K$ -equivalent if for all states $s$ , they either have the same number of tokens in $s$ or both have at least $K$ tokens in $s$ . A strategy is $K$ -deterministic if it “counts up to $K$ ”. That is, it is deterministic and for all $K$ -equivalent $\gamma_{1},\gamma_{2}$ , it plays the same action from both.

Lemma 22.

The example is a positive instance of the Random population control problem. However, for every $K\geq 0$ , every $K$ -deterministic strategy is losing.

Proof.

Referring to the relevant decisions above, a winning strategy is to

$\blacksquare$

always pick the side with the least number of tokens (one can also pick the side at random), and
$\blacksquare$

play $l$ (or $r$ ) until exactly one token is isolated.

Consider a $K$ -deterministic strategy. Say we start with $2K+2$ tokens, and $K+1$ tokens end up on both $L$ and $R$ . Our strategy must play $l$ or $r$ , say it plays $l$ . We have $K+1$ tokens in the state below $L$ and in the one above $R$ . Playing $l_{2}$ or $l_{3}$ brings us back to the previous configuration (up to renaming tokens), and playing $l_{1}$ has no effect, thus it must play $l$ . Once this is done, it must keep playing $l$ until exactly one token is in the lower state: if all tokens are in the upper state we have established that it plays $l$ , and if there are $2$ or more tokens below, every move is losing except $l$ (playing $l_{1}$ risks tokens splitting between the two left states, after which we are stuck). Therefore, the strategy must wait until one token is in the lower state, then play $l_{1}$ and then $l_{2}$ or $l_{3}$ .

$L$ now contains $K+2$ tokens and $R$ contains $K$ , which is $K$ -equivalent to $K+1$ and $K+1$ . By repeating the same reasoning, in the next round the strategy does the same thing, which yields a configuration with $K+1$ tokens in both $L$ and $R$ , meaning we are back to the initial configuration. $\hfill\blacktriangleleft$

8 Conclusion

We have shown that the Random population control problem is ExpTime-complete. We establish that it is possible to win the population MDP while staying in a part of the winning region that has low descriptive complexity, in the sense of Theorem 7. This is the key to defining an algorithm (Algorithm 1) to solve the Random population control problem using an exponential number of calls to an oracle solving the Dynamic flow problem.

These results shed new light on parameterised control and pave the way for further positive results with more ambitious objectives. For example, the tools developed in this paper may be used to address a generalised version of the problem, where infinite executions must satisfy $\omega$ -regular conditions.

A natural question that remains open is the cut-off: if there is a number $n$ such that we cannot synchronize almost surely $n$ tokens, how large can the smallest such $n$ be? In the adversarial case studied in [3], it was shown that the cut-off was doubly exponential in the worst case. We conjecture that this is also the case in our setting. We show in Appendix 7.2 that the cut-off may be doubly exponential, but we are missing a matching upper bound.

References

[1] S. Akshay, Blaise Genest, and Nikhil Vyas. Distribution-based objectives for markov decision processes. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 36–45. ACM, 2018. doi:10.1145/3209108.3209185.
[2] Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. Distributed Comput., 18(4):235–253, 2006. doi:10.1007/S00446-005-0138-3.
[3] Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, and Hugo Gimbert. Controlling a population. In 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 12:1–12:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CONCUR.2017.12.
[4] Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert, and Adwait Amit Godbole. Controlling a population. Logical Methods in Computer Science, Volume 15, Issue 3, July 2019. doi:10.23638/LMCS-15(3:6)2019.
[5] Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Distributed local strategies in broadcast networks. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 44–57. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPIcs.CONCUR.2015.44.
[6] Thomas Colcombet, Nathanaël Fijalkow, and Pierre Ohlmann. Controlling a random population. Log. Methods Comput. Sci., 17(4), 2021. doi:10.46298/LMCS-17(4:12)2021.
[7] Laurent Doyen. Stochastic games with synchronization objectives. J. ACM, 70(3):23:1–23:35, 2023. doi:10.1145/3588866.
[8] E. Allen Emerson and Kedar S. Namjoshi. Reasoning about rings. In Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 85–94. ACM Press, 1995. doi:10.1145/199448.199468.
[9] Lester Randolph Ford and Delbert Ray Fulkerson. Maximal flow through a network. Canadian journal of Mathematics, 8:399–404, 1956.
[10] Hugo Gimbert, Corto Mascle, and Patrick Totzke. Optimal sequential flows. In Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis, editors, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026), volume 374 of LIPIcs, pages 98:1–98:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2026. doi:10.4230/LIPIcs.ICALP.2026.98.
[11] Emile Hazard, Olivier Idir, and Denis Kuperberg. Explorable parity automata. CoRR, abs/2410.23187, 2024. doi:10.48550/arXiv.2410.23187.
[12] Marcin Jurdzinski, François Laroussinie, and Jeremy Sproston. Model checking probabilistic timed automata with one or two clocks. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science, pages 170–184. Springer, 2007. doi:10.1007/978-3-540-71209-1_15.
[13] Daniel Kirsten. Distance desert automata and the star height problem. RAIRO Theor. Informatics Appl., 39(3):455–509, 2005. doi:10.1051/ITA:2005027.
[14] Corto Mascle, Mahsa Shirmohammadi, and Patrick Totzke. Controlling a random population is ExpTime-hard. CoRR, abs/1909.06420, 2019. arXiv:1909.06420.
[15] Donald Ornstein. On the existence of stationary optimal strategies. Proceedings of the American Mathematical Society, 20(2):563–569, 1969. doi:10.2307/2035700.
[16] Carl Adam Petri. Kommunikation mit Automaten. Dissertation, Schriften des IIM 2, Rheinisch-Westfälisches Institut für Instrumentelle Mathematik an der Universität Bonn, 1962.
[17] Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., 1st edition, 1994. doi:10.1002/9780470316887.
[18] G. Rozenberg and A. Salomaa. Handbook of Formal Languages. Number v. 1-3 in Handbook of formal languages / G. Rozenberg; A. Salomaa. Springer, 1997.
[19] Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. Accreditation to supervise research, École normale supérieure Paris-Saclay, November 2017.
[20] A. Prasad Sistla and Steven M. German. Reasoning with many processes. In Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Ithaca, New York, USA, June 22-25, 1987, pages 138–152. IEEE Computer Society, 1987.
[21] David Soloveichik, Matthew Cook, Erik Winfree, and Jehoshua Bruck. Computation with finite stochastic chemical reaction networks. Nat. Comput., 7(4):615–633, 2008. doi:10.1007/S11047-008-9067-Y.
[22] Daniel Stan. Randomized strategies in concurrent games. (Stratégies randomisées dans les jeux concurrents). PhD thesis, University of Paris-Saclay, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01519354.
[23] Jannis Uhlendorf, Agnès Miermont, Thierry Delaveau, Gilles Charvin, François Fages, Samuel Bottani, Pascal Hersen, and Gregory Batt. In silico control of biomolecular processes. Computational Methods in Synthetic Biology, pages 277–285, 2015.

[bib.bib1] [1] S. Akshay, Blaise Genest, and Nikhil Vyas. Distribution-based objectives for markov decision processes. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 36–45. ACM, 2018. doi:10.1145/3209108.3209185.

[bib.bib2] [2] Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. Distributed Comput., 18(4):235–253, 2006. doi:10.1007/S00446-005-0138-3.

[bib.bib3] [3] Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, and Hugo Gimbert. Controlling a population. In 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 12:1–12:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CONCUR.2017.12.

[bib.bib4] [4] Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert, and Adwait Amit Godbole. Controlling a population. Logical Methods in Computer Science, Volume 15, Issue 3, July 2019. doi:10.23638/LMCS-15(3:6)2019.

[bib.bib5] [5] Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Distributed local strategies in broadcast networks. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 44–57. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPIcs.CONCUR.2015.44.

[bib.bib6] [6] Thomas Colcombet, Nathanaël Fijalkow, and Pierre Ohlmann. Controlling a random population. Log. Methods Comput. Sci., 17(4), 2021. doi:10.46298/LMCS-17(4:12)2021.

[bib.bib7] [7] Laurent Doyen. Stochastic games with synchronization objectives. J. ACM, 70(3):23:1–23:35, 2023. doi:10.1145/3588866.

[bib.bib8] [8] E. Allen Emerson and Kedar S. Namjoshi. Reasoning about rings. In Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 85–94. ACM Press, 1995. doi:10.1145/199448.199468.

[bib.bib9] [9] Lester Randolph Ford and Delbert Ray Fulkerson. Maximal flow through a network. Canadian journal of Mathematics, 8:399–404, 1956.

[bib.bib10] [10] Hugo Gimbert, Corto Mascle, and Patrick Totzke. Optimal sequential flows. In Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis, editors, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026), volume 374 of LIPIcs, pages 98:1–98:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2026. doi:10.4230/LIPIcs.ICALP.2026.98.

[bib.bib11] [11] Emile Hazard, Olivier Idir, and Denis Kuperberg. Explorable parity automata. CoRR, abs/2410.23187, 2024. doi:10.48550/arXiv.2410.23187.

[bib.bib12] [12] Marcin Jurdzinski, François Laroussinie, and Jeremy Sproston. Model checking probabilistic timed automata with one or two clocks. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science, pages 170–184. Springer, 2007. doi:10.1007/978-3-540-71209-1_15.

[bib.bib13] [13] Daniel Kirsten. Distance desert automata and the star height problem. RAIRO Theor. Informatics Appl., 39(3):455–509, 2005. doi:10.1051/ITA:2005027.

[bib.bib14] [14] Corto Mascle, Mahsa Shirmohammadi, and Patrick Totzke. Controlling a random population is ExpTime-hard. CoRR, abs/1909.06420, 2019. arXiv:1909.06420.

[bib.bib15] [15] Donald Ornstein. On the existence of stationary optimal strategies. Proceedings of the American Mathematical Society, 20(2):563–569, 1969. doi:10.2307/2035700.

[bib.bib16] [16] Carl Adam Petri. Kommunikation mit Automaten. Dissertation, Schriften des IIM 2, Rheinisch-Westfälisches Institut für Instrumentelle Mathematik an der Universität Bonn, 1962.

[bib.bib17] [17] Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., 1st edition, 1994. doi:10.1002/9780470316887.

[bib.bib18] [18] G. Rozenberg and A. Salomaa. Handbook of Formal Languages. Number v. 1-3 in Handbook of formal languages / G. Rozenberg; A. Salomaa. Springer, 1997.

[bib.bib19] [19] Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. Accreditation to supervise research, École normale supérieure Paris-Saclay, November 2017.

[bib.bib20] [20] A. Prasad Sistla and Steven M. German. Reasoning with many processes. In Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Ithaca, New York, USA, June 22-25, 1987, pages 138–152. IEEE Computer Society, 1987.

[bib.bib21] [21] David Soloveichik, Matthew Cook, Erik Winfree, and Jehoshua Bruck. Computation with finite stochastic chemical reaction networks. Nat. Comput., 7(4):615–633, 2008. doi:10.1007/S11047-008-9067-Y.

[bib.bib22] [22] Daniel Stan. Randomized strategies in concurrent games. (Stratégies randomisées dans les jeux concurrents). PhD thesis, University of Paris-Saclay, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01519354.

[bib.bib23] [23] Jannis Uhlendorf, Agnès Miermont, Thierry Delaveau, Gilles Charvin, François Fages, Samuel Bottani, Pascal Hersen, and Gregory Batt. In silico control of biomolecular processes. Computational Methods in Synthetic Biology, pages 277–285, 2015.

Optimally Controlling a Random Population

Abstract

Keywords and phrases:

Category:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Example 1.

Our Contribution.

Related work.

2 Preliminaries

Markov decision processes.

Random walks in winning regions.

Lemma 2 (Winning arenas).

Random Populations.

▶ Remark 3.

3 Symbolic Configurations

Definition 4 (Symbolic representations).

Definition 5 (K-definability).

Example 6.

4 Solving the Random Population Control Problem

Theorem 7.

▶ Remark.

Theorem 8.

Theorem 9.

Proof.

5 Theorem 6: Small Winning Arenas

Definition 10.

5.1 The Existence of Lucky Paths

Lemma 11.

Theorem 12 (Max flow-min cut [9]).

▶ Remark 13.

Theorem 14 (Integer flow theorem [9]).

Proof.

5.2 The Isolation Lemma

Definition 15 (ω-base and finite base).

Lemma 16 (Isolation Lemma).

Sketch of proof.

5.3 Proof of Theorem 7

6 Theorem 7: The Dynamic Flow Problem

Example 17.

Theorem 18 (Theorem 37 in [10]).

Lemma 19.

Proof of Theorem 8.

7 Lower bounds an a hard case

7.1 Complexity lower bound

Definition 20.

Theorem 21.

Proof sketch.

7.2 A Double-exponential Cut-off

7.3 A Butterfly

Idea.

Lemma 22.

Proof.

8 Conclusion

References

$\blacktriangleright$ Remark 3.

Definition 5 ( $K$ -definability).

$\blacktriangleright$ Remark.

$\blacktriangleright$ Remark 13.

Definition 15 ( $\omega$ -base and finite base).