# Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability

Lucie Guillou, Corto Mascle, Nicolas Waldburger

► To cite this version:

Lucie Guillou, Corto Mascle, Nicolas Waldburger. Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability. FoSSaCS 2024 - 27th International Conference on Foundations of Software Science and Computation Structures, Apr 2024, Luxembourg, Luxembourg. pp.250-270, 10.1007/978-3-031-57231-9 . hal-04569794

HAL Id: hal-04569794

https://hal.science/hal-04569794

Submitted on 6 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability*

Lucie Guillou¹, Corto Mascle², and Nicolas Waldburger³

¹ IRIF, CNRS, Université Paris Cité

² LaBRI, Université de Bordeaux

³ IRISA, Université de Rennes

**Abstract.** We consider the parameterized verification of networks of agents which communicate through unreliable broadcasts. In this model, agents have local registers whose values are unordered and initially distinct and may therefore be thought of as identifiers. When an agent broadcasts a message, it appends to the message the value stored in one of its registers. Upon reception, an agent can store the received value or test it for equality against one of its own registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We establish that this problem is decidable, although non-primitive recursive. We contrast this with the undecidability of the closely related target problem where all agents must synchronize on a given state. On the other hand, we show that the coverability problem is NP-complete when each agent only has one register.

**Keywords:** Parameterized verification · Well quasi-orders · Distributed systems

## 1 Introduction

We consider Broadcast Networks of Register Automata (BNRA), a model for networks of agents communicating by broadcasts. These systems are composed of an arbitrary number of agents whose behavior is specified with a finite automaton. This automaton is equipped with a finite set of private registers that contain values from an infinite unordered set. Initially, registers all contain distinct values, so these values can be used as identifiers. A broadcast message is composed of a symbol from a finite alphabet along with the value of one of the sender's registers. When an agent broadcasts a message, any subset of agents may receive it; this models unreliable systems with unexpected crashes and disconnections. Upon reception, an agent may store the received value or test it for equality with one of its register values. For example, an agent can check that several received messages have the same value.

<footnote>* Partly supported by ANR project PaVeDyS (ANR-23-CE48-0005).</footnote>
# Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability*

Lucie Guillou¹, Corto Mascle², and Nicolas Waldburger³

¹ IRIF, CNRS, Université Paris Cité

² LaBRI, Université de Bordeaux

³ IRISA, Université de Rennes

**Abstract.** We consider the parameterized verification of networks of agents which communicate through unreliable broadcasts. In this model, agents have local registers whose values are unordered and initially distinct and may therefore be thought of as identifiers. When an agent broadcasts a message, it appends to the message the value stored in one of its registers. Upon reception, an agent can store the received value or test it for equality against one of its own registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We establish that this problem is decidable, although non-primitive recursive. We contrast this with the undecidability of the closely related target problem where all agents must synchronize on a given state. On the other hand, we show that the coverability problem is NP-complete when each agent only has one register.

**Keywords:** Parameterized verification · Well quasi-orders · Distributed systems

## 1 Introduction

We consider Broadcast Networks of Register Automata (BNRA), a model for networks of agents communicating by broadcasts. These systems are composed of an arbitrary number of agents whose behavior is specified with a finite automaton. This automaton is equipped with a finite set of private registers that contain values from an infinite unordered set. Initially, registers all contain distinct values, so these values can be used as identifiers. A broadcast message is composed of a symbol from a finite alphabet along with the value of one of the sender's registers. When an agent broadcasts a message, any subset of agents may receive it; this models unreliable systems with unexpected crashes and disconnections. Upon reception, an agent may store the received value or test it for equality with one of its register values. For example, an agent can check that several received messages have the same value.

<footnote>* Partly supported by ANR project PaVeDyS (ANR-23-CE48-0005).</footnote>
This model was introduced in [10], as a natural extension of Reconfigurable Broadcast Networks [12]. In [10], the authors established that coverability is undecidable if the agents are allowed to send two values per message. They moreover claimed that, with one value per message, coverability was decidable and PSPACE-complete; however, the proof turned out to be incorrect [22]. As we will see, the complexity of that problem is in fact much higher.

In this paper we establish the decidability of the coverability problem and its completeness for the hyper-Ackermannian complexity class $F_{\omega^\omega}$, showing that the problem has nonprimitive recursive complexity. The lower bound comes from lossy channel systems, which consist (in their simplest version) of a finite automaton that uses an unreliable FIFO memory from which any letter may be erased at any time [3, 8, 26]. We further establish that our model lies at the frontier of decidability by showing undecidability of the target problem (where all agents must synchronize in a given state). We contrast these results with the NP-completeness of the coverability problem if each agent has only one register.

*Related work* Broadcast protocols are a widely studied class of systems in which processes are represented by nodes of a graph and can send messages to their neighbors in the graph. There are many versions depending on how one models processes, the communication graph, the shape of messages... A model with a fully connected communication graph and messages ranging over a finite alphabet was presented in [13]. When working with parameterized questions over this model (i.e., working with systems of arbitrary size), many basic problems are undecidable [14]; similar negative results were found for Ad Hoc Networks where the communication graph is fixed but arbitrary [12]. This lead the community to consider Reconfigurable Broadcast Networks (RBN) where a broadcast can be received by an arbitrary subset of agents [12].

Parameterized verification problems over RBN have been the subject of extensive study in recent years, concerning for instance reachability questions [5, 11], liveness [9] or alternative communication assumptions [4]; however, RBN have weak expressivity, in particular because agents are anonymous. In [10], RBN were extended to BNRA, the model studied in this article, by the addition of registers allowing processes to exchange identifiers.

Other approaches exist to define parameterized models with registers [6], such as dynamic register automata in which processes are allowed to spawn other processes with new identifiers and communicate integers values [1]. While basic problems on these models are in general undecidable, some restrictions on communications allow to obtain decidability [2, 20].

Parameterized verification problems often relate to the theory of well quasi-orders and the associated high complexities obtained from bounds on the length of sequences with no increasing pair (see for example [25]). In particular, our model is linked to data nets, a classical model connected to well-quasi-orders. Data nets are Petri nets in which tokens are labeled with natural numbers and can exchange and compare their labels using inequality tests [18]; in this model, the coverability problem is $F_{\omega^\omega}$-complete [15]. When one restricts data nets to only equality tests, the coverability problem becomes $F_{\omega^\omega}$-complete [21]. Data
This model was introduced in [10], as a natural extension of Reconfigurable Broadcast Networks [12]. In [10], the authors established that coverability is undecidable if the agents are allowed to send two values per message. They moreover claimed that, with one value per message, coverability was decidable and PSPACE-complete; however, the proof turned out to be incorrect [22]. As we will see, the complexity of that problem is in fact much higher.

In this paper we establish the decidability of the coverability problem and its completeness for the hyper-Ackermannian complexity class $F_{\omega^\omega}$, showing that the problem has nonprimitive recursive complexity. The lower bound comes from lossy channel systems, which consist (in their simplest version) of a finite automaton that uses an unreliable FIFO memory from which any letter may be erased at any time [3, 8, 26]. We further establish that our model lies at the frontier of decidability by showing undecidability of the target problem (where all agents must synchronize in a given state). We contrast these results with the NP-completeness of the coverability problem if each agent has only one register.

*Related work* Broadcast protocols are a widely studied class of systems in which processes are represented by nodes of a graph and can send messages to their neighbors in the graph. There are many versions depending on how one models processes, the communication graph, the shape of messages... A model with a fully connected communication graph and messages ranging over a finite alphabet was presented in [13]. When working with parameterized questions over this model (i.e., working with systems of arbitrary size), many basic problems are undecidable [14]; similar negative results were found for Ad Hoc Networks where the communication graph is fixed but arbitrary [12]. This lead the community to consider Reconfigurable Broadcast Networks (RBN) where a broadcast can be received by an arbitrary subset of agents [12].

Parameterized verification problems over RBN have been the subject of extensive study in recent years, concerning for instance reachability questions [5, 11], liveness [9] or alternative communication assumptions [4]; however, RBN have weak expressivity, in particular because agents are anonymous. In [10], RBN were extended to BNRA, the model studied in this article, by the addition of registers allowing processes to exchange identifiers.

Other approaches exist to define parameterized models with registers [6], such as dynamic register automata in which processes are allowed to spawn other processes with new identifiers and communicate integers values [1]. While basic problems on these models are in general undecidable, some restrictions on communications allow to obtain decidability [2, 20].

Parameterized verification problems often relate to the theory of well quasi-orders and the associated high complexities obtained from bounds on the length of sequences with no increasing pair (see for example [25]). In particular, our model is linked to data nets, a classical model connected to well-quasi-orders. Data nets are Petri nets in which tokens are labeled with natural numbers and can exchange and compare their labels using inequality tests [18]; in this model, the coverability problem is $F_{\omega^\omega}$-complete [15]. When one restricts data nets to only equality tests, the coverability problem becomes $F_{\omega^\omega}$-complete [21]. Data
nets with equality tests do not subsume BNRA. Indeed, in data nets, each process
can only carry one integer at a time, and problems on models of data nets where
tokens carry tuples of integers are typically undecidable [17].

*Overview* We start with the model definition and some preliminary results in Section 2. As our decidability proof is quite technical, we start by proving decidability of the coverability problem in a subcase called *signature protocols* in Section 3. We then rely on the intuitions built in that subcase to generalize the proof to the general case in Section 4. We also show the undecidability of the closely-related target problem. Finally, we prove the NP-completeness of the coverability problem for protocols with one register in Section 5. Due to space constraints, a lot of proofs, as well as some technical definitions, are only sketched in this version. Detailed proofs can be found in the appendix.

In this document, each notion is linked to its *definition* using the knowledge
package. On electronic devices, clicking on words or symbols allows to access
their definitions.

2 Preliminaries

**2.1 Definitions of the Model**

A *Broadcast Network of Register Automata* (BNRA) [10] is a model describing broadcast networks of agents with local registers. A finite transition system describes the behavior of an agent; an agent can broadcast and receive messages with integer values, store them in local registers and perform (dis)equality tests. There are arbitrarily many agents. When an agent broadcasts a message, every other agent may receive it, but does not have to do so.

**Definition 1.** A protocol with $r$ registers is a tuple $\mathcal{P} = (Q, \mathcal{M}, \Delta, q_0)$ with $Q$ a finite set of states, $q_0 \in Q$ an initial state, $\mathcal{M}$ a finite set of message types and $\Delta \subseteq Q \times \mathcal{O}_p \times Q$ a finite set of transitions, with operations $\mathcal{O}_p = \{\mathbf{br}(m, i), \mathbf{rec}(m, i, *), \mathbf{rec}(m, i, \downarrow), \mathbf{rec}(m, i, =), \mathbf{rec}(m, i, \neq) | m \in \mathcal{M}, 1 \le i \le r\}$.

Label **br** stands for broadcasts and **rec** for receptions. In a reception **rec**(m, i, α), α is its action. The set of actions is **Actions** := {=, ≠, ↓, *}, where ‘=’ is an equality test, ‘≠’ is a disequality test, ‘↓’ is a store action and ‘*’ is a dummy action with no effect. The size of **P** is |**P**| := |Q| + |**M**| + |Δ| + r.

We now define the semantics of those systems. Essentially, we have a finite
set of agents with *r* registers each; all registers initially contain distinct values. A
step consists of an agent broadcasting a message that other agents may receive.

**Definition 2 (Semantics).** Let (Q, M, Δ, q₀) be a protocol with *r* registers, and A a finite non-empty set of agents. A configuration over A is a function
nets with equality tests do not subsume BNRA. Indeed, in data nets, each process
can only carry one integer at a time, and problems on models of data nets where
tokens carry tuples of integers are typically undecidable [17].

*Overview* We start with the model definition and some preliminary results in Section 2. As our decidability proof is quite technical, we start by proving decidability of the coverability problem in a subcase called *signature protocols* in Section 3. We then rely on the intuitions built in that subcase to generalize the proof to the general case in Section 4. We also show the undecidability of the closely-related target problem. Finally, we prove the NP-completeness of the coverability problem for protocols with one register in Section 5. Due to space constraints, a lot of proofs, as well as some technical definitions, are only sketched in this version. Detailed proofs can be found in the appendix.

In this document, each notion is linked to its *definition* using the knowledge
package. On electronic devices, clicking on words or symbols allows to access
their definitions.

2 Preliminaries

2.1 Definitions of the Model

A *Broadcast Network of Register Automata* (BNRA) [10] is a model describing broadcast networks of agents with local registers. A finite transition system describes the behavior of an agent; an agent can broadcast and receive messages with integer values, store them in local registers and perform (dis)equality tests. There are arbitrarily many agents. When an agent broadcasts a message, every other agent may receive it, but does not have to do so.

**Definition 1.** A protocol with $r$ registers is a tuple $\mathcal{P} = (Q, \mathcal{M}, \Delta, q_0)$ with $Q$ a finite set of states, $q_0 \in Q$ an initial state, $\mathcal{M}$ a finite set of message types and $\Delta \subseteq Q \times \mathcal{O}_p \times Q$ a finite set of transitions, with operations $\mathcal{O}_p = \{\mathbf{br}(m, i), \mathbf{rec}(m, i, *), \mathbf{rec}(m, i, \downarrow), \mathbf{rec}(m, i, =), \mathbf{rec}(m, i, \neq) | m \in \mathcal{M}, 1 \le i \le r\}$.

Label **br** stands for broadcasts and **rec** for receptions. In a reception **rec**(m, i, α), α is its action. The set of actions is **Actions** := {=, ≠, ↓, *}, where ‘=’ is an equality test, ‘≠’ is a disequality test, ‘↓’ is a store action and ‘*’ is a dummy action with no effect. The size of **P** is |**P**| := |Q| + |**M**| + |Δ| + r.

We now define the semantics of those systems. Essentially, we have a finite
set of agents with *r* registers each; all registers initially contain distinct values. A
step consists of an agent broadcasting a message that other agents may receive.

**Definition 2 (Semantics).** Let (Q, M, Δ, q₀) be a protocol with *r* registers, and A a finite non-empty set of agents. A configuration over A is a function
<figure><img src="image_1.png" /><figcaption>Fig. 1: Example of a protocol.</figcaption></figure>

$\gamma : \mathbb{A} \to Q \times \mathbb{N}^r$ mapping each agent to its state and its register values. We write $\mathbf{st}(\gamma)$ for the state component of $\gamma$ and $\mathbf{data}(\gamma)$ for its register component.

An initial configuration $\gamma$ is one where for all $a \in \mathbb{A}$, $\mathbf{st}(\gamma)(a) = q_0$ and $\mathbf{data}(\gamma)(a, i) \neq \mathbf{data}(\gamma)(a', i')$ for all $(a, i) \neq (a', i')$.

Given a finite non-empty set of agents $\mathbb{A}$ and two configurations $\gamma, \gamma'$ over $\mathbb{A}$, a step $\gamma \to \gamma'$ is defined when there exist $m \in \mathcal{M}$, $a_0 \in \mathbb{A}$ and $i \in [1, r]$ such that $(\mathbf{st}(\gamma)(a_0), \mathbf{br}(m, i), \mathbf{st}(\gamma')(a_0)) \in \Delta$, $\mathbf{data}(\gamma)(a_0) = \mathbf{data}(\gamma')(a_0)$ and, for all $a \neq a_0$, either $\gamma'(a) = \gamma(a)$ or there exists $(\mathbf{st}(\gamma)(a), \mathbf{rec}(m, j, \alpha), \mathbf{st}(\gamma')(a)) \in \Delta$ s.t. $\mathbf{data}(\gamma')(a, j') = \mathbf{data}(\gamma)(a, j')$ for $j' \neq j$ and:

- if $\alpha = *'$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a, j)$,

- if $\alpha = \downarrow$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a_0, i)$,

- if $\alpha = ='$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a, j) = \mathbf{data}(\gamma)(a_0, i)$,

- if $\alpha = \neq$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a, j) \neq \mathbf{data}(\gamma)(a_0, i)$.

A run over $\mathbb{A}$ is a sequence of steps $\rho : \gamma_0 \to \gamma_1 \to \dots \to \gamma_k$ with $\gamma_0, \dots, \gamma_k$ configurations over $\mathbb{A}$. We write $\gamma_0 \xrightarrow{*} \gamma_k$ when there exists such a run. A run is initial when $\gamma_0$ is an initial configuration.

**Remark 3.** In our model, agents may only send one value per message. Indeed, coverability is undecidable if agents can broadcast several values at once [10].

**Example 4.** Figure 1 shows a protocol with 2 registers. Let $\mathbb{A} = \{a_1, a_2\}$. We denote by $\langle \mathbf{st}(\gamma)(a_1), \mathbf{data}(\gamma)(a_1), \mathbf{st}(\gamma)(a_2), \mathbf{data}(\gamma)(a_2) \rangle$ a configuration $\gamma$ over $\mathbb{A}$. The following sequence is an initial run:

$$ \langle q_0, (1, 2), q_0, (3, 4) \rangle \to \langle q_1, (1, 2), q_2, (1, 4) \rangle \to \langle q_3, (1, 4), q_3, (1, 4) \rangle \\ \to \langle q_4, (1, 4), q_3, (1, 4) \rangle \to \langle q_4, (1, 4), q_4, (1, 4) \rangle $$

The broadcast messages are, in this order: $(m_2, 1)$ by $a_1$, $(m_3, 4)$ by $a_2$, $(m_4, 1)$ by $a_2$ and $(m_4, 1)$ by $a_1$. In this run, each broadcast message is received by the other agent; in general, however, this does not have to be true. $\square$

**Remark 5.** From a run $\rho : \gamma_0 \xrightarrow{*} \gamma$, we can build a larger run $\rho'$ in which, for each agent $a$ of $\rho$, there are arbitrarily many extra agents in $\rho'$ that end in the same state as $a$, all with distinct register values. To obtain this, $\rho'$ make many
<figure><img src="image_2.png" /><figcaption>Fig. 1: Example of a protocol.</figcaption></figure>

$\gamma : \mathbb{A} \to Q \times \mathbb{N}^r$ mapping each agent to its state and its register values. We write $\mathbf{st}(\gamma)$ for the state component of $\gamma$ and $\mathbf{data}(\gamma)$ for its register component.

An initial configuration $\gamma$ is one where for all $a \in \mathbb{A}$, $\mathbf{st}(\gamma)(a) = q_0$ and $\mathbf{data}(\gamma)(a, i) \neq \mathbf{data}(\gamma)(a', i')$ for all $(a, i) \neq (a', i')$.

Given a finite non-empty set of agents $\mathbb{A}$ and two configurations $\gamma, \gamma'$ over $\mathbb{A}$, a step $\gamma \to \gamma'$ is defined when there exist $m \in \mathcal{M}$, $a_0 \in \mathbb{A}$ and $i \in [1, r]$ such that $(\mathbf{st}(\gamma)(a_0), \mathbf{br}(m, i), \mathbf{st}(\gamma')(a_0)) \in \Delta$, $\mathbf{data}(\gamma)(a_0) = \mathbf{data}(\gamma')(a_0)$ and, for all $a \neq a_0$, either $\gamma'(a) = \gamma(a)$ or there exists $(\mathbf{st}(\gamma)(a), \mathbf{rec}(m, j, \alpha), \mathbf{st}(\gamma')(a)) \in \Delta$ s.t. $\mathbf{data}(\gamma')(a, j') = \mathbf{data}(\gamma)(a, j')$ for $j' \neq j$ and:

- if $\alpha =*$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a, j)$,

- if $\alpha = \downarrow$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a_0, i)$,

- if $\alpha = ='$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a, j) = \mathbf{data}(\gamma)(a_0, i)$,

- if $\alpha = \neq$ then $\mathbf{data}(\gamma')(a, j) = \mathbf{data}(\gamma)(a, j) \neq \mathbf{data}(\gamma)(a_0, i)$.

A run over $\mathbb{A}$ is a sequence of steps $\rho : \gamma_0 \to \gamma_1 \to \dots \to \gamma_k$ with $\gamma_0, \dots, \gamma_k$ configurations over $\mathbb{A}$. We write $\gamma_0 \xrightarrow{*} \gamma_k$ when there exists such a run. A run is initial when $\gamma_0$ is an initial configuration.

**Remark 3.** In our model, agents may only send one value per message. Indeed, coverability is undecidable if agents can broadcast several values at once [10].

**Example 4.** Figure 1 shows a protocol with 2 registers. Let $\mathbb{A} = \{a_1, a_2\}$. We denote by $\langle \mathbf{st}(\gamma)(a_1), \mathbf{data}(\gamma)(a_1), \mathbf{st}(\gamma)(a_2), \mathbf{data}(\gamma)(a_2) \rangle$ a configuration $\gamma$ over $\mathbb{A}$. The following sequence is an initial run:

$$ \langle q_0, (1, 2), q_0, (3, 4) \rangle \to \langle q_1, (1, 2), q_2, (1, 4) \rangle \to \langle q_3, (1, 4), q_3, (1, 4) \rangle \\ \to \langle q_4, (1, 4), q_3, (1, 4) \rangle \to \langle q_4, (1, 4), q_4, (1, 4) \rangle $$

The broadcast messages are, in this order: $(m_2, 1)$ by $a_1$, $(m_3, 4)$ by $a_2$, $(m_4, 1)$ by $a_2$ and $(m_4, 1)$ by $a_1$. In this run, each broadcast message is received by the other agent; in general, however, this does not have to be true. $\square$

**Remark 5.** From a run $\rho : \gamma_0 \xrightarrow{*} \gamma$, we can build a larger run $\rho'$ in which, for each agent $a$ of $\rho$, there are arbitrarily many extra agents in $\rho'$ that end in the same state as $a$, all with distinct register values. To obtain this, $\rho'$ make many
copies of $\rho$ run in parallel on disjoint sets of agents. Because all these copies of $\rho$ do not interact with one another and because all agents start with distinct values in initial configurations, the different copies of $\rho$ have no register values in common. This property is called *copycat principle*: if state $q$ is coverable, then for all $n$ there exists an augmented run which puts $n$ agents on $q$.

**Definition 6.** The coverability problem COVER asks, given a protocol $\mathcal{P}$ and a state $q_f$, whether there is a finite non-empty set of agents $\mathcal{A}$, an initial run $\gamma_0 \stackrel{*}{\to} \gamma_f$ over $\mathcal{A}$ that covers $q_f$, i.e., there is $a \in \mathcal{A}$ such that $\text{st}(\gamma_f)(a) = q_f$.

The target problem TARGET asks, given a protocol $\mathcal{P}$ and a state $q_f$, whether there is a finite non-empty set of agents $\mathcal{A}$ and an initial run $\gamma_0 \stackrel{*}{\to} \gamma_f$ over $\mathcal{A}$ such that, for every $a \in \mathcal{A}$, $\text{st}(\gamma_f)(a) = q_f$, i.e., all agents end on $q_f$.

**Example 7.** Let $\mathcal{P}$ the protocol of Figure 1. As proven in Example 4, $(\mathcal{P}, q_4)$ is a positive instance of COVER and TARGET. However, let $\mathcal{P}'$ the protocol obtained from $\mathcal{P}$ by removing the loop on $q_4$; $(\mathcal{P}', q_4)$ becomes a negative instance of TARGET. Indeed, there must be an agent staying on $q_3$ to broadcast $m_4$. Also, $(\mathcal{P}, q_5)$ is a negative instance of COVER: we would need to be able to have one agent on $q_2$ and one agent on $q_0$ with the same value in their first registers. However, an agent in $q_0$ has performed no transition so it cannot share register values with other agents. $\square$

**Remark 8.** In [10], the authors consider the *query problem* where one looks for a run reaching a configuration satisfying some *queries*. In fact, this problem exponentially reduces to COVER hence our complexity result of $F_{\omega^\omega}$ also holds for the query problem. In the case with one register, one can even find a polynomial-time reduction hence our NP result also holds with queries.

We finally introduce *signature BNRA*, an interesting restriction of our model where register 1 is *broadcast-only* and all other registers are *reception-only*. Said otherwise, the first register acts as a permanent identifier with which agents sign their messages. An example of such a protocol is displayed in Fig. 2. Under this restriction, a message is composed of a message type along with the identifier of the sender. This restriction is relevant for pedagogical purposes: we will see that it falls into the same complexity class as the general case but makes the decidability procedure simpler.

**Definition 9 (Signature protocols).** A signature protocol with $r$ registers is a protocol $\mathcal{P} = (Q, \mathcal{M}, \Delta, q_0)$ where register 1 appears only in broadcasts in $\Delta$ and registers $i \ge 2$ appear only in receptions in $\Delta$.

## 2.2 Classical Definitions

