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

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.

Partly supported by ANR project PaVeDyS (ANR-23-CE48-0005).

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.

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 and its completeness for the hyper-Ackermannian complexity class $\textbf{F}_{\omega ^\omega }$, showing that the problem has nonprimitive recursive complexity. The lower bound comes from , 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 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 is $\textbf{F}_{\omega ^{\omega ^{\omega }}}$-complete [15]. When one restricts data nets to only equality tests, the becomes $\textbf{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 . 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 full version, available here.

In this document, each is linked to its 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 () [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 with $r$ registers is a tuple $\mathcal {P}= (Q, \mathcal {M}, \varDelta , q_0)$ with Q a finite set of states, $q_0 \in Q$ an initial state, $\mathcal {M}$ a finite set of and $\varDelta \subseteq Q \times \textsf{Op}\times Q$ a finite set of transitions, with operations $\textsf{Op}=$

$$ \{{\textbf {br}}(m, i), {\textbf {rec}}(m, i, {*}), {\textbf {rec}}(m, i, \downarrow ), {\textbf {rec}}(m, i, {=}), {\textbf {rec}}(m, i, {\ne }) \mid m\in \mathcal {M}, 1 \le i \le r\}.$$

Label ${\textbf {br}}$ stands for and ${\textbf {rec}}$ for . In a reception ${\textbf {rec}}(m, i, \alpha )$, $\alpha$ is its action. The set of actions is $\textsf{Actions}:= \{{=}, {\ne }, \downarrow , {*}\}$, where ‘${{=}}$’ is an equality test, ‘${{\ne }}$’ is a disequality test, ‘${\downarrow }$’ is a store action and ‘${{*}}$’ is a dummy action with no effect. The of $\mathcal {P}$ is $|\mathcal {P}| := |Q| + |\mathcal {M}| + |\varDelta | + 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,\mathcal {M}, \varDelta , q_0)$ be a with $r$ registers, and $\mathbb {A}$ a finite non-empty set of . A over $\mathbb {A}$ is a function $\gamma : \mathbb {A}\rightarrow Q \times \mathbb {N}^{r}$ mapping each agent to its state and its register values. We write $\textsf{st}(\gamma )$ for the state component of $\gamma$ and $\textsf{data}(\gamma )$ for its register component.

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

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

• if then $\textsf{data}(\gamma ')(a,j) = \textsf{data}(\gamma )(a,j)$,

• if then $\textsf{data}(\gamma ')(a,j) = \textsf{data}(\gamma )(a_0,i)$,

• if then $\textsf{data}(\gamma ')(a,j) = \textsf{data}(\gamma )(a,j) =\textsf{data}(\gamma )(a_0,i)$,

• if then $\textsf{data}(\gamma ')(a,j) = \textsf{data}(\gamma )(a,j) \ne \textsf{data}(\gamma )(a_0,i)$.

A over $\mathbb {A}$ is a sequence of steps $\rho : \gamma _0 \xrightarrow {} \gamma _1 \xrightarrow {} \cdots \xrightarrow {} \gamma _k$ with $\gamma _0, \dots , \gamma _k$ configurations over $\mathbb {A}$. We write $\gamma _0 \xrightarrow {*} \gamma _k$ when there exists such a . A is when $\gamma _0$ is an .

Remark 3

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

Example 4

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

$$\begin{aligned} \langle q_0, (1,2), q_0,(3,4) \rangle {} & {} \xrightarrow {} \langle q_1, (1,2), q_2,(1,4) \rangle \xrightarrow {} \langle q_3, (1,4), q_3,(1,4) \rangle \\ {} & {} \qquad \quad \xrightarrow {} \langle q_4, (1,4), q_3,(1,4) \rangle \xrightarrow {} \langle q_4, (1,4), q_4,(1,4) \rangle \end{aligned}$$

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 , each broadcast message is received by the other agent; in general, however, this does not have to be true.    $\square$

Fig. 1.

Example of a .

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 , the different copies of $\rho$ have no register values in common. This property is called : if state q is coverable, then for all n there exists an augmented which puts n agents on q.

Definition 6

The asks, given a $\mathcal {P}$ and a state $q_f$, whether there is a finite non-empty set of agents $\mathbb {A}$, an $\gamma _0 \xrightarrow {*} \gamma _f$ over $\mathbb {A}$ that $q_f$, i.e., there is $a \in \mathbb {A}$ such that $\textsf{st}(\gamma _f)(a) = q_f$.

The asks, given a $\mathcal {P}$ and a state $q_f$, whether there is there is a finite non-empty set of agents $\mathbb {A}$ and an $\gamma _0 \xrightarrow {*} \gamma _f$ over $\mathbb {A}$ such that, for every $a \in \mathbb {A}$, $\textsf{st}(\gamma _f)(a) = q_f$, i.e., all agents end on $q_f$.

Example 7

Let $\mathcal {P}$ the of Figure 1. As proven in Example 4, $(\mathcal {P},q_4)$ is a positive instance of  and . 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 . Indeed, there must be an agent staying on $q_3$ to broadcast $m_4$. Also, $(\mathcal {P}, q_5)$ is a negative instance of : 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 satisfying some queries. In fact, this problem exponentially reduces to hence our complexity result of $\textbf{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 , an interesting restriction of our model where register 1 is and all other registers are . 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 with $r$ registers is a $\mathcal {P}= (Q, \mathcal {M}, \varDelta , q_0)$ where register 1 appears only in in $\varDelta$ and registers $i \ge 2$ appear only in in $\varDelta$.

2.2 Classical Definitions

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

We highlight that our main result is the decidability of the problem. We show that the problem lies in $\textbf{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 $\varSigma$ be a finite alphabet, $w_1, w_2 \in \varSigma ^*$, $w_1$ is a of $w_2$, denoted , when $w_1$ can be obtained from $w_2$ by erasing some letters. A sequence of words $w_0, w_1, \ldots$ is good if there exist $i<j$ such that , and otherwise. Higman’s lemma [16] states that every sequence of words over a finite alphabet is finite, but there is no uniform bound. In order to bound the length of all 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

( [24]). Let $\varSigma$ a finite alphabet and $g : \mathbb {N}\rightarrow \mathbb {N}$ a primitive recursive function. There exists a function $f \in \mathscr {F}_{\omega ^{|\varSigma | - 1}}$ such that, for all $n \in \mathbb {N}$, every sequence $w_1, w_2, \ldots$ 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

  () 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 [3], but has non-primitive recursive complexity [26] and is in fact $\textbf{F}_{\omega ^{\omega }}$-complete [8]. By simulating LCS using BNRA, we obtain our $\textbf{F}_{\omega ^{\omega }}$ lower bound for the :

Proposition 11

  for is $\textbf{F}_{\omega ^\omega }$-hard.

Proof sketch. Given an $\mathcal {L}$, we build a $\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 of $\mathcal {L}$, chooses the next 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.    $\square$

3 Coverability Decidability for Signature Protocols

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

Theorem 12

  for BNRA is decidable and $\textbf{F}_{\omega ^\omega }$-complete.

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

3.1 Local runs

A is a pair $(q, \nu ) \in Q \times \mathbb {N}^r$. An from $(q,\nu )$ to $(q',\nu ')$ with transition $\delta \in \varDelta$, denoted $(q,\nu ) \xrightarrow {\textsf{int}(\delta )} (q',\nu ')$, is defined when $\nu = \nu '$ and $\delta =(q, {\textbf {br}}(m, i), q')$ is a . A from $(q,\nu )$ to $(q',\nu ')$ with transition $\delta \in \varDelta$ and value $v\in \mathbb {N}$, denoted $(q,\nu ) \xrightarrow {\textsf{ext}(\delta ,v)} (q',\nu ')$, is defined when $\delta$ is of the form $(q,{\textbf {rec}}(m, j, \alpha ),q')$ with $\nu (j') = \nu '(j')$ for all $j' \ne j$ and:

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

A value $v\in \mathbb {N}$ appearing in $u$ is if it appears in $\nu _0$ and otherwise. For $v\in \mathbb {N}$, the $v$- (resp. $v$- ) 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 for . Note that, in , the initial values of 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 , 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 u of an agent a into an actual , 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 which are words of $\mathcal {M}^*$.

To represent runs, we consider that abstract runs by representing such specifications, dependencies between them and how they are carried out. In this tree, each node is assigned a and the 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 $\tau$ over $\mathcal {P}$ is a finite tree where nodes $\mu$ have three labels:

• a of $\mathcal {P}$, written ;

• a value in $\mathbb {N}$, written ;

• a .

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

• (i) Initial values of are never received in ,

• (ii) , (recall that denotes the relation)

• (iii) For each value $v$ received in , $\mu$ has a child $\mu '$ s.t. .

Lastly, given $\tau$ an , we define its by $|\tau | := \sum _{\mu \in \tau } |\mu |$ where . Note that the 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 cannot cheat by receiving its . Condition (ii) expresses that broadcasts (at least) the messages of . We can use the subword relation (instead of equality) because messages do not have to be received. Condition (iii) expresses that, for each value v received in the , $\mu$ has a child who is able to broadcast the sequence of messages that receives with value v.

Fig. 2.

Example of a .

Example 15

Figure 2 provides an example of a . Let $\mathbb {A}= \{a_1, a_2,a_3\}$. We denote a configuration $\gamma$ by $\langle \textsf{st}(\gamma )(a_1),(\textsf{data}(\gamma )(a_1)), \textsf{st}(\gamma )(a_2),(\textsf{data}(\gamma )(a_2)), \textsf{st}(\gamma )(a_3), (\textsf{data}(\gamma )(a_3)) \rangle$. Irrelevant register values are denoted by $\_$. Let $\rho$ be the run over $\mathbb {A}$ of initial configuration $\langle q_0, (1,\_,\_), q_0, (2,\_,\_), q_0, (3,\_,\_) \rangle$ where the following occurs:

• $a_2$ broadcasts $\textsf {rdy}$, $a_1$ receives: $\langle q_1, (1,2,\_), q_0, (2,\_,\_), q_0, (3,\_,\_) \rangle$,

• $a_3$ broadcasts $\textsf {rdy}$, $a_1$ and $a_2$ receive: $\langle q_2, (1,2,3), q_5, (2,\_,\_), q_0, (3,\_,\_) \rangle$,

• $a_2$ broadcasts $\textsf {rdy}$, $a_3$ receives: $\langle q_2, (1,2,3), q_5, (2,\_,\_), q_5, (3,\_,\_) \rangle$,

• $a_2$ broadcasts $\textsf {go}$, $a_1$ receives: $\langle q_3, (1,2,3), q_6, (2,\_,\_), q_5, (3,\_,\_) \rangle$,

• $a_3$ broadcasts $\textsf {hlt}$, $a_1$ receives: $\langle q_4, (1,2,3), q_6, (2,\_,\_), q_7, (3,\_,\_) \rangle$.

Figure 3 provides an 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 . Condition (i) is trivially satisfied. Condition (ii) holds at every node because the local run of each node exactly broadcasts the of the node. Condition (iii) is satisfied at $\mu _1$: and . It is also satisfied at $\mu _2$, $\mu _3$ and $\mu _5$ because their local runs only receive $\textsf {rdy}$ and they each have a child with $\textsf {rdy}$. It is trivially satisfied at $\mu _4$ and $\mu _6$ as their have no reception.    $\square$

Fig. 3.

Example of an derived from $\rho$. Grids correspond to , a column of a grid is a . Transition $\delta _{ij}$ is the transition between state $q_i$ and state $q_j$, for example $\delta _{01} = (q_0, {\textbf {rec}}(\textsf {rdy}, 2, \downarrow ), q_1)$. If $\delta$ is a reception of $m\in \mathcal {M}$, $\textsf{ext}(\delta ,v)$ corresponds to receiving message (m, v); if $\delta$ is a broadcast of $m \in \mathcal {M}$, $\textsf{int}(\delta )$ corresponds to broadcasting $(m,\textsf{id})$ where $\textsf{id}$ is the value in the first register of the agent. Initial values of registers are irrelevant and written as ‘${\_}$’. Colors correspond to message types.

Lemma 16

Given a $\mathcal {P}$ with a state $q_f$, $q_f$ is coverable in $\mathcal {P}$ if and only if there exists an whose root is labelled by a covering $q_f$. We call such an a .

Proof

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

Let $\tau$ be a . We prove the following property by strong induction on the depth of $\mu$: for every $\mu$ in $\tau$, there exists a $\rho$ with an agent a whose in $\rho$ is and who satisfies . This is trivially true for leaves of $\tau$ because their have no reception (by condition (iii)) hence are actual by themselves. Let $\mu$ a node of $\tau$, and $v_1, \dots , v_c$ the values received in $u$. These values are 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 $\rho _1, \dots , \rho _c$ satisfying the 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 for all j and that all agents start with distinct values. We build an $\rho$ whose is the union of the 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 $u$, matching each reception with value $v_j$ in $u$ with a broadcast in $\rho _j$. This is possible because, for all j, (by (ii)).

Conversely, we prove the following by induction on the length of $\rho$: for every $\rho$, for every agent a in $\rho$ and for every $v \in \mathbb {N}$, there exists an whose root has as the projection of $\rho$ onto a and as the v- of a in $\rho$. If $\rho$ is the empty run, consider the with a single node whose and 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 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 at the root of $\tau _1$. If this last step is a broadcast, we obtain an ; if the broadcast value is v, we append the broadcast to the at the root of $\tau _2$ and we are done. Suppose that, in the last step of $\rho$, a performs a reception $(q, {\textbf {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 obtained by applying the induction to $\rho _p$, $a'$ and $v'$. Let $\tau _4$ the obtained by appending the last broadcast to the at the root of $\tau _3$ and the corresponding to the at the root of $\tau _3$. Attaching $\tau _4$ below the root of $\tau _2$ gives an satisfying the desired properties.    $\square$

The $\tau$ of Figure 3 is built from $\rho$ of Example 15 using the previous procedure. Observe that the $\tau$ is a for $q_4$. However, one can find a smaller . Indeed, in the right branch of $\tau$, $\mu _5$ and $\mu _6$ have the same , 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 .

Remark 17

With the previous notion of , 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 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, $\textsf{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 with $r+1$ registers (i.e., r registers used for reception) and a $\tau$ of minimal size. We turn the observation above into an argument that will be useful towards bounding the length of branches of a :

Lemma 18

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

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 to bound the height of $\tau$, using the previous lemma. To do so, we need a bound on the of a node with respect to its depth. The following lemma bounds the number of steps of a between two local configurations: we argue that if the 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 of a of a node with respect to the of its , 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,\nu ) \xrightarrow {*} (q', \nu ')$, there exists $u' : (q,\nu ) \xrightarrow {*} (q',\nu ')$ with $|u'| <~\psi (|\mathcal {P}|,r)$ and for all value $v' \in \mathbb {N}$, there exists $v \in \mathbb {N}$ such that .

Proof

Let $\psi (n,0) = n+1$ and $\psi (n,k+1) = 2 \, \psi (n,k) \cdot ({|\varDelta |}^{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 in a u if u has some ‘${\downarrow }$’ action on register i. Let u a , k the number of registers in $u$, $n := |\mathcal {P}|$ and $M := \psi (n,k)$. We prove by induction on the number k of 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 registers of u is such that $|I| = k+1$. If there exists an infix run of u of length M with only k registers, we shorten u using the induction hypothesis. Otherwise, every sequence of M steps in u has a ‘${\downarrow }$’ on every register of I. Because $|u| > 2 M \, (|\varDelta |^{2M} +1)$, $u$ contains at least $|\varDelta |^{2M}+1$ disjoint sequences of length 2M and some $s \in \varDelta ^{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 for the reception steps in s in the shortened run $u'$. For a given register $i \in I$, we would like to pick a ‘${\downarrow }$’ 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 $\textsf{ext}({\textbf {rec}}({m_1}, 2, {=}),v)$ in $u_1$ and a $\textsf{ext}({\textbf {rec}}({m_2}, 4, {=}),v)$ in $u_2$, we could have ${m_1}$ before ${m_2}$ in but ${m_1}$ after ${m_2}$ in , so that we do not have . We solve this issue by introducing fresh values between values of $u_1$ and values of $u_2$; because $|s| = 2M$, there is a ‘${\downarrow }$’ for each register in I in each half of s. In the shortened run $u'$, before the first ‘${\downarrow }$’ on register i (excluded), we use values of $u_1$, and after the last ‘${\downarrow }$’ 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 . Also, for every fresh value $v'$ there is a value v such that . Moreover, $u'$ is shorter than u; we conclude by iterating this shortening procedure.    $\square$

Fig. 4.

Illustration of the proof of Lemma 19.

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

Lemma 20

For all nodes $\mu , \mu '$ in $\tau$:

• 1. ,

• 2. if $\mu$ is the child of $\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$, ends with the last broadcast required by ; we identify in the broadcast steps witnessing and shorten the between these steps using Lemma 19. We thus obtain , proving 1. For the second item, by minimality of $\tau$, .    $\square$

Proposition 21

There exists a function f of class $\mathscr {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 '$, is not a subword of . Let $\mu _1, \dots , \mu _m$ the node appearing in a branch of $\tau$, from root to leaf. The sequence is a . For all , by Lemma 20. By direct induction, is bounded by $g^{(i)}(n)$ where $g: n \mapsto n \, \psi (n,n)$ is a primitive recursive function. Let h of class $\mathscr {F}_{\omega ^{|\mathcal {M}|-1}}$ the function obtained when applying the 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, 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 hence by $h'(n)$, so the total number of nodes in $\tau$ is bounded by $h'(n)^{h(n)+1}$ and the of $\tau$ by $f(n) := h'(n)^{h(n)+2}$. Because $\mathscr {F}_{\omega ^{|\mathcal {M}|-1}}$ is closed under composition with primitive-recursive functions, f is in $\mathscr {F}_{\omega ^{|\mathcal {M}|-1}}$.    $\square$

The previous argument shows that for is decidable and lies in complexity class $\textbf{F}_{\omega ^\omega }$. Because the hardness from Proposition 11 holds for , 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. describe the task of broadcasting with one of its own initial values; this is the we had in and, as before, it consists of a word $\textsf{bw}\in \mathcal {M}^*$ describing a sequence of that should be all broadcast with the same value. describe the task of broadcasting with a non-initial value received previously. More precisely, a is a pair $(\textsf{fw}, \textsf{fm}) \in \mathcal {M}^*\times \mathcal {M}$ asking to broadcast a message $(\textsf{fm},v)$ under the condition of previously receiving the sequence of $\textsf{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 . 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 , then we can consider that we have an unlimited supply of messages (m, v).

Example 22

Assume that $\mathbb {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 $\textsf {a} \cdot \textsf {b}$, then $a_2$ broadcasts $\textsf {c}$, then $a_1$ broadcasts $\textsf {a}^3$ then $a_3$ broadcasts $\textsf {b}$. The of $a_2$’s task would be of the form $(w, \textsf {c})$ where : $a_2$ must be able to broadcast (c, v) once $\textsf {a} \cdot \textsf {b}$ has been broadcast with value v. By contrast, $a_3$’s would be of the form $(w \cdot w', \textsf {c})$ where and $w' \in \{\textsf {a},\textsf {c}\}^*$ is a subword of $\textsf {a}^3$ enriched with as many $\textsf {c}$ as desired, because $a_2$ may be cloned at will. For example, one could have $w= \textsf {b}$ and $w' = \textsf {c} \cdot \textsf {a} \cdot \textsf {c}^4 \cdot \textsf {a} \cdot \textsf {c}^2$. This idea is formalized in the full version of the paper with the notion of decomposition. Using this notion, the previous condition becomes: $w \cdot w'$ admits decomposition $(\textsf {a} \cdot \textsf {b}, \textsf {c}, \textsf {a}^3)$.    $\square$

In our new , a node is either a boss node or a follower node, depending on its type of specification. A with a $\textsf{bw}$ must broadcast that sequence of with one of its . A $\mu$ with $(\textsf{fw}, \textsf{fm})$ is allowed to receive sequence of messages $\textsf{fw}$ with value (which must be ) without it being broadcast by its children. Other conditions are similar to the ones for : if $\mu$ is a node and a value received in its , $\mu$ must have a child broadcasting this word. Moreover, for each (m, v) received where v is an of the , $\mu$ must have a 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 the full version.

Example 23

Figure 5 depicts the associated to $a_1$ in the of Example 4. $\mu _3$ can have a $m_2$ reception that is not matched by its children because $m_2$ is in $\textsf{fw}(\mu _3)$. $\mu _1$ broadcasts $(m_2,1)$ before receiving $(m_4,1)$ hence the of $\mu _3$ witnesses broadcast of $(m_4,1)$.    $\square$

Fig. 5.

Example of an . $\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 ‘${\_}$’.

A is again an whose root covers $q_f$ (or broadcasts a message $m_f$, see Remark 17), with the extra condition that the root is a (a implicitly relies on its parent’s ability to broadcast).

Proposition 24

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

Proof sketch. The proof is quite similar to the one of Lemma 16, but is made more technical by the addition of nodes. When translating an to a , if the root of the tree is a $\mu$ of specification $(\textsf{fw}, \textsf{fm})$, then we actually obtain a partial run, i.e., a except that the receptions from $\textsf{fw}$ are not matched by broadcasts in the . 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 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).    $\square$

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

Lemma 25

Let $\mu \ne \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 with respectively $\textsf{bw}$ and $\textsf{bw}'$, and ;

• $\mu$ and $\mu '$ are with respectively $(\textsf{fw}, \textsf{fm})$ and $(\textsf{fw}', \textsf{fm}')$, and and $\textsf{fm}'=\textsf{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)$. The proof is more technical than the one of Lemma 19 but the idea is essentially the same. The formal statement is given below. 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 $u_0: (q_0, \nu _0) \xrightarrow {*} (q, \nu )$, $u: (q, \nu ) \xrightarrow {*} (q', \nu ')$, $u_f: (q', \nu ') \xrightarrow {*} (q_f, \nu _f)$, there exists a $u': (q, \nu ) \xrightarrow {*} (q', \nu ')$ 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}$, ,

• 2. otherwise, there exists $v\in \mathbb {N}$, not in $u_0$, such that .

It is however now much harder than in the case to bound the size of the . Indeed, the broadcasts no longer go only from children to parents in the . If $\mu _p$ is the parent of $\mu _c$, then $\mu _c$ broadcasts to $\mu _p$ if $\mu _c$ is a , but $\mu _p$ broadcasts to $\mu _c$ if $\mu _c$ is a , 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 immediately.

This leads us to arrange the so that long broadcast sequences are sent upwards, using the notion of depicted in Figure 6, formally defined as follows. The of the root is 0, the altitude of a is the altitude of its parent minus one, and the altitude of a is the altitude of its parent plus one. We denote the of $\mu$ by $\textbf{alt}(\mu )$. This way the nodes of maximal are the ones that do not need to send long sequences of messages. We will bound the size of nodes with respect to their , from the highest to the lowest, and then use the to bound the maximal and minimal . We present here a sketch of the proof.

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.

Let $\textbf{altmax}\ge 0$ (resp. $\textbf{altmin}\le 0$) denote the maximum (resp. minimum) altitude in $\tau$. We first bound the size of a node with respect to the difference between its altitude and $\textbf{altmax}$.

Lemma 27

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

Proof sketch. We proceed by induction on the altitude, from highest to lowest. A node of maximal has at most one message to broadcast (a must broadcast one message to its parent), so its size is bounded by $\psi (|\mathcal {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 (|\mathcal {P}|, r)+2) \, (|\mathcal {M}| \, r \, K + 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 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$. We finally obtain $f_0$ by iteratively applying the inequality above.    $\square$

We now bound $\textbf{altmax}$ and $\textbf{altmin}$:

Lemma 28

$\textbf{altmax}$ and $|\textbf{altmin}|$ are bounded by a function of class $\mathscr {F}_{\omega ^{|\mathcal {M}|}}$.

Proof sketch. We first bound $\textbf{altmax}$. Consider a branch of $\tau$ that has a node at $\textbf{altmax}$. We follow this branch from the root to a node of altitude $\textbf{altmax}$: for every $j \in [1,\textbf{altmax}]$, let $\mu _{j}$ be the first node of the branch that has altitude j. All such nodes are necessarily as they are above their parent. Sequence $\mu _{\textbf{altmax}}, \dots , \mu _2, \mu _1$ is so that the ith term is at altitude $\textbf{altmax}-i$ hence its size is bounded by $f_0(|\mathcal {P}| + i)$ (Lemma 27). With the observation of Lemma 25, we retrieve from the of this sequence of nodes a and we apply the to bound $\textbf{altmax}$. This yields in turn a bound on the size of the root of $\tau$. In order to bound $\textbf{altmin}$, we proceed similarly, using this time. We follow a branch from the root to a node of $\textbf{altmin}$. The sequence of nodes that are lower than all previous ones yields a sequence of , which is a by Lemma 25, and whose growth can be bounded using Lemma 27 and the bound on $\textbf{altmax}$. We apply the to bound $|\textbf{altmin}|$.    $\square$

Once we have bounded $\textbf{altmax}$ and $\textbf{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 $\mathscr {F}_{\omega ^\omega }$) on the size of a minimal 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 . This yields the main result of this paper:

Theorem 12. for BNRA is decidable and $\textbf{F}_{\omega ^\omega }$-complete.

4.2 Undecidability of the

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

Proposition 29

  is undecidable for , 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.    $\square$

5 Cover in 1-BNRA

In this section, we establish the NP-completeness of the restriction of to 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 , any message can be broadcast with a fresh value, therefore one can always circumvent ‘${{\ne }}$’ 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 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 , agent a stored a received value. Consider the last storing action performed by a: a was in a state $q_1$ and performed transition $(q_1, {\textbf {rec}}(m, 1, \downarrow ), q_2)$ upon reception of a message (m, v). Because we can assume that we have an unlimited supply of agents in $q_1$ thanks to the copycat principle, we can make as many agents as we want take transition $(q_1, {\textbf {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 \subseteq Q$ and $b \in Q \cup \{\bot \}$. 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_0\}$ 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_0$ and K to $\emptyset$, 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 for 1-BNRA is NP-complete.

6 Conclusion

We established the decidability (and $\textbf{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.