Population Protocols over Ordered Agents

Blondin, Michael; Cadilhac, Michaël; Courchesne, Benjamin; Guillou, Lucie; Mascle, Corto; Vialard, Isa

doi:10.4230/LIPIcs.ICALP.2026.167

Population Protocols over Ordered Agents

Michael Blondin

Département d’informatique, Université de Sherbrooke, Canada Michaël Cadilhac

DePaul University, Chicago, IL, USA Benjamin Courchesne

Département d’informatique, Université de Sherbrooke, Canada Lucie Guillou

MPI for Software Systems, Kaiserslautern, Germany Corto Mascle

MPI for Software Systems, Kaiserslautern, Germany Isa Vialard

MPI for Software Systems, Saarbrücken, Germany

Abstract

Population protocols are a distributed computation model in which a collection of anonymous, finite-state agents interact in randomly chosen pairs and update their states according to a fixed transition function. The computation is defined by the eventual stabilization of the population to a consensus that represents the output. In practice, it is natural to allow each agent to carry a unique identifier and compare it with that of another agent before interacting. We model this extension by having agents be totally ordered and interactions between two agents to be fireable only if their pair of identifiers falls in some condition set. For instance, $\mathsf{PP}[<]$ allows for two agents to interact only if the first one appears before the second one.

We study population protocols over ordered agents $\mathsf{PP}[\mathcal{N}]$ where $\mathcal{N}$ is a set of predicates available to restrict transition firing. We also study $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ , the immediate observation fragment of $\mathsf{PP}[\mathcal{N}]$ where only one agent changes state per interaction. Our main result is that $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ recognizes exactly the unambiguous star-free languages, which admits many other characterizations, such as two-variable first-order logic or two-way deterministic partially-ordered automata. We also provide a logic and an automaton model that fits in $\mathsf{PP}[<]$ . We further show that if the successor predicate appears in a set $\mathcal{N}$ of $\mathsf{NSPACE}(n)$ -computable predicates, then $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]=\mathsf{PP}[\mathcal{N}]=% \mathsf{NSPACE}(n)$ . Finally, we investigate the problem of deciding whether a given population protocol always stabilizes to a consensus. While this problem is decidable for unordered population protocols, we show that this is undecidable already for $\mathsf{PP}[<]$ and $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ , but conditionally decidable for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ .

Keywords and phrases:

Population protocols, First-order logic, Partially-ordered automata, Unambiguous star-free languages

Category:

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

Funding:

Michael Blondin: supported by a Discovery Grant from the Natural Sciences and Engineering Research Council of Canada (NSERC).

Copyright and License:

© Michael Blondin, Michaël Cadilhac, Benjamin Courchesne, Lucie Guillou,
Corto Mascle, and Isa Vialard; licensed under Creative Commons License CC-BY 4.0

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Formal languages and automata theory ; Theory of computation

\rightarrow

Distributed computing models ; Theory of computation

\rightarrow

Logic and verification

Related Version:

The full version with proofs is available at: https://arxiv.org/abs/2605.09937

Acknowledgements:

We thank the anonymous reviewers of ICALP 2026 for their thorough reading and valuable suggestions.

DOI:

10.4230/LIPIcs.ICALP.2026.167

Event:

53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

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

Population protocols form a well-established model of distributed computing where anonymous agents, with very limited individual computational power, work collectively to achieve a common task [3]. In this model, an input is scattered among agents that interact pairwise and must take a decision by reaching a consensus that is stable, that is, agents must eventually all agree on the output (“consensus”) and stop changing their mind (“stable”). Population protocols provide a theoretical framework for reasoning about a wide range of distributed systems, including networks of mobile sensors, chemical reaction networks, and social networks [5, 10, 11].

To familiarize the reader with population protocols, we present a classical protocol for the task of majority voting. A population consists of $n$ agents (who are not aware of $n$ ), each carrying a state from a finite set. Here, agents start with either $a$ or $b$ as their state. The population aims at collectively determining whether there are initially more $a$ ’s than $b$ ’s. At each discrete moment, a pair of agents is chosen arbitrarily and their respective state, from $Q=\{a,b,\underline{a},\underline{b}\}$ , is updated according to these rules:

active to passive	propagation of winning side	tiebreaker
$a,b\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\underline{a},% \underline{b}$	$a,\underline{b}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}a,% \underline{a}$	$\underline{a},\underline{b}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$% }}\underline{b},\underline{b}$
	$b,\underline{a}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}b,% \underline{b}$

Since agents are unordered, each rule $p,q\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}p^{\prime},q^{\prime}$ also stands for $q,p\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}q^{\prime},p^{\prime}$ . Here are three possible executions of the protocol starting from three different “inputs,” that is, assignments of an initial state $a$ or $b$ to each agent:

\displaystyle aaabb

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle aa\underline{a}b\underline{b}

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle a\underline{a}\underline{a}\underline{b}\underline{b}

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle a\underline{a}\underline{a}\underline{a}\underline{b}

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle a\underline{a}\underline{a}\underline{a}\underline{a},

\displaystyle aabbb

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle a\underline{a}\underline{b}bb

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle a\underline{a}\underline{a}bb

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle\underline{a}\underline{a}\underline{a}\underline{b}b

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle\underline{a}\underline{a}\underline{b}\underline{b}b

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle\underline{a}\underline{b}\underline{b}\underline{b}b,

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle\underline{b}\underline{b}\underline{b}\underline{b}b,

\displaystyle aabb

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle a\underline{a}\underline{b}b

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle\underline{a}\underline{a}\underline{b}\underline{b}

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle\underline{a}\underline{b}\underline{b}\underline{b}

\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{}}$}}\

\displaystyle\underline{b}\underline{b}\underline{b}\underline{b}.

Assuming fair scheduling (e.g., choosing agents uniformly at random), one can show that the population stabilizes (almost surely) to the correct outcome: if there is a majority of $a$ ’s initially, then agents eventually remain in $\{a,\underline{a}\}$ , otherwise they eventually remain in $\{b,\underline{b}\}$ .

As agents and rules are unordered, each configuration can be seen as a multiset $\bm{c}\colon Q\to\mathbb{N}$ where $\bm{c}(q)$ indicates the number of agents in state $q$ . It is known that population protocols compute precisely the subsets of $\mathbb{N}^{Q}$ that are semilinear [4], or, equivalently, that are definable in Presburger arithmetic (the first-order theory of the naturals with order and addition). In particular, majority voting amounts to computing the predicate $\varphi(\bm{c})=\bm{c}(a)>\bm{c}(b)$ .

From a modeling perspective, the fact that agents are unordered is meant to correspond to a situation in which agents are replicated and anonymous entities, and hence have no identifiers and are indistinguishable. Yet, it is natural to allow replicated agents to be totally ordered, e.g., they could be devices with a unique identifier, such as a serial number, stored in read-only memory. In this context, interactions may depend on the relationships between these identifiers.

From the perspective of automata theory, this corresponds to considering population protocols where configurations are words rather than multisets. Standard population protocols can be seen as computing commutative properties of words, such as $|w|_{a}>|w|_{b}$ , while the word setting additionally allows for noncommutative properties, such as “the middle agent has an $a$ ” or “agents strictly alternate between $a$ and $b$ .”

Contribution

Motivated by the above, we propose to study population protocols with totally-ordered agents. The class of population protocols so defined, $\mathsf{PP}[\mathcal{N}]$ , is parameterized by a set $\mathcal{N}$ of predicates over positions that can be used to restrict transition firings. Central to our study is the class $\mathsf{PP}[<]$ , in which a transition $p,q\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{<}}$}}r,s$ can only be applied to two agents in respective states $p$ and $q$ if the first agent appears before the second agent. We consider a well-studied restriction called immediate observation [4] where an interaction can only update a single agent, called the “observer.”

Our main result, Theorem 12, establishes that $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ has the same expressive power as unambiguous star-free languages, an important subclass of regular languages that admits a trove of characterizations (see [32] for a lovely survey on the pervasiveness of this class in automata theory). Hence, $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ is the class of languages captured by these formalisms over finite words:

$\blacksquare$

partially-ordered unambiguous automata [25];
$\blacksquare$

partially-ordered two-way deterministic automata [31];
$\blacksquare$

$\mathsf{LTL}[\mathbf{F}^{-1},\mathbf{F}]$ : linear temporal logic with past and future operators [15];
$\blacksquare$

$\mathsf{FO}^{2}[<]$ : the two-variable fragment of first-order logic with order [33];
$\blacksquare$

$\Delta_{2}[<]$ : the intersection of the $\exists^{*}\forall^{*}$ and $\forall^{*}\exists^{*}$ fragments of first-order logic with order [27];
$\blacksquare$

languages recognized by finite monoids from the variety $\mathsf{DA}$ [30].

This provides the first characterization of this class in terms of distributed computing, rather than automata, logic, or algebra. We will provide in Example 3 an example of a $\mathsf{PP}[<]$ protocol whose language is not regular, and therefore not expressible by $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ protocols.

In addition, we explore systematically the classes induced by our definitions:

$\blacksquare$

In Section 3, we provide a toolbox to study population protocols over ordered agents $\mathsf{PP}[\mathcal{N}]$ , regardless of $\mathcal{N}$ . We study protocols that need to stabilize only if they reach a positive consensus, which we call semi-deciders, as opposed to protocols that always stabilize to a consensus, dubbed deciders. We also refine the technology of protocols with stabilizing inputs, studied in [29], which enables a form of composition between protocols.
$\blacksquare$

In Section 4, we prove the aforementioned characterization of $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ , and in Section 5, we provide a natural logic and an automaton model expressible in $\mathsf{PP}[<]$ . In this latter section, we fall short of showing exact characterizations, but provide conjectures based on our new models.
$\blacksquare$

In Section 6, we explore the expressiveness of $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ and $\mathsf{PP}[\mathcal{N}]$ when the successor predicate is available, that is, when transitions can be restricted to fire only if they act on two adjacent agents. We show that if all the predicates of $\mathcal{N}$ are $\mathsf{NSPACE}(n)$ computable, then $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]=\mathsf{PP}[\mathcal{N}]=% \mathsf{NSPACE}(n)$ – this is arguably less surprising than our main result on $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ , as the successor allows for the left-to-right propagation of information.
$\blacksquare$

Finally, since protocols are only well-behaved when they are deciders, and since this property is semantic, we explore in Section 7 whether we can check if a given population protocol is a decider. We thus ask if the syntax of deciders is decidable – this is sometimes called the well-specification problem. We show that it is undecidable for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ , $\mathsf{PP}[+1]$ , and $\mathsf{PP}[<]$ , and conditionally decidable for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ .

Related work

Our model is closely related to the community protocols of Guerraoui and Ruppert [19]. These are population protocols where each agent has a unique identifier; each agent can store a constant number of identifiers; and interactions depend on these identifiers but only with respect to their relative order. The motivation of Guerraoui and Ruppert was to devise an extension of population protocols, as mild as possible, which would be fault-tolerant. They proved that community protocols can decide languages from $\mathsf{NSPACE}(n\log n)$ while tolerating Byzantine failures of a constant number of agents [19]. The unique identifier of each agent is considered to be stored in read-only memory, as in real-world low-cost chips, and so exempt from Byzantine failures. Our model corresponds to community protocols where each agent has a single immutable register initialized to its unique identifier.

Bournez, Cohen, and Rabie introduce homonym protocols, a parameterized restriction of community protocols, where the $n$ agents have $f(n)$ identifiers [8]. The cases of $f(n)=1$ and $f(n)=n$ are respectively population protocols (everyone has the same identifier) and community protocols (there are as many identifiers as agents). Identifiers are from $[0..f(n)-1]$ and agents can compare them with respect to $x<y$ , $x=y$ , $x=y+1$ and $x=0$ .

In [17], Gańczorz et al. introduce selective population protocols as an extension of population protocols where the state space is partitioned into finitely many “groups,” and where an interaction picks at random an initiator in state $s$ , and then a responder in state $s^{\prime}$ from the group of $s$ , provided it is nonempty. This is a powerful model that allows for zero-tests, i.e., checking whether no agent holds a certain state. Thus, selective population protocols are orthogonal to our model. However, the authors dedicate a section to the median problem: $\bigcup_{n\geq 0}\Sigma^{n}a\Sigma^{n}$ . They show that if selective population protocols are extended with the possibility of comparing keys, then they can solve the median problem in time $\mathcal{O}(\log^{4}n)$ . The authors further provide a short proof that, without leveraging the “selective” aspect of their model (i.e., groups and zero-tests), any population protocol for the median problem must work in expected time $\Omega(n)$ . This latter setting, only briefly discussed in [17], corresponds to our model.