*Fast-growing hierarchy* For $\alpha$ an ordinal in Cantor normal form, we denote by $\mathcal{F}_\alpha$ the class of functions corresponding to level $\alpha$ in the Fast-Growing Hierarchy. We denote by $\mathbf{F}_\alpha$ the associated complexity class and use the notion of $\mathbf{F}_\alpha$-completeness. All these notions are defined in [23]. We will specifically work with
copies of $\rho$ run in parallel on disjoint sets of agents. Because all these copies of $\rho$ do not interact with one another and because all agents start with distinct values in initial configurations, the different copies of $\rho$ have no register values in common. This property is called *copycat principle*: if state $q$ is coverable, then for all $n$ there exists an augmented run which puts $n$ agents on $q$.

**Definition 6.** The coverability problem COVER asks, given a protocol $\mathcal{P}$ and a state $q_f$, whether there is a finite non-empty set of agents $\mathcal{A}$, an initial run $\gamma_0 \stackrel{*}{\to} \gamma_f$ over $\mathcal{A}$ that covers $q_f$, i.e., there is $a \in \mathcal{A}$ such that $\text{st}(\gamma_f)(a) = q_f$.

The target problem TARGET asks, given a protocol $\mathcal{P}$ and a state $q_f$, whether there is there is a finite non-empty set of agents $\mathcal{A}$ and an initial run $\gamma_0 \stackrel{*}{\to} \gamma_f$ over $\mathcal{A}$ such that, for every $a \in \mathcal{A}$, $\text{st}(\gamma_f)(a) = q_f$, i.e., all agents end on $q_f$.

**Example 7.** Let $\mathcal{P}$ the protocol of Figure 1. As proven in Example 4, $(\mathcal{P}, q_4)$ is a positive instance of COVER and TARGET. However, let $\mathcal{P}'$ the protocol obtained from $\mathcal{P}$ by removing the loop on $q_4$; $(\mathcal{P}', q_4)$ becomes a negative instance of TARGET. Indeed, there must be an agent staying on $q_3$ to broadcast $m_4$. Also, $(\mathcal{P}, q_5)$ is a negative instance of COVER: we would need to be able to have one agent on $q_2$ and one agent on $q_0$ with the same value in their first registers. However, an agent in $q_0$ has performed no transition so it cannot share register values with other agents. $\square$

**Remark 8.** In [10], the authors consider the *query problem* where one looks for a run reaching a configuration satisfying some *queries*. In fact, this problem exponentially reduces to COVER hence our complexity result of $F_{\omega^\omega}$ also holds for the query problem. In the case with one register, one can even find a polynomial-time reduction hence our NP result also holds with queries.

We finally introduce *signature BNRA*, an interesting restriction of our model where register 1 is *broadcast-only* and all other registers are *reception-only*. Said otherwise, the first register acts as a permanent identifier with which agents sign their messages. An example of such a protocol is displayed in Fig. 2. Under this restriction, a message is composed of a message type along with the identifier of the sender. This restriction is relevant for pedagogical purposes: we will see that it falls into the same complexity class as the general case but makes the decidability procedure simpler.

**Definition 9 (Signature protocols).** A signature protocol with $r$ registers is a protocol $\mathcal{P} = (Q, \mathcal{M}, \Delta, q_0)$ where register 1 appears only in broadcasts in $\Delta$ and registers $i \ge 2$ appear only in receptions in $\Delta$.

## 2.2 Classical Definitions

*Fast-growing hierarchy* For $\alpha$ an ordinal in Cantor normal form, we denote by $\mathcal{F}_\alpha$ the class of functions corresponding to level $\alpha$ in the Fast-Growing Hierarchy. We denote by $\mathbf{F}_\alpha$ the associated complexity class and use the notion of $\mathbf{F}_\alpha$-completeness. All these notions are defined in [23]. We will specifically work with
complexity class $\mathbf{F}_{\omega^{\omega}}$. For readers unfamiliar with these notions, $\mathbf{F}_{\omega^{\omega}}$-complete problems are decidable but with very high complexity (non-primitive recursive, and even much higher than the Ackermann class $\mathbf{F}_{\omega}$).

We highlight that our main result is the decidability of the problem. We show that the problem lies in $\mathbf{F}_{\omega^{\omega}}$ because it does not complicate our decidability proof significantly; also, it fits nicely into the landscape of high-complexity problems arising from well quasi-orders.

*Well-quasi orders* For our decidability result, we rely on the theory of well quasi-orders in the context of subword ordering. Let $\Sigma$ be a finite alphabet, $w_1, w_2 \in \Sigma^*$, $w_1$ is a subword of $w_2$, denoted $w_1 \preceq w_2$, when $w_1$ can be obtained from $w_2$ by erasing some letters. A sequence of words $w_0, w_1, \dots$ is good if there exist $i < j$ such that $w_i \preceq w_j$, and bad otherwise. Higman's lemma [16] states that every bad sequence of words over a finite alphabet is finite, but there is no uniform bound. In order to bound the length of all bad sequences, one must bound the growth of the sequence of words. We will use the following result, known as the Length function theorem [24]:

**Theorem 10 (Length function theorem [24]).** Let $\Sigma$ a finite alphabet and $g: \mathbb{N} \to \mathbb{N}$ a primitive recursive function. There exists a function $f \in \mathcal{F}_{\omega^{|\Sigma|-1}}$ such that, for all $n \in \mathbb{N}$, every bad sequence $w_1, w_2, \dots$ such that $|w_i| \le g^{(i)}(n)$ for all $i$ has at most $f(n)$ terms (where $g^{(i)}$ denotes $g$ applied $i$ times).

## 2.3 A Complexity Lower Bound for COVER Using LCS

*Lossy channel systems (LCS)* are systems where finite-state processes communicate by sending messages from a finite alphabet through lossy FIFO channels. Unlike in the non-lossy case [7], reachability of a state is decidable for lossy channel systems [3], but has non-primitive recursive complexity [26] and is in fact $\mathbf{F}_{\omega^{\omega}}$-complete [8]. By simulating LCS using BNRA, we obtain our $\mathbf{F}_{\omega^{\omega}}$ lower bound for the coverability problem:

**Proposition 11.** COVER for signature BNRA is $\mathbf{F}_{\omega^{\omega}}$-hard.

*Proof sketch.* Given an LCS $\mathcal{L}$, we build a signature protocol $\mathcal{P}$ with two registers. Each agent starts by receiving a foreign identifier and storing it in its second register; using equality tests, it then only accepts messages with this identifier. Each agent has at most one predecessor, so the communication graph is a forest where messages propagate from roots to leaves. Each branch simulates an execution of $\mathcal{L}$. Each agent of the branch simulates a step of the execution: it receives from its predecessor a configuration of $\mathcal{L}$, chooses the next configuration of $\mathcal{L}$ and broadcasts it, sending first the location of $\mathcal{L}$ and then, letter by letter, the content of the channel. It could be that some messages are not received, hence the lossiness. The full proof can be found in Appendix A. □
complexity class $F_{\omega^\omega}$. For readers unfamiliar with these notions, $F_{\omega^\omega}$-complete problems are decidable but with very high complexity (non-primitive recursive, and even much higher than the Ackermann class $F_\omega$).

We highlight that our main result is the decidability of the problem. We show that the problem lies in $F_{\omega^\omega}$ because it does not complicate our decidability proof significantly; also, it fits nicely into the landscape of high-complexity problems arising from well quasi-orders.

*Well-quasi orders* For our decidability result, we rely on the theory of well quasi-orders in the context of subword ordering. Let $\Sigma$ be a finite alphabet, $w_1, w_2 \in \Sigma^*$, $w_1$ is a subword of $w_2$, denoted $w_1 \preceq w_2$, when $w_1$ can be obtained from $w_2$ by erasing some letters. A sequence of words $w_0, w_1, \dots$ is good if there exist $i < j$ such that $w_i \preceq w_j$, and bad otherwise. Higman's lemma [16] states that every bad sequence of words over a finite alphabet is finite, but there is no uniform bound. In order to bound the length of all bad sequences, one must bound the growth of the sequence of words. We will use the following result, known as the Length function theorem [24]:

**Theorem 10 (Length function theorem [24]).** Let $\Sigma$ a finite alphabet and $g: \mathbb{N} \to \mathbb{N}$ a primitive recursive function. There exists a function $f \in \mathcal{F}_{\omega^{|\Sigma|-1}}$ such that, for all $n \in \mathbb{N}$, every bad sequence $w_1, w_2, \dots$ such that $|w_i| \le g^{(i)}(n)$ for all $i$ has at most $f(n)$ terms (where $g^{(i)}$ denotes $g$ applied $i$ times).

## 2.3 A Complexity Lower Bound for COVER Using LCS

*Lossy channel systems (LCS)* are systems where finite-state processes communicate by sending messages from a finite alphabet through lossy FIFO channels. Unlike in the non-lossy case [7], reachability of a state is decidable for lossy channel systems [3], but has non-primitive recursive complexity [26] and is in fact $F_{\omega^\omega}$-complete [8]. By simulating LCS using BNRA, we obtain our $F_{\omega^\omega}$ lower bound for the coverability problem:

**Proposition 11.** COVER for signature BNRA is $F_{\omega^\omega}$-hard.

*Proof sketch.* Given an LCS $\mathcal{L}$, we build a signature protocol $\mathcal{P}$ with two registers. Each agent starts by receiving a foreign identifier and storing it in its second register; using equality tests, it then only accepts messages with this identifier. Each agent has at most one predecessor, so the communication graph is a forest where messages propagate from roots to leaves. Each branch simulates an execution of $\mathcal{L}$. Each agent of the branch simulates a step of the execution: it receives from its predecessor a configuration of $\mathcal{L}$, chooses the next configuration of $\mathcal{L}$ and broadcasts it, sending first the location of $\mathcal{L}$ and then, letter by letter, the content of the channel. It could be that some messages are not received, hence the lossiness. The full proof can be found in Appendix A. □
### 3 Coverability Decidability for Signature Protocols

This section and the next one are dedicated to the proof of our main result:

**Theorem 12.** *COVER for BNRA is decidable and $F_{\omega^\omega}$-complete.*

For the sake of clarity, in this section, we will first focus on the case of signature BNRA. As a preliminary, we start by defining a notion of local run meant to represent the projection of a run onto a given agent.

#### 3.1 Local runs

A *local configuration* is a pair $(q, \nu) \in Q \times \mathbb{N}^r$. An *internal step* from $(q, \nu)$ to $(q', \nu')$ with transition $\delta \in \Delta$, denoted $(q, \nu) \xrightarrow{\text{int}(\delta)} (q', \nu')$, is defined when $\nu = \nu'$ and $\delta = (q, \mathbf{br}(m, i), q')$ is a broadcast. A *reception step* from $(q, \nu)$ to $(q', \nu')$ with transition $\delta \in \Delta$ and value $v \in \mathbb{N}$, denoted $(q, \nu) \xrightarrow{\text{ext}(\delta, v)} (q', \nu')$, is defined when $\delta$ is of the form $(q, \mathbf{rec}(m, j, \alpha), q')$ with $\nu(j') = \nu'(j')$ for all $j' \neq j$ and:

- if $\alpha =*$ then $\nu(j) = \nu'(j)$, - if $\alpha ==$ then $\nu(j) = \nu'(j) = v$,

- if $\alpha = \downarrow$ then $\nu'(j) = v$, - if $\alpha = \neq$ then $\nu(j) = \nu'(j) \neq v$.

Such a reception step corresponds to receiving message $(m, v)$; in a local run, one does not specify the origin of a received message. A *local step* $(q, \nu) \to (q', \nu')$ is either a reception step or an internal step. A *local run* $u$ is a sequence of local steps denoted $(q_0, \nu_0) \stackrel{*}{\to} (q, \nu)$. Its *length* $|u|$ is its number of steps.

A value $v \in \mathbb{N}$ appearing in $u$ is *initial* if it appears in $\nu_0$ and *non-initial* otherwise. For $v \in \mathbb{N}$, the $v$-input $\text{In}_v(u)$ (resp. $v$-output $\text{Out}_v(u)$) is the sequence $m_0 \cdots m_\ell \in \mathcal{M}^*$ of message types received (resp. broadcast) with value $v$ in $u$.

#### 3.2 Unfolding Trees

We first prove decidability of COVER for signature BNRA. Note that, in signature protocols, the initial values of reception-only registers are not relevant as they can never be shared with other agents. We deduce from this idea the following informal observation:

**Observation 13** *In signature BNRA, when some agent receives a message, it can compare the value of the message only with the ones of previously received messages, i.e., check whether the sender is the same.*

If we want to turn a local run $u$ of an agent $a$ into an actual run, we must match $a$'s receptions with broadcasts. Because of Observation 13, what matters is not the actual values of the receptions in $u$ but which ones are equal to which. Therefore, for a value $v$ received in $u$, if $m_1 \dots m_k \in \mathcal{M}^*$ are the message types received in $u$ with value $v$ in this order, it means that to execute $u$, $a$ need another agent $a'$ to broadcast messages types $m_1$ to $m_k$, all with the same value. We describe what an agent needs from other agents as a set of specifications which are words of $\mathcal{M}^*$.
## 3 Coverability Decidability for Signature Protocols

This section and the next one are dedicated to the proof of our main result:

**Theorem 12.** *COVER for BNRA is decidable and $F_{\omega^\omega}$-complete.*

For the sake of clarity, in this section, we will first focus on the case of signature BNRA. As a preliminary, we start by defining a notion of local run meant to represent the projection of a run onto a given agent.

### 3.1 Local runs

A *local configuration* is a pair $(q, \nu) \in Q \times \mathbb{N}^r$. An *internal step* from $(q, \nu)$ to $(q', \nu')$ with transition $\delta \in \Delta$, denoted $(q, \nu) \xrightarrow{\text{int}(\delta)} (q', \nu')$, is defined when $\nu = \nu'$ and $\delta = (q, \mathbf{br}(m, i), q')$ is a broadcast. A *reception step* from $(q, \nu)$ to $(q', \nu')$ with transition $\delta \in \Delta$ and value $v \in \mathbb{N}$, denoted $(q, \nu) \xrightarrow{\text{ext}(\delta, v)} (q', \nu')$, is defined when $\delta$ is of the form $(q, \mathbf{rec}(m, j, \alpha), q')$ with $\nu(j') = \nu'(j')$ for all $j' \neq j$ and:

- if $\alpha =*$ then $\nu(j) = \nu'(j)$, - if $\alpha ==$ then $\nu(j) = \nu'(j) = v$,

- if $\alpha = \downarrow$ then $\nu'(j) = v$, - if $\alpha = \neq$ then $\nu(j) = \nu'(j) \neq v$.

Such a reception step corresponds to receiving message $(m, v)$; in a local run, one does not specify the origin of a received message. A *local step* $(q, \nu) \to (q', \nu')$ is either a reception step or an internal step. A *local run* $u$ is a sequence of local steps denoted $(q_0, \nu_0) \xrightarrow{*} (q, \nu)$. Its *length* $|u|$ is its number of steps.

A value $v \in \mathbb{N}$ appearing in $u$ is *initial* if it appears in $\nu_0$ and *non-initial* otherwise. For $v \in \mathbb{N}$, the $v$-input $\text{In}_v(u)$ (resp. $v$-output $\text{Out}_v(u)$) is the sequence $m_0 \cdots m_\ell \in \mathcal{M}^*$ of message types received (resp. broadcast) with value $v$ in $u$.

### 3.2 Unfolding Trees

We first prove decidability of COVER for signature BNRA. Note that, in signature protocols, the initial values of reception-only registers are not relevant as they can never be shared with other agents. We deduce from this idea the following informal observation:

**Observation 13** *In signature BNRA, when some agent receives a message, it can compare the value of the message only with the ones of previously received messages, i.e., check whether the sender is the same.*

If we want to turn a local run $u$ of an agent $a$ into an actual run, we must match $a$'s receptions with broadcasts. Because of Observation 13, what matters is not the actual values of the receptions in $u$ but which ones are equal to which. Therefore, for a value $v$ received in $u$, if $m_1 \dots m_k \in \mathcal{M}^*$ are the message types received in $u$ with value $v$ in this order, it means that to execute $u$, $a$ need another agent $a'$ to broadcast messages types $m_1$ to $m_k$, all with the same value. We describe what an agent needs from other agents as a set of specifications which are words of $\mathcal{M}^*$.
<figure><img src="image_2.png" /><figcaption>Fig. 2: Example of a signature protocol.</figcaption></figure>

To represent runs, we consider unfolding trees that abstract runs by representing such specifications, dependencies between them and how they are carried out. In this tree, each node is assigned a local run and the specification that it carries out. Because of copycat arguments, we will in fact be able to duplicate agents so that each agent only accomplishes one task, hence the tree structure.

**Definition 14.** An unfolding tree $\tau$ over $\mathcal{P}$ is a finite tree where nodes $\mu$ have three labels:

- a local run of $\mathcal{P}$, written $\mathbf{lr}(\mu)$;

- a value in $\mathbb{N}$, written $\mathbf{val}(\mu)$;

- a specification $\mathbf{spec}(\mu) \in \mathcal{M}^*$.

Moreover, all nodes $\mu$ in $\tau$ must satisfy the three following conditions:

(i) Initial values of $\mathbf{lr}(\mu)$ are never received in $\mathbf{lr}(\mu)$,

(ii) $\mathbf{spec}(\mu) \preceq \mathbf{Out}_{\mathbf{val}}(\mu)(\mathbf{lr}(\mu))$, (recall that $\preceq$ denotes the subword relation)

(iii) For each value $v$ received in $\mathbf{lr}(\mu)$, $\mu$ has a child $\mu'$ s.t. $\ln_v(\mathbf{lr}(\mu)) \preceq \mathbf{spec}(\mu')$.

Lastly, given $\tau$ an unfolding tree, we define its size by $|\tau| := \sum_{\mu \in \tau} |\mu|$ where $|\mu| := |\mathbf{lr}(\mu)| + |\mathbf{spec}(\mu)|$. Note that the size of $\tau$ takes into account the size of its nodes, so that a tree $\tau$ can be stored in space polynomial in $|\tau|$ (renaming the values appearing in $\tau$ if needed).

We explain this definition. Condition (i) enforces that the local run cannot cheat by receiving its initial values. Condition (ii) expresses that $\mathbf{lr}(\mu)$ broadcasts (at least) the messages of $\mathbf{spec}(\mu)$. We can use the subword relation $\preceq$ (instead of equality) because messages do not have to be received. Condition (iii) expresses that, for each value $v$ received in the local run $\mathbf{lr}(\mu)$, $\mu$ has a child who is able to broadcast the sequence of messages that $\mathbf{lr}(\mu)$ receives with value $v$.

**Example 15.** Figure 2 provides an example of a signature protocol. Let $\mathcal{A} = \{a_1, a_2, a_3\}$. We denote a configuration $\gamma$ by $\langle \mathbf{st}(\gamma)(a_1), (\mathbf{data}(\gamma)(a_1)), \mathbf{st}(\gamma)(a_2), (\mathbf{data}(\gamma)(a_2)), \mathbf{st}(\gamma)(a_3), (\mathbf{data}(\gamma)(a_3)) \rangle$. Irrelevant register values are denoted by $\_$. Let $\rho$ be the run over $\mathcal{A}$ of initial configuration $\langle q_0, (1, \_, \_), q_0, (2, \_, \_), q_0, (3, \_, \_\rangle$ where the following occurs:
<figure><img src="image_3.png" /><figcaption>Fig. 2: Example of a signature protocol.</figcaption></figure>

To represent runs, we consider unfolding trees that abstract runs by representing such specifications, dependencies between them and how they are carried out. In this tree, each node is assigned a local run and the specification that it carries out. Because of copycat arguments, we will in fact be able to duplicate agents so that each agent only accomplishes one task, hence the tree structure.

**Definition 14.** An unfolding tree $\tau$ over $\mathcal{P}$ is a finite tree where nodes $\mu$ have three labels:

- a local run of $\mathcal{P}$, written $\mathbf{lr}(\mu)$;

- a value in $\mathbb{N}$, written $\mathbf{val}(\mu)$;

- a specification $\mathbf{spec}(\mu) \in \mathcal{M}^*$.

Moreover, all nodes $\mu$ in $\tau$ must satisfy the three following conditions:

(i) Initial values of $\mathbf{lr}(\mu)$ are never received in $\mathbf{lr}(\mu)$,

(ii) $\mathbf{spec}(\mu) \preceq \mathbf{Out}_{\mathbf{val}}(\mu)(\mathbf{lr}(\mu))$, (recall that $\preceq$ denotes the subword relation)

(iii) For each value $v$ received in $\mathbf{lr}(\mu)$, $\mu$ has a child $\mu'$ s.t. $\ln_v(\mathbf{lr}(\mu)) \preceq \mathbf{spec}(\mu')$.

Lastly, given $\tau$ an unfolding tree, we define its size by $|\tau| := \sum_{\mu \in \tau} |\mu|$ where $|\mu| := |\mathbf{lr}(\mu)| + |\mathbf{spec}(\mu)|$. Note that the size of $\tau$ takes into account the size of its nodes, so that a tree $\tau$ can be stored in space polynomial in $|\tau|$ (renaming the values appearing in $\tau$ if needed).

We explain this definition. Condition (i) enforces that the local run cannot cheat by receiving its initial values. Condition (ii) expresses that $\mathbf{lr}(\mu)$ broadcasts (at least) the messages of $\mathbf{spec}(\mu)$. We can use the subword relation $\preceq$ (instead of equality) because messages do not have to be received. Condition (iii) expresses that, for each value $v$ received in the local run $\mathbf{lr}(\mu)$, $\mu$ has a child who is able to broadcast the sequence of messages that $\mathbf{lr}(\mu)$ receives with value $v$.

**Example 15.** Figure 2 provides an example of a signature protocol. Let $\mathcal{A} = \{a_1, a_2, a_3\}$. We denote a configuration $\gamma$ by $\langle \mathbf{st}(\gamma)(a_1), (\mathbf{data}(\gamma)(a_1)), \mathbf{st}(\gamma)(a_2), (\mathbf{data}(\gamma)(a_2)), \mathbf{st}(\gamma)(a_3), (\mathbf{data}(\gamma)(a_3)) \rangle$. Irrelevant register values are denoted by $\_$. Let $\rho$ be the run over $\mathcal{A}$ of initial configuration $\langle q_0, (1, \_, \_), q_0, (2, \_, \_), q_0, (3, \_, \_\rangle$ where the following occurs:
<figure><img src="image_3.png" /><figcaption>Fig. 3: Example of an unfolding tree derived from $\rho$. Grids correspond to local runs, a column of a grid is a local configuration. Transition $\delta_{ij}$ is the transition between state $q_i$ and state $q_j$, for example $\delta_{01} = (q_0, \text{rec}(\text{rdy}), 2, \downarrow), q_1)$. If $\delta$ is a reception of $m \in \mathcal{M}$, $\text{ext}(\delta, v)$ corresponds to receiving message $(m, v)$; if $\delta$ is a broadcast of $m \in \mathcal{M}$, $\text{int}(\delta)$ corresponds to broadcasting $(m, \text{id})$ where $\text{id}$ is the value in the first register of the agent. Initial values of reception-only registers are irrevelant and written as ‘-’. Colors correspond to message types.</figcaption></figure>

- $a_2$ broadcasts rdy, $a_1$ receives: $\langle q_1, (1, 2, -), q_0, (2, -), q_0, (3, -) \rangle$,

- $a_3$ broadcasts rdy, $a_1$ and $a_2$ receive: $\langle q_2, (1, 2, 3), q_5, (2, -), q_0, (3, -) \rangle$,

- $a_2$ broadcasts rdy, $a_3$ receives: $\langle q_2, (1, 2, 3), q_5, (2, -), q_5, (3, -) \rangle$,

- $a_2$ broadcasts go, $a_1$ receives: $\langle q_3, (1, 2, 3), q_6, (2, -), q_5, (3, -) \rangle$,

- $a_3$ broadcasts hlt, $a_1$ receives: $\langle q_4, (1, 2, 3), q_6, (2, -), q_7, (3, -) \rangle$.

Figure 3 provides an unfolding tree derived from $\rho$ by applying a procedure introduced later. Because agents $a_2$ and $a_3$ broadcast to several other agents, they each correspond to several nodes of the tree.

