Conceptio › Archive › arXiv CS

arXiv CSopen access

Population Protocols over Ordered Agents

2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

Open Source ↗Direct PDF ↓

cloud distributed-computing parallel-computing

distributed computing, parallel computing, cloud

Population Protocols over Ordered Agents Michael Blondin # Département d’informatique, Université de Sherbrooke, Canada

Michaël Cadilhac # DePaul University, Chicago, USA

Benjamin Courchesne # Département d’informatique, Université de Sherbrooke, Canada

Lucie Guillou # MPI for Software Systems, Kaiserslautern, Germany

arXiv:2605.09937v1 [cs.DC] 11 May 2026

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, PP[<] allows for two agents to interact only if the first one appears before the second one. We study population protocols over ordered agents PP[N ] where N is a set of predicates available to restrict transition firing. We also study IO-PP[N ], the immediate observation fragment of PP[N ] where only one agent changes state per interaction. Our main result is that IO-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 PP[<]. We further show that if the successor predicate appears in a set N of NSPACE(n)-computable predicates, then IO-PP[N ] = PP[N ] = 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 PP[<] and IO-PP[+1], but conditionally decidable for IO-PP[<]. 2012 ACM Subject Classification Theory of computation → Formal languages and automata theory; Theory of computation → Distributed computing models; Theory of computation → Logic and verification Keywords and phrases Population protocols, First-order logic, Partially-ordered automata, Unambiguous star-free languages Funding Michael Blondin: supported by a Discovery Grant from the Natural Sciences and Engineering Research Council of Canada (NSERC). Acknowledgements We thank the anonymous reviewers of ICALP 2026 for their thorough reading and valuable suggestions.

Population Protocols over Ordered Agents

Throughout the article, we provide hyperlinks for navigating between statements in the main text and proofs in the appendix. To go to the proof of a statement, click “"” in the left margin, and then click “(” to go back to the statement in the main text.

Contents 1 Introduction

2 Preliminaries

3 Semantic restrictions of population protocols: a toolbox 3.1 Semi-deciders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Protocols with stabilizing inputs . . . . . . . . . . . . . . . . . . . . . . . . .

7 7 8

4 Expressiveness of IO-PP[<] 9 4.1 IO-PP[<] ⊆ DA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2 DA ⊆ IO-PP[<] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 5 Expressiveness of PP[<] 5.1 First-order logic over word intervals . . . . . . . . . . . . . . . . . . . . . . . 5.2 Partially-ordered Parikh automata . . . . . . . . . . . . . . . . . . . . . . . . 5.3 The regular languages of PP[<] . . . . . . . . . . . . . . . . . . . . . . . . . .

11 11 12 14

6 Expressiveness of IO-PP[N ] and PP[N ] when successor is available 14 6.1 NSPACE(n) ⊆ IO-PP[+1] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7 Decidability of checking whether a population protocol is a decider 16 7.1 The syntax of PP[<], IO-PP[+1] and PP[+1] deciders are undecidable . . . . 16 7.2 The syntax of IO-PP[<] deciders is decidable, conditionally . . . . . . . . . . 17 8 Open questions

A Appendix A.1 Missing proofs from Section 3.1 . . . . . . . . . . . . . . . . . . . . . . . . . . A.2 Missing proofs from Section 3.2 . . . . . . . . . . . . . . . . . . . . . . . . . . A.3 Missing proofs from Section 4.1 . . . . . . . . . . . . . . . . . . . . . . . . . . A.4 Missing proofs from Section 4.2 . . . . . . . . . . . . . . . . . . . . . . . . . . A.5 Missing proofs from Section 5.1 . . . . . . . . . . . . . . . . . . . . . . . . . . A.6 Missing proofs from Section 5.2 . . . . . . . . . . . . . . . . . . . . . . . . . . A.7 Missing proofs from Section 5.3 . . . . . . . . . . . . . . . . . . . . . . . . . . A.8 Missing proofs from Section 6.1 . . . . . . . . . . . . . . . . . . . . . . . . . . A.9 Missing proofs from Section 7.1 . . . . . . . . . . . . . . . . . . . . . . . . . . A.10 Missing proofs from Section 7.2 . . . . . . . . . . . . . . . . . . . . . . . . . .

21 21 21 24 26 26 27 28 29 32 34

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

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, a, b}, is updated according to these rules: active to passive

propagation of winning side

tiebreaker

a, b − → a, b

a, b − → a, a b, a − → b, b

a, b − → b, b

Since agents are unordered, each rule p, q → − p′ , q ′ also stands for q, p → − q ′ , p′ . 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: aaabb → − aaabb → − aaabb → − aaaab → − aaaaa, aabbb → − aabbb → − aaabb → − aaabb → − aabbb → − abbbb, → − bbbbb, aabb → − aabb → − aabb → −

abbb → −

bbbb.

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, a}, otherwise they eventually remain in {b, b}. As agents and rules are unordered, each configuration can be seen as a multiset c : Q → N where c(q) indicates the number of agents in state q. It is known that population protocols compute precisely the subsets of NQ 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 φ(c) = c(a) > 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.”

Population Protocols over Ordered Agents