Further extensions include mediated population protocols [24], where communication edges have an internal state; population protocols with unordered data [6], where the input alphabet is infinite; and population protocols for graph class identification problems [37, 2], where agents aim at determining whether the communication topology satisfies some property. For other work on immediate-observation protocols, see [14, 35, 12, 34].

2 Preliminaries

Automata and logic.

We assume some familiarity with formal languages, automata theory and logic over finite words (e.g., see the textbook [12]). For a word $w\in\Sigma^{*}$ , we write $w[i]$ for the $i$ -th letter of $w$ , starting at 1, and $w[i..j]$ for the infix $w[i]w[i+1]\cdots w[j]$ . For $\sigma\in\Sigma$ , we write $|w|_{\sigma}$ for the number of occurrences of $\sigma$ in $w$ .

We write $\mathsf{FO}$ to denote first-order logic over words, where quantifiers range over positions, that is, the set $\{1,\ldots,|w|\}$ for a given word $w$ , and where $a(x)$ holds with respect to $w$ iff $w[x]=a$ (see, e.g., [12, Chap. 8] for formal definitions). We write $\mathsf{FO}[<]$ for the extension of $\mathsf{FO}$ with the numerical predicate $<$ , that allows to test whether $x<y$ for two positions $x$ and $y$ . For example, the sentence $\varphi=(\exists x)(\forall y)[a(x)\land((x<y)\rightarrow b(y))]$ describes the language $\Sigma^{*}ab^{*}$ . By abuse of notation, $\mathsf{FO}[<]$ stands for both the set of syntactic sentences and for the class of languages described by these sentences. It is well known that $\mathsf{FO}[<]$ is the class of star-free (regular) languages.

We write $\Sigma_{i}[<]$ (resp. $\Pi_{i}[<]$ ) for the fragment of $\mathsf{FO}[<]$ of sentences in prenex normal form with $i$ blocks of alternating quantifiers starting with $\exists$ (resp. $\forall$ ). For example, $\Sigma^{*}ab^{*}$ belongs to $\Sigma_{2}[<]$ due to the form of our example $\varphi$ . We let $\Delta_{i}[<]=\Sigma_{i}[<]\cap\Pi_{i}[<]$ .

Population protocols over ordered agents.

A population protocol (PP) describes how a totally-ordered set of finite-state agents interact and reach a decision about their overall initial states. Interactions can happen between any pair of agents, and predicates are used to restrict how transitions can be taken, based on the position of the agents in the order.

(Syntax.) We extend classical PPs to allow for transitions to carry a test on the positions of the totally-ordered agents. Let $\mathcal{N}\subseteq 2^{\mathbb{N}\times\mathbb{N}}$ be any set, whose elements we call numerical predicates: these will be used as the allowed tests on a transition.¹¹1These are sometimes called uniform numerical predicates in the literature, to emphasize the fact that they do not depend on the total number of agents. A natural predicate that is not uniform is $\mathbf{max}(x)$ which is true if $x$ is the position of the last agent. This technical difference will not impact our results. We let $\textbf{{true}}=\mathbb{N}^{2}$ be the always-true predicate. The set $\mathsf{PP}[\mathcal{N}]$ of PPs over $\mathcal{N}$ is the set of transition systems $(Q,\Sigma,O,\Delta)$ where $Q$ is a finite set of states, $\Sigma\subseteq Q$ is a distinguished subset of initial states, $O\colon Q\to\{\top,\bot\}$ maps each state to an opinion, and $\Delta\subseteq Q^{2}\times(\mathcal{N}\cup\{\textbf{{true}}\})\times Q^{2}$ is a set of transitions. An element of $\Delta$ is denoted $q_{1},q_{2}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{P}}$}}q_{3},q_{4}$ , expressing, intuitively, that if two distinct agents meet, the first being in position $i$ and state $q_{1}$ , the second in position $j$ and state $q_{2}$ , such that $(i,j)\in P$ , then the first agent changes its state to $q_{3}$ and the second to $q_{4}$ . We use $\Sigma$ for the set of initial states as we would like to see such protocols as language acceptors: The initial configuration should be thought of as an input word over alphabet $\Sigma$ .

If $\mathcal{N}=\{P_{1},P_{2},\ldots\}$ , we write $\mathsf{PP}[P_{1},P_{2},\ldots]$ for $\mathsf{PP}[\mathcal{N}]$ . Classical PPs can be seen as the class $\mathsf{PP}[\emptyset]$ , recalling that we assume that true is always available as a numerical predicate. Our main interest is in the class $\mathsf{PP}[<]$ , where $<$ is seen as the set of pairs $(i,j)$ with $i<j$ , but we will study more expressive predicates in Sections 3 and 6.

A PP is immediate-observation if at most one agent changes state in each interaction, i.e., every transition is of the form $a,b\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{P}}$}}a,c$ or $a,b\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{P}}$}}c,b$ . We write $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ for the class of protocols in $\mathsf{PP}[\mathcal{N}]$ that are immediate-observation.

(Semantics.) Since our agents are totally ordered, we define the configuration of a system as a word of $Q^{+}$ . Initial configurations are words of $\Sigma^{+}$ . Let $u$ and $v$ be two configurations of the same length, we say that $u$ leads to $v$ , denoted $u\to v$ , if the two configurations are equal except at potentially two distinct positions $i$ and $j$ , and there is a transition $u[i],u[j]\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{P}}$}}v[i],v[j]\in\Delta$ with $(i,j)\in P$ . We let ${\to^{*}}$ be the reflexive transitive closure of ${\to}$ .

Consensus and stability.

With $w$ a configuration, let $O(w)\in\{\bot,\top\}$ be the common opinion of all states appearing in $w$ , if there is one; otherwise $O(w)$ is undefined. A configuration $w$ is a $b$ -consensus if $O(w)=b$ . It is further $b$ -stable if $w\to^{*}v$ implies that $v$ is a $b$ -consensus.

Example 1.

We give an example of a protocol in $\mathsf{PP}[<]$ . Consider the transition system $\mathcal{P}=(\{a,b,q_{\bot}\},\{a,b\},O,\Delta)$ , with $O(a)=O(b)=\top$ , $O(q_{\bot})=\bot$ , and transitions $b,a\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{<}}$}}q_{\bot},q_{\bot}$ and $q_{\bot},\_\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\textbf{{true}}}}$}% }q_{\bot},q_{\bot}$ with “ $\_$ ” standing for any state. Every input configuration belongs to $(a+b)^{+}$ and is therefore a $\top$ -consensus (all agents output $\top$ initially). However, such configurations need not be $\top$ -stable. For instance, starting from $b a$ we can apply the rule $b,a\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{<}}$}}q_{\bot},q_{\bot}$ and obtain $q_{\bot}q_{\bot}$ , which is $\bot$ -stable. In contrast, every configuration in $a^{*}b^{*}$ is $\top$ -stable: it is a $\top$ -consensus and no transition is enabled.

Language of a PP.

Consider an infinite sequence $w_{0}\to w_{1}\to w_{2}\to\cdots$ of configurations, which we call a run. We say that it is fair if for every $w_{i}$ that appears infinitely often, each configuration of $\{v\mid w_{i}\to v\}$ appears infinitely often as well. By induction, fairness guarantees that each configuration of $\{v\mid w_{i}\to^{*}v\}$ appears infinitely often as well. Intuitively, fairness ensures that reachable configurations cannot be avoided forever (in a probabilistic setting, where the scheduling induces a probability distribution on the runs, the resulting runs are almost surely fair). We will assume that any configuration can be extended into a run, and so into a fair run, by implicitly adding “no operation” transitions.

The language of a PP $\mathcal{P}$ is the set $L(\mathcal{P})$ of initial configurations from which there is a fair run that visits a $\top$ -stable configuration. Naturally, an initial configuration can be the origin of a fair run visiting a $\top$ -stable configuration, another run visiting a $\bot$ -stable configuration, or even a run that visits no stable configurations. We single out PPs that have more crisp behaviors. We say that a PP is a decider when for all $w\in\Sigma^{*}$ , there is a $b\in\{\top,\bot\}$ such that all fair runs from $w$ visit a $b$ -stable configuration (i.e., for all finite runs from $w$ to some configuration $u$ , there is a path from $u$ to a $b$ -stable configuration). This is usually called well-specified in the literature and we justify our nomenclature in Section 3.1. We say that $L(\mathcal{P})$ is $\mathsf{PP}[\mathcal{N}]$ -decidable or $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ -decidable with the obvious meaning. We will identify $\mathsf{PP}[\mathcal{N}]$ and $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ with the class of languages decidable by these protocols.

Note that since population protocols are ill-defined when no agents are present, we adopt the convention, when working with their languages, to disregard the empty word.

Example 2.

Consider the protocol of $\mathsf{PP}[<]$ from Example 1. We show that it decides the language $a^{*}b^{*}$ . Every input in $a^{*}b^{*}$ is already $\top$ -stable. Conversely, if an input word is not in $a^{*}b^{*}$ , then it contains the factor $b a$ . Hence, in any fair run, the transition $(b,a)\to(q_{\bot},q_{\bot})$ is eventually executed. From that point on, every remaining agent eventually interacts with a $q_{\bot}$ -agent and is converted to $q_{\bot}$ , so the run reaches a configuration in $q_{\bot}^{*}$ , which is $\bot$ -stable.

Example 3.

Consider the median language $L=\bigcup_{n\in\mathbb{N}}\Sigma^{n}a\Sigma^{n}$ . Let us describe a protocol $\mathcal{P}=(Q,\Sigma,O,\Delta)$ that decides $L$ . The states are defined as $Q=\Sigma\times\{\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-1.pdf2svg.svg}}},\text{\scriptsize% \raisebox{0.25pt}{\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-5% 2-page-2.pdf2svg.svg}}},\text{\footnotesize\raisebox{-0.25pt}{\includegraphics% {dagpub-standalone-manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}\hskip 0.1% pt\}\times\{\bot,\top\}$ . The components respectively represent the input letter; a belief on whether the center is on the right, here, or on the left; and a belief on the output.

We identify input $a$ with state $(a,\text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}},\top)$ , and each input $\sigma\neq a$ with $(\sigma,\text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}},\bot)$ . We set $O((x,y,z))=z$ . The set $\Delta$ is defined by these rules, each describing a family of transitions:

	Population halving
(1)	$(x,\text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}},z),\ (x^{\prime},\text{% \scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-manual-2026-08% -03-17-37-52-page-2.pdf2svg.svg}}},z^{\prime})$	$\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{<}}$}}$	$(x,\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-1.pdf2svg.svg}}},\bot),\ (x^{\prime},\text{% \footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-manual-2026% -08-03-17-37-52-page-3.pdf2svg.svg}}}\hskip 0.1pt,\bot)$
	Center finding
(2)	$(x,\text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}},z),(x^{\prime},\text{% \footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-manual-2026% -08-03-17-37-52-page-1.pdf2svg.svg}}},z^{\prime})$	$\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{<}}$}}$	$(x,\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-1.pdf2svg.svg}}},\bot),(x^{\prime},\text{% \scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-manual-2026-08% -03-17-37-52-page-2.pdf2svg.svg}}},x^{\prime}=a)$
(3)	$(x,\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}\hskip 0.1pt,z),(x^{\prime},% \text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-manual-2% 026-08-03-17-37-52-page-2.pdf2svg.svg}}},z^{\prime})$	$\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{<}}$}}$	$(x,\text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}},x=a),(x^{\prime},\text{% \footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-manual-2026% -08-03-17-37-52-page-3.pdf2svg.svg}}}\hskip 0.1pt,\bot)$
	Output propagation
(4)	$(x,y,z),(x^{\prime},\text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub% -standalone-manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}},z^{\prime})$	$\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\textbf{{true}}}}$}}$	$(x,y,z^{\prime}),(x^{\prime},\text{\scriptsize\raisebox{0.25pt}{% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-2.pdf2svg.% svg}}},z^{\prime})$	for $y\in\{\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone% -manual-2026-08-03-17-37-52-page-1.pdf2svg.svg}}},\text{\footnotesize\raisebox% {-0.25pt}{\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-3% .pdf2svg.svg}}}\hskip 0.1pt\}$
(5)	$(x,y,\top),(x^{\prime},y^{\prime},\bot)$	$\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\textbf{{true}}}}$}}$	$(x,y,\bot),(x^{\prime},y^{\prime},\bot)$	for $y,y^{\prime}\in\{\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub% -standalone-manual-2026-08-03-17-37-52-page-1.pdf2svg.svg}}},\text{% \footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-manual-2026% -08-03-17-37-52-page-3.pdf2svg.svg}}}\hskip 0.1pt\}$