We explain why this tree is an unfolding tree. Condition (i) is trivially satisfied. Condition (ii) holds at every node because the local run of each node exactly broadcasts the specification of the node. Condition (iii) is satisfied at $\mu_1: \ln_2(\text{lr}(\mu_1)) = \text{rdy} \cdot \text{go} = \text{spec}(\mu_2)$ and $\ln_3(\text{lr}(\mu_1)) = \text{rdy} \cdot \text{hlt} = \text{spec}(\mu_3)$. It is also satisfied at $\mu_2, \mu_3$ and $\mu_5$ because their local runs only receive rdy and they each have a child with specification rdy. It is trivially satisfied at $\mu_4$ and $\mu_6$ as their local runs have no reception. $\square$
<figure><img src="image_4.png" /><figcaption>Fig. 3: Example of an unfolding tree derived from $\rho$. Grids correspond to local runs, a column of a grid is a local configuration. Transition $\delta_{ij}$ is the transition between state $q_i$ and state $q_j$, for example $\delta_{01} = (q_0, \text{rec}(\text{rdy}), 2, \downarrow), q_1)$. If $\delta$ is a reception of $m \in \mathcal{M}$, $\text{ext}(\delta, v)$ corresponds to receiving message $(m, v)$; if $\delta$ is a broadcast of $m \in \mathcal{M}$, $\text{int}(\delta)$ corresponds to broadcasting $(m, \text{id})$ where $\text{id}$ is the value in the first register of the agent. Initial values of reception-only registers are irrevelant and written as ‘-’. Colors correspond to message types.</figcaption></figure>

- $a_2$ broadcasts rdy, $a_1$ receives: $\langle q_1, (1, 2, -), q_0, (2, -), q_0, (3, -) \rangle$,

- $a_3$ broadcasts rdy, $a_1$ and $a_2$ receive: $\langle q_2, (1, 2, 3), q_5, (2, -), q_0, (3, -) \rangle$,

- $a_2$ broadcasts rdy, $a_3$ receives: $\langle q_2, (1, 2, 3), q_5, (2, -), q_5, (3, -) \rangle$,

- $a_2$ broadcasts go, $a_1$ receives: $\langle q_3, (1, 2, 3), q_6, (2, -), q_5, (3, -) \rangle$,

- $a_3$ broadcasts hlt, $a_1$ receives: $\langle q_4, (1, 2, 3), q_6, (2, -), q_7, (3, -) \rangle$.

Figure 3 provides an unfolding tree derived from $\rho$ by applying a procedure introduced later. Because agents $a_2$ and $a_3$ broadcast to several other agents, they each correspond to several nodes of the tree.

We explain why this tree is an unfolding tree. Condition (i) is trivially satisfied. Condition (ii) holds at every node because the local run of each node exactly broadcasts the specification of the node. Condition (iii) is satisfied at $\mu_1: \ln_2(\text{lr}(\mu_1)) = \text{rdy} \cdot \text{go} = \text{spec}(\mu_2)$ and $\ln_3(\text{lr}(\mu_1)) = \text{rdy} \cdot \text{hlt} = \text{spec}(\mu_3)$. It is also satisfied at $\mu_2, \mu_3$ and $\mu_5$ because their local runs only receive rdy and they each have a child with specification rdy. It is trivially satisfied at $\mu_4$ and $\mu_6$ as their local runs have no reception. $\square$
**Lemma 16.** Given a signature protocol $\mathcal{P}$ with a state $q_f, q_f$ is coverable in $\mathcal{P}$ if and only if there exists an unfolding tree whose root is labelled by a local run covering $q_f$. We call such an unfolding tree a coverability witness.

*Proof.* Given a run $\rho$, agent $a$ satisfies a specification $w \in \mathcal{M}^*$ in $\rho$ if the sequence of message types broadcast by $a$ admits $w$ as subword.

Let $\tau$ be a coverability witness. We prove the following property by strong induction on the depth of $\mu$: for every $\mu$ in $\tau$, there exists a run $\rho$ with an agent $a$ whose local run in $\rho$ is $\mathbf{lr}(\mu)$ and who satisfies specification $\mathbf{spec}(\mu)$. This is trivially true for leaves of $\tau$ because their local runs have no reception (by condition (iii)) hence are actual runs by themselves. Let $\mu$ a node of $\tau$, $u := \mathbf{lr}(\mu)$ and $v_1, \dots, v_c$ the values received in $u$. These values are non-initial thanks to condition (i); applying condition (iii) gives the existence of corresponding children $\mu_1, \dots, \mu_c$ in $\tau$. We apply the induction hypothesis on the subtrees rooted in $\mu_1, \dots, \mu_c$ to obtain runs $\rho_1, \dots, \rho_c$ satisfying the specifications of the children of $\mu$. Up to renaming agents, we can assume the set of agents of these runs are disjoint; up to renaming values, we can assume that $v_j = \mathbf{val}(\mu_j)$ for all $j$ and that all agents start with distinct values. We build an initial run $\rho$ whose agents is the union of the agents of the $c$ runs along with a fresh agent $a$. In $\rho$, we make $\rho_1$ to $\rho_c$ progress in parallel and make $a$ follow the local run $u$, matching each reception with value $v_j$ in $u$ with a broadcast in $\rho_j$. This is possible because, for all $j$, $\ln_{v_j}(u) \preceq \mathbf{spec}(\mu_j) \preceq \mathbf{Out}_{v_j}(\rho_j)$ (by (ii)).

Conversely, we prove the following by induction on the length of $\rho$: for every initial run $\rho$, for every agent $a$ in $\rho$ and for every $v \in \mathbb{N}$, there exists an unfolding tree whose root has as local run the projection of $\rho$ onto $a$ and as specification the $v$-output of $a$ in $\rho$. If $\rho$ is the empty run, consider the unfolding tree with a single node whose local run and specification are empty. Suppose now that $\rho$ has non-zero length, let $a$ an agent in $\rho$, $v \in \mathbb{N}$ and let $\rho_p$ the prefix run of $\rho$ of length $|\rho| - 1$. Let $\tau_1$ the unfolding tree obtained by applying the induction hypothesis to $\rho_p$, $a$ and $v$, and consider $\tau_2$ obtained by simply appending the last step of $a$ in $\rho$ to the local run at the root of $\tau_1$. If this last step is a broadcast, we obtain an unfolding tree; if the broadcast value is $v$, we append the broadcast message type to the specification at the root of $\tau_2$ and we are done. Suppose that, in the last step of $\rho$, $a$ performs a reception $(q, \mathbf{rec}(m, i, \alpha), q')$ of a message $(m, v')$. We might need to adapt $\tau_2$ to respect condition (iii) at the root. Let $a'$ the agent broadcasting in the last step of $\rho$. Let $\tau_3$ the unfolding tree obtained by applying the induction to $\rho_p$, $a'$ and $v'$. Let $\tau_4$ the unfolding tree obtained by appending the last broadcast to the local run at the root of $\tau_3$ and the corresponding message type to the specification at the root of $\tau_3$. Attaching $\tau_4$ below the root of $\tau_2$ gives an unfolding tree satisfying the desired properties. $\square$

The unfolding tree $\tau$ of Figure 3 is built from $\rho$ of Example 15 using the previous procedure. Observe that the unfolding tree $\tau$ is a coverability witness for $q_4$. However, one can find a smaller coverability witness. Indeed, in the right branch of $\tau$, $\mu_5$ and $\mu_6$ have the same specification, therefore $\mu_5$ can be deleted and replaced with $\mu_6$. More generally, we would have also been able to shorten the tree if we had $\mathbf{spec}(\mu_5) \preceq \mathbf{spec}(\mu_6)$.
**Lemma 16.** Given a signature protocol $\mathcal{P}$ with a state $q_f, q_f$ is coverable in $\mathcal{P}$ if and only if there exists an unfolding tree whose root is labelled by a local run covering $q_f$. We call such an unfolding tree a coverability witness.

*Proof.* Given a run $\rho$, agent $a$ satisfies a specification $w \in \mathcal{M}^*$ in $\rho$ if the sequence of message types broadcast by $a$ admits $w$ as subword.

Let $\tau$ be a coverability witness. We prove the following property by strong induction on the depth of $\mu$: for every $\mu$ in $\tau$, there exists a run $\rho$ with an agent $a$ whose local run in $\rho$ is $\mathbf{lr}(\mu)$ and who satisfies specification $\mathbf{spec}(\mu)$. This is trivially true for leaves of $\tau$ because their local runs have no reception (by condition (iii)) hence are actual runs by themselves. Let $\mu$ a node of $\tau$, $u := \mathbf{lr}(\mu)$ and $v_1, \dots, v_c$ the values received in $u$. These values are non-initial thanks to condition (i); applying condition (iii) gives the existence of corresponding children $\mu_1, \dots, \mu_c$ in $\tau$. We apply the induction hypothesis on the subtrees rooted in $\mu_1, \dots, \mu_c$ to obtain runs $\rho_1, \dots, \rho_c$ satisfying the specifications of the children of $\mu$. Up to renaming agents, we can assume the set of agents of these runs are disjoint; up to renaming values, we can assume that $v_j = \mathbf{val}(\mu_j)$ for all $j$ and that all agents start with distinct values. We build an initial run $\rho$ whose agents is the union of the agents of the $c$ runs along with a fresh agent $a$. In $\rho$, we make $\rho_1$ to $\rho_c$ progress in parallel and make $a$ follow the local run $u$, matching each reception with value $v_j$ in $u$ with a broadcast in $\rho_j$. This is possible because, for all $j$, $\ln_{v_j}(u) \preceq \mathbf{spec}(\mu_j) \preceq \mathbf{Out}_{v_j}(\rho_j)$ (by (ii)).

Conversely, we prove the following by induction on the length of $\rho$: for every initial run $\rho$, for every agent $a$ in $\rho$ and for every $v \in \mathbb{N}$, there exists an unfolding tree whose root has as local run the projection of $\rho$ onto $a$ and as specification the $v$-output of $a$ in $\rho$. If $\rho$ is the empty run, consider the unfolding tree with a single node whose local run and specification are empty. Suppose now that $\rho$ has non-zero length, let $a$ an agent in $\rho$, $v \in \mathbb{N}$ and let $\rho_p$ the prefix run of $\rho$ of length $|\rho| - 1$. Let $\tau_1$ the unfolding tree obtained by applying the induction hypothesis to $\rho_p$, $a$ and $v$, and consider $\tau_2$ obtained by simply appending the last step of $a$ in $\rho$ to the local run at the root of $\tau_1$. If this last step is a broadcast, we obtain an unfolding tree; if the broadcast value is $v$, we append the broadcast message type to the specification at the root of $\tau_2$ and we are done. Suppose that, in the last step of $\rho$, $a$ performs a reception $(q, \mathbf{rec}(m, i, \alpha), q')$ of a message $(m, v')$. We might need to adapt $\tau_2$ to respect condition (iii) at the root. Let $a'$ the agent broadcasting in the last step of $\rho$. Let $\tau_3$ the unfolding tree obtained by applying the induction to $\rho_p$, $a'$ and $v'$. Let $\tau_4$ the unfolding tree obtained by appending the last broadcast to the local run at the root of $\tau_3$ and the corresponding message type to the specification at the root of $\tau_3$. Attaching $\tau_4$ below the root of $\tau_2$ gives an unfolding tree satisfying the desired properties. $\square$

The unfolding tree $\tau$ of Figure 3 is built from $\rho$ of Example 15 using the previous procedure. Observe that the unfolding tree $\tau$ is a coverability witness for $q_4$. However, one can find a smaller coverability witness. Indeed, in the right branch of $\tau$, $\mu_5$ and $\mu_6$ have the same specification, therefore $\mu_5$ can be deleted and replaced with $\mu_6$. More generally, we would have also been able to shorten the tree if we had $\mathbf{spec}(\mu_5) \preceq \mathbf{spec}(\mu_6)$.
Remark 17. With the previous notion of coverability witness, the root has to
cover $q_f$ but may have an empty specification. However, we will later need the
length of the specification of a node to be equal to the number of tasks that
it must carry out. For this reason, we will, in the rest of this paper, consider
that the roots of coverability witnesses have a specification of length 1. This can
be formally achieved by introducing a new message type $m_f$ that may only be
broadcast from $q_f$ and require that, at the root, $\mathbf{spec} = m_f$.

3.3 Bounding the Size of a Coverability Witness

In all the following, we fix a positive instance $(\mathcal{P}, q_f)$ of COVER with $r+1$ registers (i.e., $r$ registers used for reception) and a coverability witness $\tau$ of minimal size. We turn the observation above into an argument that will be useful towards bounding the length of branches of a coverability witness:

**Lemma 18.** If a coverability witness $\tau$ for $(\mathcal{P}, q_f)$ of minimal size has two nodes $\mu, \mu'$ with $\mu$ a strict ancestor of $\mu'$ then $\mathbf{spec}(\mu)$ cannot be a subword of $\mathbf{spec}(\mu')$.

*Proof.* Otherwise, replacing the subtree rooted in $\mu$ with the one rooted in $\mu'$ would contradict minimality of $\tau$. $\square$

<figure><img src="image_4.png" /></figure>

We would now like to use the Length function theorem to bound the height of $\tau$, using the previous lemma. To do so, we need a bound on the size of a node with respect to its depth. The following lemma bounds the number of steps of a local run between two local configurations: we argue that if the local run is long enough we can replace it with a shorter one that can be executed using the same input. This will in turn bound the length of a local run of a node with respect to the size of its specification, which is the first step towards our goal.

**Lemma 19.** There exists a primitive recursive function $\psi$ so that, for every local
run $u : (q, v) \stackrel{*}{\to} (q', v')$, there exists $u' : (q, v) \stackrel{*}{\to} (q', v')$ with $|u'| < \psi(|\mathcal{P}|, r)$
and for all value $v' \in \mathbb{N}$, there exists $v \in \mathbb{N}$ such that $\ln_{v'}(u') \le \ln_v(u)$.

*Proof.* Let $\psi(n, 0) = n + 1$ and $\psi(n, k + 1) = 2\psi(n, k) \cdot (|\Delta|^{2\psi(n,k)} + 1) + 1$ for all $k$. Observe that $\psi(n, k)$ is a tower of exponentials of height $k$, which is primitive-recursive although non-elementary. A register $i \ge 2$ is *active* in a local run $u$ if $u$ has some `↓` action on register $i$. Let $u$ a local run, $k$ the number of active registers in $u$, $n := |\mathcal{P}|$ and $M := \psi(n, k)$. We prove by induction on the number $k$ of active registers in $u$ that if $|u| \ge \psi(n, k)$ then $u$ can be shortened.

If $k=0$, any state repetition can be removed. Suppose that $|u| > \psi(n, k+1)$
and that the set $I$ of active registers of $u$ is such that $|I| = k + 1$. If there exists
an infix run of $u$ of length $M$ with only $k$ active registers, we shorten $u$ using the
induction hypothesis. Otherwise, every sequence of $M$ steps in $u$ has a `↓` on
every register of $I$. Because $|u| > 2M (|\Delta|^{2M} + 1)$, $u$ contains at least $|\Delta|^{2M} + 1$
disjoint sequences of length $2M$ and some $s \in \Delta^{2M}$ appears twice: in infix run
$u_1$ first, then in infix run $u_2$. We build a shorter run $u'$ by removing all steps
between $u_1$ and $u_2$ and merging $u_1$ and $u_2$ (see Fig. 4). We need suitable values
Remark 17. With the previous notion of coverability witness, the root has to
cover $q_f$ but may have an empty specification. However, we will later need the
length of the specification of a node to be equal to the number of tasks that
it must carry out. For this reason, we will, in the rest of this paper, consider
that the roots of coverability witnesses have a specification of length 1. This can
be formally achieved by introducing a new message type $m_f$ that may only be
broadcast from $q_f$ and require that, at the root, $\mathbf{spec} = m_f$.

3.3 Bounding the Size of a Coverability Witness

In all the following, we fix a positive instance $(\mathcal{P}, q_f)$ of COVER with $r+1$ registers (i.e., $r$ registers used for reception) and a coverability witness $\tau$ of minimal size. We turn the observation above into an argument that will be useful towards bounding the length of branches of a coverability witness:

**Lemma 18.** If a coverability witness $\tau$ for $(\mathcal{P}, q_f)$ of minimal size has two nodes $\mu, \mu'$ with $\mu$ a strict ancestor of $\mu'$ then $\mathbf{spec}(\mu)$ cannot be a subword of $\mathbf{spec}(\mu')$.

*Proof.* Otherwise, replacing the subtree rooted in $\mu$ with the one rooted in $\mu'$ would contradict minimality of $\tau$. $\square$

We would now like to use the Length function theorem to bound the height
of $\tau$, using the previous lemma. To do so, we need a bound on the size of a node
with respect to its depth. The following lemma bounds the number of steps of a
local run between two local configurations: we argue that if the local run is long
enough we can replace it with a shorter one that can be executed using the same
input. This will in turn bound the length of a local run of a node with respect
to the size of its specification, which is the first step towards our goal.

**Lemma 19.** There exists a primitive recursive function $\psi$ so that, for every local
run $u : (q, v) \stackrel{*}{\to} (q', v')$, there exists $u' : (q, v) \stackrel{*}{\to} (q', v')$ with $|u'| < \psi(|\mathcal{P}|, r)$
and for all value $v' \in \mathbb{N}$, there exists $v \in \mathbb{N}$ such that $\ln_{v'}(u') \le \ln_v(u)$.

*Proof.* Let $\psi(n, 0) = n + 1$ and $\psi(n, k + 1) = 2\psi(n, k) \cdot (|\Delta|^{2\psi(n,k)} + 1) + 1$ for all $k$. Observe that $\psi(n, k)$ is a tower of exponentials of height $k$, which is primitive-recursive although non-elementary. A register $i \ge 2$ is *active* in a local run $u$ if $u$ has some `↓` action on register $i$. Let $u$ a local run, $k$ the number of active registers in $u$, $n := |\mathcal{P}|$ and $M := \psi(n, k)$. We prove by induction on the number $k$ of active registers in $u$ that if $|u| \ge \psi(n, k)$ then $u$ can be shortened.

If $k=0$, any state repetition can be removed. Suppose that $|u| > \psi(n, k+1)$
and that the set $I$ of active registers of $u$ is such that $|I| = k + 1$. If there exists
an infix run of $u$ of length $M$ with only $k$ active registers, we shorten $u$ using the
induction hypothesis. Otherwise, every sequence of $M$ steps in $u$ has a `↓` on
every register of $I$. Because $|u| > 2M (|\Delta|^{2M} + 1)$, $u$ contains at least $|\Delta|^{2M} + 1$
disjoint sequences of length $2M$ and some $s \in \Delta^{2M}$ appears twice: in infix run
$u_1$ first, then in infix run $u_2$. We build a shorter run $u'$ by removing all steps
between $u_1$ and $u_2$ and merging $u_1$ and $u_2$ (see Fig. 4). We need suitable values
<figure><img src="image_5.png" /><figcaption>Fig. 4: Illustration of the proof of Lemma 19.</figcaption></figure>

for the reception steps in $s$ in the shortened run $u'$. For a given register $i \in I$, we would like to pick a `↓` step on register $i$ in $s$, use values from $u_1$ before that step and values from $u_2$ after that step. This would guarantee that all equality and disequality tests still pass. However, there is an issue if a value $v$ appears in several registers in $u$. For example, if $v_1 = v_2 = v$ in Figure 4, we might interleave receptions of $v$ on registers 2 and 4: if we had a $\text{ext}(\text{rec}(m_1, 2, =), v)$ in $u_1$ and a $\text{ext}(\text{rec}(m_2, 4, =), v)$ in $u_2$, we could have $m_1$ before $m_2$ in $\ln_v(u)$ but $m_1$ after $m_2$ in $\ln_v(u')$, so that we do not have $\ln_v(u') \preceq \ln_v(u)$. We solve this issue by introducing fresh values between values of $u_1$ and values of $u_2$; because $|s| = 2M$, there is a `↓` for each register in $I$ in each half of $s$. In the shortened run $u'$, before the first `↓` on register $i$ (excluded), we use values of $u_1$, and after the last `↓` on register $i$ (included), we use values of $u_2$. For every value $v$ appearing in register $i$ between these two steps in $u_1$, we select a fresh value $v_f$ (i.e., a value that does not appear anywhere in the run) and consistently replace $v$ with $v_f$ (hatched blocks in Fig. 4). With this technique, receptions with values from $u_1$ and receptions with values from $u_2$ cannot get interleaved in $u'$. Therefore, for every value that appeared in $u$, we have $\ln_v(u') \preceq \ln_v(u)$. Also, for every fresh value $v'$ there is a value $v$ such that $\ln_{v'}(u') \preceq \ln_v(u)$. Moreover, $u'$ is shorter than $u$; we conclude by iterating this shortening procedure. $\square$

Using the previous lemma, we will bound the size of a node in $\tau$ with respect to its specification therefore with respect to its parent's size. By induction, we will then obtain a bound depending on the depth, and apply the Length function theorem to bound the height of the tree.

**Lemma 20.** For all nodes $\mu, \mu'$ in $\tau$:

1. $|\text{lr}(\mu)| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu)|$,

2. if $\mu$ is the child of $\mu'$, $|\text{spec}(\mu)| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu')|$.

*Proof.* Thanks to Remark 17, we assume that the specification at the root is of length 1. For the first item, by minimality of $\tau$, $\text{lr}(\mu)$ ends with the last broadcast
<figure><img src="image_5.png" /><figcaption>Fig. 4: Illustration of the proof of Lemma 19.</figcaption></figure>

for the reception steps in $s$ in the shortened run $u'$. For a given register $i \in I$, we would like to pick a `↓` step on register $i$ in $s$, use values from $u_1$ before that step and values from $u_2$ after that step. This would guarantee that all equality and disequality tests still pass. However, there is an issue if a value $v$ appears in several registers in $u$. For example, if $v_1 = v_2 = v$ in Figure 4, we might interleave receptions of $v$ on registers 2 and 4: if we had a $\text{ext}(\text{rec}(m_1, 2, =), v)$ in $u_1$ and a $\text{ext}(\text{rec}(m_2, 4, =), v)$ in $u_2$, we could have $m_1$ before $m_2$ in $\ln_v(u)$ but $m_1$ after $m_2$ in $\ln_v(u')$, so that we do not have $\ln_v(u') \preceq \ln_v(u)$. We solve this issue by introducing fresh values between values of $u_1$ and values of $u_2$; because $|s| = 2M$, there is a `↓` for each register in $I$ in each half of $s$. In the shortened run $u'$, before the first `↓` on register $i$ (excluded), we use values of $u_1$, and after the last `↓` on register $i$ (included), we use values of $u_2$. For every value $v$ appearing in register $i$ between these two steps in $u_1$, we select a fresh value $v_f$ (i.e., a value that does not appear anywhere in the run) and consistently replace $v$ with $v_f$ (hatched blocks in Fig. 4). With this technique, receptions with values from $u_1$ and receptions with values from $u_2$ cannot get interleaved in $u'$. Therefore, for every value that appeared in $u$, we have $\ln_v(u') \preceq \ln_v(u)$. Also, for every fresh value $v'$ there is a value $v$ such that $\ln_{v'}(u') \preceq \ln_v(u)$. Moreover, $u'$ is shorter than $u$; we conclude by iterating this shortening procedure. $\square$

Using the previous lemma, we will bound the size of a node in $\tau$ with respect to its specification therefore with respect to its parent's size. By induction, we will then obtain a bound depending on the depth, and apply the Length function theorem to bound the height of the tree.

**Lemma 20.** For all nodes $\mu, \mu'$ in $\tau$:

1. $|\mathbf{lr}(\mu)| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu)|$,

2. if $\mu$ is the child of $\mu'$, $|\text{spec}(\mu)| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu')|$.