Contribution Motivated by the above, we propose to study population protocols with totally-ordered agents. The class of population protocols so defined, PP[N ], is parameterized by a set N of predicates over positions that can be used to restrict transition firings. Central to our < study is the class PP[<], in which a transition p, q − → 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 IO-PP[<] has the same expressive power as unambiguous star-free languages, an important subclass of regular languages that admits a trove of characterizations (see [35] for a lovely survey on the pervasiveness of this class in automata theory). Hence, IO-PP[<] is the class of languages captured by these formalisms over finite words: partially-ordered unambiguous automata [26]; partially-ordered two-way deterministic automata [33]; LTL[F−1 , F]: linear temporal logic with past and future operators [15]; FO2 [<]: the two-variable fragment of first-order logic with order [36]; ∆2 [<]: the intersection of the ∃∗ ∀∗ and ∀∗ ∃∗ fragments of first-order logic with order [28]; languages recognized by finite monoids from the variety DA [32]. 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 PP[<] protocol whose language is not regular, and therefore not expressible by IO-PP[<] protocols. In addition, we explore systematically the classes induced by our definitions: In Section 3, we provide a toolbox to study population protocols over ordered agents PP[N ], regardless of 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 [31], which enables a form of composition between protocols. In Section 4, we prove the aforementioned characterization of IO-PP[<], and in Section 5, we provide a natural logic and an automaton model expressible in PP[<]. In this latter section, we fall short of showing exact characterizations, but provide conjectures based on our new models. In Section 6, we explore the expressiveness of IO-PP[N ] and PP[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 N are NSPACE(n) computable, then IO-PP[N ] = PP[N ] = NSPACE(n) — this is arguably less surprising than our main result on IO-PP[<], as the successor allows for the left-to-right propagation of information. 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 IO-PP[+1], PP[+1], and PP[<], and conditionally decidable for IO-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

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

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 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′ 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: S n n n≥0 Σ aΣ . They show that if selective population protocols are extended with the possibility of comparing keys, then they can solve the median problem in time O(log4 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 Ω(n). This latter setting, only briefly discussed in [17], corresponds to our model. Further extensions include mediated population protocols [25], 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 [40, 2], where agents aim at determining whether the communication topology satisfies some property. For other work on immediate-observation protocols, see [14, 38, 12, 37].

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 ∈ Σ∗ , 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] · · · w[j]. For σ ∈ Σ, we write |w|σ for the number of occurrences of σ in w. We write FO to denote first-order logic over words, where quantifiers range over positions, that is, the set {1, . . . , |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 FO[<] for the extension of FO with the numerical predicate <, that allows to test whether x < y for two positions x and y. For example, the sentence φ = (∃x)(∀y)[a(x) ∧ ((x < y) → b(y))] describes the language Σ∗ ab∗ . By abuse of notation, FO[<] stands for both the set of syntactic sentences and for the class of languages described by these sentences. It is well known that FO[<] is the class of star-free (regular) languages. We write Σi [<] (resp. Πi [<]) for the fragment of FO[<] of sentences in prenex normal form with i blocks of alternating quantifiers starting with ∃ (resp. ∀). For example, Σ∗ ab∗ belongs to Σ2 [<] due to the form of our example φ. We let ∆i [<] = Σi [<] ∩ Πi [<].

Population Protocols over Ordered Agents

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 N ⊆ 2N×N be any set, whose elements we call numerical predicates: these will be used as the allowed tests on a transition.1 We let true = N2 be the always-true predicate. The set PP[N ] of PPs over N is the set of transition systems (Q, Σ, O, ∆) where Q is a finite set of states, Σ ⊆ Q is a distinguished subset of initial states, O : Q → {⊤, ⊥} maps each state to an opinion, and ∆ ⊆ Q2 × (N ∪ {true}) × Q2 is a set P of transitions. An element of ∆ is denoted q1 , q2 − → q3 , q4 , expressing, intuitively, that if two distinct agents meet, the first being in position i and state q1 , the second in position j and state q2 , such that (i, j) ∈ P , then the first agent changes its state to q3 and the second to q4 . We use Σ 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 Σ. If N = {P1 , P2 , . . .}, we write PP[P1 , P2 , . . .] for PP[N ]. Classical PPs can be seen as the class PP[∅], recalling that we assume that true is always available as a numerical predicate. Our main interest is in the class 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., P P every transition is of the form a, b − → a, c or a, b − → c, b. We write IO-PP[N ] for the class of protocols in PP[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 Σ+ . Let u and v be two configurations of the same length, we say that u leads to v, denoted u → v, if the two configurations are equal except at potentially two distinct positions i and j, and there is a transition P u[i], u[j] − → v[i], v[j] ∈ ∆ with (i, j) ∈ P . We let →∗ be the reflexive transitive closure of →. Consensus and stability. With w a configuration, let O(w) ∈ {⊥, ⊤} 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 →∗ v implies that v is a b-consensus. ▶ Example 1. We give an example of a protocol in PP[<]. Consider the transition system P = < ({a, b, q⊥ }, {a, b}, O, ∆), with O(a) = O(b) = ⊤, O(q⊥ ) = ⊥, and transitions b, a − → q⊥ , q⊥ true and q⊥ , _ −−→ q⊥ , q⊥ with “_” standing for any state. Every input configuration belongs to (a + b)+ and is therefore a ⊤-consensus (all agents output ⊤ initially). However, such configurations need not be ⊤-stable. For instance, starting from ba we can apply the rule < b, a − → q⊥ , q⊥ and obtain q⊥ q⊥ , which is ⊥-stable. In contrast, every configuration in a∗ b∗ is ⊤-stable: it is a ⊤-consensus and no transition is enabled. Language of a PP. Consider an infinite sequence w0 → w1 → w2 → · · · of configurations, which we call a run. We say that it is fair if for every wi that appears infinitely often, each configuration of {v | wi → v} appears infinitely often as well. By induction, fairness guarantees that each configuration of {v | wi →∗ v} appears infinitely often as well. Intuitively, fairness ensures that reachable configurations cannot be avoided forever (in a probabilistic

These 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 max(x) which is true if x is the position of the last agent. This technical difference will not impact our results.

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

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 P is the set L(P) of initial configurations from which there is a fair run that visits a ⊤-stable configuration. Naturally, an initial configuration can be the origin of a fair run visiting a ⊤-stable configuration, another run visiting a ⊥-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 ∈ Σ∗ , there is a b ∈ {⊤, ⊥} 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(P) is PP[N ]-decidable or IO-PP[N ]-decidable with the obvious meaning. We will identify PP[N ] and IO-PP[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 PP[<] from Example 1. We show that it decides the language a∗ b∗ . Every input in a∗ b∗ is already ⊤-stable. Conversely, if an input word is not in a∗ b∗ , then it contains the factor ba. Hence, in any fair run, the transition (b, a) → (q⊥ , q⊥ ) is eventually executed. From that point on, every remaining agent eventually interacts with a ∗ q⊥ -agent and is converted to q⊥ , so the run reaches a configuration in q⊥ , which is ⊥-stable. S ▶ Example 3. Consider the median language L = n∈N Σn aΣn . Let us describe a protocol P = (Q, Σ, O, ∆) that decides L. The states are defined as Q = Σ × {¬, ð, «} × {⊥, ⊤}. 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, ð, ⊤), and each input σ = ̸ a with (σ, ð, ⊥). We set O((x, y, z)) = z. The set ∆ is defined by these rules, each describing a family of transitions: Population halving (1)

< ′ (x, ð, z), (x , ð, z ′ ) − → (x, ¬, ⊥), (x , «, ⊥)

(2) (3)

< ′ ′ (x, ð, z), (x , ¬, z ′ ) − → (x, ¬, ⊥), (x , ð, x = a) < ′ (x, «, z), (x′ , ð, z ′ ) − → (x, ð, x = a), (x , «, ⊥)

′

Center finding ′

Output propagation (4) (5)

true ′ ′ ′ (x, y, z), (x′ , ð, z ′ ) − −→ (x, y, z ), (x , ð, z ) true ′ ′ ′ ′ (x, y, ⊤), (x , y , ⊥) −−→ (x, y, ⊥), (x , y , ⊥)

for y ∈ {¬, «} for y, y ′ ∈ {¬, «}

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, ð, y) remains, then, by fairness and the fourth rule, it will propagate its output y, which is ⊤ 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 ⊥. Figure 1 depicts all configurations reachable from the initial configuration aab ∈ 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⊤ ¬ að b« , which is ⊤-stable. ⊥ ⊥ Note that a⊥ ¬ a« bð is a ⊥-consensus, but is not ⊥-stable.

Population Protocols over Ordered Agents

⊤ ⊥ a⊤ ð að bð

(1)

(1) ⊥ ⊥ a⊥ ¬ a« bð

(3) (5)

⊤ ⊥ a⊥ ¬ að b«

(4)

⊤ ⊥ a⊤ ¬ að b«

(2)

⊥ ⊥ a⊤ ð a¬ b«

(5) ⊤ ⊤ a⊥ ¬ að b«

(4)

(4) ⊤ ⊤ a⊤ ¬ að b«

Figure 1 Configurations reachable from aab, where xzy 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⊥ ¬ að b« → a¬ að b« → a¬ að b« → a¬ að b« → · · ·

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⊤ ¬ að b« , at the bottom, is reached. In the above specific protocol P, for each initial configuration, the reachability graph has a unique trivial bottom strongly connected component, made of one configuration of the form ¬n ð «n or ¬n «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 IO-PP[+1]. Recall that 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 N be a set of numerical predicates, all of which decidable in NSPACE(n). We have PP[N ] ⊆ NSPACE(n). Proof. Recall that a configuration is ⊤-stable if every reachable configuration from it is a ⊤-consensus (i.e., all agents have opinion ⊤). Consider a protocol in PP[N ]. The set of configurations that are not ⊤-stable is decidable in NSPACE(n). Indeed, it is sufficient to nondeterministically guess a partial run (i.e., a finite sequence of configurations w0 → w1 → · · · → wn ) that leads to a configuration that is not a ⊤-consensus. Each transition can be guessed, its condition checked, and its effect applied in NSPACE(n). By the Immerman–Szelepcsényi theorem, NSPACE(n) is closed under complement, and so the set of ⊤-stable configurations is in 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 ⊤-stable configuration. These are all tasks in NSPACE(n). ◀

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

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 ⊆ Σ+ if for all u ∈ Σ+ and every fair run ρ starting from u, we have u ∈ L iff ρ contains a ⊤-stable configuration. We use the terms PP[N ]-semi-decidable and IO-PP[N ]-semi-decidable with the obvious meaning. Note that a decider is a semi-decider in which we additionally require that u ∈ / L iff ρ visits a ⊥-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. ns

⊥

⊤

⊥

(1)

⊤ ns

⊤

(2)

⊥

⊤

⊥

(3)

⊥

⊤

(4)

⊤

(5)

⊥

(6)

Figure 2 Configurations labeled ⊤ , ⊥ and ns are ⊤-stable, ⊥-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 PP[N ]-decidable iff L and its complement are PP[N ]-semidecidable. The same holds for IO-PP[N ]. Proof sketch. We combine the two semi-deciders for L and for Σ+ \ 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 ⊥-witness. For any input u, exactly one of the two simulations eventually provides such a witness (since exactly one of u ∈ L or u ∈ / L holds), which forces all agents to converge to the correct belief and yields a stable consensus, hence a decider. ◀ We note these elementary closure properties:

▶ Lemma 7. If L1 , L2 ⊆ Σ+ are PP[N ]-semi-decidable, then it is also the case for L1 ∩ L2 and L1 ∪ L2 . This further holds for IO-PP[N ] and deciders.

Population Protocols over Ordered Agents

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 [31] for PP[∅]. Let us consider protocols where each agent keeps a copy of its input. Formally, a protocol P = (Q, Σ, O, ∆) is said to be input-saving if Q = Σ × R for some finite set R; Each σ ∈ Σ is identified with (σ, rσ ) for some rσ ∈ R; and The first component σ of any state (σ, r) ∈ Q is left unchanged by all transitions of ∆. For all w ∈ Q+ , let ι(w) ∈ Σ+ be the projection of w onto its first component. Given u, v ∈ Qn , we write u ⇝ v if either u → v, or v equals u except at a single position i where u[i] = (σ, r) and v[i] = (σ ′ , r). This second type of transitions models a “change of mind” of agent i on its input. We write ⇝∗ for the reflexive transitive closure of ⇝. Note what we do not change the definition of run, which still relies on → only. ▶ Definition 8. We say that P semi-decides L ⊆ Σ+ with stabilizing inputs if (a) P is input-saving, and (b) for all u ∈ Σ+ , all u ⇝∗ v and every fair run ρ starting from v, it is the case that ι(v) ∈ L iff ρ visits a ⊤-stable configuration. We use the term “decides” if (b) is strengthened with the condition that ι(v) ∈ / L iff ρ visits a ⊥-stable configuration. Note that this is more robust than simply semi-deciding: if P semi-decides L with stabilizing inputs, then it semi-decides L. Intuitively, after u ⇝∗ v, the configuration of the population (i.e., the projection of v onto the second component) may be incompatible with ι(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 ι(v). It is known that any language L ∈ PP[∅] can be decided, and hence semi-decided, with stabilizing inputs2 [31]. Let us turn to an example, which will be useful later: "

▶ Proposition 9. The language 0∗ 1∗ · · · k ∗ is IO-PP[<]-semi-decidable with stabilizing inputs. Proof sketch. Let Σ = {0, 1, . . . , k} and L = 0∗ 1∗ · · · k ∗ . The protocol P = (Q, Σ, ∆, O) for L is defined by Q = Σ × {⊤, ⊥}, O((σ, o)) = o, each σ ∈ Σ identified with (σ, ⊤), and these rules: (x, ⊤), (y, o) −−<−→ (x, ⊥), (y, o)

for x > y,

true

(x, ⊥), (y, o) −−−→ (x, ⊤), (y, o). The purpose of the first rule is to detect a misordering. The second rule allows any agent to nondeterministically reset itself. ◀ We now turn to closure properties of protocols with stabilizing inputs. We first cover union and intersection, then move on to (nondeterministic) alphabet rewriting.

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

▶ Lemma 10. If L1 , L2 ⊆ Σ+ are PP[N ]-semi-decidable with stabilizing inputs, then it is also the case for L1 ∩ L2 and L1 ∪ L2 . This further holds for IO-PP[N ] and deciders. Given f : Σ → 2Γ and w ∈ Σn , let f (w) = {w1′ · · · wn′ | wi′ ∈ f (wi ) for each i ∈ [1..n]}. For example, if f (0) = {a, b} and f (1) = {b, c}, then f (01) = {ab, ac, bb, bc}. We extend this S notion to languages: f (L) = w∈L f (w).

▶ Lemma 11. Let f : Σ → 2Γ . If L ⊆ Σ+ is PP[N ]-semi-decidable with stabilizing inputs, then f (L) is PP[N ]-semi-decidable with stabilizing inputs. This further holds for IO-PP[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 ∈ Σ+ compatible with the real input u ∈ Γ+ (i.e., u ∈ f (v)). Agents may revise this guess: whenever a ⊥ opinion is observed in the simulated component, an agent is allowed to change its guessed letter to any σ consistent with its input letter (preserving u ∈ f (v) letterwise). If u ∈ f (L), fairness ensures that the population can eventually rewrite the guessed word into some v ′ ∈ L, after which the simulation of the semi-decider for L reaches a ⊤-stable configuration and changes become disabled; if u ∈ / f (L), reaching a ⊤-stable configuration would force the simulated input to lie in L, which is not possible. ◀

Expressiveness of IO-PP[<]

In this section, we provide a precise characterization of the languages decided by IO-PP[<]. For any language L ⊆ Σ∗ , let us write ≡L for the syntactic congruence of L, i.e., w ≡L w′ iff uwv ∈ L ⇔ uw′ v ∈ L for all u, v ∈ Σ∗ . A language is in the class DA if it is regular, and satisfies, writing α(w) ⊆ Σ for the set of letters appearing in a word w: (∀w ∈ Σ∗ ) w ≡L w2 → (∀h ∈ α(w)∗ )[w ≡L w · h · w] , (1) It is a fascinating result of Pin and Weil [28] that DA = ∆2 [<]. We will leverage both characterizations to show the theorem below. The left-to-right inclusion will rely on (1), and the converse on DA = ∆2 [<], semi-deciders, and protocols with stabilizing inputs. ▶ Theorem 12. IO-PP[<] = DA.

4.1

IO-PP[<] ⊆ DA

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

▶ Lemma 13. Any protocol in PP[<] is a well-structured transition system w.r.t. ⪯, that is, for all u, u′ , w ∈ Q∗ with u ⪯ w and u → u′ , there exists w′ such that u′ ⪯ w′ and w → w′ . Further, the set of b-stable configurations is subword-closed and computable. As expected from the definition of DA, the core of the argument showing the inclusion of IO-PP[<] in DA will rely on a pumping argument. As a first observation, we show that, in an IO-PP[<], an infix of the form wzw with α(z) ⊆ α(w) can, in some sense, mimic the behavior of the protocol on the simpler infix w. 2

It was claimed earlier by [2], but definitions and proofs were deferred to a full paper that never appeared.

Population Protocols over Ordered Agents

▶ Lemma 14. In an IO-PP[<], if uwv →∗ u′ w′ v ′ with |u| = |u′ | and |v| = |v ′ |, then for all z with α(z) ⊆ α(w), there exists z ′ such that uwzwv →∗ u′ w′ z ′ w′ v ′ and α(z ′ ) ⊆ α(w′ ). We use this first result to show a pumping lemma on IO-PP[<]. It results from the fact that the sets of ⊤-stable and ⊥-stable configurations are subword-closed and Lemma 14.

▶ Lemma 15. Let L ∈ IO-PP[<]. There exists a computable m ≥ 1 such that, for all w1 , . . . , wm ∈ Σ+ and z ∈ Σ∗ with α(w1 ) = . . . = α(wm ) ⊇ α(z), we have w1 · · · wm ≡L (w1 · · · wm )z(w1 · · · wm ). Proof sketch. Lemma 13 indicates that for both b ∈ {⊤, ⊥}, the set of b-stable configurations is subword-closed. As a consequence, writing B ε for B ∪ {ε}, it is a finite union of languages of the form A∗1 B1ε · · · A∗k Bkε with Ai , Bi subsets of Q, the set of states of our protocol [20, Sect. 6.1.1]. Let Kb be the maximal factorization size k over all those languages, K = max(K⊤ , K⊥ ) 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⊤ , K⊥ and m. ′ Intuitively, if we have a run from w1 · · · wm to a ⊤-stable configuration w′ = w1′ · · · wm , ′ ′ then we can match w with one of the expressions above, and some wi is entirely contained in some A∗j . We then use Lemma 14 to expand the run w → w′ to a run from w′ = w1 · · · wm zw1 · · · wm f′ , by expanding the wi section into wi · · · wm zw1 · · · wi . to some b-stable configuration w We can thus show that if w is accepted, so is w′ . Similarly, we show that if w is not accepted, then it can reach a ⊥-stable configuration, and so can w′ . 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. ◀ We can now show that IO-PP[<]-decidable languages satisfy the definition of 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 ∈ IO-PP[<] and let w ∈ Σ∗ be such that w ≡L w2 . It is the case that w ≡L w · h · w for all h ∈ α(w)∗ . Proof. Lemma 15 implies that there is a (computable) number m such that wm hwm ≡L wm , and since w ≡L w2 , we obtain w ≡L w · h · w as claimed. ◀

▶ Lemma 17. Every IO-PP[<]-decidable language is regular. Moreover, given an IO-PP[<]protocol 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 (w1 · · · wm )z(w1 · · · wm ) with α(w1 ) = . . . = α(wm ) ⊇ α(z). By Lemma 15, this means that every sufficiently long word is ≡L -equivalent to a shorter one, meaning that ≡L has finitely many equivalence classes. Since we can compute m, we can compute this automaton. ◀

4.2

DA ⊆ IO-PP[<]

Recall that L ∈ Π2 [<] iff Σ∗ \ L ∈ Σ2 [<]. Since DA is equal to ∆2 [<] = Σ2 [<] ∩ Π2 [<], it is enough to prove that Σ2 [<] languages are IO-PP[<]-semi-decidable, appealing to Lemma 6 to conclude. Note that Σ2 [<] is the set of languages expressible as finite unions of languages of the form L = A∗0 a1 A∗2 · · · am−1 A∗m with the Ai ’s being subalphabets (see, e.g., [27, Thm. 8.8]).

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

Since semi-deciders are closed under union by Lemma 7, we need only show that L is IO-PP[<]semi-decidable to conclude. We start with a technical proposition that extends a result of [31] 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 DA language, we can effectively construct an IO-PP[<]-protocol recognizing the same language. "

▶ Proposition 18. The language {w ∈ Σ+ | |w|a = 1} is IO-PP[∅]-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 (σ, σ, ·). The belief component then controls the consensus: an (a, a, ⊤) agent can turn any (σ, σ, ·) with σ = ̸ a to ⊤, while the presence of any (σ, σ, ⊥) can spread ⊥ to other agents. Finally, if an a-agent observes another a, it switches to ⊥; combined with the rule that lets an a-agent reset itself to ⊤, this makes a-agents alternate forever between ⊤ and ⊥ 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 ⊥-stable consensus; if it contains exactly one a then every fair run reaches a ⊤-stable consensus; and if it contains at least two a’s then some agent flips its belief forever. ◀ ▶ Proposition 19. The language L = A∗0 a1 A∗2 · · · am−1 A∗m is IO-PP[<]-semi-decidable (with stabilizing inputs). T Proof. Let Γ = {0, 1, . . . , m}, K = 0∗ 1∗ · · · m∗ and K ′ = a∈Γ,a odd {w ∈ Γ+ | |w|a = 1}. By Proposition 9, K is IO-PP[<]-semi-decidable with stabilizing inputs. Furthermore, by Proposition 18 and Lemma 10, K ′ is IO-PP[∅]-semi-decidable with stabilizing inputs. By Lemma 10, K ∩ K ′ is IO-PP[<]-semi-decidable with stabilizing inputs. Let f (i) = Ai for even i, and f (i) = {ai } otherwise. We are done by Lemma 11 since L = f (K ∩ K ′ ). ◀

Expressiveness of PP[<]

The crisp characterization of the previous section ties IO-PP[<] to a wealth of computational models with strikingly different flavors. Chief among them, DA is characterized by a logic, ∆2 [<], and by partially-ordered unambiguous automata. A natural question is thus whether 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 PP[<]-decidable. Our formalisms will involve Presburger arithmetic, the first-order theory of the naturals with order and addition; e.g., ϕ(x) = (∃y ∈ N)[y ≥ 1 ∧ x = 2y] holds iff x is a positive even number. Write ≡c for the equivalence of naturals modulo c. It is well known that Presburger arithmetic together with ≡c with any c ≥ 2 admits quantifier elimination. For our purposes, a Presburger formula is a (quantifier-free) Boolean combination of predicates of the form Pn Pn i=1 ai xi < b or i=1 ai xi ≡c b, where ai , b ∈ Z, c ≥ 2 and variables xi are over N.

5.1

First-order logic over word intervals

▶ Definition 20. For w ∈ Σn and σ ∈ Σ, let #σ : {1, . . . , n} × {1, . . . , n} → N be the function that counts the number of occurrences of σ between two positions of w, i.e., #σ (x, y) = |w[x..y]|σ . We define FOint 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

Population Protocols over Ordered Agents

position (denoted “1”) or the last position (denoted “max”). We will study FOint [<, +, ≡], where we allow numerical values to be compared, added, and tested modulo c for any constant P c. Note that a variable x can be expressed as σ∈Σ #σ (1, x), we will thus assume that the P atomic formulas only have terms of the form #a (x, y), though we write 1 for σ∈Σ #σ (1, 1), P int int and max for σ∈Σ #σ (1, max). The logics Σint k , Πk , and ∆k are naturally defined. S ▶ Example 21. Let us show that the median language n∈N Σn aΣn belongs to ∆int 1 [<, +, ≡]. P The following predicate asserts that x is the middle position: ψ(x) = σ∈Σ #σ (1, x) = P σ∈Σ #σ (x, max). The median language can either be expressed by (∃x)[ψ(x) ∧ a(x)], or by (∀x)[(ψ(x) → a(x)) ∧ max ≡2 1]. Note that a(x) is the same as #a (x, x) = 1. We now provide a convenient characterization of languages in Σint 1 [<, +, ≡]. "

▶ Lemma 22. Any language from Σint 1 [<, +, ≡] is a finite union of languages of the form K = {a0 w1 a1 · · · wm am | wi ∈ Σ∗ , ai ∈ Σ, φ(xi,σ 7→ |wi |σ , yi,σ 7→ |ai |σ )} where m ≥ 0 and φ is a Presburger formula over variables {xi,σ | i ∈ [1..m], σ ∈ Σ} ∪ {yi,σ | i ∈ [0..m], σ ∈ Σ}. Thanks to the previous lemma, we are able to build a protocol PP[<] semi-deciding any language in Σint 1 [<, +, ≡], 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 Σint 1 [<, +, ≡] is PP[<]-semi-decidable. Proof. Let L ∈ Σint 1 [<, +, ≡]. By Lemma 22, L is a finite union of languages of the form L′ = {a0 w1 a1 · · · wm am | wi ∈ Σ∗ , ai ∈ Σ, φ(xi,σ 7→ |wi |σ , yi,σ 7→ |ai |σ )} where m ≥ 0 and φ is a Presburger formula. It suffices to show that L′ is PP[N ]-semi-decidable with stabilizing inputs. Indeed, by Lemma 10, that class of languages is closed under union. S S Let Σ = {σ | σ ∈ Σ}, Ai = Σ × {i}, Wi = Σ × {i} and Γ = i∈[0..m] Ai ∪ i∈[1..m] Wi . We justify that the three following languages K, K ′ and K ′′ over alphabet Γ are semi-decided with stabilizing inputs: ∗ ∗ Am , K = A∗0 W1∗ A∗1 · · · Wm ′ + K = {w ∈ Γ | φ(xi,σ 7→ |w|(σ,i) , yi,σ 7→ |w|(σ,i) )}, n o P P K ′′ = w ∈ Γ+ | γ∈A1 |w|γ = 1 ∧ · · · ∧ γ∈Am |w|γ = 1 (recall Ai ∩ Aj = ∅ for i = ̸ j).

Let f (2i) = Ai and f (2i + 1) = Wi+1 . We have f (0∗ 1∗ 2∗ · · · (2m)∗ ) = K. By Proposition 9 and Lemma 11, K is PP[<]-semi-decidable with stabilizing inputs. Since K ′ , K ′′ ∈ PP[∅], these two languages are PP[∅]-decidable with stabilizing inputs [2, 31]. By Lemma 10, the language K ∩ K ′ ∩ K ′′ is PP[<]-semi-decidable with stabilizing inputs. Let g((σ, i)) = g((σ, i)) = {σ}. We are done by Lemma 11 since L′ = g(K ∩ K ′ ∩ K ′′ ). ◀ "

▶ Corollary 24. ∆int 1 [<, +, ≡] ⊆ 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 A = (Q, Σ, δ, q0 , F, Ψ) where: Q is a finite set of states equipped with a partial order ≤; Σ is a finite alphabet; δ ⊆ Q × Σ × Q is the transition relation, that satisfies p ≤ q for all (p, σ, q) ∈ δ; if p = q, the transition is dubbed a self-loop, and otherwise, a progress transition;

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

q0 ∈ Q is the initial state, and F ⊆ Q is the set of final states; Ψ is a Presburger formula over variables δ. For all t = (q, σ, q ′ ) ∈ δ, we write q →t q ′ and πΣ (t) = σ. We naturally lift these notations to sequences. A word w ∈ Σ∗ is accepted by A if there exist ρ ∈ δ ∗ and q ∈ F such that q0 →ρ q, πΣ (ρ) = w and Ψ(t 7→ |ρ|t ) holds. The language of A is the set L(A) of words it accepts. Figure 3 depicts two examples of poPA. t: Σ

s: Σ a

Ψ = (s = t)

s′ : ⊏

u: a

t: ⊐

⊏, ⊐ ⊏

s: ⊏

⊐

Ψ = (u = s + s′ + t + t′ ) ∧ (t + t′ > s + s′ )

t′ : ⊐

Figure 3 Example of poPA for the median language n≥0 Σn aΣn (left) and the coDyck-witness language {an v | n ≥ 1, v ∈ {⊏, ⊐}≥n , |v[1..n]|⊐ > |v[1..n]|⊏ } (right).

Lemma 22 allows us to translate a formula from Σint 1 [<, +, ≡] into a poPA by guessing a factorization a0 w1 a1 · · · wm am with a progress transition for each ai , and a self-loop for each wi ; and then using the Presbuger acceptance formula of the automaton to verify the guess. We can also translate a poPA into a formula of Σint 1 [<, +, ≡] 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 Σint 1 [<, +, ≡]. Recall that Σ2 [<] is characterized by partially-ordered automata, while ∆2 [<] is characterized by unambiguous partially-ordered automata. We explore a similar notion for 3 ∆int 1 [<, +, ≡] and poPA. A poPA A is weakly unambiguous if every w ∈ L(A) is accepted by at most one path (w.r.t. F and Ψ). Note that the automata of Figure 3 are weakly unambiguous and can be complemented. By Theorem 25, this means that both languages belong to ∆int 1 [<, +, ≡]. 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 ∆int 1 [<, +, ≡]. In the forthcoming Conjecture 40, we postulate that these two classes coincide. We note, as a sanity check, that since ∆2 [<] is characterized by unambiguous partially-ordered automata, IO-PP[<] = DA = ∆2 [<] ⊊ ∆int 1 [<, +, ≡]. The strictness of the inclusion is in particular witnessed by the regular language {a2n | n ≥ 1} over alphabet {a}, which trivially belongs to ∆int 1 [<, +, ≡] with formula max ≡2 0. ▶ Remark 27 (Two-way models). Recall that 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. 3

The 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.

Population Protocols over Ordered Agents

5.3

The regular languages of PP[<]

Lemma 22 gives a clear form for the languages of Σint 1 [<, +, ≡]. If the language K therein is regular, this points to the formula φ not arithmetically linking the wi ’s between one another nor imposing nonregular constraints on any single wi . Hence we have naturally: ▶ Conjecture 28. Let Com be the set of commutative regular languages. Let Pol(Com) be the set of languages that are finite unions of languages L0 a1 L1 · · · an Ln with Li ∈ Com and ai letters. We conjecture that the regular languages of Σint 1 [<, +, ≡] are exactly Pol(Com). The class Pol(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 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 Σint 1 [<, +, ≡]. The class UPol(Com) is defined similarly as Pol(Com), except that we require that every word w in the marked concatenation has a unique decomposition w = w0 a1 w1 · · · an wn with wi ∈ Li . It is known [29] that UPol(Com) = Pol(Com) ∩ Pol(Com). We naturally postulate, in Conjecture 40, that the regular languages of PP[<] are exactly UPol(Com).

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

We now consider protocols where transitions may be fired only when two agents are adjacent. Formally, we look at IO-PP[N ] and PP[N ] with +1 ∈ N , where +1 (sometimes written succ in the literature) is the predicate {(x, x + 1) | x ∈ N}. This study is reminiscent of the classic study of FO2 [<, +1] [15, 23, 36, 39] that followed that of FO2 [<], the two-variable fragment of FO[<] that is as expressive as IO-PP[<]. ▶ Example 30. Recall that the set of all b-stable configurations of a PP[<] is subword-closed, and hence regular. The following PP[+1] has a non-regular set of ⊤-stable configurations: true aÝ , bÝ −− −→ a , b

+1 Ý a , a −− −→ ✓, a

+1 a , b −− −→ p , p

+1 Ý b, b −− −→ b , ✓

Let us set the opinion of each state to ⊤, except for p . The protocol is constructed so that from a configuration of the form aÝ a∗ b∗ bÝ , 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 p appears. The set of ⊤-stable configurations cannot be regular since, from w ∈ aÝ a∗ b∗ bÝ , the state p will appear iff |w|a = |w|b , e.g., aÝ abbÝ → a abb → ✓aÝ bb → ✓aÝ bÝ ✓ → ✓a b ✓ → ✓ p p ✓. The main result of this section is: ▶ Theorem 31. Let N be a set of NSPACE(n)-decidable numerical predicates that contains +1. We have IO-PP[N ] = PP[N ] = NSPACE(n). To show this result, it is enough to prove that NSPACE(n) ⊆ IO-PP[+1], since PP[N ] ⊆ NSPACE(n) has been established beforehand in Theorem 4.

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

6.1

NSPACE(n) ⊆ IO-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 PP[+1]-semi-decidable language. There exists a PP[+1]-protocol P ′ semi-deciding L and such that each +1-transition of P ′ is immediate-observation. Proof sketch. The construction turns a PP[+1]-protocol P into a new PP[+1]-protocol P ′ +1 by replacing each transition δ = (a, b) − −→ (c, d) with a short four-step handshake along the successor relation, using auxiliary markers aδ and back,δ . The four rules are: +1 δ a, b − −→ a , b +1 ack,δ aδ , back,δ − −→ c, b

+1 δ ack,δ aδ , b − −→ a , b +1 c, back,δ − −→ c, d

Intuitively, one agent announces that it wants to perform δ, 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. ◀ "

▶ Lemma 33. The language of a linear-bounded nondeterministic Turing machine is IO-PP[+1]-semi-decidable. Proof sketch. Given a linear-bounded nondeterministic Turing machine M , we construct an IO-PP[+1]-protocol P that simulates M under stabilizing inputs. Thanks to Lemma 32, we only need to ensure that true-transitions are immediate-observation. Let Σ′ be the tape alphabet of M . The protocol P works over Γ∗ where Γ = (P ∪ {−}) × ′ Σ × {fst, −, lst}. For example, w = (−, a, fst)(p, a, −)(−, b, lst) represents the configuration of M in state p, with the head on the second cell, and the tape containing aab. The protocol P simulates M using +1-transitions with the agent containing the current state p. If M accepts, then P spreads ⊤ across the population. There are two challenges: 1. Since we want to semi-decide under stabilizing inputs, 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 P is an invalid configuration of M , then the population should not reach a stable ⊤-consensus. For example, if two agents both represent the head of M , then they change their belief to ⊥ upon meeting. Similarly, we must detect whether “fst” and “lst” occur exactly in the first and last agent. The resulting protocol 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 Γ. This can be done thanks to Propositions 9 and 18 and Lemmas 10 and 11. ◀ ▶ Corollary 34. NSPACE(n) ⊆ IO-PP[+1]. Proof. Let L ∈ NSPACE(n). As NSPACE(n) is closed under complement, there exist two linear-bounded nondeterministic Turing machines M and M recognizing L and Σ+ \ L, respectively. By Lemma 33, we can build two IO-PP[+1]-protocols, say PM and PM , that semi-decide L and Σ+ \ L, respectively. Lemma 6 allows to conclude. ◀

Population Protocols over Ordered Agents

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 PP[∅] [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 [37]. We show that the problem is undecidable already for PP[<] and IO-PP[+1], and provide a natural conjecture that would entail that the problem is decidable for IO-PP[<].

7.1

The syntax of PP[<], IO-PP[+1] and PP[+1] deciders are undecidable

First, we consider the emptiness problem: given a PP[N ] protocol P, is there an execution from an initial configuration u to a ⊤-stable one? We use a technique from [37] to show a general reduction to the syntax problem. "

▶ Lemma 35. The emptiness problem for PP[N ] (resp. IO-PP[N ]) reduces to deciding the complement of the syntax of PP[N ] (resp. IO-PP[N ]) deciders. Proof sketch. From a protocol P = (Q, Σ, O, ∆), we construct a protocol P ′ such that P ′ is not a decider iff P can reach a ⊤-stable configuration. The construction adds a fresh sink state q⊥ with O(q⊥ ) = ⊥, and for every state q with O(q) = ⊥ we add a transition allowing an agent in q to switch to q⊥ . As a consequence, from any configuration that contains a ⊥-agent, a fair execution can ∗ drive the system to the ⊥-stable consensus q⊥ . On the other hand, if a ⊤-stable configuration is reachable in P, then the same configuration is reachable in P ′ and remains ⊤-stable there: none of the added transitions to q⊥ are enabled from ⊤-states. Therefore P ′ is not a decider. Conversely, if P has no reachable ⊤-stable configuration, then no fair run of P ′ stabilizes ∗ to ⊤. Every fair run stabilizes to q⊥ and P ′ decides the empty language. The construction preserves immediate observation, as each new transition updates at most one agent. ◀ This reduction, combined with the translation from linear-bounded Turing machines to IO-PP[+1] from Section 6, already yields the following result.

▶ Corollary 36. The syntax of IO-PP[+1] and PP[+1] deciders are undecidable.

▶ Theorem 37. The emptiness problem is undecidable for PP[<]. Hence the syntax of PP[<] deciders is also undecidable. Proof sketch. We reduce from the Post correspondence problem. Specifically, we take two homomorphisms h1 , h2 : B ∗ → A∗ and construct a PP[<] that can reach a ⊤-stable configuration if and only if there is a word u such that h1 (u) = h2 (u). We obtain it as a product of three protocols. One makes sure that we can only reach a ⊤-stable configuration from an initial one of the form #1 v#2 u#3 with v ∈ B ∗ and u ∈ A∗ . The two others check that we can reach a ⊤-stable configuration only when h1 (u) = v and h2 (u) = v, respectively. Each one does so by making agents simulate two reading heads going through u and v in lockstep and verifying that hi (u) = v. Initially all agents have opinion ⊥, and in order to

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

change it they must carry the reading head at some point, hence we cannot skip any letter in order to reach a ⊤-stable configuration. Hence, a ⊤-stable configuration is reachable iff there exist u, v with h1 (u) = v = h2 (u). ◀

7.2

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

We present a conjecture on the reachability relation of IO-PP[<], then show that it entails decidability of the syntax of their deciders: ▶ Conjecture 38. The set of configurations reachable from a DA language in an IO-PP[<] protocol is also a DA language. "

▶ Theorem 39. If Conjecture 38 holds, then the syntax of IO-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⊤ , K⊥ such that every input word is in one of the two, they are closed under transitions of the protocol, and from everywhere in Kb we can reach a b-stable configuration. Assuming the conjecture, we can assume that those invariants are in DA. We show that we can enumerate potential regular invariants and check the requirements, yielding the second semi-decision procedure. ◀ In fact, one could slightly strengthen the statement above: it suffices to know that the set of configurations reachable from a DA language in P (instead of in every IO-PP[<]-protocol) is also a DA language, to be able to check whether P is a decider. This means that if we can prove Conjecture 38 over only a subclass of IO-PP[<]-protocols, then we know that the syntax of that subclass is decidable.

Open questions

The most tantalizing open question left open by this work is the characterization of PP[<]. We conjecture that the logic and automata models introduced in Section 5 are tight: ▶ Conjecture 40. PP[<] is the class of languages recognized by ∆int 1 [<, +, ≡] and the class of languages recognized by weakly unambiguous poPA. The regular languages of PP[<] are exactly UPol(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. 12th International Conference on Developments in Language Theory (DLT), pages 96–107, 2008. doi:10.1007/978-3-540-85780-8_7. 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.

Population Protocols over Ordered Agents

8 9

11 12 13

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. 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. 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. Michael Blondin and François Ladouceur. Population protocols with unordered data. In Proc. 50th International Colloquium on Automata, Languages, and Programming (ICALP), pages 115:1–115:20, 2023. doi:10.4230/LIPICS.ICALP.2023.115. Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-unambiguous Parikh automata and their link to holonomic series. In Proc. 47th International Colloquium on Automata, Languages, and Programming (ICALP), pages 114:1–114:16, 2020. doi:10.4230/ LIPICS.ICALP.2020.114. 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. 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. 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. 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. Javier Esparza and Michael Blondin. Automata theory: An algorithmic approach. The MIT Press, 2023. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. In Proc. 26th International Conference on Concurrency Theory (CONCUR), pages 470–482, 2015. doi:10.4230/LIPICS.CONCUR.2015.470. Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy. Verification of immediate observation population protocols. In Proc. 29th International Conference on Concurrency Theory (CONCUR), volume 118, pages 31:1–31:16, 2018. doi:10.4230/LIPICS. CONCUR.2018.31. 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. Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi. Two-way Parikh automata. In Proc. 39th 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. Adam Ganczorz, Leszek Gasieniec, Tomasz Jurdzinski, Jakub Kowalski, and Grzegorz Stachowiak. Selective population protocols. In Proc. 26th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 225–239, 2024. doi:10.1007/978-3-031-74498-3_16. 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. Rachid Guerraoui and Eric Ruppert. Names trump malice: Tiny mobile agents can tolerate Byzantine failures. In Proc. 36th International Colloquium Automata, Languages and Programming (ICALP), pages 484–495, 2009. doi:10.1007/978-3-642-02930-1_40.

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

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.

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.

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.

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

M. Lothaire. Algebraic Combinatorics on Words. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2002.

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.

J. Andres Montoya. Asymptotic reasoning with two variables. In Proc. 31st International Workshop on Logic, Language, Information, and Computation (WoLLIC), pages 38–55, 2025. doi:10.1007/978-3-031-99536-1_3.

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.

Jean-Éric Pin and Pascal Weil. Polynomial closure and unambiguous product. In Proc. 22nd International Colloquium on Automata, Languages and Programming (ICALP), pages 348–359, 1995. doi:10.1007/3-540-60084-1_87.

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

Frank P Ramsey. On a problem of formal logic. In Classic Papers in Combinatorics, pages 1–24. Springer, 1987. doi:10.1007/978-0-8176-4842-8_1.

Michael Raskin. Modular population protocols. In Proc. 20th International Symposium on Algorithmics of Wireless Networks (ALGOWIN), pages 173–187, 2024. doi:10.1007/ 978-3-031-74580-5_13.

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

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

Michael Sipser. Introduction to the theory of computation. Thomson Course Technology, second edition, 2006.

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.

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

Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, and Chana Weil-Kennedy. Verification of population protocols with unordered data. In Proc. 51st International Colloquium on Automata, Languages, and Programming (ICALP), pages 156:1–156:20, 2024. doi:10.4230/LIPICS.ICALP.2024.156.

Chana Weil-Kennedy. Observation Petri Nets. PhD thesis, Technical University of Munich, Germany, 2023.

Philipp Weis and Neil Immerman. Structure theorem and strict alternation hierarchy for FO2 on words. In Proc. 21st International Workshop on Computer Science Logic (CSL), pages 343–357, 2007. doi:10.1007/978-3-540-74915-8_27.

Population Protocols over Ordered Agents

Hiroto Yasumi, Fukuhito Ooshita, and Michiko Inoue. Population protocols for graph class identification problems. In Proc. 25th International Conference on Principles of Distributed Systems, (OPODIS), pages 13:1–13:19, 2021. doi:10.4230/LIPICS.OPODIS.2021.13.

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

(

Appendix

A.1

Missing proofs from Section 3.1

▶ Lemma 6. A language L is PP[N ]-decidable iff L and its complement are PP[N ]-semidecidable. The same holds for IO-PP[N ]. Proof. ⇒) This is immediate, since a protocol deciding L is a semi-decider for L, and the complement protocol, obtained by swapping ⊤ and ⊥ in the opinion function, is a semi-decider for Σ+ \ L. ⇐) This requires combining the two semi-deciding protocols P+ , P− , for L and Σ+ \ L respectively, into a protocol P. We let Ps = (Qs , Σ, Os , ∆s ), for s ∈ {+, −}, and we define P = (Q, Σ′ , O, ∆) as follows. We let Q = Q+ × Q− × {+, −}, with Σ′ = {(a, a, s) | a ∈ Σ, s = + iff a ∈ L}. We identify a ∈ Σ with the state (a, a, s) ∈ Q where s = + iff a ∈ L. By this identification, the protocol P recognizes a language over Σ and is correct on single agent runs by definition (since with a single agent no transition can be taken). The third component is called the belief of the agent. The function O maps each (q+ , q− , s) to O+ (q+ ) if s = +, and ¬O− (q− ) otherwise. Finally, the transitions of P are of two kinds: (Simulation.) A transition of P+ or P− can be used, on the appropriate component Q+ or Q− . The two other components stay the same. (Flip.) If two agents have different beliefs, then one of them can flip its belief. The true numerical predicate is used for these transitions. An agent in state (q+ , q− , s) can also flip its belief by itself if Os (qs ) = ⊥. Consider u ∈ Σ+ of length at least 2. Assume that u ∈ L, the case where u ∈ / L being symmetric. Let v ∈ Post∗ (u). Let v+ and v− be the projections of v on Q+ and Q− respectively. Observe that for both s ∈ {+.−}, vs is reachable from u in Ps . In consequence, since u ∈ L, there is an execution of P+ from v+ to a ⊤-stable w+ . There is also an execution of P− from v− to a configuration w− where at least one agent has opinion ⊥. By following both those executions one after the other, we can go from v to a configuration w in P, so that the projection of w on Q+ and Q− are w+ and w− . If the agent which has opinion ⊥ in w− has opinion −, it can switch it to +. Then, we can flip all the other agents to +, by making them observe this agent. The resulting configuration is ⊤-stable. As mentioned, the case u ∈ / L is symmetric, showing that P is a decider. Furthermore, observe that if both P+ and P− are immediate observation protocols, then so is P. ◀

(

▶ Lemma 7. If L1 , L2 ⊆ Σ+ are PP[N ]-semi-decidable, then it is also the case for L1 ∩ L2 and L1 ∪ L2 . This further holds for IO-PP[N ] and deciders. Proof. The proof is standard, and we will give, in Lemma 10, a slightly more intricate proof with the same ideas, so we omit it here. ◀

A.2 (

Missing proofs from Section 3.2

▶ Proposition 9. The language 0∗ 1∗ · · · k ∗ is IO-PP[<]-semi-decidable with stabilizing inputs.

Population Protocols over Ordered Agents

Proof of correctness. Note that P is input-saving and immediate-observation. Let us show that P semi-decides L with stabilizing inputs. Let u ∈ Σ+ and u ⇝∗ v. Let v = w0 → w1 → · · · be a fair run. For the special case of |v| = 1, note that each state starts with output ⊤ and this remains so as no transition is ever enabled. Let us assume that |v| ≥ 2. Case ι(v) ∈ L. The first rule is permanently disabled in w0 . Hence, by fairness, the second rule must swap the last component of each agent to ⊤. Once this happens, the population has reached a ⊤-consensus, and the configuration cannot change anymore. Case ι(v) ∈ / L. Recall that the first component of each agent is fixed from w0 onwards. Let i < j be positions such that ι(v)[i] > ι(v)[j]. Using the second rule, all agents can change their opinion to ⊤, and then, using the first rule, agent i can change its opinion to ⊥. By fairness, this happens infinitely often, which means that the run does not stabilize. ◀ (

▶ Lemma 10. If L1 , L2 ⊆ Σ+ are PP[N ]-semi-decidable with stabilizing inputs, then it is also the case for L1 ∩ L2 and L1 ∪ L2 . This further holds for IO-PP[N ] and deciders. Proof. Let P1 = (Q1 , Σ, ∆1 , O1 ) and P2 = (Q2 , Σ, ∆2 , O2 ) be the protocols that respectively PP[N ]-semi-decide L1 and L2 with stabilizing inputs. Intersection. We simply take the product of both protocols; simulate them independently with a common input component; and output the conjunction of their outputs. Let Q1 = Σ×R1 and Q2 = Σ×R2 . Formally, we define P = (Q, Σ, ∆, O) by R = R1 ×R2 , Q = Σ × R, O((σ, q1 , q2 )) = O1 ((σ, q1 )) ∧ O2 ((σ, q2 )), and the following rules: P ′ (σ, q1 , r), (σ ′ , q2 , s) − → (σ, q3 , r), (σ , q4 , s)

P ′ for (σ, q1 ), (σ ′ , q2 ) − → (σ, q3 ), (σ , q4 ) ∈ ∆1

and r, s ∈ R2 , ′

′

(σ, r, q1 ), (σ , s, q2 ) − → (σ, r, q3 ), (σ , s, q4 )

P ′ for (σ, q1 ), (σ ′ , q2 ) − → (σ, q3 ), (σ , q4 ) ∈ ∆2

and r, s ∈ R1 . We identify each σ ∈ Σ with (σ, σ, σ). Note that P is input-saving, and immediate-observation if it is the case of P1 and P2 . Let us show that P semi-decides L = L1 ∩ L2 with stabilizing inputs. For every w ∈ Q+ , + let π1 (w) ∈ Q+ 1 be the projection of w onto its first two components, and let π2 (w) ∈ Q2 + ∗ be the projection of w onto its first and third components. Let u ∈ Σ and u ⇝ v. Let v = w0 → w1 → · · · be a fair run from v. By definition of P, the sequence πi (w0 ), πi (w1 ), · · · is a fair run of Pi . Moreover, ι(v) = ι(π1 (v)) = ι(π2 (v)). Case ι(v) ∈ L. Since ι(v) ∈ L1 ∩ L2 , the runs of P1 and P2 eventually stabilize to ⊤-stable configurations. Since O is a conjunction, the same holds for the run of P. Case ι(v) ∈ / L. Let i ∈ {1, 2} be such that ι(v) ∈ / Li . The run of Pi visits infinitely many configurations containing a state q ∈ Qi with Oi (q) = ⊥. Since O is a conjunction, the same holds for the run of P. Furthermore, if Pi is a decider, then the run of Pi eventually stabilizes to ⊥-stable configurations, which implies the same for the run of P. Union. We cannot simply take the previous construction and redefine the output mapping to O((σ, q1 , q2 )) = O1 ((σ, q1 )) ∨ O2 ((σ, q2 )). For example, if P1 and P2 have two agents with outputs ⊤⊥ and ⊥⊤ respectively, then their disjunction yields ⊤⊤, which is incorrect as neither P1 nor P2 is in a ⊤-consensus. Instead, we extend Q with an extra component {1, 2} that indicates which output should be used, and define O((σ, q1 , q2 , i)) = Oi ((σ, qi )). The transitions from ∆ simply ignore this

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

new component. However, we need to add this (immediate-observation) rule: true ′ ′ ′ ′ (σ, q1 , q2 , i), (σ ′ , q1′ , q2′ , i′ ) − −→ (σ, q1 , q2 , 3 − i), (σ , q1 , q2 , i )

for i ̸= i′ ∨ Oi (qi ) = ⊥ ∨ Oi (qi′ ) = ⊥. This way, as long as agents have not agreed on a common choice, or as long as their choice is not in a ⊤-consensus, they may change their mind. Note that this is correct even for “deciders”: If P1 and P2 both reach ⊥-stability, then agents will indefinitely change their choice, but nonetheless steadily output ⊥. ◀ (

▶ Lemma 11. Let f : Σ → 2Γ . If L ⊆ Σ+ is PP[N ]-semi-decidable with stabilizing inputs, then f (L) is PP[N ]-semi-decidable with stabilizing inputs. This further holds for IO-PP[N ]. Proof. Let P = (Q, Σ, ∆, O) be the protocol that semi-decides L with stabilizing inputs. Since P is input-saving, its states are of the form Q = Σ × R. We provide a protocol P ′ where, on input u ∈ Γ+ , the population internally starts with an arbitrary word v such that u ∈ f (v) and runs P on v. With luck, it may be the case that v ∈ L, but this needs not be the case. Therefore, the population may change its choice: If an agent of P ′ has input γ and encounters a ⊥-state of P, then it can change its internal input of P to any letter σ such that γ ∈ f (σ). Let us now describe the protocol formally. For every γ ∈ Γ, let σγ be an arbitrary letter4 of Σ such that γ ∈ f (σγ ). To handle the corner case of populations with a single agent, if there is choice such that σγ ∈ L, then we take one. We define P ′ = (Q′ , Γ, ∆′ , O′ ) as follows: Q′ = Γ × Q; We identify each γ ∈ Γ with (γ, σγ ); O′ ((γ, q)) = O(q); The transitions of ∆′ are defined by (γ, q1 ), (γ ′ , q2 ) −−P−→ (γ, q3 ), (γ ′ , q4 ) true ′ ′ (γ, q), (γ ′ , q ′ ) −− −→ (γ, σ), (γ , q )

P for γ, γ ′ ∈ Γ and (q1 , q2 ) − → (q3 , q4 ) ∈ ∆,

for γ, γ ′ ∈ Γ, q, q ′ ∈ Q and σ ∈ Σ such that γ ∈ f (σ), and O(q) = ⊥ or O(q ′ ) = ⊥.

The protocol is input-saving. The second rule is immediate-observation. Moreover, if P is immediate-observation, then it is also the case of the first rule. It remains to show that P ′ semi-decides f (L) with stabilizing inputs. For all w ∈ (Q′ )+ , let π(w) be the projection of w onto its second component. Recall that ι(w) is the projection of w onto its first component. Let u ∈ Γ+ and u ⇝∗ v. Let v = w0 → w1 → · · · be a fair run. The case where |v| = 1, and hence ι(v) = γ ∈ Γ, is trivially correct by the choice of σγ . Thus, suppose that |v| ≥ 2. Case ι(v) ∈ f (L). By hypothesis, there exists v ′ ∈ L such that ι(v) ∈ f (v ′ ). For the sake of contradiction, suppose that no ⊤-stable configuration is visited by the fair run. By assumption, there exist indices i0 < i1 < · · · such that O′ (wij ) = ⊥ for all j ≥ 0. By definition of O′ , this means that O(π(wij )) = ⊥ for all j ≥ 0. By fairness and the second rule, we can change the second component of the population to v ′ (and hence the input of P to v ′ ). Since P semi-decides L with stabilizing inputs, we can reach a ⊤-stable configuration of P in the second component. Consequently, the second rule becomes permanently disabled, which implies that P ′ visits a ⊤-stable configuration, a contradiction. 4

If no such σγ exists, then we can simply map γ to a dummy state with opinion ⊥, as no word containing γ belongs to f (L). That being said, we will never invoke the lemma with such an f .

Population Protocols over Ordered Agents

Case ι(v) ∈ / f (L). For the sake of contradiction, suppose that there exists j ≥ 0 such that O′ (wj ) = O′ (wj+1 ) = · · · = ⊤. This means that wj → wj+1 → · · · only uses the first rule. By definition of O′ , we have O(π(wj )) = O(π(wj+1 )) = · · · = ⊤. Since P semi-decides L with stabilizing inputs, this implies that ι(π(wj )) ∈ L and hence ι(wj ) ∈ f (L), which is a contradiction. ◀

A.3 (

Missing proofs from Section 4.1

▶ Lemma 13. Any protocol in PP[<] is a well-structured transition system w.r.t. ⪯, that is, for all u, u′ , w ∈ Q∗ with u ⪯ w and u → u′ , there exists w′ such that u′ ⪯ w′ and w → w′ . Further, the set of b-stable configurations is subword-closed and computable. Proof. In a PP[<], we have u → u′ if and only if there exist a, b, c, d ∈ Q and u1 , u2 , u3 ∈ Q∗ < such that u = u1 au2 bu3 , u′ = u1 cu2 du3 and (a, b) − → (c, d) ∈ ∆. Let w ∈ Q∗ be such that u ⪯ w. We can write w as w = w1 aw2 bw3 with u1 ⪯ w1 , u2 ⪯ w2 and u3 ⪯ w3 . We obtain w → w′ = w1 cw2 dw3 and u′ ⪯ w′ as desired. Let U0 = Q∗ \ O−1 (b)∗ , the set of configurations which are not b-consensuses. For all i, let Ui+1 = Ui ∪ {u ∈ Q∗ | (∃v ∈ Ui )[u → v]}, the set of configurations that can reach U0 in at S most i + 1 steps. We let Di = Q∗ \ Ui . The set of b-stable configurations is D = Q∗ \ i∈N Ui . A key observation is that since our only predicate is <, all Di are subword-closed. As a consequence, so is their intersection D. Furthermore, the sequence (Di )i∈N is a descending chain of subword-closed sets. Since ⪯ is a well quasi-order, every such chain eventually stabilizes, hence there exists i ∈ N such that Di = Di+1 . We can compute Di for each index until we find one such that Di = Di+1 . Such Di is then the set of b-stable configurations. ◀ We first show that our protocols are robust to the insertion of repeated letters, under specific contexts:

(

▶ Lemma 14. In an IO-PP[<], if uwv →∗ u′ w′ v ′ with |u| = |u′ | and |v| = |v ′ |, then for all z with α(z) ⊆ α(w), there exists z ′ such that uwzwv →∗ u′ w′ z ′ w′ v ′ and α(z ′ ) ⊆ α(w′ ). Proof. We prove this for a single step, the result follows immediately by induction. Suppose < there is a step from uwv to u′ w′ v ′ , let (a, b) − → (a′ , b′ ) be the associated transition. Since the protocol is IO, we have a = a′ or b = b′ . We assume a = a′ , the other case being symmetric. If the observing agent is in u or v, then w = w′ and we can go from uwzwv to u′ w′ z ′ w′ v ′ = ′ u wzwv ′ with the same transition. If the observing agent is in w, then u = u′ , v = v ′ and, from uwzwv, we start by applying that transition for each b in z, observing the same agent labeled a as in the step from uwv to u′ w′ v ′ . We thus turn the factor z into z ′ where all b are turned into b′ . We can then apply that same transition twice to turn each of the two copies of w to w′ . Note that α(z ′ ) = (α(z) ∪ {b′ }) \ {b}, and α(w′ ) ⊇ (α(w) ∪ {b′ }) \ {b} ⊇ α(z ′ ) as w′ is obtained from w by deleting an occurrence of b and adding an occurrence of b′ . We obtain uw′ z ′ w′ v, which is equal to u′ w′ z ′ w′ v ′ (since here u = u′ and v = v ′ ) with α(z ′ ) ⊆ α(w′ ). ◀

(

▶ Lemma 15. Let L ∈ IO-PP[<]. There exists a computable m ≥ 1 such that, for all w1 , . . . , wm ∈ Σ+ and z ∈ Σ∗ with α(w1 ) = . . . = α(wm ) ⊇ α(z), we have w1 · · · wm ≡L (w1 · · · wm )z(w1 · · · wm ). Proof. Lemma 13 indicates that for both b ∈ {⊤, ⊥}, the set of b-stable configurations is subword-closed. As a consequence, writing B ε for B∪{ε}, it is a finite union of languages of the form A∗1 B1ε · · · A∗k Bkε with Ai , Bi subsets of Q, the set of states of our protocol [20, Sect. 6.1.1]. Let Kb be the maximal factorization size k over all those languages, K = max(K⊤ , K⊥ ) and

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

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⊤ , K⊥ and m. Let w1 , . . . , wm , z ∈ Σ∗ be such that α(w1 ) = · · · = α(wm ) ⊇ α(z), and let u, v ∈ Σ∗ . We show that for both b ∈ {⊤, ⊥}, if we can reach a b-stable configuration from uw1 · · · wm v then it is also possible from uw1 · · · wm zw1 · · · wm v. This implies that uw1 · · · wm v is accepted if and only if uw1 · · · wm zw1 · · · wm v is, proving the lemma. Let b ∈ {⊤, ⊥}, suppose we can reach a b-stable configuration w′ from uw1 · · · wm v. Since ′ ′ steps are length-preserving, we can divide w′ into u′ w1′ · · · wm v where u′ , v ′ and each wi′ have the same length as u, v and each wi , respectively. Since w′ is b-stable, there exists k < Kb and an expression A∗1 B1ε · · · A∗k Bkε whose language contains w′ , and only contains b-stable words. Since m > 2Kb ≥ 2k, there exist i, j such that ′ ′ ′ ′ u′ w1′ · · · wi−1 ∈ A∗1 B1ε · · · A∗j , wi+1 · · · wm v ∈ A∗j Bjε · · · Bkε , and wi′ ∈ A∗j . ∗ ′ ′ ′ ′ Since w = uw1 · · · wm v → u w1 · · · wm v = w′ , by Lemma 14 there is a partial run from w e := (uw1 · · · wi−1 )wi (wi+1 · · · wm )z(w1 · · · wi−1 )wi (wi+1 · · · wm v) to ′ ′ ′ ′ f′ := (u′ w1′ · · · wi−1 w )wi′ z ′ wi′ (wi+1 · · · wm v)

for some z ′ with α(z ′ ) ⊆ α(wi′ ), and |z ′ | = |(wi+1 · · · wm )z(w1 · · · wi−1 )|. ′ ′ ′ ′ Furthermore, since we have u′ w1′ · · · wi−1 ∈ A∗1 B1∗ · · · A∗j , and wi+1 · · · wm v ∈ A∗j Bjε · · · Bkε , f′ ∈ A∗1 B1ε · · · A∗ B ε , hence w f′ is b-stable. and z ′ ∈ α(wi′ )∗ ⊆ A∗j , we infer w k k We have shown that if there is an execution from uw1 · · · wm v to a b-stable configuration, then there is also one from uw1 · · · wm zw1 · · · wm v to a b-stable configuration, for all u, v ∈ Σ∗ and both b ∈ {⊤, ⊥}. By definition of the language of P, this means that w1 · · · wm and w1 · · · wm zw1 · · · wm are equivalent with respect to ≡L . ◀ (

▶ Lemma 17. Every IO-PP[<]-decidable language is regular. Moreover, given an IO-PP[<]protocol P, we can construct a finite automaton with the same language. Proof. We start by showing that some patterns, reminiscent of sesquipowers [24], are unavoidable in long strings. An m-reducible pattern is a word w1 · · · wm zw1 · · · wm such that α(w1 ) = · · · = α(wm ) ⊇ α(z). We have: ▷ Claim 41. For all alphabet Q of size ℓ and all m ∈ N, there exists B(ℓ, m) ∈ N such that for all w ∈ Q∗ , if |w| ≥ B(ℓ, m) then w contains an m-reducible pattern. Proof. We proceed by induction on the size ℓ of the alphabet Q. If Q is a singleton, then the result is clear with B(1, m) = 2m + 1. Otherwise, define B(ℓ, m) = mB(ℓ − 1, m)ℓmB(ℓ−1,m) . Let w ∈ Q∗ be such that |w| ≥ B(ℓ, m), let u be an infix of w of maximal length such that |α(u)| < ℓ, and let M = |u|. If M ≥ B(ℓ − 1, m), then by induction hypothesis u contains an m-reducible pattern, thus so does w. Otherwise, we can split w into r = B(ℓ, m)/B(ℓ − 1, m) = mℓmB(ℓ−1,m) factors of length B(ℓ − 1, m), plus a suffix v: w = u1 · · · ur v. Since M < B(ℓ − 1, m), by definition of M , each uk contains all letters in Q. Since r ≥ mℓmB(ℓ−1,m) , there must exist indices i, j such that i+m < j and ui · · · ui+m−1 = uj · · · uj+m−1 . As all uk contain the same set of letters, we obtain an m-reducible pattern (ui · · · ui+m−1 )(ui+m · · · uj−1 )(uj · · · uj+m−1 ). ◀

Population Protocols over Ordered Agents

By Claim 41 applied with m taken from Lemma 15, there is a bound B such that every word of length more than B is equivalent under ≡L to a shorter word. As a consequence, every word is equivalent to a word of length at most B. This means that ≡L has finitely many equivalence classes, yielding the result by the MyhillNerode theorem. To construct an automaton for this language from an IO-PP[<]-protocol, it suffices to have one state for each word of length at most B (computable by Lemma 15 and Claim 41). For each of those words w and each letter a, there is an a-transition from w to wa if it has length ≤ B. Otherwise, wa has length B + 1 and contains an m-reducible pattern. Let v be the word obtained by reducing it. The a-transition from wa goes to v. The empty word marks the initial state, and final states are those marked by words accepted by the IO-PP[<]-protocol, which can be checked by exploring the finite configuration space reachable from them using the protocol. ◀

A.4 (

Missing proofs from Section 4.2

▶ Proposition 18. The language {w ∈ Σ+ | |w|a = 1} is IO-PP[∅]-semi-decidable with stabilizing inputs. Proof. We define P = (Q, Σ, ∆, O) by Q = Σ×Σ×{⊤, ⊥}, O((σ, σ ′ , o)) = (o∧σ = σ ′ )∨((σ = a ̸= σ ′ ), and the following rules: true (σ, a, o), q − −→ (σ, σ, ⊥), q

for σ ̸= a,

true

(a, σ, o), q −−→ (a, a, ⊤), q,

(3)

true (σ, σ, o), (a, a, ⊤) − −→ (σ, σ, ⊤), (a, a, ⊤) ′

true

′

(2)

′

for σ ̸= a,

(4)

(σ, σ, o), (σ , σ , ⊥) −−→ (σ, σ, ⊥), (σ , σ , ⊥),

(5)

true

(6)

′

(a, a, o), (a, a, o ) −−→ (a, a, ⊥), (a, a, o ).

We identify a with (a, a, ⊤), and each σ ∈ Σ \ {a} with (σ, σ, ⊥). Note that P is input-saving and immediate-observation. Let us show that P decides the language of the statement with stabilizing inputs. Let u ∈ Σ+ and u ⇝∗ v. Let v = w0 → w1 → · · · be a fair run. If |v| = 1, then v is of the form (a, a, ⊤), (a, σ ′ , ⊥), (σ, a, ⊤), or (σ, σ ′ , ⊥) where σ, σ ′ ̸= a. By definition of O, the first (resp. last) two states have output ⊤ (resp. ⊥) as desired. Suppose |v| ≥ 2. By fairness and rules (2)–(3), we can assume without loss of generality that each agent has its first two components equal and immutable along the fair run. Case |ι(v)|a = 0. Since each σ = ̸ a is identified with (σ, σ, ⊥), and since an a can only disappear via rule (2), there must exist a position i and σ = ̸ a such that v[i] = (σ, σ, ⊥). By fairness and rule (5), a ⊥-consensus can be reached. From there, all rules are disabled. Case |ι(v)|a = 1. The single agent whose first component is a can set its third component to ⊤ with rule (3), and set the third component of other agents to ⊤ with rule (4). From there, all rules are disabled and hence a ⊤-stable configuration has been reached. Case |ι(v)|a ≥ 2. By fairness, rules (3) and (6) cause the third component of a-agents to alternate indefinitely between ⊤ and ⊥. ◀

A.5 (

Missing proofs from Section 5.1

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

Proof. Let φ = (∃x1 , . . . , xm )[ψ] ∈ Σint 1 [<, +, ≡] where ψ is quantifier-free. Without loss of generality, ψ may assume that 1 = x0 < x1 < · · · < xm < xm+1 = max. Indeed, For the first and last positions, we add the two extra variables with these two constraints, and replace each other occurrence of 1 and max by x0 and xm+1 ; For the ordering, we can change the formula so that it tests all orderings: _ (∃x0 , x1 , . . . , xm , xm+1 )[x1 ≤ · · · ≤ xm ∧ ψπ ], π∈Sm

where Sm is the set of permutations over [1..m], and ψπ is ψ with xi replaced by xπ(i) ; For distinctness, we can similarly enumerate all possible equivalence classes of “=” and associate a variable to each class, e.g., if we guess that x0 < x1 = x2 < x3 = x4 < x5 , then we change the subformula to (∃y0 , y1 , y2 , y3 )[ψ ′ ] where ψ ′ is the formula obtained by renaming variables in ψ as follows: x0 7→ y0 , {x1 , x2 } 7→ y1 , {x3 , x4 } 7→ y2 and x5 7→ y3 . Once variables are strictly ordered, we can further assume that each expression #a (xi , xj ) satisfies j ∈ {i, i + 1}. Indeed, if i < j, then #σ (xi , xj ) can be substituted with j−1 X

#σ (xℓ , xℓ+1 ) −

ℓ=i

j−1 X

#σ (xℓ , xℓ ).

ℓ=i+1

Let ψ ′ denote the formula ψ where each expression #σ (xi , xi+1 ) is replaced with xi,σ , and each #σ (xi , xi ) is replaced with yi,σ . Consider K = {a0 w1 a1 · · · wn am | wi ∈ Σ∗ , ai ∈ Σ, ψ ′ (xi,σ 7→ |wi |σ , yi,σ 7→ |ai |σ )}. We claim that v |= (∃x0 , . . . , xm )[ψ] iff v ∈ K. ⇒) We take ai = v[xi ] for each i ∈ [0..m], and wi = v[xi−1 + 1..xi − 1] for each i ∈ [1..m]. By the assumptions on ψ, it is the case that ψ ′ (xi,σ 7→ |wi |σ , yi,σ 7→ |ai |σ ) holds. ⇐) We have v = a0 w1 a1 w2 · · · wm am where wi ∈ Σ∗ , ai ∈ Σ and ψ ′ (xi,σ 7→ |wi |σ , yi,σ 7→ |ai |σ )} holds. By taking xi = |a0 w1 · · · ai | for i ∈ [0..m], ψ(x0 , . . . , xm ) holds. ◀ (

▶ Corollary 24. ∆int 1 [<, +, ≡] ⊆ PP[<]. int Proof. Let L ∈ ∆int 1 [<, +, ≡]. Since L ∈ Σ1 [<, +, ≡], by Proposition 23, L is PP[<]-semidecidable. As the complement of L also belongs to Σint 1 [<, +, ≡], the same applies. Thus, we are done by Lemma 6. ◀

A.6 (

Missing proofs from Section 5.2

▶ Theorem 25. A language is recognized by some poPA iff it belongs to Σint 1 [<, +, ≡]. Proof. ⇐) Let L ∈ Σint 1 [<, +, ≡]. By Lemma 22, L can be written as a finite union of languages of the form K = {a0 w1 a1 · · · wm am | wi ∈ Σ∗ , ai ∈ Σ, φ(xi,σ 7→ |wi |σ , yi,σ 7→ |ai |σ )} where m ≥ 0 and φ is a Presburger formula. Since poPA are nondeterministic, they are trivially closed under union. Thus, it suffices to give a poPA for K, which we do below. Here, each transition labeled with “σ” stands for |Σ| distinct transitions: x1,σ : σ q0

y0,σ : σ

y1,σ : σ

x2,σ : σ

xm,σ : σ

ym,σ : σ

Ψ=φ

Population Protocols over Ordered Agents

⇒) Let A be a poPA. Let K be the words of L(A) of length at most one. We can construct a formula for each word of K: ^ ^ #σ (1, max) = 0 and φa = #a (1, max) = 1 ∧ #σ (1, max) = 0. φε = σ∈Σ

σ̸=a

Let us now consider K ′ = L(A) \ K. As A is partially ordered, its language can be described as the finite union of poPA organized as straight lines alternating between self-loops and progress transitions. As we consider K ′ (and so words of length at least 2), we can explicitly read the first and last letters, which yields automata of the following form, where ai ∈ Σ and Ai ⊆ Σ: s1,σ : σ ∈ A1 q0

t0 : a0

s2,σ : σ ∈ A2

t1 : a1

sm,σ : σ ∈ Am

tm : a m

We convert such an automaton into this formula: (∃x0 , x1 , . . . , xm )[1 = x0 < x1 < · · · < xm = max] ∧ m ^ X

m ^

#ai (xi , xi ) = 1 ∧

i=0

#σ (xi−1 + 1, xi − 1) = 0 ∧ Ψ(ti 7→ 1, si,σ 7→ #σ (xi−1 + 1, xi − 1)).

i=1 σ∈Σ\Ai

◀

We are done by taking the disjunction of all formulas. (

▶ Observation 26. If weakly-unambiguous poPA are closed under complement, then any language recognized by a weakly-unambiguous poPA belongs to ∆int 1 [<, +, ≡]. Proof. First, observe that the two automata of Figure 3 for the median and coDyck-witness languages can be complemented as follows, while remaining weakly unambiguous: s: Σ t: Σ uσ : σ ∈ Σ \ {a} Ψ = (s = t ∧ (s ≡2 0 ∧

s: ⊏ t: ⊐

W uσ = 1) ∨ V σ̸=a σ̸=a

uσ = 0)

s′ : ⊏

u: a

′

s′′ : ⊏

⊏, ⊐

t′′ : ⊐

t: ⊐ ′

Ψ = (u > s + s + t + t′ ∧ s′′ + t′′ = 0) ∨ (u = s + s′ + t + t′ ∧ t + t′ ≤ s + s′ )

In general, let A and A′ be poPA with L(A′ ) = L(A). By Theorem 25, L(A), L(A′ ) ∈ Σ1 [<, +, ≡]. Thus, L(A) = L(A′ ) ∈ Π1 [<, +, ≡] and so L(A) ∈ ∆1 [<, +, ≡]. ◀

A.7 (

Missing proofs from Section 5.3

▶ Proposition 29. The language (ab)+ does not belong to Σint 1 [<, +, ≡]. Proof. To derive a contradiction, suppose that (ab)+ belongs to Σint 1 [<, +, ≡]. By Lemma 22, (ab)+ = K1 ∪ · · · ∪ Kℓ where Kj is of the form {aj,0 wj,1 aj,1 · · · wj,mj aj,mj | wj,i ∈ Σ∗ , aj,i ∈ Σ, φj (xi,σ 7→ |wj,i |σ , yi,σ 7→ |aj,i |σ )}, mj ≥ 0 and φj is a Presburger formula. Let v = (ab)n+1 where n = max(m1 , . . . , mℓ ). We have v ∈ L and so v ∈ Kj for some j ∈ [1..ℓ]. Let v = aj,0 wj,1 aj,1 · · · wj,mj aj,mj be decomposed as in Kj . By |v| = 2n + 2 > 2mj + 1

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

′ and the pigeonhole principle, there is i ∈ [1..mj ] with |wj,i | ≥ 2. Let wj,i be a word obtained ′ from wj,i by swapping two adjacent letters. Let v be obtained from v by this change. As ′ the letter counts within wj,i and wj,i are the same, we have v ′ ∈ Kj , a contradiction. ◀

A.8 (

Missing proofs from Section 6.1

▶ Lemma 32. Let L be a PP[+1]-semi-decidable language. There exists a PP[+1]-protocol P ′ semi-deciding L and such that each +1-transition of P ′ is immediate-observation. Proof. Let P = (Q, Σ, O, ∆) be a PP[+1]-protocol. We construct a new IO-PP[+1]-protocol P ′ = (Q′ , Σ, O′ , ∆′ ) semi-deciding the same language. +1 States and outputs. For each transition δ = (a, b) − −→ (c, d) in ∆, we introduce auxiliary +1 δ ack,δ ′ δ ack,δ states a and b . Formally, Q = Q ∪ { a , b | δ = (a, b) − −→ (c, d) ∈ ∆ }. The output function ignores the auxiliary markers: O′ (q) = O(q), O′ (aδ ) = O(a) and O′ (back,δ ) = O(b). +1 Transitions. The true-transitions are left unchanged. Furthermore, for each δ = (a, b) − −→ (c, d) ∈ ∆, the set ∆′ contains these four transitions: +1 δ a, b − −→ a , b +1 δ ack,δ aδ , b − −→ a , b +1 ack,δ aδ , back,δ − −→ c, b +1 c, back,δ − −→ c, d.

Each of these steps updates at most one of the two agents at a time, and hence is immediateobservation. To avoid blocking in the presence of overlapping partial simulations, we also include the following “clean-up” rules: +1 aδ , x − −→ a, x +1 y, back,δ − −→ y, d

for x ̸= back,δ , for y ̸= aδ .

Step simulation. ▷ Claim 42. If u, v ∈ Q∗ and u → v in P, then u →∗ v in P ′ . +1 Proof. This is trivial for true-transitions. Let δ = (a, b) − −→ (c, d) be the transition used ′ in P. Let u = u1 ab u2 and v = u1 cd u2 . In P , the four transitions associated with δ yield u1 ab u2 → u1 aδ b u2 → u1 aδ back,δ u2 → u1 c back,δ u2 → u1 cd u2 . ◀

Projection to P. We define a projection f : Q′∗ → Q∗ that interprets a P ′ -configuration as a P-configuration. For w = w1 · · · wn , define f (w) = w1′ · · · wn′ by: if wi ∈ Q, then wi′ = wi ; +1 if wi = aδ for some δ = (a, b) − −→ (c, d) and i < n with wi+1 = back,δ , then wi′ = c; δ if wi = a but the above condition fails, then wi′ = a; if wi = back,δ for some δ = (a, b) → (c, d), then wi′ = d. ▷ Claim 43. Let u ∈ Q∗ and v ∈ Q′∗ . If u →∗ v in P ′ , then u →∗ f (v) in P. Proof. We prove the claim by induction on the length of u →∗ v in P ′ . The only step that +1 can change the projected configuration is the acknowledgement step (aδ , b) − −→ (aδ , back,δ ), +1 in which case f precisely applies the corresponding transition δ = (a, b) −−→ (c, d) on the projected word. All other rules leave f (·) unchanged. ◀

Population Protocols over Ordered Agents

▷ Claim 44. For every v ∈ Q′∗ reachable in P ′ , it is the case that v →∗ f (v) in P ′ . Proof. Starting from v, repeatedly apply the clean-up rules to remove every pending marker aδ not followed by the matching back,δ , and then complete each matching pair aδ back,δ by the +1 +1 two remaining simulation steps (aδ , back,δ ) − ◀ −→ (c, back,δ ) −−→ (c, d). This yields f (v). We are now ready to prove the lemma. Let us show that w ∈ L(P) iff w ∈ L(P ′ ). ⇒) Let w →∗ u in P ′ . Thanks to Claim 43, we know that w →∗ f (u) in P. Since w ∈ L(P), configuration f (u) can reach a ⊤-stable configuration v in P. Hence, thanks to Claim 44 and Claim 42, we conclude that u →∗ f (u) →∗ v in P ′ . To derive a contradiction, suppose that v is not ⊤-stable in P ′ . Configuration v can reach a non-⊤-consensus v ′ in P ′ . Consider v ′ to be such a configuration reachable in a minimal number of steps. The +1 last step must be a transition of the form (aδ , back,δ ) − −→ (c, back,δ ) with O′ (c) = O(c) = ⊥, +1 ack,δ ′ or (c, b ) −−→ (c, d), with O (d) = O(d) = ⊥. Hence, f (v ′ ) is not a ⊤-consensus in P. Therefore, f (v) = v →∗ f (v ′ ) in P by Claim 43, contradicting the ⊤-stability of v in P. ⇐) Let w →∗ u in P. By Claim 42, w →∗ u in P ′ . As w ∈ L(P ′ ), configuration u can reach a ⊤-stable configuration v in P ′ . From Claim 44, we have v →∗ f (v) in P ′ . Note that f (v) is ⊤-stable in P ′ by construction. Moreover, from Claim 43, we have u →∗ f (v) in P. To derive contradiction, suppose that f (v) is not ⊤-stable in P. We have f (v) →∗ v ′ in P for some non-⊤-consensus v ′ . Thanks to Claim 42, we obtain f (v) →∗ v ′ in P ′ , contradicting the ⊤-stability of f (v) in P ′ . Hence, f (v) is ⊤-stable in P, and so w ∈ L(P). ◀ The rest of the subsection is dedicated to proving the following lemma. (

▶ Lemma 33. The language of a linear-bounded nondeterministic Turing machine is IO-PP[+1]-semi-decidable. Let us fix a linear-bounded nondeterministic Turing machine M = (P, Σ, Σ′ , δ, p0 , pacc , prej ) where P is the set of states; Σ is the input alphabet; Σ′ ⊇ Σ is the tape alphabet; δ ⊆ (P × Σ′ ) × (P × Σ′ × {◁, ▷}) is the transition relation; and p0 , pacc , prej are respectively the initial, accepting and rejecting states. Traditionally, on input w ∈ Σ, a linear-bounded automaton has access to ⊢ w ⊣; has no left-move on ⊢; has no right-move on ⊣; and cannot overwrite the endmarkers. For convenience, we consider instead that there are no endmarkers, but that the head stays put when moving left (resp. right) from the first (resp. last) cell. It is simple to construct such a machine with the same language. We further assume that M may only enter pacc with its head on the rightmost cell, and that there is no transition from pacc . Let Γ = (P ∪ {−}) × Σ′ × {fst, −, lst}. For every s = (p, a, x) ∈ Γ, let sta(s) = p and pos(s) = x. We say that a word w ∈ Γ+ , with |w| ≥ 2, is a valid configuration of M if pos(w[i]) = fst iff i = 1, pos(w[i]) = lst iff i = |w|, there is a unique position i with sta(w[i]) ∈ P . For example, w = (−, a, fst)(p, a, −)(−, b, lst) represents the configuration where M is in state p, with its head on the second cell, and its tape containing aab. ▶ Proposition 45. Let L = {w ∈ Γ≥2 | w is a valid configuration of M and it leads to acceptance}. One can construct PP[+1]-protocol that semi-decides L with stabilizing inputs. Furthermore, its true-transitions are immediate-observations.

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

Proof. Let us construct a protocol P = (Q, Γ, O, ∆). We define Q = Γ × Γ × Γ × {⊥, ⊤, §} and O((x, y, z, o)) = (x = y ∧ o = ⊤). We identify each input γ ∈ Γ with (γ, γ, γ, ⊥). Intuitively, the state (x, y, z, o) indicates that the agent has input x; has been acting as if its input was y; currently holds z; and has output belief o. Whenever x = ̸ y, the agent has changed its mind on its input, and must consequently reset the whole population. The transitions of ∆ are defined by these rules: Simulation of M +1 (1) (∗, ∗, (p, a, ∗), ∗), (∗, ∗, (−, ∗, ∗), ∗) − −→ (∗, ∗, (−, b, ∗), ∗), (∗, ∗, (q, ∗, ∗), ∗) +1 (2) (∗, ∗, (−, ∗, ∗), ∗), (∗, ∗, (p, a, ∗), ∗) − −→ (∗, ∗, (q, ∗, ∗), ∗), (∗, ∗, (−, b, ∗), ∗) true (3) (x, ∗, (p, a, ∗), ∗) − −→ (x, ∗, (q, b, ∗), ∗) true (4) (x, ∗, (p, a, ∗), ∗) − −→ (x, ∗, (q, b, ∗), ∗)

for ((p, a), (q, b, ▷)) ∈ δ for ((p, a), (q, b, ◁)) ∈ δ for ((p, a), (q, b, ▷)) ∈ δ and pos(x) = lst for ((p, a), (q, b, ◁)) ∈ δ and pos(x) = fst

Belief propagation (5) (6)

true ′ ′ (x, ∗, ∗, ∗), (x , ∗, z ′ , ∗) − −→ (x, ∗, ∗, ⊤), (x , ∗, z , ∗) +1 (∗, ∗, ∗, ⊤), (∗, ∗, ∗, ∗) − (∗, ∗, ∗, ⊤), (∗, ∗, ∗, ⊤) −→ ′

if pos(x) = fst ∧ pos(x′ ) = lst ∧ sta(z ′ ) = pacc

Reset on input changes (7) (8) (9)

true ′ ′ (x, y, ∗, ∗), (x′ , y ′ , ∗, ∗) − −→ (x, y, ∗, ∗), (x , y , ∗, §) +1 ′ ′ ′ (∗, ∗, ∗, ∗), (x′ , ∗, ∗, §) − −→ (∗, ∗, ∗, §), (x , x , x , ⊥) true § (x, ∗, ∗, ) −−→ (x, x, x, ⊥)

if pos(x′ ) = lst ∧ (x ̸= y ∨ x′ ̸= y ′ ) if pos(x) = fst

Erroneous configuration detection (10) (11) (12)

true ′ (x, ∗, ∗, ∗), (x′ , ∗, ∗, ∗) − −→ (x, ∗, ∗, ∗), (x , ∗, ∗, ⊥) true ′ (x, ∗, ∗, ∗), (x′ , ∗, ∗, ∗) − (x, ∗, ∗, ∗), (x , ∗, ∗, ⊥) −→ +1 ′ (x, ∗, ∗, ∗), (x′ , ∗, ∗, ∗) − −→ (x, ∗, ∗, ⊥), (x , ∗, ∗, ⊥)

if sta(x), sta(x′ ) ∈ P if pos(x) = pos(x′ ) ∈ {fst, lst} if pos(x) = lst ∨ pos(x′ ) = fst

Note that all true-transitions are immediate-observation. Let us show that P semi-decides L with stabilizing inputs. Let u ∈ Γn . For the special case of n = 1, note that each state starts with output ⊥ and this remains so as no transition is ever enabled. Thus, let us assume that n ≥ 2. Let u = u0 ⇝ u1 ⇝ · · · ⇝ uℓ = v, and let v = w0 → w1 → · · · be a fair run. Without loss of generality, we may assume that ℓ = 0 or ι(uℓ ) ̸= ι(uℓ−1 ). Indeed, it suffices to take ℓ as the last moment where the input changes. We make a case distinction, where each case assumes that the previous ones do not hold. Case 1: ι(v) is a valid configuration. By validity, rules (10–12) are permanently disabled from v onwards. If ℓ > 0, then there exists a position i such that v[i] = (x, y, z, o) with x ̸= y. By validity of ι(v), we have pos(ι(v)[1]) = fst and pos(ι(v)[n]) = lst. Thus, by fairness, the population must eventually use rule (7) to assign § to agent n; use rule (8) to reset the population from right to left; and use rule (9) to complete this reset with agent 1. From there, rules (7–9) are permanently disabled. Thus, by fairness, M is simulated faithfully with rules (1–4), and ⊤ eventually spreads with rules (5–6). The case of ℓ = 0 is the same except for the fact that rules (7–9) are disabled from the very beginning, where the simulation of M already begins. Case 2: ι(v) has several “fst”, “lst” or states from P ; or a wrongly placed “fst” or “lst”. Since the first component of each agent stops changing from v onwards, fairness and rules (10–12) guarantee that at least one ⊥-belief must occur infinitely often. Case 3: ℓ = 0 and ι(v) is invalid. Rule (5) is never enabled and hence no ⊤ ever appears. Case 4: ℓ > 0 and ι(v) is invalid. By assumption, there is a position i such that v[i] = (x, y, z, o) with x = ̸ y. By the latter, we have O(v[i]) = ⊥. To obtain a ⊤-consensus, agent i

Population Protocols over Ordered Agents

must be reset. This requires having at least one § in the population. To get rid of all §, rule (9) must eventually be used. If this happens, then a “fst”-agent now has belief ⊥. By assumption, this agent must be the first one. The only way to set its belief to ⊤ is by using rule (5), which is impossible by assumption on ι(v). ◀ ▶ Proposition 46. The language L(M ) is IO-PP[+1]-semi-decidable. Proof. Let K denote the set of valid initial configurations of M . Formally, let K = Γ0 Γ∗1 Γ2 where Γ0 = {p0 } × Σ × {fst}, Γ1 = {−} × Σ × {−} and Γ2 = {−} × Σ × {lst}. Let f (i) = Γi and Ui = {w ∈ {0, 1, 2}+ : |w|i = 1}. We have K = f (0∗ 1∗ 2∗ ∩ U0 ∩ U2 ). By Proposition 9, the language 0∗ 1∗ 2∗ is IO-PP[<]-semi-decidable with stabilizing inputs. Replacing “<” by “+1” in its protocol directly yields IO-PP[+1]-semi-decidability with stabilizing inputs. Thus, by Proposition 18 and by Lemmas 10 and 11, the language K is IO-PP[+1]-semi-decidable with stabilizing inputs. Let K ′ = {w ∈ Γ≥2 | w is a valid configuration of M and it leads to acceptance}. By Proposition 45, there is a PP[+1]-protocol that semi-decides K ′ with stabilizing inputs and whose true-transitions are immediate-observations. Let g((x, y, z)) = y. We have L(M ) ∩ Σ≥2 = g(K ∩ K ′ ). Thus, by Lemmas 10 and 11, the language L(M ) ∩ Σ≥2 is PP[+1]-semi-decidable. Moreover, these two lemmas preserve immediate-observation true-transitions. Hence, by Lemma 32, the language L(M ) ∩ Σ≥2 is IO-PP[+1]-semi-decidable. We can trivially show that L(M ) ∩ Σ is IO-PP[∅]-decidable. Thus, we are done by taking the union, with Lemma 7. ◀

A.9 (

Missing proofs from Section 7.1

▶ Lemma 35. The emptiness problem for PP[N ] (resp. IO-PP[N ]) reduces to deciding the complement of the syntax of PP[N ] (resp. IO-PP[N ]) deciders. Proof. Take a protocol P = (Q, Σ, O, ∆). We build a protocol P ′ such that P ′ is not a decider if and only if a ⊤-stable configuration is reachable in P. If Σ contains a letter a with opinion ⊤, then the configuration a is ⊤-stable and reachable. In that case, we set P ′ as an arbitrary protocol which is not a decider. Otherwise, we build P ′ = (Q′ , Σ, O′ , ∆′ ) from P as follows: For each initial state a ∈ Σ in P, we add another state a with opinion ⊥. We denote Σ the set of those additional states. We also add another state q⊥ with opinion ⊥. The set of initial states of P ′ is Σ. For each true a ∈ Σ and q ∈ Q′ we add a transition (a, q) − −→ (a, q). As a consequence, from every initial configuration a1 · · · ak with k ≥ 2, we can reach its counterpart in a1 · · · ak in Σ∗ . Further, for every pair of states q1 , q2 such that at least one of the two has opinion true ⊥, we add a transition (q1 , q2 ) − −→ (q1 , q⊥ ). Note that by this last transition, from every configuration of length ≥ 2 which is not a ⊤-consensus, we can reach a configuration of q⊥ ∗ . Suppose that there is a run in P from an initial configuration u = a1 · · · ak ∈ Σ+ to a ⊤-stable configuration v in P. We must have k ≥ 2 since we assumed that all a ∈ Σ have opinion ⊥. In P ′ , the configuration u = a1 · · · ak is initial, and it can reach both q⊥ k and v, respectively a ⊥ and a ⊤-stable configuration. As a result, the protocol is not a decider. Now suppose that a ⊤-stable configuration is unreachable in P. Let u be an initial configuration and let u →∗ v. Since v is not ⊤-stable, we have v →∗ w for some configuration

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

∗ w containing a state with opinion ⊥. Thus w →∗ q⊥ and the latter is a ⊥-consensus. As a result, the protocol is a decider (and recognizes the empty language). Finally, observe that if P is immediate-observation then so is P ′ . ◀

(

▶ Corollary 36. The syntax of IO-PP[+1] and PP[+1] deciders are undecidable. Proof. In Section 6, we presented an effective construction translating a linear-bounded Turing machine into an IO-PP[+1] protocol with the same language. Since emptiness is undecidable for linear-bounded Turing machines [34, Thm. 5.10], it must also be undecidable for IO-PP[+1] protocols. By Lemma 35, so is the syntax of IO-PP[+1] deciders. ◀

(

▶ Theorem 37. The emptiness problem is undecidable for PP[<]. Hence the syntax of PP[<] deciders is also undecidable. Proof. We reduce from the Post correspondence problem (PCP), which is undecidable. We are given two finite alphabets A, B, and two homomorphisms h1 , h2 : B ∗ → A∗ , and must determine whether there exists w ∈ B ∗ such that h1 (w) = h2 (w). We construct three protocols, each in charge of verifying a property of the initial word: P0 checks that the input word is in #1 A∗ #2 B ∗ #3 ; P1 checks that h1 (u) = v for a word #1 v#2 u#3 ; P2 checks that h2 (u) = v for a word #1 v#2 u#3 . For the first one, we simply use the fact that #1 A∗ #2 B ∗ #3 is in DA, and hence recognized by an (immediate-observation) protocol P0 . In particular an input word can reach a ⊤-stable configuration if and only if it is in that language. We now construct Pi for i ∈ {1, 2}. The set of states of both protocol is {a, ahead , anext | a ∈ A} ∪ B ∪ {(b, π) | b ∈ B, π prefix of h(b)} ∪ {#1 , #2 , #2 , #3 , q⊤ }. The opinion of q⊤ is ⊤, all other states have opinion ⊥. Protocol rules are as follows, for all a, c ∈ A, b, d ∈ B and prefix π of hi (b): Start <

Head head

#1 , a − → q⊤ , a < #2 , b − → #2 , (b, ε) Next (A) <

head anext , c − → q⊤ , c < next a , #2 − → q⊤ , q ⊤

head

< next , (b, π) − , (b, πa) → a if πa is a prefix of hi (b)

Next (B) < (b, hi (b)), d − → q⊤ , (d, ε) < (b, hi (b)), #3 − → q⊤ , q⊤

Our final protocol P is simply the product of those three protocols, the opinion of a triple of states being the conjunction of their opinions. This way, we can reach a ⊤-stable configuration from an initial configuration if and only if we can reach a ⊤-stable configuration from it in all three protocols. We now show that this is the case if and only if that initial configuration is of the form #1 u#2 v#3 with u = h1 (v) = h2 (v). If the initial configuration #1 h(a1 ) · · · h(ak )#2 a1 · · · ak #3 satisfies those conditions, then ∗ it is straightforward to build an execution from it to q⊤ in both P1 and P2 . Furthermore, it can reach a ⊤-stable configuration in P0 since it is in #1 A∗ #2 B ∗ #3 . Now consider an initial configuration from which we can reach a ⊤-consensus in all three protocols. By definition of P0 , it must be of the form #1 a1 · · · ak #2 b1 · · · bℓ #3 with a1 , . . . , ak ∈ A and b1 , . . . , bℓ ∈ B.

Population Protocols over Ordered Agents

Now consider protocol Pi , with i ∈ {1, 2}. We call the states {ahead , anext | a ∈ A} ∪ {#1 } special states. It is easy to see that while we do not use the last Next (A) rule, there is exactly one special state in the configuration, and there is no special state afterwards. Also observe that only letters to the right of the special state can be modified. Since all agents must reach q⊤ , this imposes that all agents that have a state in A initially must hold the special state, one by one from left to right. A symmetric argument shows that all agents with a state in B initially must transform into q⊤ using Next (B) rules, one by one, from left to right. Now let us have a look at the < Head rule: ahead , (b, π) − → anext , (b, πa). Let w be the word obtained by taking the letter a associated with each of those transitions, in the order in which they appear in the run. By the arguments above, we must have w = a1 · · · ak , and w = hi (b1 ) · · · hi (bℓ ). As a result, the input word is indeed of the form #1 hi (b1 ) · · · hi (bℓ )#2 b1 · · · bℓ #3 . As we have shown this for both i ∈ {1, 2}, we obtain that the initial configuration must be of the form #1 u#2 v#3 with u = h1 (v) = h2 (v). In conclusion, there is a reachable ⊤-stable configuration if and only if the PCP instance has a solution. ◀

A.10 (

Missing proofs from Section 7.2

▶ Theorem 39. If Conjecture 38 holds, then the syntax of IO-PP[<] deciders is decidable. Proof. Let Post(u) = {v | u → v} and Post∗ (u) = {v | u →∗ v}. Similarly, let Pre(u) = {v | v → u} and Pre∗ (u) = {v | v →∗ u}. We extend these to sets, e.g., Post∗ (L) = S ∗ w∈L Post (w). We reuse the machinery of Section 4.1, specifically Lemma 13, Lemma 15, and the combinatorial Claim 41. If a IO-PP[<] protocol P = (Q, Σ, O, ∆) is not a decider, then it is witnessed by the configuration space of words of length n for some n ≥ 2. This can be checked for each n incrementally. We only have to provide a semi-decision procedure which returns yes if and only if the protocol is a decider. Observe that assuming Conjecture 38 holds, a protocol P is a decider if and only if there exist languages K⊤ , K⊥ in DA over Q∗ such that: K⊤ and K⊥ are disjoint; Σ∗ ⊆ K⊤ ∪ K⊥ ; For both b, for all u ∈ Kb and v ∈ Post(u), it is the case that v ∈ Kb ; For both b, Kb ⊆ Pre∗ (Cb ) with Cb the set of b-stable configurations. The right-to-left direction is clear: if such invariants exist, then the protocol recognizes K⊤ ∩ Σ∗ . For the other direction, by Theorem 12, if P is a decider then its language L is in DA, hence so is Σ∗ \ L. Take K⊤ = Post∗ (L) and K⊥ = Post∗ (Σ∗ \ L). Further, assuming Conjecture 38, K⊤ and K⊥ are also in DA. They clearly satisfy all the conditions. Given P, we enumerate automata A, B⊤ , B⊥ recognizing languages in DA. We check whether: L(A) ⊆ L(B⊤ ), Σ∗ \ L(A) ⊆ L(B⊥ ); For both b, for all u ∈ L(Bb ) and v ∈ Post(u), it is the case that v ∈ L(Bb ); For both b, L(Bb ) ⊆ Pre∗ (Cb ).

M. Blondin, M. Cadilhac, B. Courchesne, L. Guillou, C. Mascle, I. Vialard

The first condition is easy to check. For the second one, we can build a non-deterministic S automaton recognizing u∈L(Bb ) Post(u), by making it guess two positions at which it applies a transition of the protocol, while checking that the resulting word is in L(Bb ). The last condition is more subtle. To check it, we argue that if there is a word in L(Bb ) \ Pre∗ (Cb ) then there is one of bounded length. It then suffices to check inclusion over words of length below this bound. First we prove a property of language of DA by a classical use of Ramsey’s theorem. ▷ Claim 47. For every language L ⊆ Q∗ in DA, there exists m ∈ N, computable from an automaton recognizing L, such that for all n ≥ m and u1 , . . . , un , z with ∅ ̸= α(u1 ) = · · · = α(un ) ⊇ α(z), we have u1 · · · un ≡L u1 · · · un zu1 · · · un . Proof. Let (M, ·, 1M ) be the syntactic monoid of L, φ : Q∗ → M a morphism and F ⊆ M such that L = φ−1 (F ). Given a sequence of words u1 , . . . , un , consider the complete undirected graph (without loops) over {0, . . . , n}, where for all i < j the edge {i, j} is colored φ(ui+1 · · · uj ). By Ramsey’s theorem [30], there exists a uniform bound m ∈ N such that whenever n ≥ m this graph contains a monochromatic 3-clique, i.e., there are i < j < k such that φ(ui+1 · · · uj ) = φ(uj+1 · · · uk ) = φ(ui+1 · · · uk ). Let u1 , . . . , un , z with n ≥ m and ∅ ̸= α(u1 ) = · · · = α(un ) ⊇ α(z), and let i < j < k be as described above. Since φ is a morphism, φ(ui+1 · · · uk ) = φ(ui+1 · · · uj )φ(uj+1 · · · uk ) = φ(ui+1 · · · uk )2 . In other words, ui+1 · · · uk ≡L (ui+1 · · · uk )2 . By Equation (1), we have ui+1 · · · uk ≡L ui+1 · · · uk (uk+1 · · · un zu1 · · · ui )ui+1 · · · uk . By appending a prefix u1 · · · ui and a suffix uk+1 · · · un to both sides of the equivalence, we obtain u1 · · · un ≡L (u1 · · · un )z(u1 · · · un ). ◁ We are now ready to show the bound on witnesses for (the negation of) the third condition. ▷ Claim 48. We can compute a bound k such that if L(Bb ) \ Pre∗ (Cb ) is non-empty then it contains a word of length at most k. Proof. Since L(Bb ) belongs to DA, we can compute m from Bb as given by Claim 47. By Lemma 13, the set of b-stable configurations is subword-closed and computable. There is therefore a computable k such that it is made of a finite union of languages described by expressions of the form A∗1 B1ϵ · · · A∗ℓ Bℓϵ with ℓ ≤ k. Let n = max(m, k). Let w be a word in L(Bb ) \ Pre∗ (Cb ) of length > B(|Σ|, n) as given by Claim 41. The word w is of the form xu1 · · · un zu1 · · · un y with ∅ ̸= α(u1 ) = · · · = α(un ) ⊇ α(z). The word w′ = xu1 · · · un y belongs to L(Bb ) since n ≥ m. It is not in Pre∗ (Cb ) since otherwise w would be in Pre∗ (Cb ), analogously to the proof of Lemma 15. ◁ In conclusion, to check the third condition we can compute the bound k given by the claim above, and check if there is a word of length at most k in L(Bb ) \ Pre∗ (Cb ). ◀

Record · ID 175206 · SHA-256 67ff71fd1004d38b
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.