By fairness, the first rule must be used until one or zero remains. Moreover, by fairness, the second and third rules will respectively move the ’s to the left, and the ’s to the right. If some $(x,\text{\scriptsize\raisebox{0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}},y)$ remains, then, by fairness and the fourth rule, it will propagate its output $y$ , which is $\top$ iff $x=a$ , by the choice of initial states and by rule (2–3). Otherwise, if the population is of even length, the fifth rule will be used to propagate $\bot$ .

Figure 1 depicts all configurations reachable from the initial configuration $aab\in L$ . Any fair run of a population protocol leads to a bottom strongly connected component of such a reachability graph. Thus, in this example, every fair runs leads to $a_{\text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37% -52-page-1.pdf2svg.svg}}}^{\top}a_{\text{\tiny\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}}^{\top}b_{\text{% \scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-% 3.pdf2svg.svg}}}^{\top}$ , which is $\top$ -stable. Note that $a_{\text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37% -52-page-1.pdf2svg.svg}}}^{\bot}a_{\text{\scriptsize\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}^{\bot}b_{\text{% \tiny\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-2.pdf2% svg.svg}}}^{\bot}$ is a $\bot$ -consensus, but is not $\bot$ -stable.

Figure 1: Configurations reachable from

a a b

, where

x_{y}^{z}

stands for

(x,y,z)

. Self-loops arising from “no operation” transitions are omitted. The hatched nodes are consensuses; the bottom one is stable.

Further observe that the reachability graph of Figure 1 has non-trivial cycles, for instance:

a_{\text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37% -52-page-1.pdf2svg.svg}}}^{\bot}a_{\text{\tiny\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}}^{\top}{\color[rgb]% {0.9921875,0.546875,0.0703125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.9921875,0.546875,0.0703125}b_{\text{\scriptsize\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}^{\bot}}\to a_{% \text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52% -page-1.pdf2svg.svg}}}^{\bot}a_{\text{\tiny\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}}^{\top}{\color[rgb]{% 0.1015625,0.0703125,0.9921875}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.1015625,0.0703125,0.9921875}b_{\text{\scriptsize\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}^{\top}}\to a_{% \text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52% -page-1.pdf2svg.svg}}}^{\bot}a_{\text{\tiny\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}}^{\top}{\color[rgb]{% 0.9921875,0.546875,0.0703125}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.9921875,0.546875,0.0703125}b_{\text{\scriptsize\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}^{\bot}}\to a_{% \text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52% -page-1.pdf2svg.svg}}}^{\bot}a_{\text{\tiny\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}}^{\top}{\color[rgb]{% 0.1015625,0.0703125,0.9921875}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.1015625,0.0703125,0.9921875}b_{\text{\scriptsize\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}^{\top}}\to\cdots

Informally, the first and second agents are fighting to convince the third agent. However, by fairness, this is not allowed to happen indefinitely. Eventually, the configuration $a_{\text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37% -52-page-1.pdf2svg.svg}}}^{\top}a_{\text{\tiny\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-2.pdf2svg.svg}}}^{\top}b_{\text{% \scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-% 3.pdf2svg.svg}}}^{\top}$ , at the bottom, is reached.

In the above specific protocol $\mathcal{P}$ , for each initial configuration, the reachability graph has a unique trivial bottom strongly connected component, made of one configuration of the form $\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-1.pdf2svg.svg}}}^{n}\text{\scriptsize\raisebox% {0.25pt}{\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-2.% pdf2svg.svg}}}\,\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-3.pdf2svg.svg}}}\hskip 0.1pt^{n}$ or $\text{\footnotesize\raisebox{-0.25pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-1.pdf2svg.svg}}}^{n}\text{\footnotesize% \raisebox{-0.25pt}{\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-% 52-page-3.pdf2svg.svg}}}\hskip 0.1pt^{n}$ . However, in general, it needs not be unique or trivial. A fair run becomes $b$ -stable iff it visits a bottom strongly connected component whose configurations are all $b$ -consensuses.

In a decider, for a given initial configuration, all bottom strongly connected components must consist only of stable configurations, all of the same output.

We now provide a generic upper bound on the complexity of languages decided by population protocols; we will exhibit a matching lower bound in Section 6 for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ . Recall that $\mathsf{NSPACE}(n)$ is the class of languages recognized by linear-bounded nondeterministic Turing machines, i.e., nondeterministic machines that require space $O(n)$ over inputs of size $n$ . Languages of this class are exactly the context-sensitive languages [22].

Theorem 4.

Let $\mathcal{N}$ be a set of numerical predicates, all of which decidable in $\mathsf{NSPACE}(n)$ . We have $\mathsf{PP}[\mathcal{N}]\subseteq\mathsf{NSPACE}(n)$ .

Proof.

Recall that a configuration is $\top$ -stable if every reachable configuration from it is a $\top$ -consensus (i.e., all agents have opinion $\top$ ). Consider a protocol in $\mathsf{PP}[\mathcal{N}]$ . The set of configurations that are not $\top$ -stable is decidable in $\mathsf{NSPACE}(n)$ . Indeed, it is sufficient to nondeterministically guess a partial run (i.e., a finite sequence of configurations $w_{0}\to w_{1}\to\dots\to w_{n}$ ) that leads to a configuration that is not a $\top$ -consensus. Each transition can be guessed, its condition checked, and its effect applied in $\mathsf{NSPACE}(n)$ .

By the Immerman–Szelepcsényi theorem, $\mathsf{NSPACE}(n)$ is closed under complement, and so the set of $\top$ -stable configurations is in $\mathsf{NSPACE}(n)$ . Since the protocol is a decider, to check that a word $w$ is accepted, it is sufficient to nondeterministically guess a partial run from $w$ , and check that it ends in a $\top$ -stable configuration. These are all tasks in $\mathsf{NSPACE}(n)$ . $\hfill\blacktriangleleft$

3 Semantic restrictions of population protocols: a toolbox

In this section, we define two restrictions of population protocols that will be used to simplify our constructions.

We first define semi-deciders, which do not require the full behavior of deciders with respect to stable configurations. Throughout the next sections, we will see that semi-deciders are much easier to define for some languages, and we will rely on the forthcoming Lemma 6 to combine semi-deciders into deciders.

We then define protocols with stabilizing inputs, which are protocols where agents can change their mind about their input. Such protocols are harder to design, since they are more robust to change, but we show, in Lemma 11, that they exhibit a strong closure property: they are closed under alphabet rewriting.

3.1 Semi-deciders

Definition 5.

We say that a PP semi-decides $L\subseteq\Sigma^{+}$ if for all $u\in\Sigma^{+}$ and every fair run $\rho$ starting from $u$ , we have $u\in L$ iff $\rho$ contains a $\top$ -stable configuration. We use the terms $\mathsf{PP}[\mathcal{N}]$ -semi-decidable and $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ -semi-decidable with the obvious meaning.

Note that a decider is a semi-decider in which we additionally require that $u\notin L$ iff $\rho$ visits a $\bot$ -stable configuration; that is, all fair runs visit a stable configuration. Illustrating the differences, Figure 2 shows the situations that can occur for runs from an input $w$ .

Figure 2: Configurations labeled , and are

\top

-stable,

\bot

-stable, and configurations from which no stable configurations are reachable. Arrows depict partial, finite runs. Situations (1-6) can happen in PP. Only situations (4-6) can happen in semi-deciders, while only situations (5-6) can in deciders.

Our naming convention is justified by the following property:

Lemma 6.

A language $L$ is $\mathsf{PP}[\mathcal{N}]$ -decidable iff $L$ and its complement are $\mathsf{PP}[\mathcal{N}]$ -semi-decidable. The same holds for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ .

Proof sketch.

We combine the two semi-deciders for $L$ and for $\Sigma^{+}\setminus L$ by running them in parallel. Each agent stores a pair of states, one for each semi-decider, together with a belief indicating which semi-decider it currently trusts. Transitions either simulate one step of one of the semi-deciders, or flip the belief so that beliefs can align; in particular, an agent may flip when it meets an agent with the opposite belief, or when its currently trusted component produces a $\bot$ -witness. For any input $u$ , exactly one of the two simulations eventually provides such a witness (since exactly one of $u\in L$ or $u\notin L$ holds), which forces all agents to converge to the correct belief and yields a stable consensus, hence a decider. $\hfill\blacktriangleleft$

We note these elementary closure properties:

Lemma 7.

If $L_{1},L_{2}\subseteq\Sigma^{+}$ are $\mathsf{PP}[\mathcal{N}]$ -semi-decidable, then it is also the case for $L_{1}\cap L_{2}$ and $L_{1}\cup L_{2}$ . This further holds for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ and deciders.

3.2 Protocols with stabilizing inputs

Agents of a protocol are generally not aware that they have reached a stable consensus and hence “terminated.” To carry out a task A and use its output in a subsequent task B, a protocol has to perform both tasks concurrently. The protocol for task B thus guesses what the output of task A is going to be, but ought to be able to self-correct if it becomes clear that the guess was wrong. In this subsection, we introduce a formal notion for this “self-correction” which will simplify the design of composable protocols; this is inspired by a recent presentation of [29] for $\mathsf{PP}[\emptyset]$ .

Let us consider protocols where each agent keeps a copy of its input. Formally, a protocol $\mathcal{P}=(Q,\Sigma,O,\Delta)$ is said to be input-saving if

$\blacksquare$

$Q=\Sigma\times R$ for some finite set $R$ ;
$\blacksquare$

Each $\sigma\in\Sigma$ is identified with $(\sigma,r_{\sigma})$ for some $r_{\sigma}\in R$ ; and
$\blacksquare$

The first component $\sigma$ of any state $(\sigma,r)\in Q$ is left unchanged by all transitions of $\Delta$ .

For all $w\in Q^{+}$ , let $\iota(w)\in\Sigma^{+}$ be the projection of $w$ onto its first component. Given $u,v\in Q^{n}$ , we write $u\rightsquigarrow v$ if either $u\to v$ , or $v$ equals $u$ except at a single position $i$ where $u[i]=(\sigma,r)$ and $v[i]=(\sigma^{\prime},r)$ . This second type of transitions models a “change of mind” of agent $i$ on its input. We write $\rightsquigarrow^{*}$ for the reflexive transitive closure of $\rightsquigarrow$ . Note what we do not change the definition of run, which still relies on $\to$ only.

Definition 8.

We say that $\mathcal{P}$ semi-decides $L\subseteq\Sigma^{+}$ with stabilizing inputs if (a) $\mathcal{P}$ is input-saving, and (b) for all $u\in\Sigma^{+}$ , all $u\rightsquigarrow^{*}v$ and every fair run $\rho$ starting from $v$ , it is the case that $\iota(v)\in L$ iff $\rho$ visits a $\top$ -stable configuration. We use the term “decides” if (b) is strengthened with the condition that $\iota(v)\notin L$ iff $\rho$ visits a $\bot$ -stable configuration.

Note that this is more robust than simply semi-deciding: if $\mathcal{P}$ semi-decides $L$ with stabilizing inputs, then it semi-decides $L$ . Intuitively, after $u\rightsquigarrow^{*}v$ , the configuration of the population (i.e., the projection of $v$ onto the second component) may be incompatible with $\iota(v)$ since agents have possibly changed their mind several times on their input. Computing with stabilizing inputs means that the protocol is able to fix its configuration so that it reflects the expected output on $\iota(v)$ .

It is known that any language $L\in\mathsf{PP}[\emptyset]$ can be decided, and hence semi-decided, with stabilizing inputs²²2It was claimed earlier by [2], but definitions and proofs were deferred to a full paper that never appeared. [29]. Let us turn to an example, which will be useful later:

Proposition 9.

The language $0^{*}1^{*}\cdots k^{*}$ is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -semi-decidable with stabilizing inputs.

Proof sketch.

Let $\Sigma=\{0,1,\ldots,k\}$ and $L=0^{*}1^{*}\cdots k^{*}$ . The protocol $\mathcal{P}=(Q,\Sigma,\Delta,O)$ for $L$ is defined by $Q=\Sigma\times\{\top,\bot\}$ , $O((\sigma,o))=o$ , each $\sigma\in\Sigma$ identified with $(\sigma,\top)$ , and these rules:

	$\displaystyle(x,\top),(y,o)$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\mathmakebox[15pt% ][c]{<}}}$}}(x,\bot),(y,o)$	$\displaystyle\text{for $x>y$},$
	$\displaystyle(x,\bot),(y,o)$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\mathmakebox[15pt% ][c]{\textbf{{true}}}}}$}}(x,\top),(y,o).$

The purpose of the first rule is to detect a misordering. The second rule allows any agent to nondeterministically reset itself. $\hfill\blacktriangleleft$

We now turn to closure properties of protocols with stabilizing inputs. We first cover union and intersection, then move on to (nondeterministic) alphabet rewriting.

Lemma 10.