*Proof.* Thanks to Remark 17, we assume that the specification at the root is of length 1. For the first item, by minimality of $\tau$, $\mathbf{lr}(\mu)$ ends with the last broadcast
required by spec($\mu$); we identify in $\mathbf{lr}(\mu)$ the broadcast steps witnessing spec($\mu$) and shorten the local run between these steps using Lemma 19. We thus obtain $|\mathbf{lr}(\mu)| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu)|$, proving 1. For the second item, by minimality of $\tau$, $|\text{spec}(\mu)| \le \max_{v \in \mathbb{N}} |\ln_v(\mathbf{lr}(\mu'))| \le |\mathbf{lr}(\mu')| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu')|$. $\square$

**Proposition 21.** There exists a function $f$ of class $\mathcal{F}_{\omega|\mathcal{M}|-1}$ s.t. $|\tau| \le f(|\mathcal{P}|)$.

*Proof.* Let $n := |\mathcal{P}|$, let $r+1$ be the number of registers in $\mathcal{P}$. Thanks to Lemma 18, for all $\mu \ne \mu'$ in $\tau$ with $\mu$ ancestor of $\mu'$, spec($\mu$) is not a sub-word of spec($\mu'$). Let $\mu_1, \dots, \mu_m$ the node appearing in a branch of $\tau$, from root to leaf. The sequence spec($\mu_1$), $\dots$, spec($\mu_m$) is a bad sequence. For all $i \in [1, m]$, $|\text{spec}(\mu_{i+1})| \le \psi(n, r) |\text{spec}(\mu_i)|$ by Lemma 20. By direct induction, $|\text{spec}(\mu_i)|$ is bounded by $g^{(i)}(n)$ where $g: n \mapsto n \psi(n, n)$ is a primitive recursive function. Let $h$ of class $\mathcal{F}_{\omega|\mathcal{M}|-1}$ the function obtained when applying the Length function theorem on $g$ and $\mathcal{M}$; we have $m \le h(n)$.

By immediate induction, thanks to Lemma 20.2, for every node $\mu$ at depth $d$, $|\text{spec}(\mu)| \le \psi(n, r)^{d+1}$ which, by Lemma 20.1 and because $d \le h(n)$, bounds the size of every node by $h'(n) = \psi(n, n)^{h(n)+2}$. By minimality of $\tau$, the number of children of a node is bounded by the number of values appearing in its local run hence by $h'(n)$, so the total number of nodes in $\tau$ is bounded by $h'(n)^{h(n)+1}$ and the size of $\tau$ by $f(n) := h'(n)^{h(n)+2}$. Because $\mathcal{F}_{\omega|\mathcal{M}|-1}$ is closed under composition with primitive-recursive functions, $f$ is in $\mathcal{F}_{\omega|\mathcal{M}|-1}$. $\square$

The previous argument shows that COVER for signature protocols is decidable and lies in complexity class $\mathbf{F}_{\omega\omega}$. Because the hardness from Proposition 11 holds for signature protocols, COVER is in fact complete for this complexity class.

We now extend this method to the general case.

# 4 Coverability Decidability in the General Case

## 4.1 Generalizing Unfolding Trees

In the general case, a new phenomenon appears: an agent may broadcast a value that it did not initially have but that it has received and stored. In particular, an agent starting with value $v$ could broadcast $v$ then require someone else to make a broadcast with value $v$ as well. For example, in the run described in Example 4, 1 is initially a value of $a_1$ that $a_2$ receives and rebroadcasts to $a_1$.

We now have two types of specifications. *Boss specifications* describe the task of broadcasting with one of its own initial values; this is the specification we had in signature protocols and, as before, it consists of a word $bw \in \mathcal{M}^*$ describing a sequence of message types that should be all broadcast with the same value. *Follower specifications* describe the task of broadcasting with a non-initial value received previously. More precisely, a follower specification is a pair $(fw, fm) \in \mathcal{M}^* \times \mathcal{M}$ asking to broadcast a message $(fm, v)$ under the condition of previously receiving the sequence of message types $fw$ with value $v$.
required by spec($\mu$); we identify in $\mathbf{lr}(\mu)$ the broadcast steps witnessing spec($\mu$) and shorten the local run between these steps using Lemma 19. We thus obtain $|\mathbf{lr}(\mu)| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu)|$, proving 1. For the second item, by minimality of $\tau$, $|\text{spec}(\mu)| \le \max_{v \in \mathbb{N}} |\ln_v(\mathbf{lr}(\mu'))| \le |\mathbf{lr}(\mu')| \le \psi(|\mathcal{P}|, r) |\text{spec}(\mu')|$. $\square$

**Proposition 21.** *There exists a function $f$ of class $\mathcal{F}_{\omega|\mathcal{M}|-1}$ s.t. $|\tau| \le f(|\mathcal{P}|)$.*

*Proof.* Let $n := |\mathcal{P}|$, let $r+1$ be the number of registers in $\mathcal{P}$. Thanks to Lemma 18, for all $\mu \ne \mu'$ in $\tau$ with $\mu$ ancestor of $\mu'$, spec($\mu$) is not a sub-word of spec($\mu'$). Let $\mu_1, \dots, \mu_m$ the node appearing in a branch of $\tau$, from root to leaf. The sequence spec($\mu_1$), $\dots$, spec($\mu_m$) is a bad sequence. For all $i \in [1, m]$, $|\text{spec}(\mu_{i+1})| \le \psi(n, r) |\text{spec}(\mu_i)|$ by Lemma 20. By direct induction, $|\text{spec}(\mu_i)|$ is bounded by $g^{(i)}(n)$ where $g: n \mapsto n \psi(n, n)$ is a primitive recursive function. Let $h$ of class $\mathcal{F}_{\omega|\mathcal{M}|-1}$ the function obtained when applying the Length function theorem on $g$ and $\mathcal{M}$; we have $m \le h(n)$.

By immediate induction, thanks to Lemma 20.2, for every node $\mu$ at depth $d$, $|\text{spec}(\mu)| \le \psi(n, r)^{d+1}$ which, by Lemma 20.1 and because $d \le h(n)$, bounds the size of every node by $h'(n) = \psi(n, n)^{h(n)+2}$. By minimality of $\tau$, the number of children of a node is bounded by the number of values appearing in its local run hence by $h'(n)$, so the total number of nodes in $\tau$ is bounded by $h'(n)^{h(n)+1}$ and the size of $\tau$ by $f(n) := h'(n)^{h(n)+2}$. Because $\mathcal{F}_{\omega|\mathcal{M}|-1}$ is closed under composition with primitive-recursive functions, $f$ is in $\mathcal{F}_{\omega|\mathcal{M}|-1}$. $\square$

The previous argument shows that COVER for signature protocols is decidable and lies in complexity class $\mathbf{F}_{\omega\omega}$. Because the hardness from Proposition 11 holds for signature protocols, COVER is in fact complete for this complexity class.

We now extend this method to the general case.

# 4 Coverability Decidability in the General Case

## 4.1 Generalizing Unfolding Trees

In the general case, a new phenomenon appears: an agent may broadcast a value that it did not initially have but that it has received and stored. In particular, an agent starting with value $v$ could broadcast $v$ then require someone else to make a broadcast with value $v$ as well. For example, in the run described in Example 4, 1 is initially a value of $a_1$ that $a_2$ receives and rebroadcasts to $a_1$.

We now have two types of specifications. *Boss specifications* describe the task of broadcasting with one of its own initial values; this is the specification we had in signature protocols and, as before, it consists of a word $bw \in \mathcal{M}^*$ describing a sequence of message types that should be all broadcast with the same value. *Follower specifications* describe the task of broadcasting with a non-initial value received previously. More precisely, a follower specification is a pair $(fw, fm) \in \mathcal{M}^* \times \mathcal{M}$ asking to broadcast a message $(fm, v)$ under the condition of previously receiving the sequence of message types $fw$ with value $v$.
A key idea is that, if an agent that had $v$ initially receives some message $(m, v)$, then intuitively we can isolate a subset of agents that did not have $v$ initially but that are able to broadcast $(m, v)$ after receiving a sequence of messages with that value. We can then copy them many times in the spirit of the copycat principle. Each copy receives the necessary sequence of messages in parallel, and they then provide us with an unbounded supply of messages $(m, v)$. In short, if an agent broadcasts $(m, v)$ while not having $v$ as an initial value, then we can consider that we have an unlimited supply of messages $(m, v)$.

**Example 22.** Assume that $\mathsf{A} = \{a_1, a_2, a_3\}$ and let $v$ be initial for $a_1$. Consider an execution where the broadcasts with value $v$ are: $a_1$ broadcasts $\mathbf{a} \cdot \mathbf{b}$, then $a_2$ broadcasts $\mathbf{c}$, then $a_1$ broadcasts $\mathbf{a}^3$ then $a_3$ broadcasts $\mathbf{b}$. The follower specification of $a_2$'s task would be of the form $(w, \mathbf{c})$ where $w \preceq \mathbf{a} \cdot \mathbf{b}$: $a_2$ must be able to broadcast $(c, v)$ once $\mathbf{a} \cdot \mathbf{b}$ has been broadcast with value $v$. By contrast, $a_3$'s follower specification would be of the form $(w \cdot w', \mathbf{c})$ where $w \preceq \mathbf{a} \cdot \mathbf{b}$ and $w' \in \{\mathbf{a}, \mathbf{c}\}^*$ is a subword of $\mathbf{a}^3$ enriched with as many $\mathbf{c}$ as desired, because $a_2$ may be cloned at will. For example, one could have $w = \mathbf{b}$ and $w' = \mathbf{c} \cdot \mathbf{a} \cdot \mathbf{c}^4 \cdot \mathbf{a} \cdot \mathbf{c}^2$. This idea is formalized in Appendix B with the notion of *decomposition*. Using this notion, the previous condition becomes: $w \cdot w'$ *admits decomposition* $(\mathbf{a} \cdot \mathbf{b}, \mathbf{c}, \mathbf{a}^3)$. $\square$

In our new *unfolding trees*, a node is either a *boss node* or a *follower node*, depending on its type of specification. A *boss node* with a boss specification *bw* must broadcast that sequence of message types with one of its initial values. A *follower node* $\mu$ with follower specification $(fw, fm)$ is allowed to receive sequence of messages $fw$ with value $\mathbf{val}(\mu)$ (which must be non-initial) without it being broadcast by its children. Other conditions are similar to the ones for signature protocols: if $\mu$ is a node and $v \neq \mathbf{val}(\mu)$ a non-initial value received in its local run, $\mu$ must have a boss child broadcasting this word. Moreover, for each $(m, v)$ received where $v$ is an initial value of the local run, $\mu$ must have a follower child that is able to broadcast $(m, v)$ after receiving messages sent previously with value $v$; the formal statement is more technical because it takes into account the observation of Example 22. The formal definition of *unfolding tree* is given in Appendix B.

**Example 23.** Figure 5 depicts the unfolding tree associated to $a_1$ in the run of Example 4. Follower node $\mu_3$ can have a $m_2$ reception that is not matched by its children because $m_2$ is in $fw(\mu_3)$. $\mu_1$ broadcasts $(m_2, 1)$ before receiving $(m_4, 1)$ hence the follower specification of $\mu_3$ witnesses broadcast of $(m_4, 1)$. $\square$

A *coverability witness* is again an unfolding tree whose root covers $q_f$ (or broadcasts a message $m_f$, see Remark 17), with the extra condition that the root is a boss node (a follower node implicitly relies on its parent's ability to broadcast).

**Proposition 24.** An instance of COVER ($\mathcal{P}, q_f$) is positive if and only if there exists a *coverability witness* for that instance.
A key idea is that, if an agent that had $v$ initially receives some message $(m, v)$, then intuitively we can isolate a subset of agents that did not have $v$ initially but that are able to broadcast $(m, v)$ after receiving a sequence of messages with that value. We can then copy them many times in the spirit of the copycat principle. Each copy receives the necessary sequence of messages in parallel, and they then provide us with an unbounded supply of messages $(m, v)$. In short, if an agent broadcasts $(m, v)$ while not having $v$ as an initial value, then we can consider that we have an unlimited supply of messages $(m, v)$.

**Example 22.** Assume that $\mathsf{A} = \{a_1, a_2, a_3\}$ and let $v$ be initial for $a_1$. Consider an execution where the broadcasts with value $v$ are: $a_1$ broadcasts $\mathbf{a} \cdot \mathbf{b}$, then $a_2$ broadcasts $\mathbf{c}$, then $a_1$ broadcasts $\mathbf{a}^3$ then $a_3$ broadcasts $\mathbf{b}$. The follower specification of $a_2$'s task would be of the form $(w, \mathbf{c})$ where $w \preceq \mathbf{a} \cdot \mathbf{b}$: $a_2$ must be able to broadcast $(c, v)$ once $\mathbf{a} \cdot \mathbf{b}$ has been broadcast with value $v$. By contrast, $a_3$'s follower specification would be of the form $(w \cdot w', \mathbf{c})$ where $w \preceq \mathbf{a} \cdot \mathbf{b}$ and $w' \in \{\mathbf{a}, \mathbf{c}\}^*$ is a subword of $\mathbf{a}^3$ enriched with as many $\mathbf{c}$ as desired, because $a_2$ may be cloned at will. For example, one could have $w = \mathbf{b}$ and $w' = \mathbf{c} \cdot \mathbf{a} \cdot \mathbf{c}^4 \cdot \mathbf{a} \cdot \mathbf{c}^2$. This idea is formalized in Appendix B with the notion of *decomposition*. Using this notion, the previous condition becomes: $w \cdot w'$ *admits decomposition* $(\mathbf{a} \cdot \mathbf{b}, \mathbf{c}, \mathbf{a}^3)$. $\square$

In our new *unfolding trees*, a node is either a *boss node* or a *follower node*, depending on its type of specification. A *boss node* with a boss specification *bw* must broadcast that sequence of message types with one of its initial values. A *follower node* $\mu$ with follower specification (*fw*, *fm*) is allowed to receive sequence of messages *fw* with value *val*($\mu$) (which must be non-initial) without it being broadcast by its children. Other conditions are similar to the ones for signature protocols: if $\mu$ is a node and $v \neq \text{val}(\mu)$ a non-initial value received in its local run, $\mu$ must have a boss child broadcasting this word. Moreover, for each $(m, v)$ received where $v$ is an initial value of the local run, $\mu$ must have a follower child that is able to broadcast $(m, v)$ after receiving messages sent previously with value $v$; the formal statement is more technical because it takes into account the observation of Example 22. The formal definition of *unfolding tree* is given in Appendix B.

**Example 23.** Figure 5 depicts the unfolding tree associated to $a_1$ in the run of Example 4. Follower node $\mu_3$ can have a $m_2$ reception that is not matched by its children because $m_2$ is in $\text{fw}(\mu_3)$. $\mu_1$ broadcasts $(m_2, 1)$ before receiving $(m_4, 1)$ hence the follower specification of $\mu_3$ witnesses broadcast of $(m_4, 1)$. $\square$

A *coverability witness* is again an unfolding tree whose root covers $q_f$ (or broadcasts a message $m_f$, see Remark 17), with the extra condition that the root is a boss node (a follower node implicitly relies on its parent's ability to broadcast).

**Proposition 24.** An instance of COVER ($\mathcal{P}$, $q_f$) is positive if and only if there exists a *coverability witness* for that instance.
<figure><img src="image_6.png" /><figcaption>Fig. 5: Example of an unfolding tree. $\delta_{ri}$ (resp. $\delta_{bi}$) denotes the reception (resp. broadcast) transition of message $m_i$ in the protocol described in Fig. 1. Values that are never broadcast are omitted and written as ‘.’.</figcaption></figure>

*Proof sketch.* The proof is quite similar to the one of Lemma 16, but is made more technical by the addition of follower nodes. When translating an unfolding tree to a run, if the root of the tree is a follower node $\mu$ of specification $(fw, fm)$, then we actually obtain a *partial run*, i.e., a run except that the receptions from $fw$ are not matched by broadcasts in the run. We then combine this partial run with the run corresponding to the parent of $\mu$ and with the runs of other children of $\mu$ so that every reception is matched with a broadcast. For the translation from run to tree, we inductively construct the tree by extracting from the run the agents and values responsible for satisfying the specifications of each node and analyzing the messages they receive to determine their set of children (as in Example 22). See Appendix C for the proof. $\square$

**Bounding the Size of the Unfolding Tree.** Our aim is again to bound the size of a minimal coverability witness. In the following, we fix an instance $(\mathcal{P}, q_f)$ with $r$ registers and a coverability witness of minimal size. We start by providing new conditions under which a branch can be shortened; for boss specifications, it is the condition of Lemma 18 but for follower specifications, the subword relation goes the opposite direction because the shorter the requirement $fw$, the better. Details can be found in Appendix D.

**Lemma 25.** Let $\mu \neq \mu'$ be two nodes of $\tau$ such that $\mu$ is an ancestor of $\mu'$. If one of those conditions holds, then $\tau$ can be shortened (contradicting its minimality):

- $\mu$ and $\mu'$ are boss nodes with boss specifications respectively $bw$ and $bw'$, and $bw \preceq bw'$;

- $\mu$ and $\mu'$ are follower nodes with follower specifications respectively $(fw, fm)$ and $(fw', fm')$, and $fw' \preceq fw$ and $fm' = fm$.

We can generalize Lemma 19 to bound the size of a node by the number of messages that it must broadcast times a primitive-recursive function $\psi(|\mathcal{P}|, r)$.
<figure><img src="image_6.png" /><figcaption>Fig. 5: Example of an unfolding tree. $\delta_{ri}$ (resp. $\delta_{bi}$) denotes the reception (resp. broadcast) transition of message $m_i$ in the protocol described in Fig. 1. Values that are never broadcast are omitted and written as '$\bot$'.</figcaption></figure>

*Proof sketch.* The proof is quite similar to the one of Lemma 16, but is made more technical by the addition of follower nodes. When translating an unfolding tree to a run, if the root of the tree is a follower node $\mu$ of specification $(fw, fm)$, then we actually obtain a *partial run*, i.e., a run except that the receptions from $fw$ are not matched by broadcasts in the run. We then combine this partial run with the run corresponding to the parent of $\mu$ and with the runs of other children of $\mu$ so that every reception is matched with a broadcast. For the translation from run to tree, we inductively construct the tree by extracting from the run the agents and values responsible for satisfying the specifications of each node and analyzing the messages they receive to determine their set of children (as in Example 22). See Appendix C for the proof. $\square$

**Bounding the Size of the Unfolding Tree.** Our aim is again to bound the size of a minimal coverability witness. In the following, we fix an instance $(\mathcal{P}, q_f)$ with $r$ registers and a coverability witness of minimal size. We start by providing new conditions under which a branch can be shortened; for boss specifications, it is the condition of Lemma 18 but for follower specifications, the subword relation goes the opposite direction because the shorter the requirement $fw$, the better. Details can be found in Appendix D.

**Lemma 25.** Let $\mu \neq \mu'$ be two nodes of $\tau$ such that $\mu$ is an ancestor of $\mu'$. If one of those conditions holds, then $\tau$ can be shortened (contradicting its minimality):

- $\mu$ and $\mu'$ are boss nodes with boss specifications respectively $bw$ and $bw'$, and $bw \preceq bw'$;

- $\mu$ and $\mu'$ are follower nodes with follower specifications respectively $(fw, fm)$ and $(fw', fm')$, and $fw' \preceq fw$ and $fm' = fm$.

We can generalize Lemma 19 to bound the size of a node by the number of messages that it must broadcast times a primitive-recursive function $\psi(|\mathcal{P}|, r)$.
<figure><img src="image_7.png" /><figcaption>Fig. 6: Rearrangement of a tree. The root is in red, black solid arrows connect parents to children, blue dashed arrows highlight that long words of messages are sent upwards.</figcaption></figure>

The proof is more technical than the one of Lemma 19 but the idea is essentially the same. The formal statement is given below., and the proof can be found in Appendix E. One can therefore bound the size of a node with respect to the size of the nodes that it must broadcast to.

**Lemma 26.** There exists a primitive recursive function $\psi$ such that, for every protocol $\mathcal{P}$ with $r$ registers, for all local runs $u_0 : (q_0, v_0) \stackrel{*}{\to} (q, v)$, $u : (q, v) \stackrel{*}{\to} (q', v')$, $u_f : (q', v') \stackrel{*}{\to} (q_f, v_f)$, there exists a local run $u' : (q, v) \stackrel{*}{\to} (q', v')$ with $|u'| \le \psi(|\mathcal{P}|, r)$ and for all $v' \in \mathbb{N}$:

1. if $v'$ appears in $u_0$, $u$, or $u_f$, $\ln_{v'}(u') \le \ln_{v'}(u)$,

2. otherwise, there exists $v \in \mathbb{N}$, not initial in $u_0$, such that $\ln_{v'}(u') \le \ln_v(u)$.

It is however now much harder than in the signature case to bound the size of the coverability witness. Indeed, the broadcasts no longer go only from children to parents in the unfolding tree. If $\mu_p$ is the parent of $\mu_c$, then $\mu_c$ broadcasts to $\mu_p$ if $\mu_c$ is a boss node, but $\mu_p$ broadcasts to $\mu_c$ if $\mu_c$ is a follower node, in which case $\mu_c$ only broadcasts one message to $\mu_p$. Therefore, we cannot in general bound $|\mu_p|$ with respect to $|\mu_c|$ nor $|\mu_c|$ with respect to $|\mu_p|$, making us unable to apply the Length function theorem immediately.

This leads us to arrange the unfolding tree so that long broadcast sequences are sent upwards, using the notion of altitude depicted in Figure 6, formally defined as follows. The *altitude* of the root is 0, the altitude of a boss node is the altitude of its parent minus one, and the altitude of a follower node is the altitude of its parent plus one. We denote the altitude of $\mu$ by $\text{alt}(\mu)$. This way the nodes of maximal altitude are the ones that do not need to send long sequences of messages. We will bound the size of nodes with respect to their altitude, from the highest to the lowest, and then use the Length function theorem to bound the maximal and minimal altitudes. We present here a sketch of the proof. ; details are postponed to Appendix F.
<figure><img src="image_7.png" /><figcaption>Fig. 6: Rearrangement of a tree. The root is in red, black solid arrows connect parents to children, blue dashed arrows highlight that long words of messages are sent upwards.</figcaption></figure>

The proof is more technical than the one of Lemma 19 but the idea is essentially the same. The formal statement is given below, and the proof can be found in Appendix E. One can therefore bound the size of a node with respect to the size of the nodes that it must broadcast to.

**Lemma 26.** There exists a primitive recursive function $\psi$ such that, for every protocol $\mathcal{P}$ with $r$ registers, for all local runs $u_0 : (q_0, v_0) \stackrel{*}{\to} (q, v)$, $u : (q, v) \stackrel{*}{\to} (q', v')$, $u_f : (q', v') \stackrel{*}{\to} (q_f, v_f)$, there exists a local run $u' : (q, v) \stackrel{*}{\to} (q', v')$ with $|u'| \le \psi(|\mathcal{P}|, r)$ and for all $v' \in \mathbb{N}$:

1. if $v'$ appears in $u_0$, $u$, or $u_f$, $\ln_{v'}(u') \le \ln_{v'}(u)$,

2. otherwise, there exists $v \in \mathbb{N}$, not initial in $u_0$, such that $\ln_{v'}(u') \le \ln_v(u)$.

It is however now much harder than in the signature case to bound the size of the coverability witness. Indeed, the broadcasts no longer go only from children to parents in the unfolding tree. If $\mu_p$ is the parent of $\mu_c$, then $\mu_c$ broadcasts to $\mu_p$ if $\mu_c$ is a boss node, but $\mu_p$ broadcasts to $\mu_c$ if $\mu_c$ is a follower node, in which case $\mu_c$ only broadcasts one message to $\mu_p$. Therefore, we cannot in general bound $|\mu_p|$ with respect to $|\mu_c|$ nor $|\mu_c|$ with respect to $|\mu_p|$, making us unable to apply the Length function theorem immediately.

This leads us to arrange the unfolding tree so that long broadcast sequences are sent upwards, using the notion of altitude depicted in Figure 6, formally defined as follows. The *altitude* of the root is 0, the altitude of a boss node is the altitude of its parent minus one, and the altitude of a follower node is the altitude of its parent plus one. We denote the altitude of $\mu$ by $\text{alt}(\mu)$. This way the nodes of maximal altitude are the ones that do not need to send long sequences of messages. We will bound the size of nodes with respect to their altitude, from the highest to the lowest, and then use the Length function theorem to bound the maximal and minimal altitudes. We present here a sketch of the proof. ; details are postponed to Appendix F.
Let **altmax** ≥ 0 (resp. **altmin** ≤ 0) denote the maximum (resp. minimum) altitude in τ. We first bound the size of a node with respect to the difference between its altitude and **altmax**.

**Lemma 27.** *There is a primitive recursive function $f_0$ such that, for every node $\mu$ of $\tau$, $|\mu| \le f_0(|P| + \text{altmax} - \text{alt}(\mu))$.*

*Proof sketch.* We proceed by induction on the altitude, from highest to lowest. A node of maximal altitude has at most one message to broadcast (a follower node must broadcast one message to its parent), so its size is bounded by $\psi(|P|, r)$ by Lemma 26 (applying the Lemma to its local run minus its final step, i.e., the step making the broadcast to its parent). Let $\mu$ be a node of $\tau$ whose neighbors of higher altitude have size bounded by $K$. We claim that $|\mu| \le (\psi(|P|, r) + 2)(|M|rK + K)$, with $\psi$ the primitive-recursive function defined in Lemma 26. The idea is similar to the one for Lemma 20. The neighbors of higher altitude are the nodes which require sequences of messages from $\mu$. Their size bounds the number of messages that $\mu$ needs to send; we then apply Lemma 26 to bound the size of the local run of $\mu$. Lemma 37 in the appendix details these ideas. We finally obtain $f_0$ by iteratively applying the inequality above. □

We now bound **altmax** and **altmin**:

**Lemma 28.** **altmax and $|altmin|$ are bounded by a function of class $\mathcal{F}_{\omega|M|}$**.

*Proof sketch.* We first bound **altmax**. Consider a branch of $\tau$ that has a node at altitude **altmax**. We follow this branch from the root to a node of altitude **altmax**: for every $j \in [1, \text{altmax}]$, let $\mu_j$ be the first node of the branch that has altitude $j$. All such nodes are necessarily follower nodes as they are above their parent. Sequence $\mu_{\text{altmax}}, \dots, \mu_2, \mu_1$ is so that the $i$th term is at altitude **altmax** – $i$ hence its size is bounded by $f_0(|P| + i)$ (Lemma 27). With the observation of Lemma 25, we retrieve from the follower specifications of this sequence of nodes a bad sequence and we apply the Length function theorem to bound **altmax**. This yields in turn a bound on the size of the root of $\tau$. In order to bound **altmin**, we proceed similarly, using boss nodes this time. We follow a branch from the root to a node of altitude **altmin**. The sequence of nodes that are lower than all previous ones yields a sequence of boss specifications, which is a bad sequence by Lemma 25, and whose growth can be bounded using Lemma 27 and the bound on **altmax**. We apply the Length function theorem to bound $|\text{altmin}|$. □

Once we have bounded **altmax** and **altmin**, we can infer a bound on the size of all nodes (Lemma 27), and then on the length of branches: by minimality, a branch cannot have two nodes with the same specification. The bound on the size of the tree then follows from the observation that bounding the size of nodes of $\tau$ also allows to bound their number of children.

We obtain a computable bound (of the class $\mathcal{F}_{\omega^\omega}$) on the size of a minimal coverability witness if it exists. Our decidability procedure computes that bound, enumerates all trees of size below the bound and checks for each of them whether
Let **altmax** ≥ 0 (resp. **altmin** ≤ 0) denote the maximum (resp. minimum) altitude in τ. We first bound the size of a node with respect to the difference between its altitude and **altmax**.

**Lemma 27.** *There is a primitive recursive function $f_0$ such that, for every node $\mu$ of $\tau$, $|\mu| \le f_0(|P| + \text{altmax} - \text{alt}(\mu))$.*

*Proof sketch.* We proceed by induction on the altitude, from highest to lowest. A node of maximal altitude has at most one message to broadcast (a follower node must broadcast one message to its parent), so its size is bounded by $\psi(|P|, r)$ by Lemma 26 (applying the Lemma to its local run minus its final step, i.e., the step making the broadcast to its parent). Let $\mu$ be a node of $\tau$ whose neighbors of higher altitude have size bounded by $K$. We claim that $|\mu| \le (\psi(|P|, r) + 2)(|M|rK + K)$, with $\psi$ the primitive-recursive function defined in Lemma 26. The idea is similar to the one for Lemma 20. The neighbors of higher altitude are the nodes which require sequences of messages from $\mu$. Their size bounds the number of messages that $\mu$ needs to send; we then apply Lemma 26 to bound the size of the local run of $\mu$. Lemma 37 in the appendix details these ideas. We finally obtain $f_0$ by iteratively applying the inequality above. □

We now bound **altmax** and **altmin**:

**Lemma 28.** **altmax and $|altmin|$ are bounded by a function of class $\mathcal{F}_{\omega|M}|$**.

*Proof sketch.* We first bound **altmax**. Consider a branch of $\tau$ that has a node at altitude **altmax**. We follow this branch from the root to a node of altitude **altmax**: for every $j \in [1, \text{altmax}]$, let $\mu_j$ be the first node of the branch that has altitude $j$. All such nodes are necessarily follower nodes as they are above their parent. Sequence $\mu_{\text{altmax}}, \dots, \mu_2, \mu_1$ is so that the $i$th term is at altitude **altmax** – $i$ hence its size is bounded by $f_0(|P| + i)$ (Lemma 27). With the observation of Lemma 25, we retrieve from the follower specifications of this sequence of nodes a bad sequence and we apply the Length function theorem to bound **altmax**. This yields in turn a bound on the size of the root of $\tau$. In order to bound **altmin**, we proceed similarly, using boss nodes this time. We follow a branch from the root to a node of altitude **altmin**. The sequence of nodes that are lower than all previous ones yields a sequence of boss specifications, which is a bad sequence by Lemma 25, and whose growth can be bounded using Lemma 27 and the bound on **altmax**. We apply the Length function theorem to bound $|\text{altmin}|$. □

Once we have bounded **altmax** and **altmin**, we can infer a bound on the size of all nodes (Lemma 27), and then on the length of branches: by minimality, a branch cannot have two nodes with the same specification. The bound on the size of the tree then follows from the observation that bounding the size of nodes of $\tau$ also allows to bound their number of children.

We obtain a computable bound (of the class $\mathcal{F}_{\omega^\omega}$) on the size of a minimal coverability witness if it exists. Our decidability procedure computes that bound, enumerates all trees of size below the bound and checks for each of them whether
it is coverability witness. This yields the main result of this paper, whose proof
can be found in Appendix G:

**Theorem 12.** *COVER for BNRA is decidable and $F_{\omega^\omega}$-complete.*

**4.2 Undecidability of the target problem**

A natural next problem, after COVER, is the target problem (TARGET). Our COVER procedure heavily relies on the ability to add agents at no cost. For TARGET we need to guarantee that those agents can then reach the target state, which makes the problem harder. In fact, TARGET is undecidable, which indicates that our model lies at the frontier of decidability.

**Proposition 29.** *TARGET is undecidable for BNRA, even with two registers.*

*Proof sketch.* We simulate a Minsky machine with two counters. As in Proposition 11, each agent starts by storing some other agent's identifier, called its "predecessor". It then only accepts messages from its predecessor. As there are finitely many agents, there is a cycle in the predecessor graph.

In a cycle, we use the fact that *all* agents must reach state $q_f$ to simulate faithfully a run of the machine: agents alternate between receptions and broadcasts so that, in the end, they have received and sent the same number of messages, implying that no message has been lost along the cycle. We then simulate the machine by having an agent (the leader) choose transitions and the other ones simulate the counter values by memorizing a counter (1 or 2) and a binary value (0 or 1). For instance, an increment of counter 1 takes the form of a message propagated in the cycle from the leader until it finds an agent simulating counter 1 and having bit 0. This agent switches to 1 and sends an acknowledgment that propagates back to the leader. The full proof is provided in Appendix H. □

**5 Cover in 1-BNRA**

In this section, we establish the NP-completeness of the restriction of COVER to BNRA with one register per agent, called 1-BNRA. Here we simply sketch the key observations that allow us to abstract runs into short witnesses, leading to an NP algorithm for the problem.

In 1-BNRA, thanks to the copycat principle, any message can be broadcast
with a fresh value, therefore one can always circumvent `≠` tests. In the end,
our main challenge for 1-BNRA is `=` tests upon reception. For this reason, we
look at clusters of agents that share the value in their registers.

Consider a run in which some agent *a* reaches some state *q*; we can duplicate
*a* many times to have an unlimited supply of agents in state *q*. Now assume
that, at some point in the run, agent *a* stored a received value. Consider the
last storing action performed by *a*: *a* was in a state *q*₁ and performed transition
(*q*₁, *rec*(*m*, 1, ↓), *q*₂) upon reception of a message (*m*, *v*). Because we can assume
that we have an unlimited supply of agents in *q*₁ thanks to the copycat principle,
it is coverability witness. This yields the main result of this paper, whose proof
can be found in Appendix G:

**Theorem 12.** *COVER for BNRA is decidable and $F_{\omega^\omega}$-complete.*

**4.2 Undecidability of the target problem**

A natural next problem, after COVER, is the target problem (TARGET). Our COVER procedure heavily relies on the ability to add agents at no cost. For TARGET we need to guarantee that those agents can then reach the target state, which makes the problem harder. In fact, TARGET is undecidable, which indicates that our model lies at the frontier of decidability.

**Proposition 29.** *TARGET is undecidable for BNRA, even with two registers.*

*Proof sketch.* We simulate a Minsky machine with two counters. As in Proposition 11, each agent starts by storing some other agent's identifier, called its "predecessor". It then only accepts messages from its predecessor. As there are finitely many agents, there is a cycle in the predecessor graph.

In a cycle, we use the fact that *all* agents must reach state $q_f$ to simulate faithfully a run of the machine: agents alternate between receptions and broadcasts so that, in the end, they have received and sent the same number of messages, implying that no message has been lost along the cycle. We then simulate the machine by having an agent (the leader) choose transitions and the other ones simulate the counter values by memorizing a counter (1 or 2) and a binary value (0 or 1). For instance, an increment of counter 1 takes the form of a message propagated in the cycle from the leader until it finds an agent simulating counter 1 and having bit 0. This agent switches to 1 and sends an acknowledgment that propagates back to the leader. The full proof is provided in Appendix H. □

**5 Cover in 1-BNRA**

In this section, we establish the NP-completeness of the restriction of COVER to BNRA with one register per agent, called 1-BNRA. Here we simply sketch the key observations that allow us to abstract runs into short witnesses, leading to an NP algorithm for the problem.

In 1-BNRA, thanks to the copycat principle, any message can be broadcast
with a fresh value, therefore one can always circumvent `≠` tests. In the end,
our main challenge for 1-BNRA is `=` tests upon reception. For this reason, we
look at clusters of agents that share the value in their registers.

Consider a run in which some agent *a* reaches some state *q*; we can duplicate
*a* many times to have an unlimited supply of agents in state *q*. Now assume
that, at some point in the run, agent *a* stored a received value. Consider the
last storing action performed by *a*: *a* was in a state *q*₁ and performed transition
(*q*₁, *rec*(*m*, 1, ↓), *q*₂) upon reception of a message (*m*, *v*). Because we can assume
that we have an unlimited supply of agents in *q*₁ thanks to the copycat principle,
we can make as many agents as we want take transition $(q_1, \text{rec}(m, 1, \downarrow), q_2)$ at
the same time as *a* by receiving the same message $(m, v)$. These new agents end
up in $q_2$ with value $v$, and then follow *a* along every transition until they all
reach *q*, still with value $v$. In summary, because *a* has stored a value in the run,
we can have an unlimited supply of agents in state *q* with the same value as *a*.

Following those observations, we define an abstract semantics with abstract
configurations of the form (*S*, *b*, *K*) with *S*, *K* ⊆ *Q* and *b* ∈ *Q* ∪ {⊥}. The first
component *S* is a set of states that we know we can cover (hence we can assume
that there are arbitrarily many agents in all these states). We start with *S* = {q₀}
and try to increase it. To do so, we use the two other components (the *gang*)
to keep track of the set of agents sharing a value *v*: *b* (the *boss*) is the state of
the agent which had that value at the start, *K* (the *clique*) is the set of states
covered by other agents with that value. As mentioned above, we may assume
that every state of *K* is filled with as many agents with value *v* as we need. We
will thus define abstract steps which allow to simulate steps of the agents with
the value we are following. When they cover states outside of *S*, we may add
those to *S* and reset *b* to q₀ and *K* to ∅, to then start following another value. We
can bound the length of relevant abstract runs, and thus use them as witnesses
for our NP upper bound.

The NP lower bound follows from a reduction from 3SAT. An agent *a* sends a
sequence of messages representing a valuation, with its identifier, to other agents
who play the role of an external memory by broadcasting back the valuation.
This then allows *a* to check the satisfaction of a 3SAT formula.

**Theorem 30.** *The coverability problem for 1-BNRA is NP-complete.*

The formal proofs of the upper and lower bounds are given in Appendix I.

# 6 Conclusion

We established the decidability (and $F_{\omega^\omega}$-completeness) of the coverability problem for BNRA, as well as the NP-completeness of the problem for 1-BNRA. Concerning future work, one may want to push decidability further, for instance by enriching our protocols with inequality tests, as done in classical models such as data nets [15]. Reductions of other distributed models to this one are also being studied.

*Acknowledgements.* We are grateful to Arnaud Sangnier for encouraging us to work on BNRA, for the discussions about his work in [10] and for his valuable advice. We also thank Philippe Schnoebelen for the interesting discussion and Sylvain Schmitz for the exchange on complexity class $F_{\omega^\omega}$ and related topics.

References

1. Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014. LIPIcs,
we can make as many agents as we want take transition $(q_1, \mathbf{rec}(m, 1, \downarrow), q_2)$ at
the same time as *a* by receiving the same message $(m, v)$. These new agents end
up in $q_2$ with value $v$, and then follow *a* along every transition until they all
reach *q*, still with value $v$. In summary, because *a* has stored a value in the run,
we can have an unlimited supply of agents in state *q* with the same value as *a*.

Following those observations, we define an abstract semantics with abstract
configurations of the form (*S*, *b*, *K*) with *S*, *K* ⊆ *Q* and *b* ∈ *Q* ∪ {⊥}. The first
component *S* is a set of states that we know we can cover (hence we can assume
that there are arbitrarily many agents in all these states). We start with *S* = {q₀}
and try to increase it. To do so, we use the two other components (the *gang*)
to keep track of the set of agents sharing a value *v*: *b* (the *boss*) is the state of
the agent which had that value at the start, *K* (the *clique*) is the set of states
covered by other agents with that value. As mentioned above, we may assume
that every state of *K* is filled with as many agents with value *v* as we need. We
will thus define abstract steps which allow to simulate steps of the agents with
the value we are following. When they cover states outside of *S*, we may add
those to *S* and reset *b* to q₀ and *K* to ∅, to then start following another value. We
can bound the length of relevant abstract runs, and thus use them as witnesses
for our NP upper bound.

The NP lower bound follows from a reduction from 3SAT. An agent *a* sends a
sequence of messages representing a valuation, with its identifier, to other agents
who play the role of an external memory by broadcasting back the valuation.
This then allows *a* to check the satisfaction of a 3SAT formula.

**Theorem 30.** *The coverability problem for 1-BNRA is NP-complete.*

The formal proofs of the upper and lower bounds are given in Appendix I.

# 6 Conclusion

We established the decidability (and $\mathbf{F}_{\omega^\omega}$-completeness) of the coverability problem for BNRA, as well as the NP-completeness of the problem for 1-BNRA. Concerning future work, one may want to push decidability further, for instance by enriching our protocols with inequality tests, as done in classical models such as data nets [15]. Reductions of other distributed models to this one are also being studied.

*Acknowledgements.* We are grateful to Arnaud Sangnier for encouraging us to work on BNRA, for the discussions about his work in [10] and for his valuable advice. We also thank Philippe Schnoebelen for the interesting discussion and Sylvain Schmitz for the exchange on complexity class $\mathbf{F}_{\omega^\omega}$ and related topics.

References

1. Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014. LIPIcs,
vol. 29, pp. 653–665. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014).
https://doi.org/10.4230/LIPIcs.FSTTCS.2014.653

2. Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of buffered dynamic register automata. In: Networked Systems, NETYS 2015. Lecture Notes in Computer Science, vol. 9466, pp. 15–31. Springer (2015).
https://doi.org/10.1007/978-3-319-26850-7_2

3. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation **127**(2), 91–101 (1996).
https://doi.org/10.1006/inco.1996.0053

4. Balasubramanian, A.R., Bertrand, N., Markey, N.: Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018. Lecture Notes in Computer Science, vol. 10806, pp. 38–54. Springer (2018).
https://doi.org/10.1007/978-3-319-89963-3_3

5. Balasubramanian, A.R., Guillou, L., Weil-Kennedy, C.: Parameterized analysis of reconfigurable broadcast networks. In: Foundations of Software Science and Computation Structures, FoSSaCS 2022. Lecture Notes in Computer Science, vol. 13242, pp. 61–80. Springer (2022).
https://doi.org/10.1007/978-3-030-99253-8_4

6. Bollig, B., Ryabinin, F., Sangnier, A.: Reachability in distributed memory automata. In: Annual Conference on Computer Science Logic, CSL 2021. LIPICs, vol. 183, pp. 13:1–13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021).
https://doi.org/10.4230/LIPIcs.CSL.2021.13

7. Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM **30**(2), 323–342 (1983). https://doi.org/10.1145/322374.322380

8. Chambart, P., Schnoebelen, P.: The ordinal recursive complexity of lossy channel systems. In: Annual IEEE Symposium on Logic in Computer Science, LICS 2008. pp. 205–216. IEEE Computer Society (2008).
https://doi.org/10.1109/LICS.2008.47

9. Chini, P., Meyer, R., Saivasan, P.: Liveness in broadcast networks. Computing **104**(10), 2203–2223 (2022). https://doi.org/10.1007/s00607-021-00986-y

10. Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Reachability Problems, RP 2013. Lecture Notes in Computer Science, vol. 8169, pp. 109–121. Springer (2013).
https://doi.org/10.1007/978-3-642-41036-9_11

11. Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012).
https://doi.org/10.4230/LIPIcs.FSTTCS.2012.289

12. Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: CONCUR 2010. Lecture Notes in Computer Science, vol. 6269, pp. 313–327. Springer (2010). https://doi.org/10.1007/978-3-642-15375-4_22

13. Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Annual IEEE Symposium on Logic in Computer Science, LICS 1998. pp. 70–80. IEEE Computer Society (1998).
https://doi.org/10.1109/LICS.1998.705644

14. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual IEEE Symposium on Logic in Computer Science,
vol. 29, pp. 653–665. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014).
https://doi.org/10.4230/LIPIcs.FSTTCS.2014.653

2. Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of buffered dynamic register automata. In: Networked Systems, NETYS 2015. Lecture Notes in Computer Science, vol. 9466, pp. 15–31. Springer (2015).
https://doi.org/10.1007/978-3-319-26850-7_2

3. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation **127**(2), 91–101 (1996).
https://doi.org/10.1006/inco.1996.0053

4. Balasubramanian, A.R., Bertrand, N., Markey, N.: Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018. Lecture Notes in Computer Science, vol. 10806, pp. 38–54. Springer (2018).
https://doi.org/10.1007/978-3-319-89963-3_3

5. Balasubramanian, A.R., Guillou, L., Weil-Kennedy, C.: Parameterized analysis of reconfigurable broadcast networks. In: Foundations of Software Science and Computation Structures, FoSSaCS 2022. Lecture Notes in Computer Science, vol. 13242, pp. 61–80. Springer (2022).
https://doi.org/10.1007/978-3-030-99253-8_4

6. Bollig, B., Ryabinin, F., Sangnier, A.: Reachability in distributed memory automata. In: Annual Conference on Computer Science Logic, CSL 2021. LIPICs, vol. 183, pp. 13:1–13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021).
https://doi.org/10.4230/LIPIcs.CSL.2021.13

7. Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM **30**(2), 323–342 (1983). https://doi.org/10.1145/322374.322380

8. Chambart, P., Schnoebelen, P.: The ordinal recursive complexity of lossy channel systems. In: Annual IEEE Symposium on Logic in Computer Science, LICS 2008. pp. 205–216. IEEE Computer Society (2008).
https://doi.org/10.1109/LICS.2008.47

9. Chini, P., Meyer, R., Saivasan, P.: Liveness in broadcast networks. Computing **104**(10), 2203–2223 (2022). https://doi.org/10.1007/s00607-021-00986-y

10. Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Reachability Problems, RP 2013. Lecture Notes in Computer Science, vol. 8169, pp. 109–121. Springer (2013).
https://doi.org/10.1007/978-3-642-41036-9_11

11. Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012).
https://doi.org/10.4230/LIPIcs.FSTTCS.2012.289

12. Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: CONCUR 2010. Lecture Notes in Computer Science, vol. 6269, pp. 313–327. Springer (2010). https://doi.org/10.1007/978-3-642-15375-4_22

13. Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Annual IEEE Symposium on Logic in Computer Science, LICS 1998. pp. 70–80. IEEE Computer Society (1998).
https://doi.org/10.1109/LICS.1998.705644

14. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual IEEE Symposium on Logic in Computer Science,
Trento, Italy, July 2-5, 1999. pp. 352-359. IEEE Computer Society (1999).
https://doi.org/10.1109/LICS.1999.782630

15. Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal-recursive complexity of timed-arc petri nets, data nets, and other enriched nets. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. pp. 355-364. IEEE Computer Society (2012). https://doi.org/10.1109/LICS.2012.46

16. Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society s3-2(1), 326-336 (1952).
https://doi.org/10.1112/plms/s3-2.1.326

17. Lasota, S.: Decidability border for petri nets with data: WQO dichotomy conjecture. In: Kordon, F., Moldt, D. (eds.) Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS 2016, Toruń, Poland, June 19-24, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9698, pp. 20-36. Springer (2016). https://doi.org/10.1007/978-3-319-39086-4_3,
https://doi.org/10.1007/978-3-319-39086-4_3

18. Lazic, R., Newcomb, T.C., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Informaticae 88(3), 251-274 (2008).
https://doi.org/10.1007/978-3-540-73094-1_19

19. Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA (1967)

20. Rezine, O.: Verification of networks of communicating processes: Reachability problems and decidability issues. Ph.D. thesis, Uppsala University, Sweden (2017)

21. Rosa-Velardo, F.: Ordinal recursive complexity of unordered data nets. Information and Computation 254, 41-58 (2017).
https://doi.org/10.1016/j.ic.2017.02.002

22. Sangnier, A.: Erratum to parameterized verification of broadcast networks of register automata (2023), https://www.irif.fr/~sangnier/publications.html

23. Schmitz, S.: Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory 8(1), 3:1-3:36 (2016). https://doi.org/10.1145/2858784

24. Schmitz, S., Schnoebelen, P.: Multiply-recursive upper bounds with Higman's lemma. In: International Colloquium on Automata, Languages and Programming, ICALP 2011. Lecture Notes in Computer Science, vol. 6756, pp. 441-452. Springer (2011). https://doi.org/10.1007/978-3-642-22012-8_35

25. Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D'Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8052, pp. 5-24. Springer (2013). https://doi.org/10.1007/978-3-642-40184-8_2

26. Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251-261 (2002).
https://doi.org/10.1016/S0020-0190(01)00337-4
Trento, Italy, July 2-5, 1999. pp. 352-359. IEEE Computer Society (1999).
https://doi.org/10.1109/LICS.1999.782630

15. Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal-recursive complexity of timed-arc petri nets, data nets, and other enriched nets. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. pp. 355-364. IEEE Computer Society (2012). https://doi.org/10.1109/LICS.2012.46

16. Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society s3-2(1), 326-336 (1952).
https://doi.org/10.1112/plms/s3-2.1.326

17. Lasota, S.: Decidability border for petri nets with data: WQO dichotomy conjecture. In: Kordon, F., Moldt, D. (eds.) Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS 2016, Toruń, Poland, June 19-24, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9698, pp. 20-36. Springer (2016). https://doi.org/10.1007/978-3-319-39086-4_3,
https://doi.org/10.1007/978-3-319-39086-4_3

18. Lazic, R., Newcomb, T.C., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Informaticae 88(3), 251-274 (2008).
https://doi.org/10.1007/978-3-540-73094-1_19

19. Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA (1967)

20. Rezine, O.: Verification of networks of communicating processes: Reachability problems and decidability issues. Ph.D. thesis, Uppsala University, Sweden (2017)

21. Rosa-Velardo, F.: Ordinal recursive complexity of unordered data nets. Information and Computation 254, 41-58 (2017).
https://doi.org/10.1016/j.ic.2017.02.002

22. Sangnier, A.: Erratum to parameterized verification of broadcast networks of register automata (2023), https://www.irif.fr/~sangnier/publications.html

23. Schmitz, S.: Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory 8(1), 3:1-3:36 (2016). https://doi.org/10.1145/2858784

24. Schmitz, S., Schnoebelen, P.: Multiply-recursive upper bounds with Higman's lemma. In: International Colloquium on Automata, Languages and Programming, ICALP 2011. Lecture Notes in Computer Science, vol. 6756, pp. 441-452. Springer (2011). https://doi.org/10.1007/978-3-642-22012-8_35

25. Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D'Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8052, pp. 5-24. Springer (2013). https://doi.org/10.1007/978-3-642-40184-8_2

26. Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251-261 (2002).
https://doi.org/10.1016/S0020-0190(01)00337-4
# A Proof of Proposition 11

**Proposition 11.** COVER for signature BNRA is $F_{\omega^\omega}$-hard.

