Optimally Controlling a Random Population

TL;DR

This work studies the random population control problem for arbitrarily large populations of identical agents, showing that deciding almost-sure synchronization is EXPTIME-complete. The authors combine a bounded-abstraction reduction with an algebraic treatment of unbounded transfers, using the flow semigroup and its dual symbolic mincut semigroup to characterize the existence of unbounded token transfers via max-flow/min-cut duality. They provide an EXPTIME algorithm and establish EXPTIME-hardness through a Countdown-Game reduction, thereby proving optimal complexity. The paper introduces population arenas, omega-bases, and funneling/gathering strategies to manage large crowds and presents a path toward scalable verification in parameterized settings.

Abstract

The population control problem is a parameterized control problem where a population of agents has to be moved simultaneously into a target state. The decision problem asks whether this can be achieved for a finite but arbitrarily large population. We focus on the random version of this problem, where every agent is a copy of the same automaton and non-determinism on the global action chosen by the controller is resolved independently and uniformly at random. Controller seeks to almost-surely gather the agents in the target states. We show that the random population control problem is exptime-complete.

Figures (8)

• Figure 1: An automaton for which Controller wins against a random environment but not an adversarial one. The initial state is on the left and the target is the one on the right. Omitted, but implicitly present is a sink state, to which all states move on actions not shown.
• Figure 2: A positive instance of the .
• Figure 3: Controller tries to follow the black path from ${\overline{i}}$ to $\overline{F}$. Isolated tokens (in blue) may be spawned along that path. Lemma \ref{['lem:onlyone']} guarantees that they are alone in their state at all times along the path. However, we may be unlucky and diverge from the path (red arrow), with those stray tokens potentially meeting. We then try again to reach $\BoundK{W}{}$ by selecting a new black path, possibly spawning new isolated tokens (in orange). If we get unlucky again, we try to recover them using a new black path, and maybe spawning some new (green) isolated tokens. Lemma \ref{['lem:isolation']} will let us guarantee that tokens of different colors never meet before being brought back to an $\omega$. This means that we have at most $|S|$ layers, since we cannot have more than $|S|$ isolated groups. We define $Y$ as the union of all those layers: it is a "winning@@arena" "arena".
• Figure 4: The waiting (on left) and the control gadgets (on right). Edges labelled by $\Sigma_X$ are shorthand for several edges, one for each action in $\Sigma_X$. All but the depicted actions are daemonic.
• Figure 5: A (4-bit) Binary Counter. Not displayed are edges labelled by $\texttt{(dec{i})}$ that make the respective actions daemonic for state $\texttt{(i:{0})}$, and error actions $\texttt{error{i}}$, which are daemonic for $\texttt{(i:{0})}$ and $\texttt{(i:{1})}$, for all bits $i\in\{0,1,2,3\}$.

Theorems & Definitions (48)

• Example 1
• Lemma 2: Winning arenas
• Example 3
• Definition 4: Symbolic configurations and commits
• Definition 5
• Definition 6: $K$-definability
• Theorem 7: Almost-surely winning with a few stray sheep
• Remark
• Lemma 8
• Lemma 8