If $L_{1},L_{2}\subseteq\Sigma^{+}$ are $\mathsf{PP}[\mathcal{N}]$ -semi-decidable with stabilizing inputs, then it is also the case for $L_{1}\cap L_{2}$ and $L_{1}\cup L_{2}$ . This further holds for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ and deciders.

Given $f\colon\Sigma\to 2^{\Gamma}$ and $w\in\Sigma^{n}$ , let $f(w)=\{w_{1}^{\prime}\cdots w_{n}^{\prime}\mid w_{i}^{\prime}\in f(w_{i})\text% { for each }i\in[1..n]\}$ . For example, if $f(0)=\{a,b\}$ and $f(1)=\{b,c\}$ , then $f(01)=\{ab,ac,bb,bc\}$ . We extend this notion to languages: $f(L)=\bigcup_{w\in L}f(w)$ .

Lemma 11.

Let $f\colon\Sigma\to 2^{\Gamma}$ . If $L\subseteq\Sigma^{+}$ is $\mathsf{PP}[\mathcal{N}]$ -semi-decidable with stabilizing inputs, then $f(L)$ is $\mathsf{PP}[\mathcal{N}]$ -semi-decidable with stabilizing inputs. This further holds for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ .

Proof sketch.

The construction builds a protocol that semi-decides $f(L)$ by simulating, in its second component, the input-saving semi-decider for $L$ on a guessed word $v\in\Sigma^{+}$ compatible with the real input $u\in\Gamma^{+}$ (i.e., $u\in f(v)$ ). Agents may revise this guess: whenever a $\bot$ opinion is observed in the simulated component, an agent is allowed to change its guessed letter to any $\sigma$ consistent with its input letter (preserving $u\in f(v)$ letterwise). If $u\in f(L)$ , fairness ensures that the population can eventually rewrite the guessed word into some $v^{\prime}\in L$ , after which the simulation of the semi-decider for $L$ reaches a $\top$ -stable configuration and changes become disabled; if $u\notin f(L)$ , reaching a $\top$ -stable configuration would force the simulated input to lie in $L$ , which is not possible. $\hfill\blacktriangleleft$

4 Expressiveness of IO-PP $[<]$

In this section, we provide a precise characterization of the languages decided by $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ . For any language $L\subseteq\Sigma^{*}$ , let us write ${\equiv_{L}}$ for the syntactic congruence of $L$ , i.e., $w\equiv_{L}w^{\prime}$ iff $uwv\in L\Leftrightarrow uw^{\prime}v\in L$ for all $u,v\in\Sigma^{*}$ . A language is in the class $\mathsf{DA}$ if it is regular, and satisfies, writing $\alpha(w)\subseteq\Sigma$ for the set of letters appearing in a word $w$ :

\displaystyle(\forall w\in\Sigma^{*})\left[w\equiv_{L}w^{2}\rightarrow(\forall h% \in\alpha(w)^{*})[w\equiv_{L}w\cdot h\cdot w]\right],

(1)

It is a fascinating result of Pin and Weil [27] that $\mathsf{DA}=\Delta_{2}[<]$ . We will leverage both characterizations to show the theorem below. The left-to-right inclusion will rely on (1), and the converse on $\mathsf{DA}=\Delta_{2}[<]$ , semi-deciders, and protocols with stabilizing inputs.

Theorem 12.

$\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]=\mathsf{DA}$ .

4.1 IO-PP $[<]\subseteq$ DA

We first show that the set of stable configurations in a $\mathsf{PP}[<]$ , and thus in an $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ , admits a simple description. Given a finite alphabet $\Sigma$ and two words $u,v\in\Sigma^{*}$ , we say that $u$ is a subword of $v$ , written $u\preceq v$ , if $u$ can be obtained from $v$ by removing letters. It is well known that ${\preceq}$ is a well-quasi-order over $\Sigma^{*}$ [21]. A consequence is that every strictly decreasing sequence of subword-closed sets must be finite.

Lemma 13.

Any protocol in $\mathsf{PP}[<]$ is a well-structured transition system w.r.t. $\preceq$ , that is, for all $u,u^{\prime},w\in Q^{*}$ with $u\preceq w$ and $u\to u^{\prime}$ , there exists $w^{\prime}$ such that $u^{\prime}\preceq w^{\prime}$ and $w\to w^{\prime}$ . Further, the set of $b$ -stable configurations is subword-closed and computable.

As expected from the definition of $\mathsf{DA}$ , the core of the argument showing the inclusion of $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ in $\mathsf{DA}$ will rely on a pumping argument. As a first observation, we show that, in an $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ , an infix of the form $w z w$ with $\alpha(z)\subseteq\alpha(w)$ can, in some sense, mimic the behavior of the protocol on the simpler infix $w$ .

Lemma 14.

In an $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ , if $uwv\to^{*}u^{\prime}w^{\prime}v^{\prime}$ with $|u|=|u^{\prime}|$ and $|v|=|v^{\prime}|$ , then for all $z$ with $\alpha(z)\subseteq\alpha(w)$ , there exists $z^{\prime}$ such that $uwzwv\to^{*}u^{\prime}w^{\prime}z^{\prime}w^{\prime}v^{\prime}$ and $\alpha(z^{\prime})\subseteq\alpha(w^{\prime})$ .

We use this first result to show a pumping lemma on $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ . It results from the fact that the sets of $\top$ -stable and $\bot$ -stable configurations are subword-closed and Lemma 14.

Lemma 15.

Let $L\in\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ . There exists a computable $m\geq 1$ such that, for all $w_{1},\ldots,w_{m}\in\Sigma^{+}$ and $z\in\Sigma^{*}$ with $\alpha(w_{1})=\ldots=\alpha(w_{m})\supseteq\alpha(z)$ , we have $w_{1}\cdots w_{m}\equiv_{L}(w_{1}\cdots w_{m})z(w_{1}\cdots w_{m})$ .

Proof sketch.

Lemma 13 indicates that for both $b\in\{\top,\bot\}$ , the set of $b$ -stable configurations is subword-closed. As a consequence, writing $B^{\varepsilon}$ for $B\cup\{\varepsilon\}$ , it is a finite union of languages of the form $A_{1}^{*}B_{1}^{\varepsilon}\cdots A_{k}^{*}B_{k}^{\varepsilon}$ with $A_{i},B_{i}$ subsets of $Q$ , the set of states of our protocol [20, Sect. 6.1.1]. Let $K_{b}$ be the maximal factorization size $k$ over all those languages, $K=\max(K_{\top},K_{\bot})$ and $m=2K+1$ . Lemma 13 also states that the set of $b$ -stable configurations is computable for both $b$ , in particular we can compute $K_{\top},K_{\bot}$ and $m$ .

Intuitively, if we have a run from $w_{1}\cdots w_{m}$ to a $\top$ -stable configuration $w^{\prime}=w^{\prime}_{1}\cdots w^{\prime}_{m}$ , then we can match $w^{\prime}$ with one of the expressions above, and some $w^{\prime}_{i}$ is entirely contained in some $A_{j}^{*}$ .

We then use Lemma 14 to expand the run $w\to w^{\prime}$ to a run from $w^{\prime}=w_{1}\cdots w_{m}zw_{1}\cdots w_{m}$ to some $b$ -stable configuration $\widetilde{w^{\prime}}$ , by expanding the $w_{i}$ section into $w_{i}\cdots w_{m}zw_{1}\cdots w_{i}$ .

We can thus show that if $w$ is accepted, so is $w^{\prime}$ . Similarly, we show that if $w$ is not accepted, then it can reach a $\bot$ -stable configuration, and so can $w^{\prime}$ . We conclude that one is in the language if and only if the other is. To prove the congruence relation we only need to add words $u$ and $v$ around $w$ , which does not significantly alter the proof. $\hfill\blacktriangleleft$

We can now show that $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -decidable languages satisfy the definition of $\mathsf{DA}$ . In Lemma 16, we show that Equation 1 is satisfied, and in Lemma 17, that the languages are regular, concluding the proof.

Lemma 16.

Let $L\in\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ and let $w\in\Sigma^{*}$ be such that $w\equiv_{L}w^{2}$ . It is the case that $w\equiv_{L}w\cdot h\cdot w$ for all $h\in\alpha(w)^{*}$ .

Proof.

Lemma 15 implies that there is a (computable) number $m$ such that $w^{m}hw^{m}\equiv_{L}w^{m}$ , and since $w\equiv_{L}w^{2}$ , we obtain $w\equiv_{L}w\cdot h\cdot w$ as claimed. $\hfill\blacktriangleleft$

Lemma 17.

Every $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -decidable language is regular. Moreover, given an $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -protocol $\mathcal{P}$ , we can construct a finite automaton with the same language.

Proof sketch.

We show that beyond some length, every word must contain a pattern of the form $(w_{1}\cdots w_{m})z(w_{1}\cdots w_{m})$ with $\alpha(w_{1})=\ldots=\alpha(w_{m})\supseteq\alpha(z)$ . By Lemma 15, this means that every sufficiently long word is $\equiv_{L}$ -equivalent to a shorter one, meaning that $\equiv_{L}$ has finitely many equivalence classes. Since we can compute $m$ , we can compute this automaton. $\hfill\blacktriangleleft$

4.2 DA $\subseteq$ IO-PP $[<]$

Recall that $L\in\Pi_{2}[<]$ iff $\Sigma^{*}\setminus L\in\Sigma_{2}[<]$ . Since $\mathsf{DA}$ is equal to $\Delta_{2}[<]=\Sigma_{2}[<]\cap\Pi_{2}[<]$ , it is enough to prove that $\Sigma_{2}[<]$ languages are $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -semi-decidable, appealing to Lemma 6 to conclude. Note that $\Sigma_{2}[<]$ is the set of languages expressible as finite unions of languages of the form $L=A_{0}^{*}a_{1}A_{2}^{*}\cdots a_{m-1}A_{m}^{*}$ with the $A_{i}$ ’s being subalphabets (see, e.g., [26, Thm. 8.8]). Since semi-deciders are closed under union by Lemma 7, we need only show that $L$ is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -semi-decidable to conclude. We start with a technical proposition that extends a result of [29] to immediate-observation protocols, then provide a semi-decider for $L$ in Proposition 19. Since all constructions used here are effective, our proof also implies that given a finite automaton recognizing a $\mathsf{DA}$ language, we can effectively construct an $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -protocol recognizing the same language.

Proposition 18.

The language $\{w\in\Sigma^{+}\mid|w|_{a}=1\}$ is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\emptyset]$ -semi-decidable with stabilizing inputs.

Proof sketch.

Each agent stores its current input, its last input, and a belief on the output. If the current input of an agent mismatches its former one, then it resets itself to the current one. Each agent eventually stabilizes to a fixed input $(\sigma,\sigma,\cdot)$ . The belief component then controls the consensus: an $(a,a,\top)$ agent can turn any $(\sigma,\sigma,\cdot)$ with $\sigma\neq a$ to $\top$ , while the presence of any $(\sigma,\sigma,\bot)$ can spread $\bot$ to other agents. Finally, if an $a$ -agent observes another $a$ , it switches to $\bot$ ; combined with the rule that lets an $a$ -agent reset itself to $\top$ , this makes $a$ -agents alternate forever between $\top$ and $\bot$ whenever there are at least two $a$ ’s, preventing stabilization in that case. As a result, if the input contains no $a$ then every fair run reaches a $\bot$ -stable consensus; if it contains exactly one $a$ then every fair run reaches a $\top$ -stable consensus; and if it contains at least two $a$ ’s then some agent flips its belief forever. $\hfill\blacktriangleleft$

Proposition 19.

The language $L=A_{0}^{*}a_{1}A_{2}^{*}\cdots a_{m-1}A_{m}^{*}$ is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -semi-decidable (with stabilizing inputs).

Proof.

Let $\Gamma=\{0,1,\ldots,m\}$ , $K=0^{*}1^{*}\cdots m^{*}$ and $K^{\prime}=\bigcap_{a\in\Gamma,a\text{ odd}}\{w\in\Gamma^{+}\mid|w|_{a}=1\}$ . By Proposition 9, $K$ is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -semi-decidable with stabilizing inputs. Furthermore, by Propositions 18 and 10, $K^{\prime}$ is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\emptyset]$ -semi-decidable with stabilizing inputs. By Lemma 10, $K\cap K^{\prime}$ is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -semi-decidable with stabilizing inputs. Let $f(i)=A_{i}$ for even $i$ , and $f(i)=\{a_{i}\}$ otherwise. We are done by Lemma 11 since $L=f(K\cap K^{\prime})$ . $\hfill\blacktriangleleft$

5 Expressiveness of PP $[<]$

