[name=Fact]fact [name=Observation]observation
#1co,coNP,NP,PSPACE,coPSPACE,NPSPACE,PTIME,EXPTIME,EXPSPACE,NEXPTIME,
LOGSPACE, TOWER, BNRA [coverability problem]Cover [1]cov(#1) [1]val(#1)
[1]ag(#1) ⊴ [2]gang_#1(#2) [2]b_#1(#2) [2]K_#1(#2) [2]abs_#1(#2) [1]In(#1)
[2]In_#1(#2) [1]Out(#1) [2]Out_#1(#2) [2]#2—_#1 [1]L^#1 [1]lr(#1) [1]val(#1)
[1]bw(#1) [1]fw(#1) [1]fm(#1) [1]spec(#1) [target problem]Target ⪯ [1]mem(#1)
[1]perf(#1) intro notioncolor=Ruby Red, emphasize notioncolor=Blue Sapphire
anchor point color=Ruby Red, anchor point shape=corner intro
unknowncolor=Gamboge, emphasize intro unknown contcolor=Gamboge, emphasize kl
unknowncolor=Gamboge kl unknown contcolor=Gamboge notion — signature BNRA —
signature notion — broadcast-only notion — reception-only notion — signature —
signature protocol — signature protocols notion — specification@sg —
specifications@sg notion — unfolding trees@signature — unfolding tree@sg —
node@sg notion — coverability witness@sg notion — size@treesg — size@sg notion
— length notion — active@sg notion — signature case notion — missing broadcast
— missing broadcasts notion —Broadcast Network of Register Automata —BNRA
notion — copycat principle — copycat notion — protocol — protocols notion —
notion — definition notion — broadcasts — broadcast notion — receptions —
reception notion — local tests — local test — local equality test — local
equality tests — local disequality tests — local disequality test notion
—coverability witness —coverability witnesses notion — simple — simple
protocol — simple protocols notion — size notion — step — steps notion —
agents — agent notion — covers notion — configuration — configurations notion
— initial configuration — initial configurations notion — transition —
transitions notion — action — actions notion — equality test notion —
disequality test notion — store action notion — dummy action notion — run —
runs notion — Length function theorem notion — subword — subword order notion
— size@tree notion — message type — message types notion — good notion — bad —
bad sequence notion — initial run — initial@run — initial runs notion —
initial partial run — initial@partial — initial partial runs notion — input —
$v$-input — $v$-inputs — $v^{\prime}$-input — $v$-input — $v^{\prime}$-input —
$v$-input — $v^{\prime}$-input notion — output — $v$-output — $v$-outputs —
$v^{\prime}$-output — $v$-output — $v^{\prime}$-output — $v$-output —
$v^{\prime}$-output notion — local run — local runs notion — local
configuration — local configurations notion — query — queries notion — query
coverability problem notion — contradictory — non-contradictory notion —
abstract configuration — abstract configurations notion — abstract step —
abstract steps notion — abstract run — abstract runs notion — gang — gangs
notion — clique notion — Broadcast from boss — broadcast from boss notion —
Broadcast from clique — broadcast from clique notion — External broadcast —
external broadcast notion — Gang reset — gang reset — gang resets — resets —
reset notion — boss nodes — boss node — boss — bosses notion — boss
specification — boss specifications — Boss specification — Boss specifications
notion — follower — followers — follower node — Follower node — follower nodes
notion — follower specification — follower specifications — Follower
specification — Follower specifications notion — unfolding tree — unfolding
trees notion — partial run — partial runs notion — altitude — altitudes notion
— admits decomposition — admit decomposition notion — decomposition —
decompositions notion — trace — traces notion — specification — specifications
notion — active — active register — active registers notion — shortening
property notion — local step — local steps notion — reception step — reception
steps notion — internal step — internal steps notion — unmatched reception —
unmatched receptions notion — Cover — cover problem — coverability problem —
coverability — Cover notion — Target — target problem — target reachability
problem — Target notion — lossy channel system — lossy channel systems — Lossy
channel systems — LCS notion — root notion — link notion — push notion — pop
notion — reachability problem@lcs notion — memory slot — memory slots notion —
perfect configurations — perfect configuration — perfect notion — internal
test@global notion — internal message@global — internal messages@global notion
— external message@global — external messages@global notion — internal
step@global notion — partial step — partial steps notion — projection notion —
input@partial notion — output@partial notion — subtree — subtrees notion —
initial — initial value — initial values — Initial Values notion — non-initial
— non-initial value — non-initial values — Non-initial Values

11institutetext: IRIF, CNRS, Université Paris Cité 22institutetext: LaBRI,
Université de Bordeaux 33institutetext: IRISA, Université de Rennes

# Parameterized Broadcast Networks with Registers: from NP to the Frontiers of
Decidability††thanks: Partly supported by ANR project PaVeDyS
(ANR-23-CE48-0005).

Lucie Guillou 11 Corto Mascle 22 Nicolas Waldburger 33

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

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 -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
$\mathbf{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, 26,
8]. 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
-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 [11, 5], 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
$\mathbf{F}_{\omega^{\omega^{\omega}}}$-complete [15]. When one restricts data
nets to only equality tests, the ”coverability problem” becomes
$\mathbf{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 -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\mathsf{Op}\times Q$ a finite set of transitions,
with operations $\mathsf{Op}=$

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

Label br stands for ””broadcasts”” and rec for ””receptions””. In a reception
$\textbf{rec}(m,i,\alpha)$, $\alpha$ is its _action_. The set of actions is
$\mathsf{Actions}:=\\{{=},{\neq},\downarrow,{*}\\}$, where $\mlq{=}\mrq$ is an
_equality test_ , $\mlq{\neq}\mrq$ is a _disequality test_ ,
$\mlq\downarrow\mrq$ is a _store action_ and $\mlq{*}\mrq$ is a _dummy action_
with no effect. The ””size”” of $\mathcal{P}$ is
$|\mathcal{P}|:=|Q|+|\mathcal{M}|+|\Delta|+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},\Delta,q_{0})$ be a ”protocol” with $r$ registers, and
$\mathbb{A}$ a finite non-empty set of ””agents””. A ””configuration”” over
$\mathbb{A}$ is a function $\gamma:\mathbb{A}\to Q\times\mathbb{N}^{r}$
mapping each agent to its state and its register values. We write
$\mathsf{st}(\gamma)$ for the state component of $\gamma$ and
$\mathsf{data}(\gamma)$ for its register component.

An initial configuration $\gamma$ is one where for all $a\in\mathbb{A}$,
$\mathsf{st}(\gamma)(a)=q_{0}$ and
$\mathsf{data}(\gamma)(a,i)\neq\mathsf{data}(\gamma)(a^{\prime},i^{\prime})$
for all $(a,i)\neq(a^{\prime},i^{\prime})$.

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

  * •

if $\alpha=\mlq{*}\mrq$ then
$\mathsf{data}(\gamma^{\prime})(a,j)=\mathsf{data}(\gamma)(a,j)$,

  * •

if $\alpha=\mlq\downarrow\mrq$ then
$\mathsf{data}(\gamma^{\prime})(a,j)=\mathsf{data}(\gamma)(a_{0},i)$,

  * •

if $\alpha=\mlq{=}\mrq$ then
$\mathsf{data}(\gamma^{\prime})(a,j)=\mathsf{data}(\gamma)(a,j)=\mathsf{data}(\gamma)(a_{0},i)$,

  * •

if $\alpha=\mlq{\neq}\mrq$ then
$\mathsf{data}(\gamma^{\prime})(a,j)=\mathsf{data}(\gamma)(a,j)\neq\mathsf{data}(\gamma)(a_{0},i)$.

A ””run”” 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 ”run”. A ”run”
is ””initial@@run”” 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\mathsf{st}(\gamma)(a_{1}),\mathsf{data}(\gamma)(a_{1}),\mathsf{st}(\gamma)(a_{2}),\mathsf{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\xrightarrow{}\langle
q_{1},(1,2),q_{2},(1,4)\rangle\xrightarrow{}\langle
q_{3},(1,4),q_{3},(1,4)\rangle\\\ \xrightarrow{}\langle
q_{4},(1,4),q_{3},(1,4)\rangle\xrightarrow{}\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.

$q_{0}$$q_{1}$$q_{3}$$q_{2}$$q_{4}$$q_{5}$$\textbf{br}(m_{1},1)$$\textbf{br}(m_{2},1)$$\textbf{rec}(m_{2},1,\downarrow)$$\textbf{rec}(m_{3},2,\downarrow)$$\textbf{br}(m_{3},2)$$\textbf{br}(m_{4},1)$$\textbf{rec}(m_{4},1,=)$$\textbf{br}(m_{4},1)$$\textbf{rec}(m_{1},1,=)$
Figure 1: Example of a ”protocol”.

###### Remark 5

From a run $\rho:\gamma_{0}\xrightarrow{\ast}\gamma$, we can build a larger
run $\rho^{\prime}$ in which, for each agent $a$ of $\rho$, there are
arbitrarily many extra agents in $\rho^{\prime}$ that end in the same state as
$a$, all with distinct register values. To obtain this, $\rho^{\prime}$ 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”” * asks, given a ”protocol” $\mathcal{P}$ and a
state $q_{f}$, whether there is a finite non-empty set of agents $\mathbb{A}$,
an ”initial run” $\gamma_{0}\xrightarrow{*}\gamma_{f}$ over $\mathbb{A}$ that
””covers”” $q_{f}$, _i.e._ , there is $a\in\mathbb{A}$ such that
$\mathsf{st}(\gamma_{f})(a)=q_{f}$.

The ””target problem”” * asks, given a ”protocol” $\mathcal{P}$ and a state
$q_{f}$, whether there is there is a finite non-empty set of agents
$\mathbb{A}$ and an ”initial run” $\gamma_{0}\xrightarrow{*}\gamma_{f}$ over
$\mathbb{A}$ such that, for every $a\in\mathbb{A}$,
$\mathsf{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 and . However, let
$\mathcal{P}^{\prime}$ the protocol obtained from $\mathcal{P}$ by removing
the loop on $q_{4}$; $(\mathcal{P}^{\prime},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.

###### 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 hence our complexity result of
$\mathbf{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
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\geq 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
$\mathscr{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}\intro*\subword w_{2}$, 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 $w_{i}\subword 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 2.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\mathscr{F}_{\omega^{|\Sigma|-1}}$ such that, for all $n\in\mathbb{N}$,
every ”bad” sequence $w_{1},w_{2},\ldots$ such that $|w_{i}|\leq 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 ()

for ”signature BNRA” is $\mathbf{F}_{\omega^{\omega}}$-hard.

######  Proof (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 0.A.

##  3 Coverability Decidability for Signature Protocols

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

######  Theorem 3.1 ()

for BNRA is decidable and $\mathbf{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^{\prime},\nu^{\prime})$ with
transition $\delta\in\Delta$, denoted
$(q,\nu)\xrightarrow{\mathsf{int}(\delta)}(q^{\prime},\nu^{\prime})$, is
defined when $\nu=\nu^{\prime}$ and $\delta=(q,\textbf{br}(m,i),q^{\prime})$
is a ”broadcast”. A ””reception step”” from $(q,\nu)$ to
$(q^{\prime},\nu^{\prime})$ with transition $\delta\in\Delta$ and value
$v\in\mathbb{N}$, denoted
$(q,\nu)\xrightarrow{\mathsf{ext}(\delta,v)}(q^{\prime},\nu^{\prime})$, is
defined when $\delta$ is of the form $(q,\textbf{rec}(m,j,\alpha),q^{\prime})$
with $\nu(j^{\prime})=\nu^{\prime}(j^{\prime})$ for all $j^{\prime}\neq j$
and:

  * •

if $\alpha=\mlq{*}\mrq$ then $\nu(j)=\nu^{\prime}(j)$,

  * •

if $\alpha=\mlq\downarrow\mrq$ then $\nu^{\prime}(j)=v$,

  * •

if $\alpha=\mlq{=}\mrq$ then $\nu(j)=\nu^{\prime}(j)=v$,

  * •

if $\alpha=\mlq{\neq}\mrq$ then $\nu(j)=\nu^{\prime}(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)\xrightarrow{}(q^{\prime},\nu^{\prime})$ 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”” $\intro*\vinput{v}{u}$ (resp. $v$-””output””
$\intro*\voutput{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 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: 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 3.2, 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^{\prime}$ 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@@sg” which are words of $\mathcal{M}^{*}$.

To represent runs, we consider ”unfolding trees@@signature” 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@@sg” 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 2

An ””unfolding tree@@sg”” $\tau$ over $\mathcal{P}$ is a finite tree where
nodes $\mu$ have three labels:

  * •

a ”local run” of $\mathcal{P}$, written $\intro*\localrunlabel{\mu}$;

  * •

a value in $\mathbb{N}$, written $\intro*\valuelabel{\mu}$;

  * •

a ””specification@@sg”” $\intro*\speclabel{\mu}\in\mathcal{M}^{*}$.

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

  1. (i)

Initial values of $\localrunlabel{\mu}$ are never received in
$\localrunlabel{\mu}$,

  2. (ii)

$\speclabel{\mu}\subword\voutput{\valuelabel{\mu}}{\localrunlabel{\mu}}$,
_(recall that $\subword$ denotes the ”subword” relation)_

  3. (iii)

For each value $v$ received in $\localrunlabel{\mu}$, $\mu$ has a child
$\mu^{\prime}$ s.t.
$\vinput{v}{\localrunlabel{\mu}}\subword\speclabel{\mu^{\prime}}$.

Lastly, given $\tau$ an ”unfolding tree@@sg”, we define its ””size@@treesg””
by $|\tau|:=\sum_{\mu\in\tau}|\mu|$ where
$|\mu|:=|\localrunlabel{\mu}|+|\speclabel{\mu}|$. Note that the ”size@@treesg”
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
$\localrunlabel{\mu}$ broadcasts (at least) the messages of $\speclabel{\mu}$.
We can use the subword relation $\subword$ (instead of equality) because
messages do not have to be received. Condition (iii) expresses that, for each
value $v$ received in the ”local run” $\localrunlabel{\mu}$, $\mu$ has a child
who is able to broadcast the sequence of messages that $\localrunlabel{\mu}$
receives with value $v$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$q_{6}$$q_{7}$$\textbf{br}(\textsf{go},1)$$\textbf{br}(\textsf{hlt},1)$$\textbf{br}(\textsf{rdy},1)$$\textbf{br}(\textsf{rdy},1)$$\textbf{rec}(\textsf{rdy},2,\downarrow)$$\textbf{rec}(\textsf{rdy},3,\downarrow)$$\textbf{rec}(\textsf{go},2,{=})$$\textbf{rec}(\textsf{hlt},3,{=})$$\textbf{rec}(\textsf{rdy},2,{*})$

Figure 2: Example of a ”signature protocol”.

###### Example 3

Figure 2 provides an example of a ”signature protocol”. Let
$\mathbb{A}=\\{a_{1},a_{2},a_{3}\\}$. We denote a configuration $\gamma$ by
$\langle\mathsf{st}(\gamma)(a_{1}),(\mathsf{data}(\gamma)(a_{1})),\\\
\mathsf{st}(\gamma)(a_{2}),(\mathsf{data}(\gamma)(a_{2})),\mathsf{st}(\gamma)(a_{3}),(\mathsf{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 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@@sg” 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@@sg”. Condition (i) is
trivially satisfied. Condition (ii) holds at every node because the local run
of each node exactly broadcasts the ”specification@@sg” of the node. Condition
(iii) is satisfied at $\mu_{1}$:
$\vinput{2}{\localrunlabel{\mu_{1}}}=\textsf{rdy}\cdot\textsf{go}=\speclabel{\mu_{2}}$
and
$\vinput{3}{\localrunlabel{\mu_{1}}}=\textsf{rdy}\cdot\textsf{hlt}=\speclabel{\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@@sg” rdy.
It is trivially satisfied at $\mu_{4}$ and $\mu_{6}$ as their ”local runs”
have no reception.

Node $\mu_{1}$ ($a_{1}$ in $\rho$)$\mathsf{spec}=\varepsilon$$v=1$reg $1$reg
$2$reg
$3$$q_{0}$$1$$\\_$$\\_$$\rightarrow$${\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\mathsf{ext}(\delta_{01},2)}$$q_{1}$$1$$2$$\\_$$\rightarrow$${\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\mathsf{ext}(\delta_{12},3)}$$q_{2}$$1$$2$$3$$\rightarrow$${\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}\mathsf{ext}(\delta_{23},2)}$$q_{3}$$1$$2$$3$$\rightarrow$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@cmyk@stroke{0}{1}{1}{0}\pgfsys@color@cmyk@fill{0}{1}{1}{0}\mathsf{ext}(\delta_{34},3)}$$q_{4}$$1$$2$$3$$q_{0}$$2$$\\_$$\\_$$\rightarrow$${\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\mathsf{int}(\delta_{00})}$$q_{5}$$2$$\\_$$\\_$$\rightarrow$${\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\mathsf{ext}(\delta_{05},4)}$$q_{5}$$2$$\\_$$\\_$$\rightarrow$$\mathsf{int}(\delta_{56})$$q_{6}$$2$$\\_$$\\_$Node
$\mu_{2}$
($a_{2}$)$\mathsf{spec}={\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\textsf{rdy}}\cdot{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}\textsf{go}}$$v=2$$q_{0}$$3$$\\_$$\\_$$\rightarrow$$\mathsf{int}(\delta_{00})$$q_{0}$$3$$\\_$$\\_$$\rightarrow$${\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\mathsf{ext}(\delta_{05},5)}$$q_{5}$$3$$\\_$$\\_$$\rightarrow$$\mathsf{int}(\delta_{57})$$q_{7}$$3$$\\_$$\\_$Node
$\mu_{3}$
($a_{3}$)$\mathsf{spec}={\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\textsf{rdy}}\cdot{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@cmyk@stroke{0}{1}{1}{0}\pgfsys@color@cmyk@fill{0}{1}{1}{0}\textsf{hlt}}$$v=3$$q_{0}$$4$$\\_$$\\_$$\rightarrow$$\mathsf{int}(\delta_{00}){}$$q_{0}$$4$$\\_$$\\_$Node
$\mu_{4}$
($a_{3}$)$\mathsf{spec}={{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\textsf{rdy}}}$$v=4$$q_{0}$$5$$\\_$$\\_$$\rightarrow$${\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\mathsf{ext}(\delta_{05},6)}$$q_{5}$$5$$\\_$$\\_$$\rightarrow$$\mathsf{int}(\delta_{55})$$q_{5}$$5$$\\_$$\\_$Node
$\mu_{5}$
($a_{2}$)$\mathsf{spec}={{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color@cmyk@fill{0}{0}{0.5}{0.5}\textsf{rdy}}}$$v=5$$q_{0}$$6$$\\_$$\\_$$\rightarrow$$\mathsf{int}(\delta_{00})$$q_{0}$$6$$\\_$$\\_$Node
$\mu_{6}$
($a_{3}$)$\mathsf{spec}={{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{0.5}{0.5}\pgfsys@color<EMAIL_ADDRESS>Figure 3: Example of an ”unfolding tree@@sg” 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},\textbf{rec}(\textsf{rdy},2,\downarrow),q_{1})$. If
$\delta$ is a reception of $m\in\mathcal{M}$, $\mathsf{ext}(\delta,v)$
corresponds to receiving message $(m,v)$; if $\delta$ is a broadcast of
$m\in\mathcal{M}$, $\mathsf{int}(\delta)$ corresponds to broadcasting
$(m,\mathsf{id})$ where $\mathsf{id}$ is the value in the first register of
the agent. Initial values of ”reception-only” registers are irrevelant and
written as $\mlq\\_\mrq$. Colors correspond to message types.

###### Lemma 4

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@@sg”
whose root is labelled by a ”local run” covering $q_{f}$. We call such an
”unfolding tree@@sg” a ””coverability witness@@sg””.

###### Proof

Given a ”run” $\rho$, agent $a$ _satisfies a ”specification@@sg”_
$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@@sg”. 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
$\localrunlabel{\mu}$ and who satisfies ”specification@@sg” $\speclabel{\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:=\localrunlabel{\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@@sg” 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}=\valuelabel{\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$,
$\vinput{v_{j}}{u}\subword\speclabel{\mu_{j}}\subword\voutput{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@@sg” whose root has as
”local run” the projection of $\rho$ onto $a$ and as ”specification@@sg” the
$v$-”output” of $a$ in $\rho$. If $\rho$ is the empty run, consider the
”unfolding tree@@sg” with a single node whose ”local run” and
”specification@@sg” 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@@sg”
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@@sg”; if the broadcast value is $v$,
we append the broadcast ”message type” to the ”specification@@sg” 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^{\prime})$ of a message
$(m,v^{\prime})$. We might need to adapt $\tau_{2}$ to respect condition (iii)
at the root. Let $a^{\prime}$ the agent broadcasting in the last step of
$\rho$. Let $\tau_{3}$ the ”unfolding tree@@sg” obtained by applying the
induction to $\rho_{p}$, $a^{\prime}$ and $v^{\prime}$. Let $\tau_{4}$ the
”unfolding tree@@sg” obtained by appending the last broadcast to the ”local
run” at the root of $\tau_{3}$ and the corresponding ”message type” to the
”specification@@sg” at the root of $\tau_{3}$. Attaching $\tau_{4}$ below the
root of $\tau_{2}$ gives an ”unfolding tree@@sg” satisfying the desired
properties.

The ”unfolding tree@@sg” $\tau$ of Figure 3 is built from $\rho$ of Example 3
using the previous procedure. Observe that the ”unfolding tree@@sg” $\tau$ is
a ”coverability witness@@sg” for $q_{4}$. However, one can find a smaller
”coverability witness@@sg”. Indeed, in the right branch of $\tau$, $\mu_{5}$
and $\mu_{6}$ have the same ”specification@@sg”, 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
$\speclabel{\mu_{5}}\subword\speclabel{\mu_{6}}$.

###### Remark 5

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,
$\mathsf{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
”coverability witness@@sg” $\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@@sg”:

###### Lemma 6

If a ”coverability witness@@sg” $\tau$ for $(\mathcal{P},q_{f})$ of minimal
size has two nodes $\mu,\mu^{\prime}$ with $\mu$ a strict ancestor of
$\mu^{\prime}$ then $\speclabel{\mu}$ cannot be a subword of
$\speclabel{\mu^{\prime}}$.

###### Proof

Otherwise, replacing the subtree rooted in $\mu$ with the one rooted in
$\mu^{\prime}$ would contradict minimality of $\tau$.

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@@treesg” 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@@sg” of its
”specification@@sg”, which is the first step towards our goal.

###### Lemma 7

There exists a primitive recursive function $\psi$ so that, for every local
run $u:(q,\nu)\xrightarrow{*}(q^{\prime},\nu^{\prime})$, there exists
$u^{\prime}:(q,\nu)\xrightarrow{*}(q^{\prime},\nu^{\prime})$ with
$|u^{\prime}|<~{}\psi(|\mathcal{P}|,r)$ and for all value
$v^{\prime}\in\mathbb{N}$, there exists $v\in\mathbb{N}$ such that
$\vinput{v^{\prime}}{u^{\prime}}\subword\vinput{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\geq 2$ is
””active@@sg”” in a ”local run” $u$ if $u$ has some $\mlq\downarrow\mrq$
action on register $i$. Let $u$ a ”local run”, $k$ the number of ”active@@sg”
registers in $u$, $n:=|\mathcal{P}|$ and $M:=\psi(n,k)$. We prove by induction
on the number $k$ of ”active@@sg” registers in $u$ that if $|u|\geq\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@@sg” registers of $u$ is such that $|I|=k+1$.
If there exists an infix run of $u$ of length $M$ with only $k$ ”active@@sg”
registers, we shorten $u$ using the induction hypothesis. Otherwise, every
sequence of $M$ steps in $u$ has a $\mlq\downarrow\mrq$ 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^{\prime}$ 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^{\prime}$. For a given register
$i\in I$, we would like to pick a $\mlq\downarrow\mrq$ 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
$\mathsf{ext}(\textbf{rec}({m_{1}},2,{=}),v)$ in $u_{1}$ and a
$\mathsf{ext}(\textbf{rec}({m_{2}},4,{=}),v)$ in $u_{2}$, we could have
${m_{1}}$ before ${m_{2}}$ in $\vinput{v}{u}$ but ${m_{1}}$ after ${m_{2}}$ in
$\vinput{v}{u^{\prime}}$, so that we do not have
$\vinput{v}{u^{\prime}}\subword\vinput{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 $\mlq\downarrow\mrq$ for each register in $I$ in
each half of $s$. In the shortened run $u^{\prime}$, before the _first_
$\mlq\downarrow\mrq$ on register $i$ (excluded), we use values of $u_{1}$, and
after the _last_ $\mlq\downarrow\mrq$ 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^{\prime}$. Therefore, for every value that appeared in $u$, we have
$\vinput{v}{u^{\prime}}\subword\vinput{v}{u}$. Also, for every fresh value
$v^{\prime}$ there is a value $v$ such that
$\vinput{v^{\prime}}{u^{\prime}}\subword\vinput{v}{u}$. Moreover, $u^{\prime}$
is shorter than $u$; we conclude by iterating this shortening procedure.

Original local runreg $2$reg $3$reg $4$$v_{2}$$v_{1}$$\mlq\downarrow\mrq$
actionsShortened local runreg $2$reg $3$reg
$4$$s$$v_{2}^{\prime}$$m_{2}$$m_{1}$ fresh
---
values
$v_{1}$$s$$s$ Figure 4: Illustration of the proof of Lemma 7.

Using the previous lemma, we will bound the size of a node in $\tau$ with
respect to its ”specification@@sg” 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 8

For all nodes $\mu,\mu^{\prime}$ in $\tau$:

  1. 1.

$|\localrunlabel{\mu}|\leq\psi(|\mathcal{P}|,r)\,|\speclabel{\mu}|$,

  2. 2.

if $\mu$ is the child of $\mu^{\prime}$,
$|\speclabel{\mu}|\leq\psi(|\mathcal{P}|,r)\,|\speclabel{\mu^{\prime}}|$.

###### Proof

Thanks to Remark 5, we assume that the specification at the root is of length
$1$. For the first item, by minimality of $\tau$, $\localrunlabel{\mu}$ ends
with the last broadcast required by $\speclabel{\mu}$; we identify in
$\localrunlabel{\mu}$ the broadcast steps witnessing $\speclabel{\mu}$ and
shorten the ”local run” between these steps using Lemma 7. We thus obtain
$|\localrunlabel{\mu}|\leq\psi(|\mathcal{P}|,r)\,|\speclabel{\mu}|$, proving
1. For the second item, by minimality of $\tau$,
$|\speclabel{\mu}|\leq\max_{v\in\mathbb{N}}|\vinput{v}{\localrunlabel{\mu^{\prime}}}|\leq|\localrunlabel{\mu^{\prime}}|\leq\psi(|\mathcal{P}|,r)\,|\speclabel{\mu^{\prime}}|$.

###### Proposition 9

There exists a function $f$ of class $\mathscr{F}_{\omega^{|\mathcal{M}|-1}}$
s.t. $|\tau|\leq f(|\mathcal{P}|)$.

###### Proof

Let $n:=|\mathcal{P}|$, let $r+1$ be the number of registers in $\mathcal{P}$.
Thanks to Lemma 6, for all $\mu\neq\mu^{\prime}$ in $\tau$ with $\mu$ ancestor
of $\mu^{\prime}$, $\speclabel{\mu}$ is not a subword of
$\speclabel{\mu^{\prime}}$. Let $\mu_{1},\dots,\mu_{m}$ the node appearing in
a branch of $\tau$, from root to leaf. The sequence
$\speclabel{\mu_{1}},\dots,\speclabel{\mu_{m}}$ is a ”bad sequence”. For all
$i\in[1,m]$, $|\speclabel{\mu_{i+1}}|\leq\psi(n,r)\,|\speclabel{\mu_{i}}|$ by
Lemma 8. By direct induction, $|\speclabel{\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 $\mathscr{F}_{\omega^{|\mathcal{M}|-1}}$ the
function obtained when applying the ”Length function theorem” on $g$ and
$\mathcal{M}$; we have $m\leq h(n)$.

By immediate induction, thanks to Lemma 8.2, for every node $\mu$ at depth
$d$, $|\speclabel{\mu}|\leq\psi(n,r)^{d+1}$ which, by Lemma 8.1 and because
$d\leq h(n)$, bounds the size of every node by
$h^{\prime}(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^{\prime}(n)$, so the total number of nodes in $\tau$ is
bounded by $h^{\prime}(n)^{h(n)+1}$ and the ”size@@treesg” of $\tau$ by
$f(n):=h^{\prime}(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}}$.

The previous argument shows that for ”signature protocols” is decidable and
lies in complexity class $\mathbf{F}_{\omega^{\omega}}$. Because the hardness
from Proposition 11 holds for ”signature protocols”, 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@@sg” we had in ”signature protocols” and, as before, it
consists of a word $\mathsf{bw}\in\mathcal{M}^{\ast}$ 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
$(\mathsf{fw},\mathsf{fm})\in\mathcal{M}^{*}\times\mathcal{M}$ asking to
broadcast a message $(\mathsf{fm},v)$ under the condition of previously
receiving the sequence of ”message types” $\mathsf{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 1

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 c,
then $a_{1}$ broadcasts $\textsf{a}^{3}$ then $a_{3}$ broadcasts b. The
”follower specification” of $a_{2}$’s task would be of the form
$(w,\textsf{c})$ where $w\subword\textsf{a}\cdot\textsf{b}$: $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 ”follower specification” would be of
the form $(w\cdot w^{\prime},\textsf{c})$ where
$w\subword\textsf{a}\cdot\textsf{b}$ and
$w^{\prime}\in\\{\textsf{a},\textsf{c}\\}^{*}$ is a subword of
$\textsf{a}^{3}$ enriched with as many c as desired, because $a_{2}$ may be
cloned at will. For example, one could have $w=\textsf{b}$ and
$w^{\prime}=\textsf{c}\cdot\textsf{a}\cdot\textsf{c}^{4}\cdot\textsf{a}\cdot\textsf{c}^{2}$.
This idea is formalized in Appendix 0.B with the notion of _decomposition_.
Using this notion, the previous condition becomes: $w\cdot w^{\prime}$ _admits
decomposition_ $(\textsf{a}\cdot\textsf{b},\textsf{c},\textsf{a}^{3})$.

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” $\mathsf{bw}$ must broadcast that sequence of ”message types”
with one of its ”initial values”. A ””follower node”” $\mu$ with ”follower
specification” $(\mathsf{fw},\mathsf{fm})$ is allowed to receive sequence of
messages $\mathsf{fw}$ with value $\valuelabel{\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\valuelabel{\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 1. The
formal definition of _unfolding tree_ is given in Appendix 0.B.

###### Example 2

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 $\mathsf{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)$.

Boss node $\mu_{1}$ ($a_{1}$ in $\rho$)$\mathsf{bw}=\varepsilon$$v=1$reg
$1$reg
$2$$q_{0}$$1$$\\_$$\rightarrow$$\mathsf{int}(\delta_{b2})$$q_{1}$$1$$\\_$$\rightarrow$$\mathsf{ext}(\delta_{r3},2)$$q_{3}$$1$$2$$\rightarrow$$\mathsf{ext}(\delta_{r4},1)$$q_{4}$$1$$2$$\rightarrow$$\mathsf{int}(\delta_{b4})$$q_{4}$$1$$2$$q_{0}$$\\_$$2$$\rightarrow$$\mathsf{ext}(\delta_{r2},3)$$q_{2}$$3$$2$$\rightarrow$$\mathsf{int}(\delta_{b3})$$q_{3}$$3$$2$Boss
node $\mu_{2}$
($a_{2}$)$\mathsf{bw}={\color[rgb]{0.176,0.904,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.176,0.904,0.2}\pgfsys@color@cmyk@stroke{0.728}{0}{0.704}{0.096}\pgfsys@color@cmyk@fill{0.728}{0}{0.704}{0.096}m_{3}}$$v=2$$q_{0}$$\\_$$\\_$$\rightarrow$$\mathsf{ext}(\delta_{r2},1)$$q_{2}$$1$$\\_$$\rightarrow$$\mathsf{int}(\delta_{b3})$$q_{3}$$1$$\\_$$\rightarrow$$\mathsf{int}(\delta_{b4})$$q_{3}$$1$$\\_$Follower
node $\mu_{3}$
($a_{2}$)$\mathsf{fw}={\color[rgb]{1,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0.5}\pgfsys@color@cmyk@stroke{0}{1}{0.50}{0}\pgfsys@color@cmyk@fill{0}{1}{0.50}{0}m_{2}},\mathsf{fm}={\color[rgb]{0.65,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0,0}\pgfsys@color@cmyk@stroke{0}{0.85}{0.87}{0.35}\pgfsys@color@cmyk@fill{0}{0.85}{0.87}{0.35}m_{4}}$$v=1$$q_{0}$$3$$\\_$$\rightarrow$$\mathsf{int}(\delta_{b2}){}$$q_{1}$$3$$\\_$Boss
node $\mu_{4}$
($a_{1}$)$\mathsf{bw}={\color[rgb]{1,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0.5}\pgfsys@color@cmyk@stroke{0}{1}{0.50}{0}\pgfsys@color<EMAIL_ADDRESS>Figure 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 $\mlq\\_\mrq$.

A ””coverability witness”” is again an ”unfolding tree” whose root covers
$q_{f}$ (or broadcasts a message $m_{f}$, see Remark 5), with the extra
condition that the root is a ”boss node” (a ”follower node” implicitly relies
on its parent’s ability to broadcast).

######  Proposition 3 ()

An instance of $(\mathcal{P},q_{f})$ is positive if and only if there exists a
”coverability witness” for that instance.

######  Proof (Proof sketch)

The proof is quite similar to the one of Lemma 4, 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
$(\mathsf{fw},\mathsf{fm})$, then we actually obtain a _partial run_ , _i.e._
, a ”run” except that the receptions from $\mathsf{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 1). See Appendix 0.C for the proof.

####  4.1.1 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 6 but for ”follower specifications”, the subword relation
goes the opposite direction because the shorter the requirement $\mathsf{fw}$,
the better. Details can be found in Appendix 0.D.

######  Lemma 4 ()

Let $\mu\neq\mu^{\prime}$ be two nodes of $\tau$ such that $\mu$ is an
ancestor of $\mu^{\prime}$. If one of those conditions holds, then $\tau$ can
be shortened (contradicting its minimality):

  * •

$\mu$ and $\mu^{\prime}$ are ”boss nodes” with ”boss specifications”
respectively $\mathsf{bw}$ and $\mathsf{bw}^{\prime}$, and
$\mathsf{bw}\subword\mathsf{bw}^{\prime}$;

  * •

$\mu$ and $\mu^{\prime}$ are ”follower nodes” with ”follower specifications”
respectively $(\mathsf{fw},\mathsf{fm})$ and
$(\mathsf{fw}^{\prime},\mathsf{fm}^{\prime})$, and
$\mathsf{fw}^{\prime}\subword\mathsf{fw}$ and
$\mathsf{fm}^{\prime}=\mathsf{fm}$.

We can generalize Lemma 7 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 7
but the idea is essentially the same. The formal statement is given below. ,
and the proof can be found in Appendix 0.E. One can therefore bound the size
of a node with respect to the size of the nodes that it must broadcast to.

######  Lemma 5 ()

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},\nu_{0})\xrightarrow{*}(q,\nu)$,
$u:(q,\nu)\xrightarrow{*}(q^{\prime},\nu^{\prime})$,
$u_{f}:(q^{\prime},\nu^{\prime})\xrightarrow{*}(q_{f},\nu_{f})$, there exists
a ”local run” $u^{\prime}:(q,\nu)\xrightarrow{*}(q^{\prime},\nu^{\prime})$
with $|u^{\prime}|\leq\psi(|\mathcal{P}|,r)$ and for all
$v^{\prime}\in\mathbb{N}$:

  1. 1.

if $v^{\prime}$ appears in $u_{0}$, $u$, or $u_{f}$,
$\vinput{v^{\prime}}{u^{\prime}}\subword\vinput{v^{\prime}}{u}$,

  2. 2.

otherwise, there exists $v\in\mathbb{N}$, not ”initial” in $u_{0}$, such that
$\vinput{v^{\prime}}{u^{\prime}}\subword\vinput{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 $\mathbf{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 0.F.

altitude-2-101BossFollowerBossBossFollowerBossBossFollowerFollowerBoss Figure
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 $\mathbf{altmax}\geq 0$ (resp. $\mathbf{altmin}\leq 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 $\mathbf{altmax}$.

######  Lemma 6 ()

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

######  Proof (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(|\mathcal{P}|,r)$ by Lemma 5 (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|\leq(\psi(|\mathcal{P}|,r)+2)\,(|\mathcal{M}|\,r\,K+K)$, with $\psi$ the
primitive-recursive function defined in Lemma 5. The idea is similar to the
one for Lemma 8. 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 5 to bound the size of
the local run of $\mu$. Lemma 1 in the appendix details these ideas. We
finally obtain $f_{0}$ by iteratively applying the inequality above.

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

###### Lemma 7

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

######  Proof (Proof sketch)

We first bound $\mathbf{altmax}$. Consider a branch of $\tau$ that has a node
at ”altitude” $\mathbf{altmax}$. We follow this branch from the root to a node
of altitude $\mathbf{altmax}$: for every $j\in[1,\mathbf{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_{\mathbf{altmax}},\dots,\mu_{2},\mu_{1}$ is so that the $i$th
term is at altitude $\mathbf{altmax}-i$ hence its size is bounded by
$f_{0}(|\mathcal{P}|+i)$ (Lemma 6). With the observation of Lemma 4, we
retrieve from the ”follower specifications” of this sequence of nodes a ”bad
sequence” and we apply the ”Length function theorem” to bound
$\mathbf{altmax}$. This yields in turn a bound on the size of the root of
$\tau$. In order to bound $\mathbf{altmin}$, we proceed similarly, using ”boss
nodes” this time. We follow a branch from the root to a node of ”altitude”
$\mathbf{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
4, and whose growth can be bounded using Lemma 6 and the bound on
$\mathbf{altmax}$. We apply the ”Length function theorem” to bound
$|\mathbf{altmin}|$.

Once we have bounded $\mathbf{altmax}$ and $\mathbf{altmin}$, we can infer a
bound on the size of all nodes (Lemma 6), 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 ”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 0.G:

See 3.1

###  4.2 Undecidability of the ”target problem”

A natural next problem, after , is the ”target problem” (). 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 8 ()

is undecidable for ”BNRA”, even with two registers.

######  Proof (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 0.H.

##  5 Cover in 1-BNRA

In this section, we establish the -completeness of the restriction of 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 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 $\mlq{\neq}\mrq$
tests. In the end, our main challenge for 1-BNRA is $\mlq{=}\mrq$ 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_{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 upper bound.

The 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 5.1 ()

The ”coverability problem” for 1-BNRA is -complete.

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

##  6 Conclusion

We established the decidability (and
$\mathbf{F}_{\omega^{\omega}}$-completeness) of the coverability problem for
BNRA, as well as the -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, 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

##  Appendix 0.A Proof of Proposition 11

See 11

###### 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\\{\mathsf{read}(x),\mathsf{write}(x)\mid
x\in\Sigma\\}\times L$; $\mathsf{write}(x)$ corresponds to writing $x$ at the
end of the channel and $\mathsf{read}(x)$ to reading $x$ at the beginning 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^{\prime},w^{\prime})$ using $d\in D$, denoted
$(l,w)\xrightarrow{d}_{\mathcal{L}}(l^{\prime},w^{\prime})$, when

  * •

$d=(l,\mathsf{write}(x),l^{\prime})$ for some $x\in\Sigma$ and
$w^{\prime}\subword w\cdot x$,

  * •

$d=(l,\mathsf{read}(x),l^{\prime})$ for some $x\in\Sigma$ and $x\cdot
w^{\prime}\subword w$.

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

The existence of a step is denoted
$(l,w)\xrightarrow{}_{\mathcal{L}}(l^{\prime},w^{\prime})$, and its transitive
closure is denoted $\xrightarrow{*}_{\mathcal{L}}$. The (location)
””reachability problem@@lcs”” 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@@lcs”.

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 7(a).

The predecessor graph of a run of $\mathcal{P}$, defined by the graph
$(\mathbb{A},E)$ where $(a^{\prime},a)\in E$ whenever $a^{\prime}$ 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
predecesor; 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 $\mathbf{wait}$, an agents will receive the location $l$ from its
predecessor and go to state $\mathbf{s}(l)$; from there, it will non-
deterministically pick a transition of $\mathcal{L}$ and apply it. See Figure
7(b) for a depiction of transitions from some state $\mathbf{s}(l_{1})$ (all
$\mathbf{s}(l)$, $l\neq l_{1}$, and corresponding transitions are omitted in
the figure). Finally, the objective state of our system is
$q_{f}:=\mathbf{f}(l_{f})$.

$q_{0}$rootlink$\mathbf{f}(l_{0})$$\mathbf{wait}$$\textbf{br}(\mathsf{init},1)$$\textbf{br}(\mathsf{l_{s}},1)$$\textbf{br}(\mathsf{\\#},1)$$\textbf{rec}(\mathsf{init},2,\downarrow)$$\textbf{br}(\mathsf{init},1)$
(a) The initial part of $\mathcal{P}$

$\mathbf{wait}$$\mathbf{s}(l_{1})$$\mathbf{t}(d)$$\mathbf{u}(d)$$\mathbf{f}(l_{2})$$\mathbf{t}(d^{\prime})$$\mathbf{u}(d^{\prime})$$\mathbf{f}(l_{3})$$\textbf{rec}(\mathsf{l_{1}},2,{=})$$\textbf{br}(\mathsf{l_{2}},1)$$\textbf{rec}(\mathsf{a},2,{=})$$\textbf{rec}(\mathsf{a},2,{=})$$\textbf{br}(\mathsf{a},1)$$\textbf{rec}(\mathsf{b},2,{=})$$\textbf{br}(\mathsf{b},1)$$\textbf{rec}(\mathsf{\\#},2,{=})$$\textbf{br}(\\#,1)$$\textbf{br}(\mathsf{a},1)$$\textbf{rec}(\mathsf{a},2,{=})$$\textbf{rec}(\mathsf{b},2,{=})$$\textbf{br}(\mathsf{b},1)$$\textbf{rec}(\mathsf{\\#},2,{=})$$\textbf{br}(\\#,1)$$\textbf{br}(\mathsf{l_{3}},1)$$\textbf{br}(\mathsf{a},1)$
(b) Part of $\mathcal{P}$ encoding transitions from $l_{1}$. Here,
$\mathcal{L}$ has symbols $\Sigma=\\{\mathsf{a},\mathsf{b}\\}$ and there are
two transitions from $l_{1}$: $d=(l_{1},\mathsf{read}(a),l_{2})$ and
$d^{\prime}=(l_{1},\mathsf{write}(b),l_{3})$.

Figure 7: Depiction of the protocol $\mathcal{P}$ built in the ”lossy channel
system” reduction of Proposition 11.

We claim that $(\mathcal{P},q_{f})$ is a positive instance of if 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{*}_{\mathcal{L}}(l_{f},w)$.
Decompose the witness into
$(l_{0},w_{0})\xrightarrow{}_{\mathcal{L}}(l_{1},w_{1})\xrightarrow{}_{\mathcal{L}}(l_{2},w_{2})\cdots\xrightarrow{}_{\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 $\mathbb{A}:=\\{0,\dots,n\\}$.
Agent $0$ becomes the ”root” and for all $i\geq 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 $\mathbf{f}(l_{i})$ and
the sequence of ”message types” sent by agent $i$ admits as subword
$\mathsf{init}\cdot\mathsf{l_{i}}\cdot w_{i}\cdot\mathsf{\\#}$. 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
$\mathbf{s}(l_{i})$. It moves to $\mathbf{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 $\mathbf{f}(l_{i+1})$.

  * •

if $d=(l_{i},\mathsf{write}(x),l_{i+1})$ is a push, then
$w_{i+1}=w_{i}^{\prime}\cdot y$ where $w_{i}^{\prime}\subword w_{i}$ and
$y\in\\{\varepsilon,x\\}$. We can make agent $i+1$ broadcast
$\mathsf{init}\cdot\mathsf{l_{i}}\cdot w^{\prime}_{i}\cdot x\cdot\mathsf{\\#}$
which admits as subword $\mathsf{init}\cdot\mathsf{l_{i+1}}\cdot
w_{i+1}\cdot\mathsf{\\#}$.

  * •

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

This concludes the induction step. When applied to $i=n$, this builds an
”initial run” where agent $n$ ends on $\mathbf{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
$\mathsf{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
$\mathbf{f}(l_{i})$ and broadcasts a word of the form $\mathsf{init}\cdot
l_{i}\cdot w_{i}\cdot\mathsf{\\#}$; 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.

##  Appendix 0.B Definitions and Notations of Section 4

We will first define the notion of decomposition, which is a formalization of
the observation in Example 1. A ””decomposition”” is a tuple
$\mathtt{dec}=(w_{0},m_{1},\ldots,m_{\ell},w_{\ell})$ with
$w_{0},\ldots,w_{\ell}\in\mathcal{M}^{*}$, and
$m_{1},\cdots,m_{\ell}\in\mathcal{M}$, with $m_{i}\neq m_{j}$ for all $i\neq
j$. In particular we have $\ell\leq|\mathcal{M}|$. A word
$w\in\mathcal{M}^{*}$ ””admits decomposition””
$\mathtt{dec}=(w_{0},m_{1},\ldots,m_{\ell},w_{\ell})$ if $w\subword
w^{\prime}_{0}w^{\prime}_{1}\cdots w^{\prime}_{\ell}$ where for all $j$,
$w^{\prime}_{j}$ can be obtained from $w_{j}$ by adding letters from
$\\{m_{1},\ldots,m_{j}\\}$. We denote by $\intro*\langdec{\mathtt{dec}}$ the
language of words that ”admit decomposition” $\mathtt{dec}$.

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

###### Definition 1

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

  * •

a ”local run” of $\mathcal{P}$, written $\reintro*\localrunlabel{\mu}$,
starting in the initial state with distinct register values;

  * •

a value in $\mathbb{N}$, written $\reintro*\valuelabel{\mu}$;

  * •

a specification $\reintro*\speclabel{\mu}$, which is either a word
$\intro*\bosslabel{\mu}\in\mathcal{M}^{*}$ (””boss specification””) or a pair
$(\intro*\followlabelword{\mu},\intro*\followlabelmessage{\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:

  1. (i)

For each ”non-initial value” $v\neq\valuelabel{\mu}$ of $\localrunlabel{\mu}$,
$\mu$ has a child $\mu^{\prime}$ which is a ”boss node” such that
$\vinput{v}{\localrunlabel{\mu}}$ is a subword of $\bosslabel{\mu^{\prime}}$.

  2. (ii)

For each ”initial value” $v$ in $\localrunlabel{\mu}$, there is a
”decomposition”
$\mathtt{dec}=(w_{0},m_{1},w_{1},\ldots,m_{\ell},w_{\ell})$ s.t.:

     * •

$\localrunlabel{\mu}$ may be split into successive ”local runs”
$u_{0},\dots,u_{\ell}$ where, for all $i\in[1,\ell]$,
$w_{i}\subword\voutput{v}{u_{i}}$ and
$\vinput{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 $\followlabelmessage{\mu_{i}}=m_{i}$ and
$\followlabelword{\mu_{i}}\in\langdec{\mathtt{dec}_{i}}$ where
$\mathtt{dec}_{i}=(w_{0},m_{1},w_{1},\ldots,m_{i-1},w_{i-1})$.

  3. (iii)

If $\mu$ is a ”follower node” then $\valuelabel{\mu}$ is not an ”initial
value” of $u$, $\vinput{\valuelabel{\mu}}{u}\subword\followlabelword{\mu}$ and
$\voutput{\valuelabel{\mu}}{u}$ contains $\followlabelmessage{\mu}$.

  4. (iv)

If $\mu$ is a ”boss node”, then $\valuelabel{\mu}$ is an ”initial value” of
$\localrunlabel{\mu}$ and the ”decomposition” $\mathtt{dec}$ of (ii) for
$\valuelabel{\mu}$ satisfies that $\bosslabel{\mu}\in\langdec{\mathtt{dec}}$.

Lastly, as before, given $\tau$ an ”unfolding tree”, we define its
””size@@tree”” by
$|\tau|:=\sum_{\mu\in\tau}|\localrunlabel{\mu}|+|\speclabel{\mu}|+1$.

We now explain this definition. Let $\mu$ be a node of an ”unfolding tree”
$\tau$ and let $u:=\localrunlabel{\mu}$. As before, $u$ encodes the ”local
run” of a given agent, $\speclabel{\mu}$ encodes the specification that this
”local run” carries out and $\valuelabel{\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”
$\localrunlabel{\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 $\vinput{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 $\vinput{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”
$\mathtt{dec}=(w_{0},m_{1},w_{1},\ldots,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},\ldots,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
$\voutput{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}^{\prime}\cdot w_{1}^{\prime}\cdots w_{i-1}^{\prime}$
where, for all $j\leq i-1$, $w_{j}$ is obtained from $\voutput{v}{u_{i}}$ by
adding symbols from $\\{m_{1},\dots,m_{j-1}\\}$, which we state as
$\followlabelword{\mu_{i}}\in\langdec{\mathtt{dec}_{i}}$.

Condition (iii) directly states that a ”follower node” $\mu$ receives word
$\followlabelword{\mu}$ with value $\valuelabel{\mu}$ and broadcasts message
$(\followlabelmessage{\mu},\valuelabel{\mu})$. Condition (iv) expresses that a
”boss node” witnesses the broadcast of a sequence of messages
$\bosslabel{\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
$\bosslabel{\mu}\in\langdec{\mathtt{dec}}$ and not simply
$\voutput{\valuelabel{\mu}}{u}\subword\bosslabel{\mu}$.

##  Appendix 0.C Proof of Proposition 3

See 3

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” $\mathsf{bw}$ if there exists
$v\in\mathbb{N}$ such that $\mathsf{bw}$ is a subword of the sequence of
messages sent with value $v$ in $\rho$.

  * •

A ”run” $\rho$ satisfies a ”follower specification”
$(\mathsf{fw},\mathsf{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 $\mathsf{fw}$ and agent $a$ broadcasts $\mathsf{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” $\mathsf{bw}$ if its root
$\mu$ is a ”boss node” and $\mathsf{bw}$ is a subword of its ”specification”
label $\bosslabel{\mu}$.

  * •

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

Note that reduces to the existence of an ”initial run” satisfying a ”boss
specification”: it suffices to consider
$\mathcal{M}^{\prime}:=\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 0.C.1 and a ”run” from an ”unfolding tree” in Section
0.C.2.

###  0.C.1 Construction of an ”unfolding tree” from an ”initial run”

###### Lemma 1

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

###### Proof

We proceed by strong induction on
$\mathbb{N}\times\\{\text{follower},\text{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 $\mathsf{spec}$, there
exist a value $v$ and an agent $a$ in $\rho$ such that:

  * •

if $\mathsf{spec}$ is a ”boss specification” $\mathsf{bw}$, $\mathsf{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 $\mathsf{spec}$ is a ”follower specification” $(\mathsf{fw},\mathsf{fm})$,
then $a$ is an agent whose $v$-”input” is a subword of $\mathsf{fw}$ and that
broadcasts $\mathsf{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” $\mathsf{spec}$ as labels, and attach subtrees to it
so that it forms an ”unfolding tree”.

We do the following for every value $v^{\prime}$ in $u$. If $v^{\prime}$ is
”non-initial” in $u$ and $v^{\prime}\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^{\prime}$ whose root
is a ”boss node” with ”boss specification” $\vinput{v^{\prime}}{u}$, and we
attach $\tau^{\prime}$ below $\mu$ in $\tau$. If $v^{\prime}=v$ and
$v^{\prime}$ is ”non-initial” then $\mathsf{spec}$ is a ”follower
specification” and we do not need to add any children, as the
$v^{\prime}$-input of $u$ is covered by the specification. Assume now that
$v^{\prime}$ 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\ldots\cdot\rho_{\ell}$ where, for all
$i\in[1,l]$:

  * •

agents from $\mathbb{A}\setminus\\{a\\}$ do not broadcast $m_{i}$ with value
$v^{\prime}$ in $\rho_{0}\cdot\ldots\cdot\rho_{i-1}$,

  * •

$\rho_{i}$ starts with a broadcast of $m_{i}$ with value $v^{\prime}$ by some
agent $a_{i}\in\mathbb{A}\setminus\\{a\\}$.

Let $w_{i}$ the sequence broadcast by $a$ with value $v^{\prime}$ in
$\rho_{i}$. This forms a ”decomposition”
$\mathtt{dec}:=(w_{0},m_{1},w_{1},\ldots,m_{\ell},w_{\ell})$. For all
$i\in[1,\ell]$, we write $\mathtt{dec}_{i}$ for the ”decomposition”
$\mathtt{dec}_{i}=(w_{0},m_{1},w_{1},\ldots,m_{i-1},w_{i-1})$. For every
$i\in[1,\ell-1]$, let $\tilde{\rho}_{i}$ the run
$\rho_{0}\cdot\ldots\cdot\rho_{i-1}$ plus the first step of $\rho_{i}$ (where
$(m_{i},v^{\prime})$ is broadcast). Let $w_{i}^{\prime}$ the
$v^{\prime}$-”input” of $a_{i}$ in $\tilde{\rho}_{i}$: it is in
$\langdec{\mathtt{dec}_{i}}$ by construction of $\mathtt{dec}$. Agent $a_{i}$
is a witness that $\tilde{\rho}_{i}$ satisfies ”follower specification”
$(w^{\prime}_{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}^{\prime},m_{i})$. If
$\tilde{\rho_{i}}=\rho$, then $i=\ell$, $v^{\prime}=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^{\prime}=v$, $v$ is ”initial” for $a$ and
$\mathsf{spec}$ is a ”boss specification” $\mathsf{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}^{\prime},m_{\ell})$. We have obtained, for every $i\in[1,\ell]$, an
”unfolding tree” $\tau_{i}$ satisfying ”follower specification”
$(w_{i}^{\prime},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 $\mathsf{spec}$ for
agent $a$. We have therefore built an ”unfolding tree” $\tau$ satisfying
$\mathsf{spec}$.

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

######  Lemma 2 ()

If there exists an ”unfolding tree” over $\mathcal{P}$ satisfying a ”boss
specification” $\mathsf{bw}\in\mathcal{M}^{*}$ then there exists an ”initial
run” $\rho$ of $\mathcal{P}$ satisfying $\mathsf{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 3

Let $\gamma,\gamma^{\prime}$ two configurations.

A ””partial step”” $\gamma\xrightarrow{}_{p}\gamma^{\prime}$ is defined if
either $\gamma\xrightarrow{}\gamma^{\prime}$ (normal ”step”) or there exist
$m\in\mathcal{M}$, $v\in\mathbb{N}$ such that for all agent $a$ either
$\gamma(a)=\gamma^{\prime}(a)$ or
$\gamma(a)\xrightarrow{\mathsf{ext}(\delta,v)}\gamma^{\prime}(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@@partial”” if it starts in an ”initial configuration”. The $v$-input
$\reintro*\vinput{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 $\reintro*\voutput{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 2:

###### Lemma 4

For every ”unfolding tree” $\tau$:

  * •

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

  * •

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

    * –

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

    * –

$\vinput{v}{\rho}\subword\mathsf{fw}$,

    * –

$\voutput{v}{\rho}$ contains $\mathsf{fm}$.

###### Proof

We prove it by induction on the ”size” of the ”unfolding tree”. Let $\tau$ be
a ”unfolding tree”, $\mu$ its root, $u:=\localrunlabel{\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.

####  0.C.2.1 Step 1: ”Non-initial Values”

For each non-initial value $v\neq\valuelabel{\mu}$ of $u$, $\mu$ has a ”boss”
child of specification $w$ such that $\vinput{v}{u}\subword w$. By induction
hypothesis, there is an ”initial run” $\rho^{\prime}$ satisfying ”boss
specification” $w$. Up to renaming agents, assume that $\rho$ and
$\rho^{\prime}$ have disjoint agents. We rename values in $\rho^{\prime}$ so
that $w$ is broadcast in $\rho^{\prime}$ with value $v$, and $\rho^{\prime}$
has no other shared value with $\rho$. We use the broadcasts made by
$\rho^{\prime}$ 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.

####  0.C.2.2 Step 2: ”Initial Values”

Let $v$ be an ”initial value” of $u$, and $\mathtt{dec}=\\\
(w_{0},m_{1},w_{1},\ldots,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 $\followlabelmessage{\mu_{j}}=m_{j}$ and
$\followlabelword{\mu_{j}}\in\langdec{\mathtt{dec}_{j}}$ with
$\mathtt{dec}_{j}=(w_{0},m_{1},w_{1},\ldots,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},\ldots,\rho_{\ell}$ with
$w_{i}\subword\voutput{v}{\rho_{i}}$ and
$\vinput{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$, $\vinput{v}{\tilde{\rho_{j}}}\subword\followlabelword{\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 $\followlabelword{\mu_{j}}\in\langdec{\mathtt{dec}_{j}}$
and $\vinput{v}{\tilde{\rho_{j}}}\subword\followlabelword{\mu_{j}}$, we can
split $\tilde{\rho}_{j}$ into $\tilde{\rho}_{j,0},\ldots,\tilde{\rho}_{j,j-1}$
so that $\vinput{v}{\tilde{\rho}_{j,i}}\subword\tilde{w}_{j,i}$ where
$\tilde{w}_{j,i}$ can be obtained by adding letters from
$\\{m_{1},\ldots,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},\ldots,m_{i}$. We obtain a run
section whose $v$-”output” still contains $w_{i}$ and whose ”$v$-input” only
contains $m_{1},\ldots,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

$\localrunlabel{\mu}$$\rho_{1}$$\rho_{2}$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}c\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}c\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\bosslabel{\mu}=aac$$\rho_{1}\text{
satisfies }(a,b)$$\rho_{2}\text{ satisfies
}(ab,c)$$\mathtt{dec}=(a,b,a,c,\varepsilon)$$\mathtt{dec}_{1}=(a)$$\mathtt{dec}_{2}=(a,b,a)$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}c\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}c\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\rho_{2}$$\localrunlabel{\mu}$
We compose $\localrunlabel{\mu}$ with $\rho_{2}$ to obtain a ”partial run”
$\rho^{\prime}$ which outputs the desired word $aac$
$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}c\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}c\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{rec}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}})$$\textbf{br}(\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}c\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$$\rho_{2}$$\rho^{\prime}$
We compose $\rho^{\prime}$ 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”. Figure 8: An illustration of
the composition operation from the proof of Lemma 2

The resulting run $\rho^{\prime}$ can still be split into
$\rho^{\prime}_{0}\cdots\rho^{\prime}_{\ell}$ where
$w_{i}\subword\voutput{v}{\rho_{i}}$ and
$\vinput{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=\valuelabel{\mu}$ then we have
$\bosslabel{\mu}\in\langdec{\mathtt{dec}}$, and we need to ensure that
$\bosslabel{\mu}$ is broadcast in $\rho$ with value $v$. Let
$\mathsf{bw}_{0},\ldots,\mathsf{bw}_{\ell}$ such that
$\bosslabel{\mu}\subword\mathsf{bw}_{0}\cdots\mathsf{bw}_{\ell}$ and for all
$j$, $\mathsf{bw}_{j}$ can be obtained by adding letters from
$\\{m_{1},\ldots,m_{j}\\}$ in $w_{j}$. We use the composition operation to
extend the output of $\rho$, so that
$\mathsf{bw}_{i}\subword\voutput{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},\ldots,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=\valuelabel{\mu}$ and $\mu$ is a ”boss node”,
$\bosslabel{\mu}\subword\voutput{v}{\rho}$.

####  0.C.2.3 Concluding the procedure

We distinguish two cases depending on the type of ”specification” of $\mu$.

  * •

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

  * •

if $\mu$ is a ”follower node”, we apply steps $1$ and $2$ to every value in
$V\setminus\\{\valuelabel{\mu}\\}$ to obtain a ”partial run” $\rho$ with no
”unmatched reception” on values different from $\valuelabel{\mu}$. Moreover,
because the behavior of $\rho$ with respect to $\valuelabel{\mu}$ is the one
of $u$, we have that $\vinput{\valuelabel{\mu}}{\rho}\subword\mathsf{fw}$ and
$\voutput{\valuelabel{\mu}}{\rho}$ contains $\mathsf{fm}$, concluding the
proof.

##  Appendix 0.D Proof of Lemma 4

See 4

###### Proof

Let $\tau_{\mu}$, $\tau_{\mu^{\prime}}$ be the subtrees rooted in $\mu$,
$\mu^{\prime}$ respectively. Let $\tau^{\prime}$ be the tree obtained by
replacing $\tau_{\mu}$ with $\tau_{\mu^{\prime}}$; it is strictly smaller than
$\tau$. We prove that $\tau^{\prime}$ 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^{\prime}$. Assume that $\mu$ is not
the root of $\tau$, and let $\mu_{p}$ its parent in $\tau^{\prime}$. 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
$\vinput{v}{\localrunlabel{\mu_{p}}}\subword\bosslabel{\mu}\subword\bosslabel{\mu^{\prime}}$
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
$\followlabelmessage{\mu}=m_{i}$ and
$\followlabelword{\mu}\in\langdec{\mathtt{dec}_{i}}$. In this case, we also
have $\followlabelmessage{\mu^{\prime}}=m_{i}$ and, because
$\followlabelword{\mu^{\prime}}\subword\followlabelword{\mu}$ and
$\langdec{\mathtt{dec}_{i}}$ is closed by subword, we have
$\followlabelword{\mu^{\prime}}\in\langdec{\mathtt{dec}_{i}}$ and condition
(ii) is satisfied. In both cases, $\tau^{\prime}$ is an ”unfolding tree” with
the same root specification as $\tau$ hence a ”coverability witness”.

##  Appendix 0.E Generalization of Lemma 7

See 5

The function $\psi$ is actually not the same as in Lemma 7 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
$(\\{\mathsf{ext}(\delta,v)\mid\delta\in\Delta,v\in\mathbb{N}\\}\cup\\{\mathsf{int}(\delta)\mid\delta\in\Delta\\})^{*}$.
The ”trace” of a ”local run” $u$ is the ”trace” $\mathsf{tr}(u)$ corresponding
to the ”local steps” performed in $u$. Given a ”trace” $\mathsf{tr}$, we write
$(q,\nu)\xrightarrow{\mathsf{tr}}(q^{\prime},\nu^{\prime})$ when there exists
a ”local run” of ”trace” $\mathsf{tr}$ from $(q,\nu)$ to
$(q^{\prime},\nu^{\prime})$.

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_{0}$ ($W$ then contains $r$ values) and $V$ the set of values
appearing in $u_{0}$, $u$ or $u_{f}$.

###### Lemma 1

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,\nu)\xrightarrow{*}(q^{\prime},\nu^{\prime})$ 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^{\prime}:(q,\nu)\xrightarrow{*}(q^{\prime},\nu^{\prime})$ such that we have
$\mathsf{len}(u^{\prime})\leq\psi(|\mathcal{P}|-r+|W|,r)$ and:

  1. 1.

for all $v\in V$, $\vinput{v}{u^{\prime}}\subword\vinput{v}{u}$,

  2. 2.

for all $v^{\prime}\in\mathbb{N}\setminus V$, there exists
$v\in\mathbb{N}\setminus W$ such that
$\vinput{v^{\prime}}{u^{\prime}}\subword\vinput{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^{\prime}$,
because the initial values in $u$ would not correspond to the ones in
$u^{\prime}$. This is why we state the lemma for every $W\subseteq V$.

Original local runreg $1$reg $2$reg $3$reg $4$$v$$v$$\mlq\downarrow\mrq$
actionsremoved partShortened local runreg $1$reg $2$reg $3$reg
$4$$s,\Theta$$v$fresh values$s,\Theta$$s,\Theta$ Figure 9: Illustration of the
proof of Lemma 5. $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.

###### Proof

Given a ”local run” $u$, register $i$ is ””active”” in $u$ if at least one
$\mlq\downarrow\mrq$ step on register $i$ is performed in $u$.

We define the function $\psi(n,k)$ recursively as $\psi(n,0)=n+1$ and
$\psi(n,k+1)=2(\psi(n,k)+1)[(n+1)^{4(\psi(n,k)+1)}+1]$. This function is
clearly primitive recursive, although non-elementary; it grows as a tower of
exponentials of height $k$ where each floor of the tower is polynomial in $n$.

We prove the ””shortening property””:
Let $W$ a finite set a values and $n:=|\mathcal{P}|-r+|W|$. Let a ”local run”
$u:(q_{i},\nu_{i})\xrightarrow{*}(q_{f},\nu_{f})$ with $k$ ”active registers”
with $\mathsf{len}(u)>\psi(n,k)$ and let $V\subseteq\mathbb{N}$ finite that
contains every message value appearing in $u$ such that $W\subseteq V$. We
claim that $u$ can be shortened into a local run
$u^{\prime}:(q_{i},\nu_{i})\xrightarrow{*}(q_{f},\nu_{f})$ with $k$ active
registers such that $\mathsf{len}(u^{\prime})<\mathsf{len}(u)$ and:

  * •

for all $v\in V$, $\vinput{v}{u^{\prime}}\subword\vinput{v}{u}$,

  * •

for all $v^{\prime}\in\mathbb{N}\setminus V$, there exists
$v\in\mathbb{N}\setminus W$ such that $\vinput{v^{\prime}}{u^{\prime}}$ is a
subword of $\vinput{v}{u}$.

We proceed by induction on the number $k$ of ”active registers” in the ”local
run”. If $k=0$, register values do not change in $u$. As
$\psi(n,0)=n+1\geq|Q|+1$, $u$ goes through the same state twice, hence all
steps in between may be removed to get $u^{\prime}$. Then for all
$v\in\mathbb{N}$, $\vinput{v}{u^{\prime}}\subword\vinput{v}{u}$.

Suppose that the property is true for any ”local run” with $\leq k$ ”active
registers”, and consider one $u:(q_{i},\nu_{i})\xrightarrow{*}(q_{f},\nu_{f})$
with $k+1$ ”active registers” such that
$\mathsf{len}(u)>\psi(|\mathcal{P}|-r+|W|,k+1)$.

First, if there exists an infix ”local run” $u_{i}$ of $u$ of length
$\psi(n,k)+1$ with only $k$ active registers, then it suffices to apply the
induction hypothesis on $u_{i}$. Suppose now that there exists no such infix
”local run”. Let $I\subseteq[1,r]$ the set of ”active registers” in $u$,
$|I|=k+1$. Let $M:=\psi(n,k){+}1$, we have
$\psi(n,k+1)=2M[((n+1)^{2})^{2M}+1]$. In any sequence of $M$ ”local steps” in
a row in $u$, there is a $\mlq\downarrow\mrq$ transition on every register in
$I$. We can assume that no local configuration appears twice in $u$ (otherwise
we can simply cut the steps between those two appearances to get
$u^{\prime}$).

In what follows we will consider two infixes of $u$ of length $2M$, following
the same sequence of transitions and with the same values of $W$ appearing at
the same times in the same registers. Their existence is guaranteed by the
length of $u$. As a $\mlq\downarrow\mrq$ action is performed twice on each
register in those two infixes, we will be able to reduce the run as in Fig. 9.

For every $i$, let $\delta_{i}$ the $i$-th transition in $u$, and let
$\theta_{i}\in W\cup\\{\bot\\}$ be such that

$\theta_{i}=\begin{cases}&v\text{ if the $i$th step of $u$ is a "reception
step" $\mathsf{ext}(\delta_{i},v)$ with $v\in W$ }\\\ &\bot\text{
otherwise}\end{cases}$

For every $i\in[0,(n+1)^{4M}]$, we write $s_{i}$ the sequence $\delta_{2M\cdot
i+1},\delta_{2M\cdot i+2},\cdots,\delta_{2M\cdot i+2M}$ and $\Theta_{i}$ the
sequence $\theta_{2M\cdot i},\theta_{2M\cdot i+1},\cdots,\theta_{2M\cdot
i+2M}$. There are $|\Delta|^{2M}$ possible sequences for $s_{i}$ and
$[|W|+1]^{2M}$ possible sequences for $\Theta_{i}$. By the pigeonhole
principle there exist two indices $i_{a},i_{b}$ such that the sequences
$s_{i_{a}}$ and $s_{i_{b}}$ are equal and also the sequences $\Theta_{i_{a}}$
and $\Theta_{i_{b}}$ are equal (as $|\Delta|(|W|+1)\leq(n+1)^{2}$ because
$n=|\mathcal{P}|-r+|W|$). There exist two infix ”local runs”
$u_{a}:(q_{1},\nu_{1})\xrightarrow{*}(q_{2},\nu_{2})$,
$u_{b}:(q_{3},\nu_{3})\xrightarrow{*}(q_{4},\nu_{4})$ in $u$ such that
$(q_{2},\nu_{2})$ appears strictly before $(q_{3},\nu_{3})$ in $u$ and $u_{a}$
and $u_{b}$ both have the same sequences of transitions, which we call $s$,
and of receptions of values from $W$, which we call $\Theta$.

Although $u_{a}$ and $u_{b}$ have the same sequence of transitions, their
”traces” may differ because their ”reception steps” may have different values.
We build a ”trace” $\mathsf{tr}$ such that
$(q_{1},\nu_{1})\xrightarrow{\mathsf{tr}}(q_{4},\nu_{4})$ where the underlying
sequence of transitions of $\mathsf{tr}$ is $s$ and the receptions of values
of $W$ match $\Theta$.

For every active register $i\in I$, let $e_{i}\in[1,2M]$ denote the index of
the first $\mlq\downarrow\mrq$ on register $i$ in $s$ and $f_{i}\in[1,2M]$ the
index of the last $\mlq\downarrow\mrq$ on register $i$ in $s$. By hypothesis,
because $s$ is of length $2M$, it contains at least two $\mlq\downarrow\mrq$
on register $i$, one in the first half and one in the second half, hence
$e_{i}\leq M<M+1\leq f_{i}$.

For every $j\in[1,2M]$, let $\delta_{j}$ denote the $j$-th transition of $s$.
First, if $\delta_{j}$ is a ”broadcast”, we define the $j$-th ”local step” of
$\mathsf{tr}$ as $\mathsf{int}(\delta_{j})$. Suppose now that $\delta_{j}$ is
a ”reception” of the form $\textbf{rec}(m,i,\alpha)$. The $j$-th ”local step”
of $u_{a}$ (resp. $u_{b}$) has underlying transition $\delta_{j}$ hence is a
”reception step” of the form $\mathsf{ext}(\delta_{j},v_{a})$ for some
$v_{a}\in V$ (resp. $\mathsf{ext}(\delta_{j},v_{b})$ for some $v_{b}\in V$).
Because $V$ is finite and $W\subseteq V$, there exists an injective function
$\phi:V\rightarrow\mathbb{N}$ such that for all $v\in W$, $\phi(v)=v$ and for
all $v\notin W$, $\phi(v)\notin V$. We define the $j$-th ”local step” of
$\mathsf{tr}$ to be $\mathsf{ext}(\delta_{j},v)$ where:

  * •

if $i\notin I$ then its value stays the same throughout $u$, then we set
$v=v_{a}(=v_{b})$

  * •

if $i\in I$ then

    * –

if $j<e_{i}$, $v=v_{a}$,

    * –

if $e_{i}\leq j<f_{i}$, $v=\phi(v_{a})$,

    * –

if $f_{i}\leq j$, $v=v_{b}$.

We now claim that $(q_{1},\nu_{1})\xrightarrow{\mathsf{tr}}(q_{4},\nu_{4})$.
First, for every active register $i$, the last $\mlq\downarrow\mrq$ step on
register $i$ has value $\nu_{4}(i)$ in $\mathsf{tr}$ (as we are in the case
$f_{i}\leq j$). Hence if every ”local step” is valid then the final ”local
configuration” is $(q_{4},\nu_{4})$. For every $l\in[0,2M]$, let
$\mathsf{tr}_{l}$ denote the prefix of $\mathsf{tr}$ of length $l$. We prove
by induction on $l$ that $\mathsf{tr}_{l}$ is valid from $(q_{1},\nu_{1})$. It
is trivially true for $l=0$. Assume that we have
$(q_{1},\nu_{1})\xrightarrow{\mathsf{tr}_{l}}(q,\nu)$ and let $\lambda$ such
that $\mathsf{tr}_{l}\cdot\lambda=\mathsf{tr}_{l+1}$. Let $\delta$ the
underlying transition of $\lambda$. First, $q$ is the initial state of
$\delta$ because $\lambda$ is valid at step $l+1$ of $u_{a}$ (and $u_{b}$).
Hence if $\delta$ is a ”broadcast” then $\lambda$ is valid from $(q,\nu)$.
Suppose now that $\lambda$ is a ”reception step”; let
$\delta=:\textbf{rec}(m,i,\alpha)$. Let $v_{a}$, $v_{b}$ be the value of
$\lambda$ in $u_{a}$ and $u_{b}$ respectively.

Let $\nu_{a},\nu_{b}$ be the content of registers after the $l$-th step in
$u_{a}$ and $u_{b}$ respectively. If $i\notin I$ then $\alpha$ is either
$\mlq{*}\mrq$ or a test, which is valid as $\nu(i)=\nu_{a}(i)=\nu_{b}(i)$
(value of register $i$ does not change in $u$). Suppose now that $i\in I$, the
only problematic case is the one of tests, _i.e._ ,
$\alpha\in\\{\mlq{\neq}\mrq,\mlq{=}\mrq\\}$. In this case, we prove that
$v\mathrel{\alpha}\nu(i)$. First, because the corresponding step is valid in
$u_{a}$ and $u_{b}$, we have $\nu_{a}(i)\mathrel{\alpha}v_{a}$ and
$\nu_{b}(i)\mathrel{\alpha}v_{b}$. We distinguish cases depending on $l+1$:

  * •

$l+1<e_{i}$: $\nu(i)=\nu_{a}(i)$, $v=v_{a}$ and
$\nu_{a}(i)\mathrel{\alpha}v_{a}$.

  * •

$e_{i}\leq l+1<f_{i}$: We have $v=\phi(v_{a})$. Moreover, because $e_{i}<l+1$,
there is at least one $\mlq\downarrow\mrq$ on register $i$ in
$\mathsf{tr}_{l}$. Consider the last such transition in $\mathsf{tr}_{l}$; its
index $j$ satisfies $e_{i}\leq j<f_{i}$ by definition of $e_{i}$, hence the
value of the corresponding ”reception step” in $u_{a}$ is $\nu_{a}(i)$ and its
value in $\mathsf{tr}_{l}$ is $\phi(\nu_{a}(i))$. One has
$\nu_{a}(i)\mathrel{\alpha}v_{a}$ therefore (by injectivity of $\phi$ for
$\alpha=\mlq{\neq}\mrq$) $\phi(\nu_{a}(i))\mathrel{\alpha}\phi(v_{a})$.

  * •

$f_{i}\leq l+1$: $\nu(i)=\nu_{b}(i)$ and $v=v_{b}$, and because the ”internal
step” is valid in $u_{b}$ we have $\nu_{b}(i)\mathrel{\alpha}v_{b}$.

This proves that $\lambda$ is valid from $(q,\nu)$ which concludes the
induction. We have proven that
$(q_{1},\nu_{1})\xrightarrow{\mathsf{tr}}(q_{4},\nu_{4})$; moreover