*Proof.* We provide here a polynomial-time reduction from reachability for lossy channel systems with a single channel. A lossy channel system with a single channel is a finite-state machine that has the ability to buffer symbols in a lossy FIFO queue [26]. Let $\mathcal{L} := (L, \Sigma, D)$ be a lossy channel system, where $L$ is a finite set of locations, $\Sigma$ is a finite set of symbols and $D \subseteq L \times \{\text{read}(x), \text{write}(x) | x \in \Sigma\} \times L$; $\text{write}(x)$ corresponds to writing $x$ at the end of the channel and $\text{read}(x)$ to reading $x$ at the beginning of the channel. A configuration of $\mathcal{L}$ is a pair in $L \times \Sigma^*$ denoting the location and the content of the channel. There exists a step from $(l, w)$ to $(l', w')$ using $d \in D$, denoted $(l, w) \xrightarrow{d} \mathcal{L}$ $(l', w')$, when

- $d = (l, \text{write}(x), l')$ for some $x \in \Sigma$ and $w' \preceq w \cdot x$,

- $d = (l, \text{read}(x), l')$ for some $x \in \Sigma$ and $x \cdot w' \preceq w$.

where $\preceq$ denotes the subword order, which encodes the lossiness of the channel.

The existence of a step is denoted $(l, w) \xrightarrow{\mathcal{L}} (l', w')$, and its transitive closure is denoted $\xrightarrow{\mathcal{L}}^*$. The (location) *reachability problem* asks, given $\mathcal{L}$ and two locations $l_s, l_f \in L$, whether $(l_s, \varepsilon) \xrightarrow{\mathcal{L}} (l_f, w)$ for some $w$.

We construct a signature protocol $\mathcal{P}$ with two registers (register 1 is broadcast-only, register 2 is reception-only) and a state $q_f$ that may be covered if and only if $(\mathcal{L}, q_i, q_f)$ is a positive instance of the reachability problem.

In some initial phase, each agent may become a *link* and store some other agent's identifier (its *predecessor*); in that case, it will test further messages for equality so that only messages from the predecessor are accepted. Otherwise, it will become a *root* and will not receive any message in the future. A depiction of this initial phase can be found in Figure 7a.

The predecessor graph of a run of $\mathcal{P}$, defined by the graph $(\mathcal{A}, E)$ where $(a', a) \in E$ whenever $a'$ is the predecessor of $a$, will be a forest where each branch will simulate an execution of $\mathcal{L}$. A given agent $a$ of a given branch encodes one step of the execution in the lossy channel system. A root agent is at the root of its tree and simply broadcasts the initial configuration $(l_s, \varepsilon)$ of $\mathcal{L}$; special character \# encodes the end of the broadcast of the channel's content. If $a$ is a link agent, then it will receive from its predecessor a location of the system and (a subword of) the content of the channel. Agent $a$ will in turn broadcast to the next agent in the branch, sending the new location of the system and the new content of the channel which $a$ rebroadcasts on-the-fly letter by letter as it receives it. Agent $a$ only modifies the beginning of the channel if it decides to encode a pop and the end of the channel if it decides to encode a push. Messages might get lost, which is why we cannot encode non-lossy channel systems.

Observe that this construction only guarantees that agents have at most one predecessor; it does not guarantee that all agents are in the same branch or that any agent is the predecessor of at most one agent. This is fine because the information only propagates forward in a branch, and never propagates in between branches.
A Proof of Proposition 11

**Proposition 11.** COVER for signature BNRA is $F_{\omega^\omega}$-hard.

*Proof.* We provide here a polynomial-time reduction from reachability for lossy channel systems with a single channel. A lossy channel system with a single channel is a finite-state machine that has the ability to buffer symbols in a lossy FIFO queue [26]. Let $\mathcal{L} := (L, \Sigma, D)$ be a lossy channel system, where $L$ is a finite set of locations, $\Sigma$ is a finite set of symbols and $D \subseteq L \times \{\text{read}(x), \text{write}(x) | x \in \Sigma\} \times L$; $\text{write}(x)$ corresponds to writing $x$ at the end of the channel and $\text{read}(x)$ to reading $x$ at the beginning of the channel. A configuration of $\mathcal{L}$ is a pair in $L \times \Sigma^*$ denoting the location and the content of the channel. There exists a step from $(l, w)$ to $(l', w')$ using $d \in D$, denoted $(l, w) \xrightarrow{d} \mathcal{L}$ $(l', w')$, when

- $d = (l, \text{write}(x), l')$ for some $x \in \Sigma$ and $w' \preceq w \cdot x$,

- $d = (l, \text{read}(x), l')$ for some $x \in \Sigma$ and $x \cdot w' \preceq w$.

where $\preceq$ denotes the subword order, which encodes the lossiness of the channel.

The existence of a step is denoted $(l, w) \to_{\mathcal{L}} (l', w')$, and its transitive closure is denoted $\stackrel{*}{\to}_{\mathcal{L}}$. The (location) *reachability problem* asks, given $\mathcal{L}$ and two locations $l_s, l_f \in L$, whether $(l_s, \varepsilon) \stackrel{*}{\to}_{\mathcal{L}} (l_f, w)$ for some $w$.

We construct a signature protocol $\mathcal{P}$ with two registers (register 1 is broadcast-only, register 2 is reception-only) and a state $q_f$ that may be covered if and only if $(\mathcal{L}, q_i, q_f)$ is a positive instance of the reachability problem.

In some initial phase, each agent may become a *link* and store some other agent's identifier (its *predecessor*); in that case, it will test further messages for equality so that only messages from the predecessor are accepted. Otherwise, it will become a *root* and will not receive any message in the future. A depiction of this initial phase can be found in Figure 7a.

The predecessor graph of a run of $\mathcal{P}$, defined by the graph $(\mathcal{A}, E)$ where $(a', a) \in E$ whenever $a'$ is the predecessor of $a$, will be a forest where each branch will simulate an execution of $\mathcal{L}$. A given agent $a$ of a given branch encodes one step of the execution in the lossy channel system. A root agent is at the root of its tree and simply broadcasts the initial configuration $(l_s, \varepsilon)$ of $\mathcal{L}$; special character \# encodes the end of the broadcast of the channel's content. If $a$ is a link agent, then it will receive from its predecessor a location of the system and (a subword of) the content of the channel. Agent $a$ will in turn broadcast to the next agent in the branch, sending the new location of the system and the new content of the channel which $a$ rebroadcasts on-the-fly letter by letter as it receives it. Agent $a$ only modifies the beginning of the channel if it decides to encode a pop and the end of the channel if it decides to encode a push. Messages might get lost, which is why we cannot encode non-lossy channel systems.

Observe that this construction only guarantees that agents have at most one predecessor; it does not guarantee that all agents are in the same branch or that any agent is the predecessor of at most one agent. This is fine because the information only propagates forward in a branch, and never propagates in between branches.
From state **wait**, an agents will receive the location *l* from its predecessor and go to state **s**(*l*); from there, it will non-deterministically pick a transition of *L* and apply it. See Figure 7b for a depiction of transitions from some state **s**(*l*₁) (all **s**(*l*), *l* ≠ *l*₁, and corresponding transitions are omitted in the figure). Finally, the objective state of our system is *q*ᵢ := **f**(*l*ᵢ).

<figure><img src="image_8.png" /><figcaption>(b) Part of $\mathcal{P}$ encoding transitions from $l_1$. Here, $\mathcal{L}$ has symbols $\Sigma = \{\mathbf{a}, \mathbf{b}\}$ and there are two transitions from $l_1$: $d = (l_1, \mathbf{read}(\mathbf{a}), l_2)$ and $d' = (l_1, \mathbf{write}(\mathbf{b}), l_3)$.</figcaption></figure>

<caption>Fig. 7: Depiction of the protocol $\mathcal{P}$ built in the lossy channel system reduction of Proposition 11.</caption>

We claim that ($\mathcal{P}$, $q_f$) is a positive instance of COVERif and only if ($\mathcal{L}$, $l_f$) is a positive instance of the reachability problem for lossy channel systems. First, suppose that there exists $w \in \Sigma^*$ such that $(l_0, \varepsilon) \xrightarrow{\ast} \mathcal{L} (l_f, w)$. Decompose the witness into $(l_0, w_0) \to \mathcal{L} (l_1, w_1) \to \mathcal{L} (l_2, w_2) \cdots \to \mathcal{L} (l_n, w_n)$ with $l_n = l_f$ and $w_n = w$. We build an initial run of $\mathcal{P}$ that covers $q_f$. It has set of agents $\mathcal{A} := \{0, \dots, n\}$. Agent 0 becomes the root and for all $i \ge 1$, agent $i$ becomes a link
From state **wait**, an agents will receive the location *l* from its predecessor and go to state **s**(*l*); from there, it will non-deterministically pick a transition of *L* and apply it. See Figure 7b for a depiction of transitions from some state **s**(*l*₁) (all **s**(*l*), *l* ≠ *l*₁, and corresponding transitions are omitted in the figure). Finally, the objective state of our system is *q*ᵢ := **f**(*l*ᵢ).

<figure><img src="image_8.png" /><figcaption>(b) Part of $\mathcal{P}$ encoding transitions from $l_1$. Here, $\mathcal{L}$ has symbols $\Sigma = \{\mathbf{a}, \mathbf{b}\}$ and there are two transitions from $l_1$: $d = (l_1, \mathbf{read}(\mathbf{a}), l_2)$ and $d' = (l_1, \mathbf{write}(\mathbf{b}), l_3)$.</figcaption></figure>

<caption>Fig. 7: Depiction of the protocol $\mathcal{P}$ built in the lossy channel system reduction of Proposition 11.</caption>

We claim that ($\mathcal{P}$, $q_f$) is a positive instance of COVERif and only if ($\mathcal{L}$, $l_f$) is a positive instance of the reachability problem for lossy channel systems. First, suppose that there exists $w \in \Sigma^*$ such that $(l_0, \varepsilon) \xrightarrow{\ast} \mathcal{L} (l_f, w)$. Decompose the witness into $(l_0, w_0) \to \mathcal{L} (l_1, w_1) \to \mathcal{L} (l_2, w_2) \cdots \to \mathcal{L} (l_n, w_n)$ with $l_n = l_f$ and $w_n = w$. We build an initial run of $\mathcal{P}$ that covers $q_f$. It has set of agents $\mathcal{A} := \{0, \dots, n\}$. Agent 0 becomes the root and for all $i \ge 1$, agent $i$ becomes a link
with predecessor agent $i-1$. By induction on $i$, we build an execution using agents 0 to $i$ such that agent $i$ ends on state $f(l_i)$ and the sequence of message types sent by agent $i$ admits as subword $\text{init} \cdot l_i \cdot w_i \cdot \#$. For $i=0$, this condition is easily met by making agent 0 become root. We make agent $i+1$ do the following. It receives from agent $i$ state $l_i$ and goes to $s(l_i)$. It moves to $t(d)$ where $d \in D$ is such that $(l_i, w_i) \xrightarrow{d} \mathcal{L}(l_{i+1}, w_{i+1})$. It then follows the branch and gets to $f(l_{i+1})$.

- if $d = (l_i, \text{write}(x), l_{i+1})$ is a push, then $w_{i+1} = w'_i \cdot y$ where $w'_i \preceq w_i$ and $y \in \{\varepsilon, x\}$. We can make agent $i+1$ broadcast $\text{init} \cdot l_i \cdot w'_i \cdot x \cdot \#$ which admits as subword $\text{init} \cdot l_{i+1} \cdot w_{i+1} \cdot \#$.

- if $d = (l_i, \text{read}(x), l_{i+1})$ is a pop then $w_i = u \cdot w'_{i+1}$ where $w_{i+1} \preceq w'_{i+1}$ and $x \preceq u$. By lossiness, agent $i+1$ only receives $x$ from $u$ and goes to $\mathbf{u}(d)$. We make it broadcast $\text{init} \cdot l_{i+1} \cdot w'_{i+1} \cdot \#$ which admits as subword $\text{init} \cdot l_{i+1} \cdot w_{i+1} \cdot \#$.

This concludes the induction step. When applied to $i=n$, this builds an initial run where agent $n$ ends on $f(l_n)$, which is a witness that $(\mathcal{P}, q_f)$ is positive.

Suppose now that $(\mathcal{P}, q_f)$ is positive. Let $\rho : \gamma_0 \xrightarrow{*} \gamma_f$ where $\gamma_f$ covers $q_f$. The predecessor graph obtained at the end of $\rho$ is a forest; there can be no cycle as it would imply that all agents in the cycle are link, which is a contradiction by considering the agent of the cycle sending the first init message. Consider in $\rho$ a branch of agents $a_0, \dots, a_n$ such that $a_i$ is the predecessor of $a_{i+1}$ for each $i \in [0, n-1]$, $a_0$ is the root and $a_n$ covers $q_f$.

From the run $\rho$ projected onto this branch, it is quite simple to build an execution of $\mathcal{L}$ that covers $q_f$. By structure of the protocol, because $a_n$ covers $q_f$, every agent $a_i$ ends on some $f(l_i)$ and broadcasts a word of the form $\text{init} \cdot l_i \cdot w_i \cdot \#$; this can be proven with an immediate backwards induction. It then suffices to analyse the behavior of $a_{i+1}$ to prove that $(l_i, w_i) \xrightarrow{\mathcal{L}} (l_{i+1}, w_{i+1})$. In particular, because $a_0$ is a root, $l_0 = l_s$ and $w_0 = \varepsilon$, which concludes the proof. $\square$

## B Definitions and Notations of Section 4

We will first define the notion of decomposition, which is a formalization of the observation in Example 22. A *decomposition* is a tuple $\text{dec} = (w_0, m_1, \dots, m_\ell, w_\ell)$ with $w_0, \dots, w_\ell \in \mathcal{M}^*$, and $m_1, \dots, m_\ell \in \mathcal{M}$, with $m_i \neq m_j$ for all $i \neq j$. In particular we have $\ell \le |\mathcal{M}|$. A word $w \in \mathcal{M}^*$ admits decomposition $\text{dec} = (w_0, m_1, \dots, m_\ell, w_\ell)$ if $w \preceq w'_0 w'_1 \dots w'_\ell$ where for all $j$, $w'_j$ can be obtained from $w_j$ by adding letters from $\{m_1, \dots, m_j\}$. We denote by $\mathcal{L}^{\text{dec}}$ the language of words that admit decomposition $\text{dec}$.

We are now ready to formally define unfolding trees in the general case.

**Definition 31.** An unfolding tree $\tau$ over $\mathcal{P}$ is a finite tree where nodes $\mu$ have three labels:

- a local run of $\mathcal{P}$, written $\text{lr}(\mu)$, starting in the initial state with distinct register values;

- a value in $\mathbb{N}$, written $\text{val}(\mu)$;
with predecessor agent $i-1$. By induction on $i$, we build an execution using agents 0 to $i$ such that agent $i$ ends on state $f(l_i)$ and the sequence of message types sent by agent $i$ admits as subword $\text{init} \cdot l_i \cdot w_i \cdot \#$. For $i=0$, this condition is easily met by making agent 0 become root. We make agent $i+1$ do the following. It receives from agent $i$ state $l_i$ and goes to $s(l_i)$. It moves to $t(d)$ where $d \in D$ is such that $(l_i, w_i) \xrightarrow{d} \mathcal{L}(l_{i+1}, w_{i+1})$. It then follows the branch and gets to $f(l_{i+1})$.

- if $d = (l_i, \text{write}(x), l_{i+1})$ is a push, then $w_{i+1} = w'_i \cdot y$ where $w'_i \preceq w_i$ and $y \in \{\varepsilon, x\}$. We can make agent $i+1$ broadcast $\text{init} \cdot l_i \cdot w'_i \cdot x \cdot \#$ which admits as subword $\text{init} \cdot l_{i+1} \cdot w_{i+1} \cdot \#$.

- if $d = (l_i, \text{read}(x), l_{i+1})$ is a pop then $w_i = u \cdot w'_{i+1}$ where $w_{i+1} \preceq w'_{i+1}$ and $x \preceq u$. By lossiness, agent $i+1$ only receives $x$ from $u$ and goes to $\mathbf{u}(d)$. We make it broadcast $\text{init} \cdot l_{i+1} \cdot w'_{i+1} \cdot \#$ which admits as subword $\text{init} \cdot l_{i+1} \cdot w_{i+1} \cdot \#$.

This concludes the induction step. When applied to $i=n$, this builds an initial run where agent $n$ ends on $f(l_n)$, which is a witness that $(\mathcal{P}, q_f)$ is positive.

Suppose now that $(\mathcal{P}, q_f)$ is positive. Let $\rho : \gamma_0 \xrightarrow{*} \gamma_f$ where $\gamma_f$ covers $q_f$. The predecessor graph obtained at the end of $\rho$ is a forest; there can be no cycle as it would imply that all agents in the cycle are link, which is a contradiction by considering the agent of the cycle sending the first init message. Consider in $\rho$ a branch of agents $a_0, \dots, a_n$ such that $a_i$ is the predecessor of $a_{i+1}$ for each $i \in [0, n-1]$, $a_0$ is the root and $a_n$ covers $q_f$.

From the run $\rho$ projected onto this branch, it is quite simple to build an execution of $\mathcal{L}$ that covers $q_f$. By structure of the protocol, because $a_n$ covers $q_f$, every agent $a_i$ ends on some $f(l_i)$ and broadcasts a word of the form $\text{init} \cdot l_i \cdot w_i \cdot \#$; this can be proven with an immediate backwards induction. It then suffices to analyse the behavior of $a_{i+1}$ to prove that $(l_i, w_i) \xrightarrow{\mathcal{L}} (l_{i+1}, w_{i+1})$. In particular, because $a_0$ is a root, $l_0 = l_s$ and $w_0 = \varepsilon$, which concludes the proof. $\square$

## B Definitions and Notations of Section 4

We will first define the notion of decomposition, which is a formalization of the observation in Example 22. A *decomposition* is a tuple $\text{dec} = (w_0, m_1, \dots, m_\ell, w_\ell)$ with $w_0, \dots, w_\ell \in \mathcal{M}^*$, and $m_1, \dots, m_\ell \in \mathcal{M}$, with $m_i \neq m_j$ for all $i \neq j$. In particular we have $\ell \le |\mathcal{M}|$. A word $w \in \mathcal{M}^*$ *admits decomposition* $\text{dec} = (w_0, m_1, \dots, m_\ell, w_\ell)$ if $w \preceq w'_0 w'_1 \dots w'_\ell$ where for all $j$, $w'_j$ can be obtained from $w_j$ by adding letters from $\{m_1, \dots, m_j\}$. We denote by $\mathcal{L}^{\text{dec}}$ the language of words that admit decomposition $\text{dec}$.

We are now ready to formally define unfolding trees in the general case.

**Definition 31.** An unfolding tree $\tau$ over $\mathcal{P}$ is a finite tree where nodes $\mu$ have three labels:

- a local run of $\mathcal{P}$, written $\text{lr}(\mu)$, starting in the initial state with distinct register values;

- a value in $\mathbb{N}$, written $\text{val}(\mu)$;
- a specification **spec**($\mu$), which is either a word **bw**($\mu$) $\in \mathcal{M}^*$ (boss specification) or a pair (**fw**($\mu$), **fm**($\mu$)) $\in \mathcal{M}^* \times \mathcal{M}$ (follower specification). In the first case we say that the node is a boss node, otherwise it is a follower node.

Moreover, all nodes $\mu$ must satisfy the four following conditions:

(i) For each non-initial value $v \neq \textbf{val}(\mu)$ of $\mathbf{lr}(\mu)$, $\mu$ has a child $\mu'$ which is a boss node such that $\ln_v(\mathbf{lr}(\mu))$ is a subword of $\mathbf{bw}(\mu')$.

(ii) For each initial value $v$ in $\mathbf{lr}(\mu)$, there is a decomposition
$\mathbf{dec} = (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$ s.t.:
- $\mathbf{lr}(\mu)$ may be split into successive local runs $u_0, \dots, u_\ell$ where, for all $i \in [1, \ell]$, $w_i \le \text{Out}_v(u_i)$ and $\ln_v(u_i) \in \{m_1, \dots, m_{i-1}\}^*$,
- for all $i \in [1, \ell]$, $\mu$ has a child $\mu_i$ which is a follower node such that $\mathbf{fm}(\mu_i) = m_i$ and $\mathbf{fw}(\mu_i) \in \mathcal{L}^{\text{dec}_i}$ where $\mathbf{dec}_i = (w_0, m_1, w_1, \dots, m_{i-1}, w_{i-1})$.

(iii) If $\mu$ is a follower node then $\textbf{val}(\mu)$ is not an initial value of $u$, $\ln_{\textbf{val}(\mu)}(u) \le \textbf{fw}(\mu)$ and $\text{Out}_{\textbf{val}(\mu)}(u)$ contains $\mathbf{fm}(\mu)$.

(iv) If $\mu$ is a boss node, then $\textbf{val}(\mu)$ is an initial value of $\mathbf{lr}(\mu)$ and the decomposition $\mathbf{dec}$ of (ii) for $\textbf{val}(\mu)$ satisfies that $\mathbf{bw}(\mu) \in \mathcal{L}^{\text{dec}}$.

Lastly, as before, given $\tau$ an unfolding tree, we define its size by $|\tau| := \sum_{\mu \in \tau} |\mathbf{lr}(\mu)| + |\mathbf{spec}(\mu)| + 1$.

We now explain this definition. Let $\mu$ be a node of an unfolding tree $\tau$ and let $u := \mathbf{lr}(\mu)$. As before, $u$ encodes the local run of a given agent, $\mathbf{spec}(\mu)$ encodes the specification that this local run carries out and $\mathbf{val}(\mu)$ encodes the value for which the specification is carried out.

Conditions (i) and (ii) state that the specifications of the children of $\mu$ are witnesses that messages received in the local run $\mathbf{lr}(\mu)$ can be broadcast by other agents. Conditions (iii) and (iv) state that $\mu$ is a witness that its specification is carried out.

As before, condition (i) expresses that, for every non-initial value $v$ of $u$, $\mu$ must have a boss child witnessing that $\ln_v(u)$ can indeed be broadcast. Because $v$ was first stored by a reception step of $u$, any other (fresh) value with sequence of message types containing $\ln_v(u)$ also works and we do not impose the value label of this child to be $v$.

We now explain condition (ii), which states the existence of a decomposition for each initial value, which serves as a summary of the broadcasts made with that value. Let $v$ be an initial value of $u$. Consider a run where $u$ is the local run of agent $a$. If another agent broadcasts with value $v$, it has first received and stored $v$. By duplicating agents, we may afterwards assume that we have an unlimited supply of messages $(m, v)$. Therefore the crucial information is the times at which each message type is first broadcast with $v$ by an agent other than $a$.

The decomposition $\mathbf{dec} = (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$ should be understood as follows: In the run we are representing, $a$ first broadcasts messages of $w_0$ with value $v$, after which other agents are able to broadcast $(m_1, v)$. Then $a$ broadcasts $w_1$ (and may receive $m_1$), after which other agents can broadcast $(m_2, v)$, and
- a specification **spec**($\mu$), which is either a word **bw**($\mu$) $\in \mathcal{M}^*$ (boss specification) or a pair (**fw**($\mu$), **fm**($\mu$)) $\in \mathcal{M}^* \times \mathcal{M}$ (follower specification). In the first case we say that the node is a boss node, otherwise it is a follower node.

Moreover, all nodes $\mu$ must satisfy the four following conditions:

(i) For each non-initial value $v \neq \textbf{val}(\mu)$ of $\mathbf{lr}(\mu)$, $\mu$ has a child $\mu'$ which is a boss node such that $\ln_v(\mathbf{lr}(\mu))$ is a subword of $\mathbf{bw}(\mu')$.

(ii) For each initial value $v$ in $\mathbf{lr}(\mu)$, there is a decomposition
$\mathbf{dec} = (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$ s.t.:
- $\mathbf{lr}(\mu)$ may be split into successive local runs $u_0, \dots, u_\ell$ where, for all $i \in [1, \ell]$, $w_i \le \text{Out}_v(u_i)$ and $\ln_v(u_i) \in \{m_1, \dots, m_{i-1}\}^*$,
- for all $i \in [1, \ell]$, $\mu$ has a child $\mu_i$ which is a follower node such that $\mathbf{fm}(\mu_i) = m_i$ and $\mathbf{fw}(\mu_i) \in \mathcal{L}^{\text{dec}_i}$ where $\mathbf{dec}_i = (w_0, m_1, w_1, \dots, m_{i-1}, w_{i-1})$.

(iii) If $\mu$ is a follower node then $\textbf{val}(\mu)$ is not an initial value of $u$, $\ln_{\textbf{val}(\mu)}(u) \le \textbf{fw}(\mu)$ and $\text{Out}_{\textbf{val}(\mu)}(u)$ contains $\mathbf{fm}(\mu)$.

(iv) If $\mu$ is a boss node, then $\textbf{val}(\mu)$ is an initial value of $\mathbf{lr}(\mu)$ and the decomposition $\mathbf{dec}$ of (ii) for $\textbf{val}(\mu)$ satisfies that $\mathbf{bw}(\mu) \in \mathcal{L}^{\text{dec}}$.

Lastly, as before, given $\tau$ an unfolding tree, we define its size by $|\tau| := \sum_{\mu \in \tau} |\mathbf{lr}(\mu)| + |\mathbf{spec}(\mu)| + 1$.

We now explain this definition. Let $\mu$ be a node of an unfolding tree $\tau$ and let $u := \mathbf{lr}(\mu)$. As before, $u$ encodes the local run of a given agent, $\mathbf{spec}(\mu)$ encodes the specification that this local run carries out and $\mathbf{val}(\mu)$ encodes the value for which the specification is carried out.

Conditions (i) and (ii) state that the specifications of the children of $\mu$ are witnesses that messages received in the local run $\mathbf{lr}(\mu)$ can be broadcast by other agents. Conditions (iii) and (iv) state that $\mu$ is a witness that its specification is carried out.

As before, condition (i) expresses that, for every non-initial value $v$ of $u$, $\mu$ must have a boss child witnessing that $\ln_v(u)$ can indeed be broadcast. Because $v$ was first stored by a reception step of $u$, any other (fresh) value with sequence of message types containing $\ln_v(u)$ also works and we do not impose the value label of this child to be $v$.

We now explain condition (ii), which states the existence of a decomposition for each initial value, which serves as a summary of the broadcasts made with that value. Let $v$ be an initial value of $u$. Consider a run where $u$ is the local run of agent $a$. If another agent broadcasts with value $v$, it has first received and stored $v$. By duplicating agents, we may afterwards assume that we have an unlimited supply of messages $(m, v)$. Therefore the crucial information is the times at which each message type is first broadcast with $v$ by an agent other than $a$.

The decomposition $\mathbf{dec} = (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$ should be understood as follows: In the run we are representing, $a$ first broadcasts messages of $w_0$ with value $v$, after which other agents are able to broadcast $(m_1, v)$. Then $a$ broadcasts $w_1$ (and may receive $m_1$), after which other agents can broadcast $(m_2, v)$, and
so on. To sustain that description, we need to be able to split $u$ into $u_0, \dots, u_\ell$, with each $u_i$ broadcasting $w_i$ and only receiving messages $m_1, \dots, m_{i-1}$ over value $v$. We also need a follower child for each $m_i$ to witness that other agents may broadcast it. For every $i$, the sequence of messages available with value $v$ during $u_i$ is $\text{Out}_v(u_i)$ expanded by freely adding symbols from $\{m_1, \dots, m_{i-1}\}$. Therefore, the follower child $\mu_i$ responsible for the broadcast of $(m_i, v)$ may first receive with value $v$ a subword of $w_0' \cdot w_1' \cdots w_{i-1}'$ where, for all $j \le i-1$, $w_j$ is obtained from $\text{Out}_v(u_i)$ by adding symbols from $\{m_1, \dots, m_{j-1}\}$, which we state as $\text{fw}(\mu_i) \in \mathcal{L}^{\text{dec}_i}$.

Condition (iii) directly states that a follower node $\mu$ receives word $\text{fw}(\mu)$ with value $\text{val}(\mu)$ and broadcasts message $(\text{fm}(\mu), \text{val}(\mu))$. Condition (iv) expresses that a boss node witnesses the broadcast of a sequence of messages $\text{bw}(\mu)$ with a single value; whereas in the signature protocol case, in this sequence, some messages may come from auxiliary agents encoded in follower children, which is why we have the condition that $\text{bw}(\mu) \in \mathcal{L}^{\text{dec}}$ and not simply $\text{Out}_{\text{val}(\mu)}(u) \preceq \text{bw}(\mu)$.

## C Proof of Proposition 24

**Proposition 24.** An instance of COVER ($\mathcal{P}$, $q_f$) is positive if and only if there exists a coverability witness for that instance.

We make the meaning of the specification labels more concrete by defining the criteria for an initial run to satisfy a specification.

- A run $\rho$ satisfies a boss specification $\text{bw}$ if there exists $v \in \mathbb{N}$ such that $\text{bw}$ is a subword of the sequence of messages sent with value $v$ in $\rho$.

- A run $\rho$ satisfies a follower specification $(\text{fw}, \text{fm})$ if there exist a value $v$ and an agent $a$ such that $v$ is not an initial value of $a$, the $v$-input of $a$ in $\rho$ is a subword of $\text{fw}$ and agent $a$ broadcasts $\text{fm}$ with value $v$ at some point.

For an unfolding tree, satisfying a specification simply means that its root is labeled with that specification or a better one.

- An unfolding tree satisfies a boss specification $\text{bw}$ if its root $\mu$ is a boss node and $\text{bw}$ is a subword of its specification label $\text{bw}(\mu)$.

- An unfolding tree satisfies a follower specification $(\text{fw}, \text{fm})$ if its root $\mu$ is a follower node such that $\text{fm} = \text{fm}(\mu)$ and $\text{fw}(\mu)$ is a subword of $\text{fw}$.

Note that COVER reduces to the existence of an initial run satisfying a boss specification: it suffices to consider $\mathcal{M}' := \mathcal{M} \cup \{m_f\}$ with $m_f \notin \mathcal{M}$ and to add a loop on $q_f$ broadcasting $m_f$. Therefore, it suffices to prove that initial runs of $\mathcal{P}$ and unfolding trees satisfy the same boss specifications. We prove the two directions in the two following sections: we construct an unfolding tree from a run in Section C.1 and a run from an unfolding tree in Section C.2.
so on. To sustain that description, we need to be able to split $u$ into $u_0, \dots, u_\ell$, with each $u_i$ broadcasting $w_i$ and only receiving messages $m_1, \dots, m_{i-1}$ over value $v$. We also need a follower child for each $m_i$ to witness that other agents may broadcast it. For every $i$, the sequence of messages available with value $v$ during $u_i$ is $\text{Out}_v(u_i)$ expanded by freely adding symbols from $\{m_1, \dots, m_{i-1}\}$. Therefore, the follower child $\mu_i$ responsible for the broadcast of $(m_i, v)$ may first receive with value $v$ a subword of $w'_0 \cdot w'_1 \cdots w'_{i-1}$ where, for all $j \le i-1$, $w_j$ is obtained from $\text{Out}_v(u_i)$ by adding symbols from $\{m_1, \dots, m_{j-1}\}$, which we state as $\text{fw}(\mu_i) \in \mathcal{L}^{\text{dec}_i}$.

Condition (iii) directly states that a follower node $\mu$ receives word $\text{fw}(\mu)$ with value $\text{val}(\mu)$ and broadcasts message $(\text{fm}(\mu), \text{val}(\mu))$. Condition (iv) expresses that a boss node witnesses the broadcast of a sequence of messages $\text{bw}(\mu)$ with a single value; whereas in the signature protocol case, in this sequence, some messages may come from auxiliary agents encoded in follower children, which is why we have the condition that $\text{bw}(\mu) \in \mathcal{L}^{\text{dec}}$ and not simply $\text{Out}_{\text{val}(\mu)}(u) \preceq \text{bw}(\mu)$.

C Proof of Proposition 24

**Proposition 24.** An instance of COVER ($\mathcal{P}$, $q_f$) is positive if and only if there exists a coverability witness for that instance.

We make the meaning of the specification labels more concrete by defining the criteria for an initial run to satisfy a specification.

- A run $\rho$ satisfies a boss specification $\mathbf{bw}$ if there exists $v \in \mathbb{N}$ such that $\mathbf{bw}$ is a subword of the sequence of messages sent with value $v$ in $\rho$.

- A run $\rho$ satisfies a follower specification $(\text{fw}, \text{fm})$ if there exist a value $v$ and an agent $a$ such that $v$ is not an initial value of $a$, the $v$-input of $a$ in $\rho$ is a subword of $\text{fw}$ and agent $a$ broadcasts $\text{fm}$ with value $v$ at some point.

For an unfolding tree, satisfying a specification simply means that its root is labeled with that specification or a better one.

- An unfolding tree satisfies a boss specification $\mathbf{bw}$ if its root $\mu$ is a boss node and $\mathbf{bw}$ is a subword of its specification label $\mathbf{bw}(\mu)$.

- An unfolding tree satisfies a follower specification $(\text{fw}, \text{fm})$ if its root $\mu$ is a follower node such that $\text{fm} = \text{fm}(\mu)$ and $\text{fw}(\mu)$ is a subword of $\text{fw}$.

Note that COVER reduces to the existence of an initial run satisfying a boss specification: it suffices to consider $\mathcal{M}' := \mathcal{M} \cup \{m_f\}$ with $m_f \notin \mathcal{M}$ and to add a loop on $q_f$ broadcasting $m_f$. Therefore, it suffices to prove that initial runs of $\mathcal{P}$ and unfolding trees satisfy the same boss specifications. We prove the two directions in the two following sections: we construct an unfolding tree from a run in Section C.1 and a run from an unfolding tree in Section C.2.
### C.1 Construction of an unfolding tree from an initial run

**Lemma 32.** If there exists an initial run $\rho$ of $\mathcal{P}$ satisfying some specification spec then there exists a finite unfolding tree $\tau$ over $\mathcal{P}$ satisfying spec.

*Proof.* We proceed by strong induction on $\mathbb{N} \times \{\text{follower, boss}\}$ ordered by lexicographic order (follower being lower than boss). The first component is the length of the run and the second component is the type of specification. This means that, for a fixed run length, we prove our property for boss specifications then for follower specifications.

If $\rho$ is of length 0, then its specification must be an empty boss specification and the tree with a single node labeled with an empty local run and an empty specification satisfies it.

Let $\rho$ be an initial run, and assume that the property is true for initial runs whose length is less than the one of $\rho$. Write $\mathbb{A}$ the set of agents of $\rho$. Because $\rho$ satisfies spec, there exist a value $v$ and an agent $a$ in $\rho$ such that:

- if spec is a boss specification $bw$, $bw$ is a subword of the sequence of message types sent with value $v$ in $\rho$ and $a$ is the agent which has $v$ as an initial value,

- if spec is a follower specification ($fw, fm$), then $a$ is an agent whose $v$-input is a subword of $fw$ and that broadcasts $fm$ with value $v$.

If the last step of $u$ does not include a broadcast with value $v$, then we remove it and apply the induction hypothesis. Assume that the last step of $\rho$ involves a broadcast with value $v$. Let $u$ the local run of $a$ in $\rho$. We set the root $\mu$ of our tree $\tau$ to have local run $u$, value $v$ and specification spec as labels, and attach subtrees to it so that it forms an unfolding tree.

We do the following for every value $v'$ in $u$. If $v'$ is non-initial in $u$ and $v' \neq v$, because the last step of $\rho$ is a broadcast with value $v$, we apply the induction hypothesis on $\rho$ without its last step to obtain an unfolding tree $\tau'$ whose root is a boss node with boss specification $\ln_{v'}(u)$, and we attach $\tau'$ below $\mu$ in $\tau$. If $v' = v$ and $v'$ is non-initial then spec is a follower specification and we do not need to add any children, as the $v'$-input of $u$ is covered by the specification. Assume now that $v'$ is initial in $u$. We split $\rho$ according to the first broadcast of each message type by agents other than $a$; we obtain $m_1, \dots, m_\ell \in \mathcal{M}$ distinct message types such that $\rho = \rho_0 \cdot \rho_1 \cdot \dots \cdot \rho_\ell$ where, for all $i \in [1, l]$:

- agents from $\mathbb{A} \setminus \{a\}$ do not broadcast $m_i$ with value $v'$ in $\rho_0 \cdot \dots \cdot \rho_{i-1}$,

- $\rho_i$ starts with a broadcast of $m_i$ with value $v'$ by some agent $a_i \in \mathbb{A} \setminus \{a\}$.

Let $w_i$ the sequence broadcast by $a$ with value $v'$ in $\rho_i$. This forms a decomposition $\text{dec} := (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$. For all $i \in [1, \ell]$, we write $\text{dec}_i$ for the decomposition $\text{dec}_i = (w_0, m_1, w_1, \dots, m_{i-1}, w_{i-1})$. For every $i \in [1, \ell - 1]$, let $\tilde{\rho}_i$ the run $\rho_0 \cdot \dots \cdot \rho_{i-1}$ plus the first step of $\rho_i$ (where $(m_i, v')$ is broadcast). Let $w'_i$ the $v'$-input of $a_i$ in $\tilde{\rho}_i$: it is in $\mathcal{L}^{\text{dec}_i}$ by construction of $\text{dec}$. Agent $a_i$ is a witness that $\tilde{\rho}_i$ satisfies follower specification $(w'_i, m_i)$. If $\tilde{\rho}_i$ is smaller than $\rho$, we apply the induction hypothesis and obtain an unfolding tree $\tau_i$ satisfying
## C.1 Construction of an unfolding tree from an initial run

**Lemma 32.** If there exists an initial run $\rho$ of $\mathcal{P}$ satisfying some specification spec then there exists a finite unfolding tree $\tau$ over $\mathcal{P}$ satisfying spec.

*Proof.* We proceed by strong induction on $\mathbb{N} \times \{\text{follower, boss}\}$ ordered by lexicographic order (follower being lower than boss). The first component is the length of the run and the second component is the type of specification. This means that, for a fixed run length, we prove our property for boss specifications then for follower specifications.

If $\rho$ is of length 0, then its specification must be an empty boss specification and the tree with a single node labeled with an empty local run and an empty specification satisfies it.

Let $\rho$ be an initial run, and assume that the property is true for initial runs whose length is less than the one of $\rho$. Write $\mathbb{A}$ the set of agents of $\rho$. Because $\rho$ satisfies spec, there exist a value $v$ and an agent $a$ in $\rho$ such that:

- if spec is a boss specification $bw$, $bw$ is a subword of the sequence of message types sent with value $v$ in $\rho$ and $a$ is the agent which has $v$ as an initial value,

- if spec is a follower specification ($fw, fm$), then $a$ is an agent whose $v$-input is a subword of $fw$ and that broadcasts $fm$ with value $v$.

If the last step of $u$ does not include a broadcast with value $v$, then we remove it and apply the induction hypothesis. Assume that the last step of $\rho$ involves a broadcast with value $v$. Let $u$ the local run of $a$ in $\rho$. We set the root $\mu$ of our tree $\tau$ to have local run $u$, value $v$ and specification spec as labels, and attach subtrees to it so that it forms an unfolding tree.

We do the following for every value $v'$ in $u$. If $v'$ is non-initial in $u$ and $v' \neq v$, because the last step of $\rho$ is a broadcast with value $v$, we apply the induction hypothesis on $\rho$ without its last step to obtain an unfolding tree $\tau'$ whose root is a boss node with boss specification $\ln_{v'}(u)$, and we attach $\tau'$ below $\mu$ in $\tau$. If $v' = v$ and $v'$ is non-initial then spec is a follower specification and we do not need to add any children, as the $v'$-input of $u$ is covered by the specification. Assume now that $v'$ is initial in $u$. We split $\rho$ according to the first broadcast of each message type by agents other than $a$; we obtain $m_1, \dots, m_\ell \in \mathcal{M}$ distinct message types such that $\rho = \rho_0 \cdot \rho_1 \cdot \dots \cdot \rho_\ell$ where, for all $i \in [1, l]$:

- agents from $\mathbb{A} \setminus \{a\}$ do not broadcast $m_i$ with value $v'$ in $\rho_0 \cdot \dots \cdot \rho_{i-1}$,

- $\rho_i$ starts with a broadcast of $m_i$ with value $v'$ by some agent $a_i \in \mathbb{A} \setminus \{a\}$.

Let $w_i$ the sequence broadcast by $a$ with value $v'$ in $\rho_i$. This forms a decomposition $\text{dec} := (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$. For all $i \in [1, \ell]$, we write $\text{dec}_i$ for the decomposition $\text{dec}_i = (w_0, m_1, w_1, \dots, m_{i-1}, w_{i-1})$. For every $i \in [1, \ell - 1]$, let $\tilde{\rho}_i$ the run $\rho_0 \cdot \dots \cdot \rho_{i-1}$ plus the first step of $\rho_i$ (where $(m_i, v')$ is broadcast). Let $w'_i$ the $v'$-input of $a_i$ in $\tilde{\rho}_i$: it is in $\mathcal{L}^{\text{dec}_i}$ by construction of $\text{dec}$. Agent $a_i$ is a witness that $\tilde{\rho}_i$ satisfies follower specification $(w'_i, m_i)$. If $\tilde{\rho}_i$ is smaller than $\rho$, we apply the induction hypothesis and obtain an unfolding tree $\tau_i$ satisfying
follower specification $(w'_i, m_i)$. If $\tilde{\rho}_i = \rho$, then $i = \ell$, $v' = v$ ($\rho$ ends with a broadcast with value $v$) and $\rho$ ends with a broadcast $(m_\ell, v)$ by agent $a_\ell$. Moreover, since $v' = v$, $v$ is initial for $a$ and spec is a boss specification bw. Because in our induction order boss specifications are above follower specifications, we can apply the induction hypothesis and obtain an unfolding tree $\tau_\ell$ satisfying follower specification $(w'_\ell, m_\ell)$. We have obtained, for every $i \in [1, \ell]$, an unfolding tree $\tau_i$ satisfying follower specification $(w'_i, m_i)$, which we attach below $\mu$.

Overall we have attached one boss node below $\mu$ for each non-initial value in $u$ (except $v$ if $\mu$ is a follower node), thanks to which (i) is satisfied at $\mu$, and there are well-chosen follower nodes below $\mu$ for each initial value in $u$, thanks to which (ii) is satisfied as well. Conditions (iii) and (iv) hold because $\rho$ satisfies spec for agent $a$. We have therefore built an unfolding tree $\tau$ satisfying spec. $\square$

## C.2 Construction of an initial run from an unfolding tree

**Lemma 33.** If there exists an unfolding tree over $\mathcal{P}$ satisfying a boss specification bw $\in \mathcal{M}^*$ then there exists an initial run $\rho$ of $\mathcal{P}$ satisfying bw.

We start by defining partial runs, which are runs where some receptions are not matched by broadcasts. Intuitively, this will allow us to build partial runs from unfolding trees whose root is a follower node, which implicitly rely on their parent for some broadcasts. We will therefore construct inductively partial runs from nodes of the tree; we will obtain complete runs by matching reception and broadcasts of different partial runs.

**Definition 34.** Let $\gamma, \gamma'$ two configurations.

A partial step $\gamma \to_p \gamma'$ is defined if either $\gamma \to \gamma'$ (normal step) or there exist $m \in \mathcal{M}$, $v \in \mathbb{N}$ such that for all agent $a$ either $\gamma(a) = \gamma'(a)$ or $\gamma(a) \xrightarrow{\text{ext}(\delta, v)} \gamma'(a)$ with $\delta$ a transition receiving message type $m$ (unmatched reception).

A partial run is a sequence of partial steps. Note that a local run can be seen as a partial run with a single agent. A partial run is initial if it starts in an initial configuration. The v-input $\text{ln}_v(\rho)$ of a partial run $\rho$ is the sequence $m_0 \cdots m_k$ of message types corresponding to unmatched receptions with value $v$ in $\rho$. Its v-output $\text{Out}_v(\rho)$ is the sequence of message types corresponding to broadcasts with value $v$ in $\rho$.

We will prove the following, more general version of Lemma 33:

**Lemma 35.** For every unfolding tree $\tau$:

- if $\tau$ satisfies a boss specification bw $\in \mathcal{M}^*$, then there exists an initial run $\rho$ satisfying bw,

- if $\tau$ satisfies a follower specification (fw, fm) then there exist an initial partial run $\rho$ and a value $v$ such that:

* all unmatched receptions in $\rho$ are with value $v$,

* $\text{ln}_v(\rho) \le$ fw,

* $\text{Out}_v(\rho)$ contains fm.
follower specification $(w'_i, m_i)$. If $\tilde{\rho}_i = \rho$, then $i = \ell$, $v' = v$ ($\rho$ ends with a broadcast with value $v$) and $\rho$ ends with a broadcast $(m_\ell, v)$ by agent $a_\ell$. Moreover, since $v' = v$, $v$ is initial for $a$ and spec is a boss specification bw. Because in our induction order boss specifications are above follower specifications, we can apply the induction hypothesis and obtain an unfolding tree $\tau_\ell$ satisfying follower specification $(w'_\ell, m_\ell)$. We have obtained, for every $i \in [1, \ell]$, an unfolding tree $\tau_i$ satisfying follower specification $(w'_i, m_i)$, which we attach below $\mu$.

Overall we have attached one boss node below $\mu$ for each non-initial value in $u$ (except $v$ if $\mu$ is a follower node), thanks to which (i) is satisfied at $\mu$, and there are well-chosen follower nodes below $\mu$ for each initial value in $u$, thanks to which (ii) is satisfied as well. Conditions (iii) and (iv) hold because $\rho$ satisfies spec for agent $a$. We have therefore built an unfolding tree $\tau$ satisfying spec. $\square$

## C.2 Construction of an initial run from an unfolding tree

**Lemma 33.** If there exists an unfolding tree over $\mathcal{P}$ satisfying a boss specification bw $\in \mathcal{M}^*$ then there exists an initial run $\rho$ of $\mathcal{P}$ satisfying bw.

We start by defining partial runs, which are runs where some receptions are not matched by broadcasts. Intuitively, this will allow us to build partial runs from unfolding trees whose root is a follower node, which implicitly rely on their parent for some broadcasts. We will therefore construct inductively partial runs from nodes of the tree; we will obtain complete runs by matching reception and broadcasts of different partial runs.

**Definition 34.** Let $\gamma, \gamma'$ two configurations.

A partial step $\gamma \to_p \gamma'$ is defined if either $\gamma \to \gamma'$ (normal step) or there exist $m \in \mathcal{M}$, $v \in \mathbb{N}$ such that for all agent $a$ either $\gamma(a) = \gamma'(a)$ or $\gamma(a) \xrightarrow{\text{ext}(\delta, v)} \gamma'(a)$ with $\delta$ a transition receiving message type $m$ (unmatched reception).

A partial run is a sequence of partial steps. Note that a local run can be seen as a partial run with a single agent. A partial run is initial if it starts in an initial configuration. The v-input $\text{ln}_v(\rho)$ of a partial run $\rho$ is the sequence $m_0 \cdots m_k$ of message types corresponding to unmatched receptions with value $v$ in $\rho$. Its v-output $\text{Out}_v(\rho)$ is the sequence of message types corresponding to broadcasts with value $v$ in $\rho$.

We will prove the following, more general version of Lemma 33:

**Lemma 35.** For every unfolding tree $\tau$:

- if $\tau$ satisfies a boss specification bw $\in \mathcal{M}^*$, then there exists an initial run $\rho$ satisfying bw,

- if $\tau$ satisfies a follower specification (fw, fm) then there exist an initial partial run $\rho$ and a value $v$ such that:

* all unmatched receptions in $\rho$ are with value $v$,

* $\text{ln}_v(\rho) \le$ fw,

* $\text{Out}_v(\rho)$ contains fm.
*Proof.* We prove it by induction on the size of the unfolding tree. Let $\tau$ be a unfolding tree, $\mu$ its root, $u := \text{lr}(\mu)$ and $V$ the set of values appearing in $u$. We will combine $u$ with runs given by children of $\mu$ to construct $\rho$ satisfying the desired property. We build $\rho$ inductively in two steps.

**Step 1: Non-initial Values** For each non-initial value $v \neq \text{val}(\mu)$ of $u$, $\mu$ has a boss child of specification $w$ such that $\ln_v(u) \preceq w$. By induction hypothesis, there is an initial run $\rho'$ satisfying boss specification $w$. Up to renaming agents, assume that $\rho$ and $\rho'$ have disjoint agents. We rename values in $\rho'$ so that $w$ is broadcast in $\rho'$ with value $v$, and $\rho'$ has no other shared value with $\rho$. We use the broadcasts made by $\rho'$ to match the unmatched receptions with value $v$ in $\rho$: this gives us a new partial run $\rho$ with no unmatched reception with value $v$ and whose behaviour on other values of $V$ is the same as before.

**Step 2: Initial Values** Let $v$ be an initial value of $u$, and $\text{dec} = (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$ the decomposition from condition (ii). We have that, for all $j \in [1, \ell]$, $\mu$ has a follower child $\mu_j$ labelled by $\text{fm}(\mu_j) = m_j$ and $\text{fw}(\mu_j) \in \mathcal{L}^{\text{dec}_j}$ with $\text{dec}_j = (w_0, m_1, w_1, \dots, m_{j-1}, w_{j-1})$.

The behavior of the run $\rho$ with respect to $v$ is the one of $u$, as we have not added any broadcasts or receptions with $v$. Hence we can split $\rho$ into $\rho_0, \dots, \rho_\ell$ with $w_i \preceq \text{Out}_v(\rho_i)$ and $\ln_v(\rho_i) \in \{m_1, \dots, m_i\}^*$ for all $i$.

By induction hypothesis applied to $\mu_j$, for all $j$, there exists an initial partial run $\tilde{\rho}_j$ whose only unmatched receptions are on $v$, $\ln_v(\tilde{\rho}_j) \preceq \text{fw}(\mu_j)$ and such that $\tilde{\rho}_j$ broadcasts $(m_j, v)$ in its last step. Again, we rename agents and values so that the sets of agents of $\rho$ and of every $\tilde{\rho}_j$ are all disjoint and the only shared value between any of these runs is $v$. As $\text{fw}(\mu_j) \in \mathcal{L}^{\text{dec}_j}$ and $\ln_v(\tilde{\rho}_j) \preceq \text{fw}(\mu_j)$, we can split $\tilde{\rho}_j$ into $\tilde{\rho}_{j,0}, \dots, \tilde{\rho}_{j,j-1}$ so that $\ln_v(\tilde{\rho}_{j,i}) \preceq \tilde{w}_{j,i}$ where $\tilde{w}_{j,i}$ can be obtained by adding letters from $\{m_1, \dots, m_j\}$ to $w_i$.

We use the following composition operation: consider $\rho$ and one of the $\tilde{\rho}_j$. We can design a new run in which we execute both runs in parallel over disjoint sets of agents. We match each $\tilde{\rho}_{j,i}$ with $\rho_i$ so that the broadcasts of $\rho_i$ with value $v$ forming $w_i$ are received in $\tilde{\rho}_{j,i}$ and the only remaining missing broadcasts in that section of the run are of $m_1, \dots, m_i$. We obtain a run section whose $v$-output still contains $w_i$ and whose $v$-input only contains $m_1, \dots, m_i$. This lets us get to a point where the next step in $\tilde{\rho}_j$ is a broadcast $(m_j, v)$ and $\rho$ has been executed up to the beginning of $\rho_j$. We may then use the $(m_j, v)$ broadcast at any moment in the rest of $\rho$ either to complete an unmatched reception or to extend the $v$-output of $\rho$.

This construction is illustrated in Figure

The resulting run $\rho'$ can still be split into $\rho'_0 \cdots \rho'_\ell$ where $w_i \preceq \text{Out}_v(\rho_i)$ and $\ln_v(\rho_i) \in \{m_1, \dots, m_i\}^*$ for all $i$. Its input on all values other than $v$ is the same as the one of $\rho$. This procedure can thus be iterated.

If $v = \text{val}(\mu)$ then we have $\text{bw}(\mu) \in \mathcal{L}^{\text{dec}}$, and we need to ensure that $\text{bw}(\mu)$ is broadcast in $\rho$ with value $v$. Let $\text{bw}_0, \dots, \text{bw}_\ell$ such that $\text{bw}(\mu) \preceq \text{bw}_0 \cdots \text{bw}_\ell$ and for all $j$, $\text{bw}_j$ can be obtained by adding letters from $\{m_1, \dots, m_j\}$ in $w_j$. We
*Proof.* We prove it by induction on the size of the unfolding tree. Let $\tau$ be a unfolding tree, $\mu$ its root, $u := \text{lr}(\mu)$ and $V$ the set of values appearing in $u$. We will combine $u$ with runs given by children of $\mu$ to construct $\rho$ satisfying the desired property. We build $\rho$ inductively in two steps.

**Step 1: Non-initial Values** For each non-initial value $v \neq \text{val}(\mu)$ of $u$, $\mu$ has a boss child of specification $w$ such that $\ln_v(u) \preceq w$. By induction hypothesis, there is an initial run $\rho'$ satisfying boss specification $w$. Up to renaming agents, assume that $\rho$ and $\rho'$ have disjoint agents. We rename values in $\rho'$ so that $w$ is broadcast in $\rho'$ with value $v$, and $\rho'$ has no other shared value with $\rho$. We use the broadcasts made by $\rho'$ to match the unmatched receptions with value $v$ in $\rho$: this gives us a new partial run $\rho$ with no unmatched reception with value $v$ and whose behaviour on other values of $V$ is the same as before.

**Step 2: Initial Values** Let $v$ be an initial value of $u$, and $\text{dec} = (w_0, m_1, w_1, \dots, m_\ell, w_\ell)$ the decomposition from condition (ii). We have that, for all $j \in [1, \ell]$, $\mu$ has a follower child $\mu_j$ labelled by $\text{fm}(\mu_j) = m_j$ and $\text{fw}(\mu_j) \in \mathcal{L}^{\text{dec}_j}$ with $\text{dec}_j = (w_0, m_1, w_1, \dots, m_{j-1}, w_{j-1})$.

The behavior of the run $\rho$ with respect to $v$ is the one of $u$, as we have not added any broadcasts or receptions with $v$. Hence we can split $\rho$ into $\rho_0, \dots, \rho_\ell$ with $w_i \preceq \text{Out}_v(\rho_i)$ and $\ln_v(\rho_i) \in \{m_1, \dots, m_i\}^*$ for all $i$.

By induction hypothesis applied to $\mu_j$, for all $j$, there exists an initial partial run $\tilde{\rho}_j$ whose only unmatched receptions are on $v$, $\ln_v(\tilde{\rho}_j) \preceq \text{fw}(\mu_j)$ and such that $\tilde{\rho}_j$ broadcasts $(m_j, v)$ in its last step. Again, we rename agents and values so that the sets of agents of $\rho$ and of every $\tilde{\rho}_j$ are all disjoint and the only shared value between any of these runs is $v$. As $\text{fw}(\mu_j) \in \mathcal{L}^{\text{dec}_j}$ and $\ln_v(\tilde{\rho}_j) \preceq \text{fw}(\mu_j)$, we can split $\tilde{\rho}_j$ into $\tilde{\rho}_{j,0}, \dots, \tilde{\rho}_{j,j-1}$ so that $\ln_v(\tilde{\rho}_{j,i}) \preceq \tilde{w}_{j,i}$ where $\tilde{w}_{j,i}$ can be obtained by adding letters from $\{m_1, \dots, m_j\}$ to $w_i$.

We use the following composition operation: consider $\rho$ and one of the $\tilde{\rho}_j$. We can design a new run in which we execute both runs in parallel over disjoint sets of agents. We match each $\tilde{\rho}_{j,i}$ with $\rho_i$ so that the broadcasts of $\rho_i$ with value $v$ forming $w_i$ are received in $\tilde{\rho}_{j,i}$ and the only remaining missing broadcasts in that section of the run are of $m_1, \dots, m_i$. We obtain a run section whose $v$-output still contains $w_i$ and whose $v$-input only contains $m_1, \dots, m_i$. This lets us get to a point where the next step in $\tilde{\rho}_j$ is a broadcast $(m_j, v)$ and $\rho$ has been executed up to the beginning of $\rho_j$. We may then use the $(m_j, v)$ broadcast at any moment in the rest of $\rho$ either to complete an unmatched reception or to extend the $v$-output of $\rho$.

This construction is illustrated in Figure

The resulting run $\rho'$ can still be split into $\rho'_0 \cdots \rho'_\ell$ where $w_i \preceq \text{Out}_v(\rho_i)$ and $\ln_v(\rho_i) \in \{m_1, \dots, m_i\}^*$ for all $i$. Its input on all values other than $v$ is the same as the one of $\rho$. This procedure can thus be iterated.

If $v = \text{val}(\mu)$ then we have $\text{bw}(\mu) \in \mathcal{L}^{\text{dec}}$, and we need to ensure that $\text{bw}(\mu)$ is broadcast in $\rho$ with value $v$. Let $\text{bw}_0, \dots, \text{bw}_\ell$ such that $\text{bw}(\mu) \preceq \text{bw}_0 \cdots \text{bw}_\ell$ and for all $j$, $\text{bw}_j$ can be obtained by adding letters from $\{m_1, \dots, m_j\}$ in $w_j$. We
<figure><img src="image_9.png" /></figure>

<figure><img src="image_10.png" /></figure>

We compose $\mathrm{lr}(\mu)$ with $\rho_2$ to obtain a partial run $\rho'$ which outputs the desired word $aac$

<figure><img src="image_11.png" /></figure>

We compose $\rho'$ with $\rho_2$ to match an unmatched reception $b$

... and iterate compositions with $\rho_1$ and $\rho_2$ until the run does not have any unmatched reception.

<caption>Fig. 8: An illustration of the composition operation from the proof of Lemma 33</caption>

use the composition operation to extend the output of $\rho$, so that $bw_i \preceq \mathrm{Out}_v(\rho_i)$ for all $i$.

Then, in all cases, we apply the composition as many times as necessary to match the unmatched receptions: while there is an unmatched reception of some $(m_j, v)$ we compose $\rho$ with $\tilde{\rho}_j$ to eliminate it. We may be adding some unmatched receptions of $(m_i, v)$ for some $i < j$. This procedure terminates as the number of unmatched receptions of $m_\ell, \dots, m_1$ decreases at each iteration for the lexicographic ordering.

In the end we obtain a run $\rho$ with no unmatched reception on $v$, and such that, if $v = \mathrm{val}(\mu)$ and $\mu$ is a boss node, $bw(\mu) \preceq \mathrm{Out}_v(\rho)$.

**Concluding the procedure** We distinguish two cases depending on the type of specification of $\mu$.

- If $\mu$ is a boss node of boss specification $bw$, we apply steps 1 and 2 to every value in $V$, which can be done because $\mathrm{val}(\mu)$ is initial in $u$. We then obtain an initial run $\rho$ with no unmatched receptions satisfying boss specification $bw$ for value $\mathrm{val}(\mu)$.

- if $\mu$ is a follower node, we apply steps 1 and 2 to every value in $V \setminus \{\mathrm{val}(\mu)\}$ to obtain a partial run $\rho$ with no unmatched reception on values different from $\mathrm{val}(\mu)$. Moreover, because the behavior of $\rho$ with respect to $\mathrm{val}(\mu)$ is
$$
\begin{array}{ccc}
\text{lr}(\mu) & \xrightarrow{\substack{\mathbf{br}(a) \\ \mathbf{rec}(b)}} & \rho_1 \xrightarrow{\substack{\mathbf{br}(b) \\ \mathbf{rec}(a)}} \rho_2 \xrightarrow{\substack{\mathbf{br}(c) \\ \mathbf{rec}(a)\mathbf{rec}(b)}} \\
& & \\
& \mathbf{bw}(\mu) = \text{aac} & \rho_1 \text{ satisfies } (a, b) \qquad \rho_2 \text{ satisfies } (ab, c) \\
& \mathbf{dec} = (a, b, a, c, \varepsilon) & \mathbf{dec}_1 = (a) \qquad \mathbf{dec}_2 = (a, b, a)
\end{array}
$$

<figure><img src="image_9.png" /></figure>

We compose $\text{lr}(\mu)$ with $\rho_2$
to obtain a partial run $\rho'$
which outputs the desired
word $aac$

<figure><img src="image_10.png" /></figure>

We compose $\rho'$ with $\rho_2$ to
match an unmatched recep-
tion $b$

... and iterate compositions
with $\rho_1$ and $\rho_2$ until the
run does not have any un-
matched reception.

<caption>Fig. 8: An illustration of the composition operation from the proof of Lemma 33</caption>

use the composition operation to extend the output of $\rho$, so that $bw_i \preceq \text{Out}_v(\rho_i)$ for all $i$.

Then, in all cases, we apply the composition as many times as necessary to match the unmatched receptions: while there is an unmatched reception of some $(m_j, v)$ we compose $\rho$ with $\tilde{\rho}_j$ to eliminate it. We may be adding some unmatched receptions of $(m_i, v)$ for some $i < j$. This procedure terminates as the number of unmatched receptions of $m_\ell, \dots, m_1$ decreases at each iteration for the lexicographic ordering.

In the end we obtain a run $\rho$ with no unmatched reception on $v$, and such that, if $v = \text{val}(\mu)$ and $\mu$ is a boss node, $bw(\mu) \preceq \text{Out}_v(\rho)$.

**Concluding the procedure** We distinguish two cases depending on the type of specification of $\mu$.

- If $\mu$ is a boss node of boss specification $bw$, we apply steps 1 and 2 to every value in $V$, which can be done because $\text{val}(\mu)$ is initial in $u$. We then obtain an initial run $\rho$ with no unmatched receptions satisfying boss specification $bw$ for value $\text{val}(\mu)$.

- if $\mu$ is a follower node, we apply steps 1 and 2 to every value in $V \setminus \{\text{val}(\mu)\}$ to obtain a partial run $\rho$ with no unmatched reception on values different from $\text{val}(\mu)$. Moreover, because the behavior of $\rho$ with respect to $\text{val}(\mu)$ is
the one of $u$, we have that $\ln_{\text{val}(\mu)}(\rho) \preceq \text{fw}$ and $\text{Out}_{\text{val}(\mu)}(\rho)$ contains $\text{fm}$,
concluding the proof.
$\square$

D Proof of Lemma 25

**Lemma 25.** Let $\mu \neq \mu'$ be two nodes of $\tau$ such that $\mu$ is an ancestor of $\mu'$. If one of those conditions holds, then $\tau$ can be shortened (contradicting its minimality):

- $\mu$ and $\mu'$ are boss nodes with boss specifications respectively bw and bw', and bw $\preceq$ bw';

- $\mu$ and $\mu'$ are follower nodes with follower specifications respectively (fw, fm) and (fw', fm'), and fw' $\preceq$ fw and fm' = fm.

Proof. Let $\tau_\mu$, $\tau_{\mu'}$ be the subtrees rooted in $\mu$, $\mu'$ respectively. Let $\tau'$ be the tree obtained by replacing $\tau_\mu$ with $\tau_{\mu'}$; it is strictly smaller than $\tau$. We prove that $\tau'$ is an unfolding tree. The only problematic node is the parent of $\mu$ if it exists, because it does not have the same children in $\tau$ and in $\tau'$. Assume that $\mu$ is not the root of $\tau$, and let $\mu_p$ its parent in $\tau'$. The only problematic values are the ones that had $\mu$ as witness in conditions (i) (if $\mu$ is a boss node) and (ii) (if $\mu$ is a follower node). Let $v$ such a value. If $\mu$ is a boss node ($v$ is non-initial), we have $\ln_v(\text{lr}(\mu_p)) \preceq \text{bw}(\mu) \preceq \text{bw}(\mu')$ hence condition (i) is also satisfied. If $\mu$ is a follower node ($v$ is initial), then, reusing the notations of condition (ii), $\mu$ was such that $\text{fm}(\mu) = m_i$ and $\text{fw}(\mu) \in \mathcal{L}^{\text{dec}_i}$. In this case, we also have $\text{fm}(\mu') = m_i$ and, because $\text{fw}(\mu') \preceq \text{fw}(\mu)$ and $\mathcal{L}^{\text{dec}_i}$ is closed by subword, we have $\text{fw}(\mu') \in \mathcal{L}^{\text{dec}_i}$ and condition (ii) is satisfied. In both cases, $\tau'$ is an unfolding tree with the same root specification as $\tau$ hence a coverability witness.
$\square$

E Generalization of Lemma 19

**Lemma 26.** There exists a primitive recursive function $\psi$ such that, for every protocol $\mathcal{P}$ with $r$ registers, for all local runs $u_0 : (q_0, v_0) \stackrel{*}{\to} (q, v)$, $u : (q, v) \stackrel{*}{\to} (q', v')$, $u_f : (q', v') \stackrel{*}{\to} (q_f, v_f)$, there exists a local run $u' : (q, v) \stackrel{*}{\to} (q', v')$ with $|u'| \le \psi(|\mathcal{P}|, r)$ and for all $v' \in \mathbb{N}$:

1. if $v'$ appears in $u_0$, $u$, or $u_f$, $\ln_{v'}(u') \preceq \ln_{v'}(u)$,

2. otherwise, there exists $v \in \mathbb{N}$, not initial in $u_0$, such that $\ln_{v'}(u') \preceq \ln_v(u)$.

The function $\psi$ is actually not the same as in Lemma 19 although it is also a tower of exponentials.

We start by defining the notion of trace, which is a local run annotated with
received values. A *trace* is a sequence in ({ext(δ, v) | δ ∈ Δ, v ∈ N} ∪ {int(δ) |
δ ∈ Δ})*. The trace of a local run *u* is the trace tr(*u*) corresponding to the local
steps performed in *u*. Given a trace tr, we write (q, v) $\xrightarrow{\text{tr}}$ (q', v') when there
exists a local run of trace tr from (q, v) to (q', v').
the one of $u$, we have that $\ln_{\text{val}(\mu)}(\rho) \preceq \text{fw}$ and $\text{Out}_{\text{val}(\mu)}(\rho)$ contains $\text{fm}$,
concluding the proof.
$\square$

D Proof of Lemma 25

**Lemma 25.** Let $\mu \neq \mu'$ be two nodes of $\tau$ such that $\mu$ is an ancestor of $\mu'$. If one of those conditions holds, then $\tau$ can be shortened (contradicting its minimality):

- $\mu$ and $\mu'$ are boss nodes with boss specifications respectively bw and bw', and $bw \preceq bw'$;

- $\mu$ and $\mu'$ are follower nodes with follower specifications respectively (fw, fm) and (fw', fm'), and $fw' \preceq fw$ and $fm' = fm$.

*Proof.* Let $\tau_\mu$, $\tau_{\mu'}$ be the subtrees rooted in $\mu$, $\mu'$ respectively. Let $\tau'$ be the tree obtained by replacing $\tau_\mu$ with $\tau_{\mu'}$; it is strictly smaller than $\tau$. We prove that $\tau'$ is an unfolding tree. The only problematic node is the parent of $\mu$ if it exists, because it does not have the same children in $\tau$ and in $\tau'$. Assume that $\mu$ is not the root of $\tau$, and let $\mu_p$ its parent in $\tau'$. The only problematic values are the ones that had $\mu$ as witness in conditions (i) (if $\mu$ is a boss node) and (ii) (if $\mu$ is a follower node). Let $v$ such a value. If $\mu$ is a boss node ($v$ is non-initial), we have $\ln_v(\text{lr}(\mu_p)) \preceq \text{bw}(\mu) \preceq \text{bw}(\mu')$ hence condition (i) is also satisfied. If $\mu$ is a follower node ($v$ is initial), then, reusing the notations of condition (ii), $\mu$ was such that $\text{fm}(\mu) = m_i$ and $\text{fw}(\mu) \in \mathcal{L}^{\text{dec}_i}$. In this case, we also have $\text{fm}(\mu') = m_i$ and, because $\text{fw}(\mu') \preceq \text{fw}(\mu)$ and $\mathcal{L}^{\text{dec}_i}$ is closed by subword, we have $\text{fw}(\mu') \in \mathcal{L}^{\text{dec}_i}$ and condition (ii) is satisfied. In both cases, $\tau'$ is an unfolding tree with the same root specification as $\tau$ hence a coverability witness.
$\square$

E Generalization of Lemma 19

**Lemma 26.** *There exists a primitive recursive function $\psi$ such that, for every protocol $\mathcal{P}$ with $r$ registers, for all local runs $u_0 : (q_0, v_0) \stackrel{*}{\to} (q, v)$, $u : (q, v) \stackrel{*}{\to} (q', v')$, $u_f : (q', v') \stackrel{*}{\to} (q_f, v_f)$, there exists a local run $u' : (q, v) \stackrel{*}{\to} (q', v')$ with $|u'| \le \psi(|\mathcal{P}|, r)$ and for all $v' \in \mathbb{N}$:*

1. if $v'$ appears in $u_0$, $u$, or $u_f$, $\ln_{v'}(u') \preceq \ln_{v'}(u)$,

2. otherwise, there exists $v \in \mathbb{N}$, not initial in $u_0$, such that $\ln_{v'}(u') \preceq \ln_v(u)$.

The function $\psi$ is actually not the same as in Lemma 19 although it is also a tower of exponentials.

We start by defining the notion of trace, which is a local run annotated with
received values. A *trace* is a sequence in ({ext($\delta$, $v$) | $\delta \in \Delta$, $v \in \mathbb{N}$} ∪ {int($\delta$) | $\delta \in \Delta$})*. The trace of a local run *u* is the trace tr(*u*) corresponding to the local
steps performed in *u*. Given a trace tr, we write (*q*, *v*) $\xrightarrow{\text{tr}}$ (*q*', *v*') when there
exists a local run of trace tr from (*q*, *v*) to (*q*', *v*').
We actually prove a more general version of the lemma. The previous lemma
can be obtained simply by applying the following one with W the set of initial
values of u₀ (W then contains r values) and V the set of values appearing in u₀,
u or u_f.

**Lemma 36.** *There exists a primitive recursive function $\psi(n,r)$ such that, for every protocol $\mathcal{P}$ with $r$ registers per agent, for every local run $u : (q, v) \stackrel{*}{\to} (q', v')$ in $\mathcal{P}$, for every $V \subseteq \mathbb{N}$ finite such that $V$ contains all message values appearing in $u$, for every $W \subseteq V$, there exists a local run $u' : (q, v) \stackrel{*}{\to} (q', v')$ such that we have $\text{len}(u') \le \psi(|\mathcal{P}| - r + |W|, r)$ and:*

1. for all $v \in V$, $\ln_v(u') \le \ln_v(u)$,

2. for all $v' \in \mathbb{N} \setminus V$, there exists $v \in \mathbb{N} \setminus W$ such that $\ln_{v'}(u') \le \ln_v(u)$.

Intuitively, the set $V$ represents values that are already used and therefore
cannot be used as fresh values, and $W$ represents values that should not be
copied (e.g., initial values of the run). However, stating the lemma only with $W$
equal to the initial values in $u$ would not allow us to apply the lemma on $u$ an
infix local run of a larger local run $u'$, because the initial values in $u$ would not
correspond to the ones in $u'$. This is why we state the lemma for every $W \subseteq V$.

<figure><img src="image_12.png" /><figcaption>Fig. 9: Illustration of the proof of Lemma 26. $s \in \Delta^{2M}$ corresponds to the repeating sequence of transitions of length $2M$. Register 4 contains value $v \in W$. Because both sides have the same $\Theta$, they coincide on values in $W$ such as $v$; only values that are not in $W$ are replaced by fresh values, hence $v$ is kept in the shortened local run.</figcaption></figure>
We actually prove a more general version of the lemma. The previous lemma
can be obtained simply by applying the following one with W the set of initial
values of u₀ (W then contains r values) and V the set of values appearing in u₀,
u or u_f.

**Lemma 36.** *There exists a primitive recursive function ψ(n, r) such that, for every protocol P with r registers per agent, for every local run u : (q, ν) ↛ (q', ν') in P, for every V ⊆ N finite such that V contains all message values appearing in u, for every W ⊆ V, there exists a local run u' : (q, ν) ↛ (q', ν') such that we have len(u') ≤ ψ(|P| - r + |W|, r) and:*

1. for all $v \in V$, $\ln_v(u') \le \ln_v(u)$,

2. for all $v' \in \mathbb{N} \setminus V$, there exists $v \in \mathbb{N} \setminus W$ such that $\ln_{v'}(u') \le \ln_v(u)$.

Intuitively, the set *V* represents values that are already used and therefore
cannot be used as fresh values, and *W* represents values that should not be
copied (e.g., initial values of the run). However, stating the lemma only with *W*
equal to the initial values in *u* would not allow us to apply the lemma on *u* an
infix local run of a larger local run *u'*, because the initial values in *u* would not
correspond to the ones in *u'*. This is why we state the lemma for every *W* ⊆ *V*.

<figure><img src="image_11.png" /><figcaption>Fig. 9: Illustration of the proof of Lemma 26. *s* ∈ Δ<sup>2M</sup> corresponds to the repeating sequence of transitions of length 2*M*. Register 4 contains value *v* ∈ *W*. Because both sides have the same *Θ*, they coincide on values in *W* such as *v*; only values that are not in *W* are replaced by fresh values, hence *v* is kept in the shortened local run.</figcaption></figure>