The crisp characterization of the previous section ties $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ to a wealth of computational models with strikingly different flavors. Chief among them, $\mathsf{DA}$ is characterized by a logic, $\Delta_{2}[<]$ , and by partially-ordered unambiguous automata. A natural question is thus whether $\mathsf{PP}[<]$ also admits such a diverse array of characterizations. We fall short of providing exact characterizations, but offer, in this section, two large classes of languages, one logically-defined and one based on partially-ordered automata, that are $\mathsf{PP}[<]$ -decidable.

Our formalisms will involve Presburger arithmetic, the first-order theory of the naturals with order and addition; e.g., $\phi(x)=(\exists y\in\mathbb{N})[y\geq 1\land x=2y]$ holds iff $x$ is a positive even number. Write $\equiv_{c}$ for the equivalence of naturals modulo $c$ . It is well known that Presburger arithmetic together with $\equiv_{c}$ with any $c\geq 2$ admits quantifier elimination. For our purposes, a Presburger formula is a (quantifier-free) Boolean combination of predicates of the form $\sum_{i=1}^{n}a_{i}x_{i}<b$ or $\sum_{i=1}^{n}a_{i}x_{i}\equiv_{c}b$ , where $a_{i},b\in\mathbb{Z}$ , $c\geq 2$ and variables $x_{i}$ are over $\mathbb{N}$ .

5.1 First-order logic over word intervals

Definition 20.

For $w\in\Sigma^{n}$ and $\sigma\in\Sigma$ , let $\#_{\sigma}\colon\{1,\ldots,n\}\times\{1,\ldots,n\}\to\mathbb{N}$ be the function that counts the number of occurrences of $\sigma$ between two positions of $w$ , i.e., $\#_{\sigma}(x,y)=|w[x..y]|_{\sigma}$ . We define $\mathsf{FO}^{\mathrm{int}}$ as first-order logic over word intervals, that is, with access to numerical values $\#_{a}(x,y)$ where $x$ and $y$ are either first-order variables, the first position (denoted “ $1$ ”) or the last position (denoted “ $\mathbf{max}$ ”). We will study $\mathsf{FO}^{\mathrm{int}}[<,+,\equiv]$ , where we allow numerical values to be compared, added, and tested modulo $c$ for any constant $c$ . Note that a variable $x$ can be expressed as $\sum_{\sigma\in\Sigma}\#_{\sigma}(1,x)$ , we will thus assume that the atomic formulas only have terms of the form $\#_{a}(x,y)$ , though we write $1$ for $\sum_{\sigma\in\Sigma}\#_{\sigma}(1,1)$ , and $\mathbf{max}$ for $\sum_{\sigma\in\Sigma}\#_{\sigma}(1,\mathbf{max})$ . The logics $\Sigma^{\mathrm{int}}_{k}$ , $\Pi^{\mathrm{int}}_{k}$ , and $\Delta^{\mathrm{int}}_{k}$ are naturally defined.

Example 21.

Let us show that the median language $\bigcup_{n\in\mathbb{N}}\Sigma^{n}a\Sigma^{n}$ belongs to $\Delta^{\mathrm{int}}_{1}[<,+,\equiv]$ . The following predicate asserts that $x$ is the middle position: $\psi(x)=\sum_{\sigma\in\Sigma}\#_{\sigma}(1,x)=\sum_{\sigma\in\Sigma}\#_{% \sigma}(x,\mathbf{max})$ . The median language can either be expressed by $(\exists x)[\psi(x)\land a(x)]$ , or by $(\forall x)[(\psi(x)\rightarrow a(x))\land\mathbf{max}\equiv_{2}1]$ . Note that $a(x)$ is the same as $\#_{a}(x,x)=1$ .

We now provide a convenient characterization of languages in $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ .

Lemma 22.

Any language from $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ is a finite union of languages of the form $K=\{a_{0}w_{1}a_{1}\cdots w_{m}a_{m}\mid w_{i}\in\Sigma^{*},a_{i}\in\Sigma,% \varphi(x_{i,\sigma}\mapsto|w_{i}|_{\sigma},y_{i,\sigma}\mapsto|a_{i}|_{\sigma% })\}$ where $m\geq 0$ and $\varphi$ is a Presburger formula over variables $\{x_{i,\sigma}\mid i\in[1..m],\sigma\in\Sigma\}\cup\{y_{i,\sigma}\mid i\in[0..% m],\sigma\in\Sigma\}$ .

Thanks to the previous lemma, we are able to build a protocol $\mathsf{PP}[<]$ semi-deciding any language in $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ , by building semi-deciders with stabilizing inputs for each $K$ , and then using the closure properties presented in Section 3.2.

Proposition 23.

Any language from $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ is $\mathsf{PP}[<]$ -semi-decidable.

Proof.

Let $L\in\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ . By Lemma 22, $L$ is a finite union of languages of the form $L^{\prime}=\{a_{0}w_{1}a_{1}\cdots w_{m}a_{m}\mid w_{i}\in\Sigma^{*},a_{i}\in% \Sigma,\varphi(x_{i,\sigma}\mapsto|w_{i}|_{\sigma},y_{i,\sigma}\mapsto|a_{i}|_% {\sigma})\}$ where $m\geq 0$ and $\varphi$ is a Presburger formula. It suffices to show that $L^{\prime}$ is $\mathsf{PP}[\mathcal{N}]$ -semi-decidable with stabilizing inputs. Indeed, by Lemma 10, that class of languages is closed under union.

Let $\underline{\Sigma}=\{\underline{\sigma}\mid\sigma\in\Sigma\}$ , $A_{i}=\underline{\Sigma}\times\{i\}$ , $W_{i}=\Sigma\times\{i\}$ and $\Gamma=\bigcup_{i\in[0..m]}A_{i}\cup\bigcup_{i\in[1..m]}W_{i}$ . We justify that the three following languages $K$ , $K^{\prime}$ and $K^{\prime\prime}$ over alphabet $\Gamma$ are semi-decided with stabilizing inputs:

$\blacksquare$

$K=A_{0}^{*}W_{1}^{*}A_{1}^{*}\cdots W_{m}^{*}A_{m}^{*}$ ,
$\blacksquare$

$K^{\prime}=\{w\in\Gamma^{+}\mid\varphi(x_{i,\sigma}\mapsto|w|_{(\sigma,i)},y_{% i,\sigma}\mapsto|w|_{(\underline{\sigma},i)})\}$ ,
$\blacksquare$

$K^{\prime\prime}=\left\{w\in\Gamma^{+}\mid\sum_{\gamma\in A_{1}}|w|_{\gamma}=1% \land\cdots\land\sum_{\gamma\in A_{m}}|{w}|_{\gamma}=1\right\}$ (recall $A_{i}\cap A_{j}=\emptyset$ for $i\neq j$ ).

Let $f(2i)=A_{i}$ and $f(2i+1)=W_{i+1}$ . We have $f(0^{*}1^{*}2^{*}\cdots(2m)^{*})=K$ . By Propositions 9 and 11, $K$ is $\mathsf{PP}[<]$ -semi-decidable with stabilizing inputs. Since $K^{\prime},K^{\prime\prime}\in\mathsf{PP}[\emptyset]$ , these two languages are $\mathsf{PP}[\emptyset]$ -decidable with stabilizing inputs [2, 29].

By Lemma 10, the language $K\cap K^{\prime}\cap K^{\prime\prime}$ is $\mathsf{PP}[<]$ -semi-decidable with stabilizing inputs. Let $g((\sigma,i))=g((\underline{\sigma},i))=\{\sigma\}$ . We are done by Lemma 11 since $L^{\prime}=g(K\cap K^{\prime}\cap K^{\prime\prime})$ . $\hfill\blacktriangleleft$

Corollary 24.

$\Delta^{\mathrm{int}}_{1}[<,+,\equiv]\subseteq\mathsf{PP}[<]$ .

In the forthcoming Conjecture 40, we postulate that these two classes coincide.

5.2 Partially-ordered Parikh automata

A partially-ordered nondeterministic Parikh automaton (poPA) is a tuple $\mathcal{A}=(Q,\Sigma,\delta,q_{0},F,\Psi)$ where:

$\blacksquare$

$Q$ is a finite set of states equipped with a partial order $\leq$ ;
$\blacksquare$

$\Sigma$ is a finite alphabet;
$\blacksquare$

$\delta\subseteq Q\times\Sigma\times Q$ is the transition relation, that satisfies $p\leq q$ for all $(p,\sigma,q)\in\delta$ ; if $p=q$ , the transition is dubbed a self-loop, and otherwise, a progress transition;
$\blacksquare$

$q_{0}\in Q$ is the initial state, and $F\subseteq Q$ is the set of final states;
$\blacksquare$

$\Psi$ is a Presburger formula over variables $\delta$ .

For all $t=(q,\sigma,q^{\prime})\in\delta$ , we write $q\to^{t}q^{\prime}$ and $\pi_{\Sigma}(t)=\sigma$ . We naturally lift these notations to sequences. A word $w\in\Sigma^{*}$ is accepted by $\mathcal{A}$ if there exist $\rho\in\delta^{*}$ and $q\in F$ such that $q_{0}\to^{\rho}q$ , $\pi_{\Sigma}(\rho)=w$ and $\Psi(t\mapsto|\rho|_{t})$ holds. The language of $\mathcal{A}$ is the set $L(\mathcal{A})$ of words it accepts. Figure 3 depicts two examples of poPA.

Figure 3: Example of poPA for the median language

\bigcup_{n\geq 0}\Sigma^{n}a\Sigma^{n}

(left) and the coDyck-witness language

\{a^{n}v\mid n\geq 1,v\in\{\sqsubset,\sqsupset\}^{\geq n},|v[1..n]|_{\sqsupset% }>|v[1..n]|_{\sqsubset}\}

(right).

Lemma 22 allows us to translate a formula from $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ into a poPA by guessing a factorization $a_{0}w_{1}a_{1}\cdots w_{m}a_{m}$ with a progress transition for each $a_{i}$ , and a self-loop for each $w_{i}$ ; and then using the Presbuger acceptance formula of the automaton to verify the guess. We can also translate a poPA into a formula of $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ by guessing the position of the progress transitions and verifying the validity of the path. This yields:

Theorem 25.

A language is recognized by some poPA iff it belongs to $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ .

Recall that $\Sigma_{2}[<]$ is characterized by partially-ordered automata, while $\Delta_{2}[<]$ is characterized by unambiguous partially-ordered automata. We explore a similar notion for $\Delta^{\mathrm{int}}_{1}[<,+,\equiv]$ and poPA. A poPA $\mathcal{A}$ is weakly unambiguous³³3The nomenclature, introduced in [7], stems from prior studies [9] which called “unambiguous” the PA with an unambiguous underlying automaton. We note that the examples of Figure 3 can be shown, using the tools of [9], not to be expressible with unambiguous PA. if every $w\in L(\mathcal{A})$ is accepted by at most one path (w.r.t. $F$ and $\Psi$ ). Note that the automata of Figure 3 are weakly unambiguous and can be complemented. By Theorem 25, this means that both languages belong to $\Delta^{\mathrm{int}}_{1}[<,+,\equiv]$ . More generally, we conjecture that weakly-unambiguous poPA are closed under complement.

Observation 26.

If weakly-unambiguous poPA are closed under complement, then any language recognized by a weakly-unambiguous poPA belongs to $\Delta^{\mathrm{int}}_{1}[<,+,\equiv]$ .

In the forthcoming Conjecture 40, we postulate that these two classes coincide. We note, as a sanity check, that since $\Delta_{2}[<]$ is characterized by unambiguous partially-ordered automata, $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]=\mathsf{DA}=\Delta_{2}[<]\subsetneq% \Delta^{\mathrm{int}}_{1}[<,+,\equiv]$ . The strictness of the inclusion is in particular witnessed by the regular language $\{a^{2n}\mid n\geq 1\}$ over alphabet $\{a\}$ , which trivially belongs to $\Delta^{\mathrm{int}}_{1}[<,+,\equiv]$ with formula $\mathbf{max}\equiv_{2}0$ .

Remark 27 (Two-way models).

Recall that $\mathsf{DA}$ is also characterized by two-way deterministic partially-ordered automata. We can show that two-way poPA are equivalent to poPA. However, defining two-way deterministic PA as two-way deterministic automata with a Presburger constraint, it is known that the model is as expressive as unambiguous PA [16], which cannot express the languages of Figure 3.

5.3 The regular languages of PP $[<]$

Lemma 22 gives a clear form for the languages of $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ . If the language $K$ therein is regular, this points to the formula $\varphi$ not arithmetically linking the $w_{i}$ ’s between one another nor imposing nonregular constraints on any single $w_{i}$ . Hence we have naturally:

Conjecture 28.

Let $\mathrm{Com}$ be the set of commutative regular languages. Let $\mathrm{Pol}(\mathrm{Com})$ be the set of languages that are finite unions of languages $L_{0}a_{1}L_{1}\cdots a_{n}L_{n}$ with $L_{i}\in\mathrm{Com}$ and $a_{i}$ letters. We conjecture that the regular languages of $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ are exactly $\mathrm{Pol}(\mathrm{Com})$ .

The class $\mathrm{Pol}(\mathrm{Com})$ has been studied in previous works: [1] conjectures that they correspond to the regular languages requiring $O(\log n)$ communication and [18] shows that it is included in the largest class of languages, closed under the so-called positive variety operations, that does not contain $(ab)^{+}$ . We recall, for contrast, that $\mathsf{DA}$ is the largest class of aperiodic regular languages, closed under the variety operations, that does not contain $(ab)^{+}$ . To give additional credence to our conjecture, we show:

Proposition 29.

The language $(ab)^{+}$ does not belong to $\Sigma^{\mathrm{int}}_{1}[<,+,\equiv]$ .

The class $\mathrm{UPol}(\mathrm{Com})$ is defined similarly as $\mathrm{Pol}(\mathrm{Com})$ , except that we require that every word $w$ in the marked concatenation has a unique decomposition $w=w_{0}a_{1}w_{1}\cdots a_{n}w_{n}$ with $w_{i}\in L_{i}$ . It is known [28] that $\mathrm{UPol}(\mathrm{Com})=\mathrm{Pol}(\mathrm{Com})\cap\overline{\mathrm{% Pol}(\mathrm{Com})}$ . We naturally postulate, in Conjecture 40, that the regular languages of $\mathsf{PP}[<]$ are exactly $\mathrm{UPol}(\mathrm{Com})$ .

6 Expressiveness of IO-PP $[\mathcal{N}]$ and PP $[\mathcal{N}]$ when successor is available

We now consider protocols where transitions may be fired only when two agents are adjacent. Formally, we look at $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ and $\mathsf{PP}[\mathcal{N}]$ with $+1\in\mathcal{N}$ , where $+1$ (sometimes written $\mathbf{succ}$ in the literature) is the predicate $\{(x,x+1)\mid x\in\mathbb{N}\}$ . This study is reminiscent of the classic study of $\mathsf{FO}^{2}[<,+1]$ [15, 23, 33, 36] that followed that of $\mathsf{FO}^{2}[<]$ , the two-variable fragment of $\mathsf{FO}[<]$ that is as expressive as $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ .

Example 30.

Recall that the set of all $b$ -stable configurations of a $\mathsf{PP}[<]$ is subword-closed, and hence regular. The following $\mathsf{PP}[+1]$ has a non-regular set of $\top$ -stable configurations:

	$\displaystyle a^{\text{\tiny\includegraphics{dagpub-standalone-manual-2026-08-% 03-17-37-52-page-6.pdf2svg.svg}}},b^{\text{\tiny\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-6.pdf2svg.svg}}}$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\mathmakebox[15pt% ][c]{\mathclap{\textbf{{true}}}}}}$}}a^{\text{\raisebox{-1.0pt}{% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-4.pdf2svg.% svg}}}},b^{\text{\raisebox{-1.0pt}{\includegraphics{dagpub-standalone-manual-2% 026-08-03-17-37-52-page-5.pdf2svg.svg}}}}$	$\displaystyle a^{\text{\raisebox{-1.0pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-4.pdf2svg.svg}}}},a$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\mathmakebox[15pt% ][c]{\mathclap{+1}}}}$}}\text{\scriptsize\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-7.pdf2svg.svg}},a^{\text{\tiny\includegraphics% {dagpub-standalone-manual-2026-08-03-17-37-52-page-6.pdf2svg.svg}}}$	$\displaystyle a^{\text{\raisebox{-1.0pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-4.pdf2svg.svg}}}},b^{\text{\raisebox{-1.0pt}{% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-5.pdf2svg.% svg}}}}$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\mathmakebox[15pt% ][c]{\mathclap{+1}}}}$}}\text{\scriptsize\,\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-8.pdf2svg.svg}\,},\text{\scriptsize\,% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-8.pdf2svg.% svg}\,}$
	$\displaystyle b,b^{\text{\raisebox{-1.0pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-5.pdf2svg.svg}}}}$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{\mathmakebox[15pt% ][c]{\mathclap{+1}}}}$}}b^{\text{\tiny\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-6.pdf2svg.svg}}},\text{\scriptsize% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-7.pdf2svg.% svg}}$

Let us set the opinion of each state to $\top$ , except for . The protocol is constructed so that from a configuration of the form $a^{\text{\tiny\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-% page-6.pdf2svg.svg}}}a^{*}b^{*}b^{\text{\tiny\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-6.pdf2svg.svg}}}$ , one marker moves to the right along the $a$ ’s, while the other synchronously moves to the left along the $b$ ’s. If they meet at the frontier between $a$ ’s and $b$ ’s, it means there are as many $a$ ’s and $b$ ’s, and that state appears.

The set of $\top$ -stable configurations cannot be regular since, from $w\in a^{\text{\tiny\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-% 52-page-6.pdf2svg.svg}}}a^{*}b^{*}b^{\text{\tiny\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-6.pdf2svg.svg}}}$ , the state will appear iff $|w|_{a}=|w|_{b}$ , e.g.,

a^{\text{\tiny\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-% page-6.pdf2svg.svg}}}abb^{\text{\tiny\includegraphics{dagpub-standalone-manual% -2026-08-03-17-37-52-page-6.pdf2svg.svg}}}\to a^{\text{\raisebox{-1.0pt}{% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-4.pdf2svg.% svg}}}}abb^{\text{\raisebox{-1.0pt}{\includegraphics{dagpub-standalone-manual-% 2026-08-03-17-37-52-page-5.pdf2svg.svg}}}}\to\text{\scriptsize\includegraphics% {dagpub-standalone-manual-2026-08-03-17-37-52-page-7.pdf2svg.svg}}a^{\text{% \tiny\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-6.pdf2% svg.svg}}}bb^{\text{\raisebox{-1.0pt}{\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-5.pdf2svg.svg}}}}\to\text{\scriptsize% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-7.pdf2svg.% svg}}a^{\text{\tiny\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-% 52-page-6.pdf2svg.svg}}}b^{\text{\tiny\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-6.pdf2svg.svg}}}\text{\scriptsize% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-7.pdf2svg.% svg}}\to\text{\scriptsize\includegraphics{dagpub-standalone-manual-2026-08-03-% 17-37-52-page-7.pdf2svg.svg}}a^{\text{\raisebox{-1.0pt}{\includegraphics{% dagpub-standalone-manual-2026-08-03-17-37-52-page-4.pdf2svg.svg}}}}b^{\text{% \raisebox{-1.0pt}{\includegraphics{dagpub-standalone-manual-2026-08-03-17-37-5% 2-page-5.pdf2svg.svg}}}}\text{\scriptsize\includegraphics{dagpub-standalone-% manual-2026-08-03-17-37-52-page-7.pdf2svg.svg}}\to\text{\scriptsize% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-7.pdf2svg.% svg}}\text{\scriptsize\,\includegraphics{dagpub-standalone-manual-2026-08-03-1% 7-37-52-page-8.pdf2svg.svg}\,}\text{\scriptsize\,\includegraphics{dagpub-% standalone-manual-2026-08-03-17-37-52-page-8.pdf2svg.svg}\,}\text{\scriptsize% \includegraphics{dagpub-standalone-manual-2026-08-03-17-37-52-page-7.pdf2svg.% svg}}.

The main result of this section is:

Theorem 31.

Let $\mathcal{N}$ be a set of $\mathsf{NSPACE}(n)$ -decidable numerical predicates that contains $+1$ . We have $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]=\mathsf{PP}[\mathcal{N}]=% \mathsf{NSPACE}(n)$ .

To show this result, it is enough to prove that $\mathsf{NSPACE}(n)\subseteq\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ , since $\mathsf{PP}[\mathcal{N}]\subseteq\mathsf{NSPACE}(n)$ has been established beforehand in Theorem 4.

6.1 $\mathsf{NSPACE}(n)\subseteq\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$

We start by showing that transitions using the successor predicate can be simulated with immediate-observation transitions.

Lemma 32.

Let $L$ be a $\mathsf{PP}[+1]$ -semi-decidable language. There exists a $\mathsf{PP}[+1]$ -protocol $\mathcal{P}^{\prime}$ semi-deciding $L$ and such that each $+1$ -transition of $\mathcal{P}^{\prime}$ is immediate-observation.

Proof sketch.

The construction turns a $\mathsf{PP}[+1]$ -protocol $\mathcal{P}$ into a new $\mathsf{PP}[+1]$ -protocol $\mathcal{P}^{\prime}$ by replacing each transition $\delta=(a,b)\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{+1}}$}}(c,d)$ with a short four-step handshake along the successor relation, using auxiliary markers $a^{\delta}$ and $b^{\mathsf{ack},\delta}$ . The four rules are:

	$\displaystyle a,b$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{+1}}$}}a^{\delta},b$	$\displaystyle a^{\delta},b$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{+1}}$}}a^{\delta}% ,b^{\mathsf{ack},\delta}$
	$\displaystyle a^{\delta},b^{\mathsf{ack},\delta}$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{+1}}$}}c,b^{% \mathsf{ack},\delta}$	$\displaystyle c,b^{\mathsf{ack},\delta}$	$\displaystyle\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\smash{+1}}$}}c,d$

Intuitively, one agent announces that it wants to perform $\delta$ , the neighbor acknowledges, and the two agents then update one after the other; additional clean-up rules erase incomplete handshakes so that executions cannot block when several handshakes overlap. $\hfill\blacktriangleleft$

Lemma 33.

The language of a linear-bounded nondeterministic Turing machine is $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ -semi-decidable.

Proof sketch.

Given a linear-bounded nondeterministic Turing machine $M$ , we construct an $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ -protocol $\mathcal{P}$ that simulates $M$ under stabilizing inputs. Thanks to Lemma 32, we only need to ensure that true-transitions are immediate-observation.

Let $\Sigma^{\prime}$ be the tape alphabet of $M$ . The protocol $\mathcal{P}$ works over $\Gamma^{*}$ where $\Gamma=(P\cup\{-\})\times\Sigma^{\prime}\times\{\text{fst},-,\text{lst}\}$ . For example, $w=(-,a,\text{fst})(p,a,-)(-,b,\text{lst})$ represents the configuration of $M$ in state $p$ , with the head on the second cell, and the tape containing $a a b$ .

The protocol $\mathcal{P}$ simulates $M$ using $+1$ -transitions with the agent containing the current state $p$ . If $M$ accepts, then $\mathcal{P}$ spreads $\top$ across the population. There are two challenges:

1.

Since we want to semi-decide under stabilizing inputs, $\mathcal{P}$ must reset the population and the simulation of $M$ whenever an agent changes its mind on its input. This is implemented as follows. Any agent who has changed its mind can flag the last agent. Using $+1$ -transitions, this can spread from right to left, resetting the population along the way.
2.

If the input of $\mathcal{P}$ is an invalid configuration of $M$ , then the population should not reach a stable $\top$ -consensus. For example, if two agents both represent the head of $M$ , then they change their belief to $\bot$ upon meeting. Similarly, we must detect whether “fst” and “lst” occur exactly in the first and last agent.

The resulting protocol $\mathcal{P}$ does not semi-decide the language of $M$ , but rather the set of configurations of $M$ leading to acceptance. So, we need to intersect with the set of initial configurations, and then project onto the second component of $\Gamma$ . This can be done thanks to Propositions 9, 18, 10, and 11. $\hfill\blacktriangleleft$

Corollary 34.

$\mathsf{NSPACE}(n)\subseteq\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ .

Proof.

Let $L\in\mathsf{NSPACE}(n)$ . As $\mathsf{NSPACE}(n)$ is closed under complement, there exist two linear-bounded nondeterministic Turing machines $M$ and $\overline{M}$ recognizing $L$ and $\Sigma^{+}\setminus L$ , respectively. By Lemma 33, we can build two $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ -protocols, say $\mathcal{P}_{M}$ and $\mathcal{P}_{\overline{M}}$ , that semi-decide $L$ and $\Sigma^{+}\setminus L$ , respectively. Lemma 6 allows to conclude. $\hfill\blacktriangleleft$

7 Decidability of checking whether a population protocol is a decider

A good portion of our results assumes that a given population protocol is a decider or a semi-decider in order to construct an object (a Turing machine in Theorem 4, a formula in Theorem 12, etc.). To fully understand how constructive these proofs are, we ought to study whether it is decidable, given a population protocol, to check if it is a decider. In other words, is the syntax of deciders decidable? From the perspective of formal verification, this is also a natural problem, known as the well-specification problem. It is decidable for $\mathsf{PP}[\emptyset]$ [13], and undecidable when protocols are extended with an infinite alphabet (where agents carry data from an infinite domain, and transitions can use equality constraints between those data), except for immediate-observation protocols [34].

We show that the problem is undecidable already for $\mathsf{PP}[<]$ and $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ , and provide a natural conjecture that would entail that the problem is decidable for $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ .

7.1 The syntax of PP $[<]$ , $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ and $\mathsf{PP}[+1]$ deciders are undecidable

First, we consider the emptiness problem: given a $\mathsf{PP}[\mathcal{N}]$ protocol $\mathcal{P}$ , is there an execution from an initial configuration $u$ to a $\top$ -stable one? We use a technique from [34] to show a general reduction to the syntax problem.

Lemma 35.

The emptiness problem for $\mathsf{PP}[\mathcal{N}]$ (resp. $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ ) reduces to deciding the complement of the syntax of $\mathsf{PP}[\mathcal{N}]$ (resp. $\text{$\mathsf{IO}$-$\mathsf{PP}$}[\mathcal{N}]$ ) deciders.

Proof sketch.

From a protocol $\mathcal{P}=(Q,\Sigma,O,\Delta)$ , we construct a protocol $\mathcal{P}^{\prime}$ such that $\mathcal{P}^{\prime}$ is not a decider iff $\mathcal{P}$ can reach a $\top$ -stable configuration. The construction adds a fresh sink state $q_{\bot}$ with $O(q_{\bot})=\bot$ , and for every state $q$ with $O(q)=\bot$ we add a transition allowing an agent in $q$ to switch to $q_{\bot}$ .

As a consequence, from any configuration that contains a $\bot$ -agent, a fair execution can drive the system to the $\bot$ -stable consensus $q_{\bot}^{*}$ . On the other hand, if a $\top$ -stable configuration is reachable in $\mathcal{P}$ , then the same configuration is reachable in $\mathcal{P}^{\prime}$ and remains $\top$ -stable there: none of the added transitions to $q_{\bot}$ are enabled from $\top$ -states. Therefore $\mathcal{P}^{\prime}$ is not a decider.

Conversely, if $\mathcal{P}$ has no reachable $\top$ -stable configuration, then no fair run of $\mathcal{P}^{\prime}$ stabilizes to $\top$ . Every fair run stabilizes to $q_{\bot}^{*}$ and $\mathcal{P}^{\prime}$ decides the empty language. The construction preserves immediate observation, as each new transition updates at most one agent. $\hfill\blacktriangleleft$

This reduction, combined with the translation from linear-bounded Turing machines to $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ from Section 6, already yields the following result.

Corollary 36.

The syntax of $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ and $\mathsf{PP}[+1]$ deciders are undecidable.

Theorem 37.

The emptiness problem is undecidable for $\mathsf{PP}[<]$ . Hence the syntax of $\mathsf{PP}[<]$ deciders is also undecidable.

Proof sketch.

We reduce from the Post correspondence problem. Specifically, we take two homomorphisms $h_{1},h_{2}\colon B^{*}\to A^{*}$ and construct a $\mathsf{PP}[<]$ that can reach a $\top$ -stable configuration if and only if there is a word $u$ such that $h_{1}(u)=h_{2}(u)$ . We obtain it as a product of three protocols. One makes sure that we can only reach a $\top$ -stable configuration from an initial one of the form $\#_{1}v\#_{2}u\#_{3}$ with $v\in B^{*}$ and $u\in A^{*}$ . The two others check that we can reach a $\top$ -stable configuration only when $h_{1}(u)=v$ and $h_{2}(u)=v$ , respectively. Each one does so by making agents simulate two reading heads going through $u$ and $v$ in lockstep and verifying that $h_{i}(u)=v$ . Initially all agents have opinion $\bot$ , and in order to change it they must carry the reading head at some point, hence we cannot skip any letter in order to reach a $\top$ -stable configuration.

Hence, a $\top$ -stable configuration is reachable iff there exist $u, v$ with $h_{1}(u)=v=h_{2}(u)$ . $\hfill\blacktriangleleft$

7.2 The syntax of IO-PP $[<]$ deciders is decidable, conditionally

We present a conjecture on the reachability relation of $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ , then show that it entails decidability of the syntax of their deciders:

Conjecture 38.

The set of configurations reachable from a $\mathsf{DA}$ language in an $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ protocol is also a $\mathsf{DA}$ language.

Theorem 39.

If Conjecture 38 holds, then the syntax of $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ deciders is decidable.

Proof sketch.

We use two semi-decision procedures. The first one checks, for each length $n$ , if the protocol is a decider on words of length $n$ . If the input protocol is not a decider, we will observe it for some $n$ . The second one looks for invariants witnessing that the protocol is a decider. We look for two disjoint languages $K_{\top},K_{\bot}$ such that every input word is in one of the two, they are closed under transitions of the protocol, and from everywhere in $K_{b}$ we can reach a $b$ -stable configuration. Assuming the conjecture, we can assume that those invariants are in $\mathsf{DA}$ . We show that we can enumerate potential regular invariants and check the requirements, yielding the second semi-decision procedure. $\hfill\blacktriangleleft$

In fact, one could slightly strengthen the statement above: it suffices to know that the set of configurations reachable from a $\mathsf{DA}$ language in $\mathcal{P}$ (instead of in every $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -protocol) is also a $\mathsf{DA}$ language, to be able to check whether $\mathcal{P}$ is a decider. This means that if we can prove Conjecture 38 over only a subclass of $\text{$\mathsf{IO}$-$\mathsf{PP}$}[<]$ -protocols, then we know that the syntax of that subclass is decidable.

8 Open questions

The most tantalizing open question left open by this work is the characterization of $\mathsf{PP}[<]$ . We conjecture that the logic and automata models introduced in Section 5 are tight:

Conjecture 40.

$\mathsf{PP}[<]$ is the class of languages recognized by $\Delta^{\mathrm{int}}_{1}[<,+,\equiv]$ and the class of languages recognized by weakly unambiguous poPA. The regular languages of $\mathsf{PP}[<]$ are exactly $\mathrm{UPol}(\mathrm{Com})$ .

Conjecture 40 would entail in particular that weakly unambiguous poPA are closed under complement. We note that it is not known whether weakly unambiguous PA themselves are closed under complement, but it may be easier to show such closure under the partially ordered assumption.

Conjecture 38 is also very natural and left open.

References

[1] Anil Ada. On the non-deterministic communication complexity of regular languages. In Proc. $\text{12}^{\text{th}}$ International Conference on Developments in Language Theory (DLT), pages 96–107, 2008. doi:10.1007/978-3-540-85780-8_7.
[2] Dana Angluin, James Aspnes, Melody Chan, Michael J. Fischer, Hong Jiang, and René Peralta. Stably computable properties of network graphs. In First IEEE International Conference on Distributed Computing in Sensor Systems (DCOSS), pages 63–74, 2005. doi:10.1007/11502593_8.
[3] Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. Distributed Computing, 18(4):235–253, 2006. doi:10.1007/s00446-005-0138-3.
[4] Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing, 20(4):279–304, 2007. doi:10.1007/s00446-007-0040-2.
[5] James Aspnes and Eric Ruppert. An introduction to population protocols. In Middleware for Network Eccentric and Mobile Applications, pages 97–120. Springer, 2009. doi:10.1007/978-3-540-89707-1_5.
[6] Michael Blondin and François Ladouceur. Population protocols with unordered data. In Proc. $\text{50}^{\text{th}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 115:1–115:20, 2023. doi:10.4230/LIPIcs.ICALP.2023.115.
[7] Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-unambiguous Parikh automata and their link to holonomic series. In Proc. $\text{47}^{\text{th}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 114:1–114:16, 2020. doi:10.4230/LIPIcs.ICALP.2020.114.
[8] Olivier Bournez, Johanne Cohen, and Mikaël Rabie. Homonym population protocols. Theory of Computing Systems, 62(5):1318–1346, 2018. doi:10.1007/S00224-017-9833-2.
[9] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. International Journal of Foundations of Computer Science, 24(7):1099–1116, 2013. doi:10.1142/S0129054113400339.
[10] Ho-Lin Chen, David Doty, and David Soloveichik. Deterministic function computation with chemical reaction networks. Natural Computing, 13(4):517–534, 2014. doi:10.1007/S11047-013-9393-6.
[11] Zoë Diamadi and Michael J Fischer. A simple game for the study of trust in distributed systems. Wuhan University Journal of Natural Sciences, 6(1):72–82, 2001. doi:10.1007/BF03160228.
[12] Javier Esparza and Michael Blondin. Automata theory: An algorithmic approach. The MIT Press, 2023.
[13] Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. In Proc. $\text{26}^{\text{th}}$ International Conference on Concurrency Theory (CONCUR), pages 470–482, 2015. doi:10.4230/LIPIcs.CONCUR.2015.470.
[14] Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy. Verification of immediate observation population protocols. In Proc. $\text{29}^{\text{th}}$ International Conference on Concurrency Theory (CONCUR), volume 118, pages 31:1–31:16, 2018. doi:10.4230/LIPIcs.CONCUR.2018.31.
[15] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Information and Computation, 179(2):279–295, 2002. doi:10.1006/INCO.2001.2953.
[16] Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi. Two-way Parikh automata. In Proc. $\text{39}^{\text{th}}$ IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 40:1–40:14, 2019. doi:10.4230/LIPIcs.FSTTCS.2019.40.
[17] Adam Ganczorz, Leszek Gasieniec, Tomasz Jurdzinski, Jakub Kowalski, and Grzegorz Stachowiak. Selective population protocols. In Proc. $\text{26}^{\text{th}}$ International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 225–239, 2024. doi:10.1007/978-3-031-74498-3_16.
[18] Antonio Cano Gómez, Giovanna Guaiana, and Jean-Éric Pin. Regular languages and partial commutations. Information and Computation, 230:76–96, 2013. doi:10.1016/J.IC.2013.07.003.
[19] Rachid Guerraoui and Eric Ruppert. Names trump malice: Tiny mobile agents can tolerate Byzantine failures. In Proc. $\text{36}^{\text{th}}$ International Colloquium Automata, Languages and Programming (ICALP), pages 484–495, 2009. doi:10.1007/978-3-642-02930-1_40.
[20] Simon Halfon. On Effective Representations of Well Quasi-Orderings. (Représentations Effectives des Beaux Pré-Ordres). PhD thesis, Université Paris-Saclay, France, 2018. URL: https://tel.archives-ouvertes.fr/tel-01945232.
[21] Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, s3-2(1):326–336, 1952. doi:10.1112/plms/s3-2.1.326.
[22] Sige-Yuki Kuroda. Classes of languages and linear-bounded automata. Information and Control, 7(2):207–223, 1964. doi:10.1016/S0019-9958(64)90120-2.
[23] Kamal Lodaya, Paritosh K. Pandya, and Simoni S. Shah. Around dot depth two. In Proc. $\text{14}^{\text{th}}$ International Conference on Developments in Language Theory (DLT), pages 303–315, 2010. doi:10.1007/978-3-642-14455-4_28.
[24] Othon Michail, Ioannis Chatzigiannakis, and Paul G. Spirakis. Mediated population protocols. Theoretical Computer Science, 412(22):2434–2450, 2011. doi:10.1016/J.TCS.2011.02.003.
[25] J. Andres Montoya. Asymptotic reasoning with two variables. In Proc. $\text{31}^{\text{st}}$ International Workshop on Logic, Language, Information, and Computation (WoLLIC), pages 38–55, 2025. doi:10.1007/978-3-031-99536-1_3.
[26] Jean-Éric Pin. Syntactic semigroups. In Handbook of Formal Languages, Volume 1: Word, Language, Grammar, pages 679–746. Springer, 1997. doi:10.1007/978-3-642-59136-5_10.
[27] Jean-Éric Pin and Pascal Weil. Polynomial closure and unambiguous product. In Proc. $\text{22}^{\text{nd}}$ International Colloquium on Automata, Languages and Programming (ICALP), pages 348–359, 1995. doi:10.1007/3-540-60084-1_87.
[28] Thomas Place and Marc Zeitoun. All about unambiguous polynomial closure. TheoretiCS, 2, 2023. doi:10.46298/THEORETICS.23.11.
[29] Michael Raskin. Modular population protocols. In Proc. $\text{20}^{\text{th}}$ International Symposium on Algorithmics of Wireless Networks (ALGOWIN), pages 173–187, 2024. doi:10.1007/978-3-031-74580-5_13.
[30] Marcel-Paul Schützenberger. Sur le produit de concaténation non ambigü. Semigroup Forum, 13(1):47–75, 1976. doi:10.1007/bf02194921.
[31] Thomas Schwentick, Denis Thérien, and Heribert Vollmer. Partially-ordered two-way automata: A new characterization of DA. In Proc. $\text{5}^{\text{th}}$ International Conference on Developments in Language Theory (DLT), pages 239–250, 2001. doi:10.1007/3-540-46011-X_20.
[32] Pascal Tesson and Denis Thérien. Diamonds are forever: The variety DA. In Semigroups, algorithms, automata and languages, pages 475–499. World Scientific, 2002. doi:10.1142/5050.
[33] Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Proc. $\text{30}^{\text{th}}$ Annual ACM Symposium on the Theory of Computing (STOC), pages 234–240, 1998. doi:10.1145/276698.276749.
[34] Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, and Chana Weil-Kennedy. Verification of population protocols with unordered data. In Proc. $\text{51}^{\text{st}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 156:1–156:20, 2024. doi:10.4230/LIPIcs.ICALP.2024.156.
[35] Chana Weil-Kennedy. Observation Petri Nets. PhD thesis, Technical University of Munich, Germany, 2023. URL: https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20230320-1691161-1-3.
[36] Philipp Weis and Neil Immerman. Structure theorem and strict alternation hierarchy for $\text{FO}^{\text{2}}$ on words. In Proc. $\text{21}^{\text{st}}$ International Workshop on Computer Science Logic (CSL), pages 343–357, 2007. doi:10.1007/978-3-540-74915-8_27.
[37] Hiroto Yasumi, Fukuhito Ooshita, and Michiko Inoue. Population protocols for graph class identification problems. In Proc. $\text{25}^{\text{th}}$ International Conference on Principles of Distributed Systems, (OPODIS), pages 13:1–13:19, 2021. doi:10.4230/LIPIcs.OPODIS.2021.13.

[bib.bib1] [1] Anil Ada. On the non-deterministic communication complexity of regular languages. In Proc. $\text{12}^{\text{th}}$ International Conference on Developments in Language Theory (DLT), pages 96–107, 2008. doi:10.1007/978-3-540-85780-8_7.

[bib.bib2] [2] Dana Angluin, James Aspnes, Melody Chan, Michael J. Fischer, Hong Jiang, and René Peralta. Stably computable properties of network graphs. In First IEEE International Conference on Distributed Computing in Sensor Systems (DCOSS), pages 63–74, 2005. doi:10.1007/11502593_8.

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

[bib.bib4] [4] Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing, 20(4):279–304, 2007. doi:10.1007/s00446-007-0040-2.

[bib.bib5] [5] James Aspnes and Eric Ruppert. An introduction to population protocols. In Middleware for Network Eccentric and Mobile Applications, pages 97–120. Springer, 2009. doi:10.1007/978-3-540-89707-1_5.

[bib.bib6] [6] Michael Blondin and François Ladouceur. Population protocols with unordered data. In Proc. $\text{50}^{\text{th}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 115:1–115:20, 2023. doi:10.4230/LIPIcs.ICALP.2023.115.

[bib.bib7] [7] Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-unambiguous Parikh automata and their link to holonomic series. In Proc. $\text{47}^{\text{th}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 114:1–114:16, 2020. doi:10.4230/LIPIcs.ICALP.2020.114.

[bib.bib8] [8] Olivier Bournez, Johanne Cohen, and Mikaël Rabie. Homonym population protocols. Theory of Computing Systems, 62(5):1318–1346, 2018. doi:10.1007/S00224-017-9833-2.

[bib.bib9] [9] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. International Journal of Foundations of Computer Science, 24(7):1099–1116, 2013. doi:10.1142/S0129054113400339.

[bib.bib10] [10] Ho-Lin Chen, David Doty, and David Soloveichik. Deterministic function computation with chemical reaction networks. Natural Computing, 13(4):517–534, 2014. doi:10.1007/S11047-013-9393-6.

[bib.bib11] [11] Zoë Diamadi and Michael J Fischer. A simple game for the study of trust in distributed systems. Wuhan University Journal of Natural Sciences, 6(1):72–82, 2001. doi:10.1007/BF03160228.

[bib.bib12] [12] Javier Esparza and Michael Blondin. Automata theory: An algorithmic approach. The MIT Press, 2023.

[bib.bib13] [13] Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. In Proc. $\text{26}^{\text{th}}$ International Conference on Concurrency Theory (CONCUR), pages 470–482, 2015. doi:10.4230/LIPIcs.CONCUR.2015.470.

[bib.bib14] [14] Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy. Verification of immediate observation population protocols. In Proc. $\text{29}^{\text{th}}$ International Conference on Concurrency Theory (CONCUR), volume 118, pages 31:1–31:16, 2018. doi:10.4230/LIPIcs.CONCUR.2018.31.

[bib.bib15] [15] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Information and Computation, 179(2):279–295, 2002. doi:10.1006/INCO.2001.2953.

[bib.bib16] [16] Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi. Two-way Parikh automata. In Proc. $\text{39}^{\text{th}}$ IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 40:1–40:14, 2019. doi:10.4230/LIPIcs.FSTTCS.2019.40.

[bib.bib17] [17] Adam Ganczorz, Leszek Gasieniec, Tomasz Jurdzinski, Jakub Kowalski, and Grzegorz Stachowiak. Selective population protocols. In Proc. $\text{26}^{\text{th}}$ International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 225–239, 2024. doi:10.1007/978-3-031-74498-3_16.

[bib.bib18] [18] Antonio Cano Gómez, Giovanna Guaiana, and Jean-Éric Pin. Regular languages and partial commutations. Information and Computation, 230:76–96, 2013. doi:10.1016/J.IC.2013.07.003.

[bib.bib19] [19] Rachid Guerraoui and Eric Ruppert. Names trump malice: Tiny mobile agents can tolerate Byzantine failures. In Proc. $\text{36}^{\text{th}}$ International Colloquium Automata, Languages and Programming (ICALP), pages 484–495, 2009. doi:10.1007/978-3-642-02930-1_40.

[bib.bib20] [20] Simon Halfon. On Effective Representations of Well Quasi-Orderings. (Représentations Effectives des Beaux Pré-Ordres). PhD thesis, Université Paris-Saclay, France, 2018. URL: https://tel.archives-ouvertes.fr/tel-01945232.

[bib.bib21] [21] Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, s3-2(1):326–336, 1952. doi:10.1112/plms/s3-2.1.326.

[bib.bib22] [22] Sige-Yuki Kuroda. Classes of languages and linear-bounded automata. Information and Control, 7(2):207–223, 1964. doi:10.1016/S0019-9958(64)90120-2.

[bib.bib23] [23] Kamal Lodaya, Paritosh K. Pandya, and Simoni S. Shah. Around dot depth two. In Proc. $\text{14}^{\text{th}}$ International Conference on Developments in Language Theory (DLT), pages 303–315, 2010. doi:10.1007/978-3-642-14455-4_28.

[bib.bib24] [24] Othon Michail, Ioannis Chatzigiannakis, and Paul G. Spirakis. Mediated population protocols. Theoretical Computer Science, 412(22):2434–2450, 2011. doi:10.1016/J.TCS.2011.02.003.

[bib.bib25] [25] J. Andres Montoya. Asymptotic reasoning with two variables. In Proc. $\text{31}^{\text{st}}$ International Workshop on Logic, Language, Information, and Computation (WoLLIC), pages 38–55, 2025. doi:10.1007/978-3-031-99536-1_3.

[bib.bib26] [26] Jean-Éric Pin. Syntactic semigroups. In Handbook of Formal Languages, Volume 1: Word, Language, Grammar, pages 679–746. Springer, 1997. doi:10.1007/978-3-642-59136-5_10.

[bib.bib27] [27] Jean-Éric Pin and Pascal Weil. Polynomial closure and unambiguous product. In Proc. $\text{22}^{\text{nd}}$ International Colloquium on Automata, Languages and Programming (ICALP), pages 348–359, 1995. doi:10.1007/3-540-60084-1_87.

[bib.bib28] [28] Thomas Place and Marc Zeitoun. All about unambiguous polynomial closure. TheoretiCS, 2, 2023. doi:10.46298/THEORETICS.23.11.

[bib.bib29] [29] Michael Raskin. Modular population protocols. In Proc. $\text{20}^{\text{th}}$ International Symposium on Algorithmics of Wireless Networks (ALGOWIN), pages 173–187, 2024. doi:10.1007/978-3-031-74580-5_13.

[bib.bib30] [30] Marcel-Paul Schützenberger. Sur le produit de concaténation non ambigü. Semigroup Forum, 13(1):47–75, 1976. doi:10.1007/bf02194921.

[bib.bib31] [31] Thomas Schwentick, Denis Thérien, and Heribert Vollmer. Partially-ordered two-way automata: A new characterization of DA. In Proc. $\text{5}^{\text{th}}$ International Conference on Developments in Language Theory (DLT), pages 239–250, 2001. doi:10.1007/3-540-46011-X_20.

[bib.bib32] [32] Pascal Tesson and Denis Thérien. Diamonds are forever: The variety DA. In Semigroups, algorithms, automata and languages, pages 475–499. World Scientific, 2002. doi:10.1142/5050.

[bib.bib33] [33] Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Proc. $\text{30}^{\text{th}}$ Annual ACM Symposium on the Theory of Computing (STOC), pages 234–240, 1998. doi:10.1145/276698.276749.

[bib.bib34] [34] Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, and Chana Weil-Kennedy. Verification of population protocols with unordered data. In Proc. $\text{51}^{\text{st}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 156:1–156:20, 2024. doi:10.4230/LIPIcs.ICALP.2024.156.

[bib.bib35] [35] Chana Weil-Kennedy. Observation Petri Nets. PhD thesis, Technical University of Munich, Germany, 2023. URL: https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20230320-1691161-1-3.

[bib.bib36] [36] Philipp Weis and Neil Immerman. Structure theorem and strict alternation hierarchy for $\text{FO}^{\text{2}}$ on words. In Proc. $\text{21}^{\text{st}}$ International Workshop on Computer Science Logic (CSL), pages 343–357, 2007. doi:10.1007/978-3-540-74915-8_27.

[bib.bib37] [37] Hiroto Yasumi, Fukuhito Ooshita, and Michiko Inoue. Population protocols for graph class identification problems. In Proc. $\text{25}^{\text{th}}$ International Conference on Principles of Distributed Systems, (OPODIS), pages 13:1–13:19, 2021. doi:10.4230/LIPIcs.OPODIS.2021.13.

Population Protocols over Ordered Agents

Abstract

Keywords and phrases:

Category:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Contribution

Related work

2 Preliminaries

Automata and logic.

Population protocols over ordered agents.

Consensus and stability.

Example 1.

Language of a PP.

Example 2.

Example 3.

Theorem 4.

Proof.

3 Semantic restrictions of population protocols: a toolbox

3.1 Semi-deciders

Definition 5.

Lemma 6.

Proof sketch.

Lemma 7.

3.2 Protocols with stabilizing inputs

Definition 8.

Proposition 9.

Proof sketch.

Lemma 10.

Lemma 11.

Proof sketch.

4 Expressiveness of IO-PP[<]

Theorem 12.

4.1 IO-PP[<]⊆ DA

Lemma 13.

Lemma 14.

Lemma 15.

Proof sketch.

Lemma 16.

Proof.

Lemma 17.

Proof sketch.

4.2 DA ⊆ IO-PP[<]

Proposition 18.

Proof sketch.

Proposition 19.

Proof.

5 Expressiveness of PP[<]

5.1 First-order logic over word intervals

Definition 20.

Example 21.

Lemma 22.

Proposition 23.

Proof.

Corollary 24.

5.2 Partially-ordered Parikh automata

Theorem 25.

Observation 26.

Remark 27 (Two-way models).

5.3 The regular languages of PP[<]

Conjecture 28.

Proposition 29.

6 Expressiveness of IO-PP[𝓝] and PP[𝓝] when successor is available

Example 30.

Theorem 31.

6.1 𝗡𝗦𝗣𝗔𝗖𝗘⁢(𝒏)⊆𝗜𝗢-𝗣𝗣⁢[+𝟏]

Lemma 32.

Proof sketch.

Lemma 33.

Proof sketch.

Corollary 34.

Proof.

4 Expressiveness of IO-PP $[<]$

4.1 IO-PP $[<]\subseteq$ DA

4.2 DA $\subseteq$ IO-PP $[<]$

5 Expressiveness of PP $[<]$

5.3 The regular languages of PP $[<]$

6 Expressiveness of IO-PP $[\mathcal{N}]$ and PP $[\mathcal{N}]$ when successor is available

6.1 $\mathsf{NSPACE}(n)\subseteq\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$

7.1 The syntax of PP $[<]$ , $\text{$\mathsf{IO}$-$\mathsf{PP}$}[+1]$ and $\mathsf{PP}[+1]$ deciders are undecidable

7.2 The syntax of IO-PP $[<]$ deciders is decidable, conditionally