*Proof.* Given a local run $u$, register $i$ is *active* in $u$ if at least one `↓` 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 $\text{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' : (q_i, \nu_i) \xrightarrow{*} (q_f, \nu_f)$ with $k$ active registers such that $\text{len}(u') < \text{len}(u)$ and:

- for all $v \in V$, $\text{ln}_v(u') \preceq \text{ln}_v(u)$,

- for all $v' \in \mathbb{N} \setminus V$, there exists $v \in \mathbb{N} \setminus W$ such that $\text{ln}_{v'}(u')$ is a subword of $\text{ln}_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 \ge |Q|+1$, $u$ goes through the same state twice, hence all steps in between may be removed to get $u'$. Then for all $v \in \mathbb{N}$, $\text{ln}_v(u') \preceq \text{ln}_v(u)$.

Suppose that the property is true for any local run with $\le k$ active registers, and consider one $u : (q_i, \nu_i) \xrightarrow{*} (q_f, \nu_f)$ with $k+1$ active registers such that $\text{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 `↓` 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'$).

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 `↓` 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 \{\perp\}$ be such that

$$ \theta_i = \begin{cases} v & \text{if the } i\text{th step of } u \text{ is a reception step } \text{ext}(\delta_i, v) \text{ with } v \in W \\ \perp & \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}, \dots, \delta_{2M \cdot i+2M}$ and $\Theta_i$ the sequence $\theta_{2M \cdot i}, \theta_{2M \cdot i+1}, \dots, \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
*Proof.* Given a local run $u$, register $i$ is active in $u$ if at least one `↓` 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) \stackrel{*}{\to} (q_f, \nu_f)$ with $k$ active registers with $\text{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' : (q_i, \nu_i) \stackrel{*}{\to} (q_f, \nu_f)$ with $k$ active registers such that $\text{len}(u') < \text{len}(u)$ and:

- for all $v \in V$, $\text{ln}_v(u') \preceq \text{ln}_v(u)$,

- for all $v' \in \mathbb{N} \setminus V$, there exists $v \in \mathbb{N} \setminus W$ such that $\text{ln}_{v'}(u')$ is a subword of $\text{ln}_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 \ge |Q|+1$, $u$ goes through the same state twice, hence all steps in between may be removed to get $u'$. Then for all $v \in \mathbb{N}$, $\text{ln}_v(u') \preceq \text{ln}_v(u)$.

Suppose that the property is true for any local run with $\le k$ active registers, and consider one $u : (q_i, \nu_i) \stackrel{*}{\to} (q_f, \nu_f)$ with $k+1$ active registers such that $\text{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 `↓` 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'$).

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 `↓` 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 \{\perp\}$ be such that

$$ \theta_i = \begin{cases} v & \text{if the } i\text{th step of } u \text{ is a reception step } \text{ext}(\delta_i, v) \text{ with } v \in W \\ \perp & \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}, \dots, \delta_{2M \cdot i+2M}$ and $\Theta_i$ the sequence $\theta_{2M \cdot i}, \theta_{2M \cdot i+1}, \dots, \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) \le (n+1)^2$ because $n = |\mathcal{P}|-r+|W|$). There exist two infix local runs $u_a : (q_1, \nu_1) \stackrel{*}{\rightarrow} (q_2, \nu_2)$, $u_b : (q_3, \nu_3) \stackrel{*}{\rightarrow} (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 tr such that $(q_1, \nu_1) \xrightarrow{\text{tr}} (q_4, \nu_4)$ where the underlying sequence of transitions of 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 `↓` on register $i$ in $s$ and $f_i \in [1, 2M]$ the index of the last `↓` on register $i$ in $s$. By hypothesis, because $s$ is of length $2M$, it contains at least two `↓` on register $i$, one in the first half and one in the second half, hence $e_i \le M < M+1 \le 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 tr as int($\delta_j$). Suppose now that $\delta_j$ is a reception of the form 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 ext($\delta_j, v_a$) for some $v_a \in V$ (resp. 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 tr to be 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 \le j < f_i$, $v = \phi(v_a)$,

• if $f_i \le j$, $v = v_b$.

We now claim that $(q_1, \nu_1) \xrightarrow{\text{tr}} (q_4, \nu_4)$. First, for every active register $i$, the last `↓` step on register $i$ has value $\nu_4(i)$ in tr (as we are in the case $f_i \le 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 $\text{tr}_l$ denote the prefix of tr of length $l$. We prove by induction on $l$ that $\text{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{\text{tr}_l} (q, \nu)$ and let $\lambda$ such that $\text{tr}_{l+1} \cdot \lambda = \text{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 =: \text{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 `*` 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 \{\ne', ='\}$. In this case, we prove that $v \alpha \nu(i)$. First, because the corresponding step is valid in $u_a$ and $u_b$, we have $\nu_a(i) \alpha v_a$ and $\nu_b(i) \alpha v_b$. We distinguish cases depending on $l+1$:

$$- l+1 < e_i: \nu(i) = \nu_a(i), v = v_a \text{ and } \nu_a(i) \alpha v_a.$$
equal and also the sequences $\Theta_{i_a}$ and $\Theta_{i_b}$ are equal (as $|\Delta|(|W| + 1) \le (n + 1)^2$ because $n = |\mathcal{P}|-r+|W|$). There exist two infix local runs $u_a : (q_1, \nu_1) \stackrel{*}{\to} (q_2, \nu_2)$, $u_b : (q_3, \nu_3) \stackrel{*}{\to} (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 tr such that $(q_1, \nu_1) \xrightarrow{\text{tr}} (q_4, \nu_4)$ where the underlying sequence of transitions of 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 `↓` on register $i$ in $s$ and $f_i \in [1, 2M]$ the index of the last `↓` on register $i$ in $s$. By hypothesis, because $s$ is of length $2M$, it contains at least two `↓` on register $i$, one in the first half and one in the second half, hence $e_i \le M < M + 1 \le 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 tr as int($\delta_j$). Suppose now that $\delta_j$ is a reception of the form 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 ext($\delta_j, v_a$) for some $v_a \in V$ (resp. 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 \to \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 tr to be 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 \le j < f_i$, $v = \phi(v_a)$,

• if $f_i \le j$, $v = v_b$.

We now claim that $(q_1, \nu_1) \xrightarrow{\text{tr}} (q_4, \nu_4)$. First, for every active register $i$, the last `↓` step on register $i$ has value $\nu_4(i)$ in tr (as we are in the case $f_i \le 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 $\text{tr}_l$ denote the prefix of tr of length $l$. We prove by induction on $l$ that $\text{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{\text{tr}_l} (q, \nu)$ and let $\lambda$ such that $\text{tr}_{l+1} \cdot \lambda = \text{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 =: \text{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 `*` 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 \{\ne', ='\}$. In this case, we prove that $v \alpha \nu(i)$. First, because the corresponding step is valid in $u_a$ and $u_b$, we have $\nu_a(i) \alpha v_a$ and $\nu_b(i) \alpha v_b$. We distinguish cases depending on $l+1$:

$$- l + 1 < e_i: \nu(i) = \nu_a(i), v = v_a \text{ and } \nu_a(i) \alpha v_a.$$
- $e_i \le l+1 < f_i$: We have $v = \phi(v_a)$. Moreover, because $e_i < l+1$, there is at least one `↓` on register $i$ in $\text{tr}_l$. Consider the last such transition in $\text{tr}_l$; its index $j$ satisfies $e_i \le 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 $\text{tr}_l$ is $\phi(\nu_a(i))$. One has $\nu_a(i) \alpha v_a$ therefore (by injectivity of $\phi$ for $\alpha = \ne$) $\phi(\nu_a(i)) \alpha \phi(v_a)$.

- $f_i \le 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) \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{\text{tr}} (q_4, \nu_4)$; moreover tr is of length $2M$ and there are at least $4M > 2M+1$ steps between $(q_1, \nu_1)$ and $(q_4, \nu_4)$ in $u$. Therefore, replacing this part of $u$ with $(q_1, \nu_1) \xrightarrow{\text{tr}} (q_4, \nu_4)$ yields a shorter local run $u' : (q_i, \nu_i) \xrightarrow{\ast} (q_f, \nu_f)$.

It remains to prove the conditions on the $v$-input of $u'$ for each $v$. If suffices to prove the condition for the part between $(q_1, \nu_1)$ to $(q_4, \nu_4)$, because the rest of $u$ is left untouched.

Let $(q_m, \nu_m)$ the local configuration after $M$ steps of tr from $(q_1, \nu_1)$; write $u_1$ the local run from $(q_1, \nu_1)$ to $(q_m, \nu_m)$ corresponding to the first $M$ steps of tr in $u'$, and $u_2$ the local run from $(q_m, \nu_m)$ to $(q_4, \nu_4)$ corresponding to the last $M$ steps of tr in $u'$.

Let $v \in V$. We claim that $\ln_v(u_1)$ is a subword of $\ln_v(u_a)$ and $\ln_v(u_2)$ is a subword of $\ln_v(u_b)$. Indeed, in the construction of tr, the reception steps in the first $M$ steps were those of $u_a$ except that some values were replaced with fresh values in $N \setminus V$, and similarly with $u_b$ and the last $M$ steps. Overall, this proves that $\ln_v(u')$ is a subword of $\ln_v(u)$ for every $v \in V$ and values of $V$ satisfy condition 1.

Let $v' \in N \setminus V$; $v'$ does not appear in $u$. Either $v'$ does not appear in $u'$ in which case the desired property is true, or there exists $v \in V$ such that $v' = \phi(v)$. As $\phi$ is injective and $\phi(W) = W$ and $v' \notin W$, $v \notin W$. But then $\ln_{v'}(u_1)$ is a subword of $\ln_v(u_a)$ and $\ln_{v'}(u_2)$ is a subword of $\ln_v(u_b)$. Indeed, in $u_1$, the reception steps with value $\phi(v)$ correspond to reception steps in $u_a$ with value $v$, and similarly for $u_2$ and $u_b$. This proves condition 2 for every $v' \in N \setminus V$. Overall, we have proven the existence of a local run $u' : (q_i, \nu_i) \xrightarrow{\ast} (q_f, \nu_f)$ that satisfies conditions 1 and 2 and that is strictly shorter than $u$, which proves the shortening property.

We build a local run of length less that $\psi(|\mathcal{P}|-r+|W|, r)$ as follows. We start with $u^{(0)} := u$ and $V^{(0)}$ the set of values of messages appearing in $u^{(0)}$. For every $k$ such that $\text{len}(u^{(0)}) > \psi(|\mathcal{P}|-r+|W|, r)$, we apply the shortening property on $u^{(k)}$ and $V^{(k)}$ to obtain $u^{(k+1)}$ and define $V^{(k+1)}$ by $V^{(k)} \cup X$ where $X$ is the set of values of messages in $u^{(k+1)}$, which is finite. The construction stops when $\text{len}(u^{(k)}) \le \psi(|\mathcal{P}|-r+|W|, r)$, which concludes the proof of the lemma. $\square$

# F Bounding the Size of the Minimal Coverability Witness

In this section, we prove that we can obtain a computable bound on $\tau$, and that the problem is decidable in complexity class $F_{\omega^\omega}$. All bounds provided in this
- $e_i \le l+1 < f_i$: We have $v = \phi(v_a)$. Moreover, because $e_i < l+1$, there is at least one `↓` on register $i$ in $\mathrm{tr}_l$. Consider the last such transition in $\mathrm{tr}_l$; its index $j$ satisfies $e_i \le 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 $\mathrm{tr}_l$ is $\phi(\nu_a(i))$. One has $\nu_a(i) \alpha v_a$ therefore (by injectivity of $\phi$ for $\alpha = \ne$) $\phi(\nu_a(i)) \alpha \phi(v_a)$.

- $f_i \le 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) \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{\mathrm{tr}} (q_4, \nu_4)$; moreover $\mathrm{tr}$ is of length $2M$ and there are at least $4M > 2M+1$ steps between $(q_1, \nu_1)$ and $(q_4, \nu_4)$ in $u$. Therefore, replacing this part of $u$ with $(q_1, \nu_1) \xrightarrow{\mathrm{tr}} (q_4, \nu_4)$ yields a shorter local run $u' : (q_i, \nu_i) \xrightarrow{\ast} (q_f, \nu_f)$.

It remains to prove the conditions on the $v$-input of $u'$ for each $v$. If suffices to prove the condition for the part between $(q_1, \nu_1)$ to $(q_4, \nu_4)$, because the rest of $u$ is left untouched.

Let $(q_m, \nu_m)$ the local configuration after $M$ steps of $\mathrm{tr}$ from $(q_1, \nu_1)$; write $u_1$ the local run from $(q_1, \nu_1)$ to $(q_m, \nu_m)$ corresponding to the first $M$ steps of $\mathrm{tr}$ in $u'$, and $u_2$ the local run from $(q_m, \nu_m)$ to $(q_4, \nu_4)$ corresponding to the last $M$ steps of $\mathrm{tr}$ in $u'$.

Let $v \in V$. We claim that $\ln_v(u_1)$ is a subword of $\ln_v(u_a)$ and $\ln_v(u_2)$ is a subword of $\ln_v(u_b)$. Indeed, in the construction of $\mathrm{tr}$, the reception steps in the first $M$ steps were those of $u_a$ except that some values were replaced with fresh values in $N \setminus V$, and similarly with $u_b$ and the last $M$ steps. Overall, this proves that $\ln_v(u')$ is a subword of $\ln_v(u)$ for every $v \in V$ and values of $V$ satisfy condition 1.

Let $v' \in N \setminus V$; $v'$ does not appear in $u$. Either $v'$ does not appear in $u'$ in which case the desired property is true, or there exists $v \in V$ such that $v' = \phi(v)$. As $\phi$ is injective and $\phi(W) = W$ and $v' \notin W$, $v \notin W$. But then $\ln_{v'}(u_1)$ is a subword of $\ln_v(u_a)$ and $\ln_{v'}(u_2)$ is a subword of $\ln_v(u_b)$. Indeed, in $u_1$, the reception steps with value $\phi(v)$ correspond to reception steps in $u_a$ with value $v$, and similarly for $u_2$ and $u_b$. This proves condition 2 for every $v' \in N \setminus V$. Overall, we have proven the existence of a local run $u' : (q_i, \nu_i) \xrightarrow{\ast} (q_f, \nu_f)$ that satisfies conditions 1 and 2 and that is strictly shorter that $u$, which proves the shortening property.

We build a local run of length less that $\psi(|\mathcal{P}|-r+|W|, r)$ as follows. We start with $u^{(0)} := u$ and $V^{(0)}$ the set of values of messages appearing in $u^{(0)}$. For every $k$ such that $\mathrm{len}(u^{(0)}) > \psi(|\mathcal{P}|-r+|W|, r)$, we apply the shortening property on $u^{(k)}$ and $V^{(k)}$ to obtain $u^{(k+1)}$ and define $V^{(k+1)}$ by $V^{(k)} \cup X$ where $X$ is the set of values of messages in $u^{(k+1)}$, which is finite. The construction stops when $\mathrm{len}(u^{(k)}) \le \psi(|\mathcal{P}|-r+|W|, r)$, which concludes the proof of the lemma. $\square$

# F Bounding the Size of the Minimal Coverability Witness

In this section, we prove that we can obtain a computable bound on $\tau$, and that the problem is decidable in complexity class $F_{\omega^\omega}$. All bounds provided in this
section are independent from $\tau$. We start by proving that one can bound the size of a node with respect to the size of its neighbors of higher altitude.

**Lemma 37.** Let $\mu$ be a node of $\tau$ such that all neighbors of $\mu$ of higher altitude have size bounded by $K$. Then $|\mu| \le (\psi(|\mathcal{P}|, r) + 2)(|\mathcal{M}|rK + K)$, with $\psi$ the primitive-recursive function defined in Lemma 26.

*Proof.* Let $u := \text{lr}(\mu)$. For each initial value $v$ in $u$, $\mu$ has at most $|\mathcal{M}|$ follower children, by definition of a decomposition. Because there are at most $r$ initial values, this makes at most $|\mathcal{M}|r$ follower children and each one of them requires at most $K$ messages. If $\mu$ is a follower node or the root, then the number of messages it must broadcast is then bounded by $|\mathcal{M}|rK + 1$. If $\mu$ is a boss node and not the root, then its parent has higher altitude hence $|\text{bw}(\mu)| \le K$ and $\mu$ must broadcast at most $|\mathcal{M}|rK + K$ messages in total. This bounds by $|\mathcal{M}|rK + K + 1$ the number of messages $u$ needs to broadcast. Lemma 26 then lets us reduce the number of steps between those messages without breaking the unfolding tree conditions: the inputs of values that were already in the run can only decrease. For the other values, let $v$ be a value that was not in the run before, its input is a subword of the one of a previous value. Hence $\mu$ has a boss child whose specification covers the $v$-input of the new local run. This bounds $|u|$ by $(\psi(|\mathcal{P}|, r) + 1)(|\mathcal{M}|rK + K)$, with $\psi$ the function described in Lemma 26; the bound on $|\mu|$ follows. $\square$

We now formally prove Lemma 27:

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

*Proof.* Let $f_0 : k \mapsto ((\psi(k, k) + 2)(k^2 + 2))^{k+1}$. Also, let $N := |\mathcal{P}|$. First, if $\mu$ has altitude $\text{altmax}$, then it has no follower child, hence applying Lemma 37 with $K = 0$ bounds $|\mu|$ by $\psi(|\mathcal{P}|, r) \le \psi(N, N) \le f_0(N)$. Let $\mu$ be a node with $\text{alt}(\mu) < \text{altmax}$, and suppose that the statement is true for altitudes greater than $\text{alt}(\mu)$.

Let $d = \text{altmax} - \text{alt}(\mu)$. We apply Lemma 37 with $K := f_0(N + d - 1)$:

$$ 
\begin{aligned}
|\mu| &\le (\psi(N, N) + 2)(N^2K + K) \\
&\le (\psi(N + d, N + d) + 2)f_0(N + d - 1)((N + d)^2 + 2) \\
&\le f_0(N + d)
\end{aligned}
$$

$\square$

**Lemma 38.** There exists a function $f_1 \in \mathcal{F}_{\omega|\mathcal{M}|}$ such that $\text{altmax} \le f_1(|\mathcal{P}|)$.

*Proof.* Let $\text{altmax}$ be the maximal altitude of a node in $\tau$. Consider a branch of $\tau$ reaching altitude $\text{altmax}$; for every $j \in [1, \text{altmax}]$, let $\mu_j$ the first node of this branch to reach altitude $j$. For every $j \ge 1$, $\mu_j$ is a follower nodes as otherwise its predecessor in the branch would have altitude greater than $j$ hence the branch must have crossed altitude $j$ before.
section are independent from $\tau$. We start by proving that one can bound the size of a node with respect to the size of its neighbors of higher altitude.

**Lemma 37.** Let $\mu$ be a node of $\tau$ such that all neighbors of $\mu$ of higher altitude have size bounded by $K$. Then $|\mu| \le (\psi(|\mathcal{P}|, r) + 2)(|\mathcal{M}|rK + K)$, with $\psi$ the primitive-recursive function defined in Lemma 26.

*Proof.* Let $u := \text{lr}(\mu)$. For each initial value $v$ in $u$, $\mu$ has at most $|\mathcal{M}|$ follower children, by definition of a decomposition. Because there are at most $r$ initial values, this makes at most $|\mathcal{M}|r$ follower children and each one of them requires at most $K$ messages. If $\mu$ is a follower node or the root, then the number of messages it must broadcast is then bounded by $|\mathcal{M}|rK + 1$. If $\mu$ is a boss node and not the root, then its parent has higher altitude hence $|\text{bw}(\mu)| \le K$ and $\mu$ must broadcast at most $|\mathcal{M}|rK + K$ messages in total. This bounds by $|\mathcal{M}|rK + K + 1$ the number of messages $u$ needs to broadcast. Lemma 26 then lets us reduce the number of steps between those messages without breaking the unfolding tree conditions: the inputs of values that were already in the run can only decrease. For the other values, let $v$ be a value that was not in the run before, its input is a subword of the one of a previous value. Hence $\mu$ has a boss child whose specification covers the $v$-input of the new local run. This bounds $|u|$ by $(\psi(|\mathcal{P}|, r) + 1)(|\mathcal{M}|rK + K)$, with $\psi$ the function described in Lemma 26; the bound on $|\mu|$ follows. $\square$

We now formally prove Lemma 27:

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

*Proof.* Let $f_0 : k \mapsto ((\psi(k, k) + 2)(k^2 + 2))^{k+1}$. Also, let $N := |\mathcal{P}|$. First, if $\mu$ has altitude $\text{altmax}$, then it has no follower child, hence applying Lemma 37 with $K = 0$ bounds $|\mu|$ by $\psi(|\mathcal{P}|, r) \le \psi(N, N) \le f_0(N)$. Let $\mu$ be a node with $\text{alt}(\mu) < \text{altmax}$, and suppose that the statement is true for altitudes greater than $\text{alt}(\mu)$.

Let $d = \text{altmax} - \text{alt}(\mu)$. We apply Lemma 37 with $K := f_0(N + d - 1)$:

$$ 
\begin{aligned}
|\mu| &\le (\psi(N, N) + 2)(N^2K + K) \\
&\le (\psi(N + d, N + d) + 2)f_0(N + d - 1)((N + d)^2 + 2) \\
&\le f_0(N + d)
\end{aligned}
$$

$\square$

**Lemma 38.** There exists a function $f_1 \in \mathcal{F}_{\omega|\mathcal{M}|}$ such that $\text{altmax} \le f_1(|\mathcal{P}|)$.

*Proof.* Let $\text{altmax}$ be the maximal altitude of a node in $\tau$. Consider a branch of $\tau$ reaching altitude $\text{altmax}$; for every $j \in [1, \text{altmax}]$, let $\mu_j$ the first node of this branch to reach altitude $j$. For every $j \ge 1$, $\mu_j$ is a follower nodes as otherwise its predecessor in the branch would have altitude greater than $j$ hence the branch must have crossed altitude $j$ before.
We will bound **altmax** using the Length function theorem. For simplicity, we will encode the **fm** part using a fresh character added to our alphabet. This is why we obtain a function in $\mathcal{F}_{w|\mathcal{M}}$ and not $\mathcal{F}_{w|\mathcal{M}-1}$; in fact, one could obtain the latter bound using Theorem 5.3. of [24], but the proof would be more involved.

Let $\# \notin \mathcal{M}$ be a fresh letter. For all $i \in [1, \text{altmax}]$ let $\mu'_i = \mu_{\text{altmax}-i+1}$ and $w_i = \text{fw}(\mu'_i) \cdot \# \cdot \text{fm}(\mu'_i) \in (\mathcal{M} \cup \{\#\})^*$.

We cannot have $w_i \le w_j$ for $i < j$: indeed, this would imply $\text{fw}(\mu'_i) \le \text{fm}(\mu'_j)$ and $\text{fm}(\mu'_i) = \text{fw}(\mu'_j)$, which is a contradiction according to Lemma 25. As a result, the sequence $(w_i)_{1 \le i \le \text{altmax}}$ is a bad sequence over the alphabet $\mathcal{M} \cup \{\#\}$. Furthermore, by Lemma 27, for all $i$, $|\mu_i| \le f_0(|\mathcal{P}| + i)$ therefore $|w_i| \le f_0^{(i)}(|\mathcal{P}|)$. Because $f_0$ is primitive-recursive, we can apply Theorem 10: there exists a function $f_1 \in \mathcal{F}_{\omega|\mathcal{M}}$ such that the sequence $(w_i)_{i \in [1, \text{altmax}]}$ is of length at most $f_1(|\mathcal{P}|)$, hence $\text{altmax} \le f_1(|\mathcal{P}|)$. $\square$

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

For all $i$, let $w_i = \text{fw}(\mu'_i) \# \text{fm}(\mu'_i)$ where $\mu'_i$ is the first follower node at altitude $\text{altmax} - i + 1$.

By Lemma 27 we can bound the length of $w_i$ by $f_0(|\mathcal{P}| + i)$, which lets us to bound the number of red dots using Lemma 25 and the Length function theorem.

<caption>Fig. 10: Illustration of the proof of Lemma 38.</caption>

The bound on the maximal altitude, along with Lemma 27, bounds the size of the root of $\tau$ by $f_0(|\mathcal{P}| + f_1(|\mathcal{P}|))$. Let **altmin** := $\min_{\mu \in \tau} \text{alt}(\mu) \le 0$ the minimal altitude in $\tau$. By a similar argument but with boss nodes, we can bound $|\text{altmin}|:$

**Lemma 39.** There exists a function $f_2 \in \mathcal{F}_{\omega|\mathcal{M}}$ such that $|\text{altmin}| \le f_2(|\mathcal{P}|)$.

*Proof.* Consider a branch of $\tau$ reaching **altmin**, let $\mu_1, \dots, \mu_{|\text{altmin}|}$ be nodes of $\tau$ such that $\mu_i$ is the first node of the branch to reach altitude $-i$. All these nodes are boss nodes because a follower node has higher altitude than its parent. For all $i \in [0, \text{altmin}]$ let $\mu'_i = \mu_{|\text{altmin}|-i}$ and $w_i = \text{bw}(\mu'_i) \in \mathcal{M}^*$. By Lemma 25, $(w_i)_{i \in [1, \text{altmin}]}$ is a bad sequence. By Lemmas 27 and 38, for all $i$, we have $|w_i| \le f_0(|\mathcal{P}| + f_1(|\mathcal{P}|) + i)$. Let $N := |\mathcal{P}| + f_1(|\mathcal{P}|) + 1$; we have $|w_i| \le f_0^{(i)}(N)$.

Because $f_0$ is primitive recursive, we can apply Theorem 10: we obtain $h \in \mathcal{F}_{\omega|\mathcal{M}-1}$ such that $\text{altmin} \le h(N)$. Let $f_2 : n \mapsto h(n + f_1(n) + 1)$; we have $\text{altmin} \le f_2(|\mathcal{P}|)$. Moreover, $f_2$ is a function of $\mathcal{F}_{\omega|\mathcal{M}}$ because $f_1, h \in \mathcal{F}_{\omega|\mathcal{M}}$ and $\mathcal{F}_{\omega|\mathcal{M}}$ is closed under composition. $\square$
We will bound **altmax** using the Length function theorem. For simplicity, we will encode the **fm** part using a fresh character added to our alphabet. This is why we obtain a function in $\mathcal{F}_{w|\mathcal{M}|}$ and not $\mathcal{F}_{w|\mathcal{M}|-1}$; in fact, one could obtain the latter bound using Theorem 5.3. of [24], but the proof would be more involved.

Let $\# \notin \mathcal{M}$ be a fresh letter. For all $i \in [1, \text{altmax}]$ let $\mu'_i = \mu_{\text{altmax}-i+1}$ and $w_i = \text{fw}(\mu'_i) \cdot \# \cdot \text{fm}(\mu'_i) \in (\mathcal{M} \cup \{\#\})^*$.

We cannot have $w_i \le w_j$ for $i < j$: indeed, this would imply $\text{fw}(\mu'_i) \le \text{fm}(\mu'_j)$ and $\text{fm}(\mu'_i) = \text{fw}(\mu'_j)$, which is a contradiction according to Lemma 25. As a result, the sequence $(w_i)_{1 \le i \le \text{altmax}}$ is a bad sequence over the alphabet $\mathcal{M} \cup \{\#\}$. Furthermore, by Lemma 27, for all $i$, $|\mu_i| \le f_0(|\mathcal{P}| + i)$ therefore $|w_i| \le f_0^{(i)}(|\mathcal{P}|)$. Because $f_0$ is primitive-recursive, we can apply Theorem 10: there exists a function $f_1 \in \mathcal{F}_{\omega|\mathcal{M}|}$ such that the sequence $(w_i)_{i \in [1, \text{altmax}]}$ is of length at most $f_1(|\mathcal{P}|)$, hence $\text{altmax} \le f_1(|\mathcal{P}|)$. $\square$

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

For all $i$, let $w_i = \text{fw}(\mu'_i) \# \text{fm}(\mu'_i)$ where $\mu'_i$ is the first follower node at altitude $\text{altmax} - i + 1$.

By Lemma 27 we can bound the length of $w_i$ by $f_0(|\mathcal{P}| + i)$, which lets us to bound the number of red dots using Lemma 25 and the Length function theorem.

<caption>Fig. 10: Illustration of the proof of Lemma 38.</caption>

The bound on the maximal altitude, along with Lemma 27, bounds the size of the root of $\tau$ by $f_0(|\mathcal{P}| + f_1(|\mathcal{P}|))$. Let **altmin** := $\min_{\mu \in \tau} \text{alt}(\mu) \le 0$ the minimal altitude in $\tau$. By a similar argument but with boss nodes, we can bound $|\text{altmin}|:$

**Lemma 39.** There exists a function $f_2 \in \mathcal{F}_{\omega|\mathcal{M}|}$ such that $|\text{altmin}| \le f_2(|\mathcal{P}|)$.

*Proof.* Consider a branch of $\tau$ reaching **altmin**, let $\mu_1, \dots, \mu_{|\text{altmin}|}$ be nodes of $\tau$ such that $\mu_i$ is the first node of the branch to reach altitude $-i$. All these nodes are boss nodes because a follower node has higher altitude than its parent. For all $i \in [0, \text{altmin}]$ let $\mu'_i = \mu_{|\text{altmin}|-i}$ and $w_i = \text{bw}(\mu'_i) \in \mathcal{M}^*$. By Lemma 25, $(w_i)_{i \in [1, \text{altmin}]}$ is a bad sequence. By Lemmas 27 and 38, for all $i$, we have $|w_i| \le f_0(|\mathcal{P}| + f_1(|\mathcal{P}|) + i)$. Let $N := |\mathcal{P}| + f_1(|\mathcal{P}|) + 1$; we have $|w_i| \le f_0^{(i)}(N)$.

Because $f_0$ is primitive recursive, we can apply Theorem 10: we obtain $h \in \mathcal{F}_{\omega|\mathcal{M}|-1}$ such that $\text{altmin} \le h(N)$. Let $f_2 : n \mapsto h(n + f_1(n) + 1)$; we have $\text{altmin} \le f_2(|\mathcal{P}|)$. Moreover, $f_2$ is a function of $\mathcal{F}_{\omega|\mathcal{M}|}$ because $f_1, h \in \mathcal{F}_{\omega|\mathcal{M}|}$ and $\mathcal{F}_{\omega|\mathcal{M}|}$ is closed under composition. $\square$
With the bounds on the maximal and minimal altitudes, Lemma 27 yields a bound on the size of all nodes in the tree.

**Lemma 40.** There exists $f_3 \in \mathcal{F}_{\omega|\mathcal{M}|}$ such that, for all $\mu$ in $\tau$, $|\mu| \le f_3(|\mathcal{P}|)$.

*Proof.* Using Lemmas 27, 38 and 39, we obtain that, for every node $\mu$, the value `altmax-alt`($\mu$) is at most $f_1(|\mathcal{P}|)+f_2(|\mathcal{P}|)$. Applying Lemma 27 proves that, for all $\mu$ in $\tau$, $|\mu| \le f_0(f_1(|\mathcal{P}|)+f_2(|\mathcal{P}|)) \le f_3(|\mathcal{P}|)$ where $f_3: n \mapsto f_0(f_1(n)+f_2(n))$; $f_3$ is in $\mathcal{F}_{\omega|\mathcal{M}|}$ as $\mathcal{F}_{\omega|\mathcal{M}|}$ contains all primitive recursive functions and is closed under composition. $\square$

Finally, as we now have a bound on all nodes, we can easily bound the length of branches and the number of children of all nodes to get abound on the total size of the tree.

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

*Proof.* Recall that the size of $\tau$ is defined as the sum of the sizes of its nodes.

Let $N = |\mathcal{P}|$. By Lemma 40, for each $\mu$ in $\tau$ we have $|\mu| \le f_3(N)$, hence the local run of $\mu$ contains at most $f_3(N)$ values. By minimality of $\tau$, each value requires at most 1 boss child and $|\mathcal{M}|$ follower children hence $\mu$ has at most $(|\mathcal{M}| + 1)f_3(N) \le Nf_3(N)$ children. Moreover, there are less than $f_4(N) := Nf_3(N)$ possible specifications in $\tau$ hence each branch of $\tau$ is of length less than $f_4(N)$ (by minimality, a branch does not have twice the same specification). This bounds the total number of nodes in $\tau$ by $f_5(N) := (Nf_3(N))^{f_4(N)+1}$ hence we obtain $|\tau| \le f(N)$ where $f: n \mapsto f_3(n)f_5(n)$. Because $\mathcal{F}_{\omega|\mathcal{M}|}$ is closed under composition with primitive recursive functions, we have $f \in \mathcal{F}_{\omega|\mathcal{M}|}$. $\square$

# G Proof of Theorem 12

We now prove the main result of this paper:

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

*Proof.* The lower bound is given by the reduction from lossy channel system reachability in Proposition 11.

For the upper bound, let $(\mathcal{P}, q_f)$ be an instance of COVER. By Propositions 24 and 41, $(\mathcal{P}, q_f)$ is positive if and only if it has a coverability witness of size bounded by $f(|\mathcal{P}|)$ where $f \in \mathcal{F}_{\omega|\mathcal{M}|}$. Up to renaming agents and values, we can moreover assume that all agents and values appearing in this coverability witness are bounded by $f(|\mathcal{P}|)$, which bounds the size of the description of such a coverability witness by a polynomial in $f(|\mathcal{P}|)$. An algorithm for COVERconsists in enumerating all such descriptions and accepting if one finds a coverability witness. This can all be done in time exponential in $f(|\mathcal{P}|)$, thus this algorithm terminates in time $f'(|\mathcal{P}|)$ where $f' \in \mathcal{F}_{\omega|\mathcal{M}|}$. This proves that COVERlies in complexity class $\mathbf{F}_{\omega^\omega}$. $\square$
With the bounds on the maximal and minimal altitudes, Lemma 27 yields a bound on the size of all nodes in the tree.

**Lemma 40.** There exists $f_3 \in \mathcal{F}_{\omega|\mathcal{M}|}$ such that, for all $\mu$ in $\tau$, $|\mu| \le f_3(|\mathcal{P}|)$.

*Proof.* Using Lemmas 27, 38 and 39, we obtain that, for every node $\mu$, the value `altmax-alt`($\mu$) is at most $f_1(|\mathcal{P}|)+f_2(|\mathcal{P}|)$. Applying Lemma 27 proves that, for all $\mu$ in $\tau$, $|\mu| \le f_0(f_1(|\mathcal{P}|)+f_2(|\mathcal{P}|)) \le f_3(|\mathcal{P}|)$ where $f_3: n \mapsto f_0(f_1(n)+f_2(n))$; $f_3$ is in $\mathcal{F}_{\omega|\mathcal{M}|}$ as $\mathcal{F}_{\omega|\mathcal{M}|}$ contains all primitive recursive functions and is closed under composition. $\square$

Finally, as we now have a bound on all nodes, we can easily bound the length of branches and the number of children of all nodes to get abound on the total size of the tree.

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

*Proof.* Recall that the size of $\tau$ is defined as the sum of the sizes of its nodes.

Let $N = |\mathcal{P}|$. By Lemma 40, for each $\mu$ in $\tau$ we have $|\mu| \le f_3(N)$, hence the local run of $\mu$ contains at most $f_3(N)$ values. By minimality of $\tau$, each value requires at most 1 boss child and $|\mathcal{M}|$ follower children hence $\mu$ has at most $(|\mathcal{M}| + 1)f_3(N) \le Nf_3(N)$ children. Moreover, there are less than $f_4(N) := Nf_3(N)$ possible specifications in $\tau$ hence each branch of $\tau$ is of length less than $f_4(N)$ (by minimality, a branch does not have twice the same specification). This bounds the total number of nodes in $\tau$ by $f_5(N) := (Nf_3(N))^{f_4(N)+1}$ hence we obtain $|\tau| \le f(N)$ where $f: n \mapsto f_3(n)f_5(n)$. Because $\mathcal{F}_{\omega|\mathcal{M}|}$ is closed under composition with primitive recursive functions, we have $f \in \mathcal{F}_{\omega|\mathcal{M}|}$. $\square$

# G Proof of Theorem 12

We now prove the main result of this paper:

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

*Proof.* The lower bound is given by the reduction from lossy channel system reachability in Proposition 11.

For the upper bound, let $(\mathcal{P}, q_f)$ be an instance of COVER. By Propositions 24 and 41, $(\mathcal{P}, q_f)$ is positive if and only if it has a coverability witness of size bounded by $f(|\mathcal{P}|)$ where $f \in \mathcal{F}_{\omega|\mathcal{M}|}$. Up to renaming agents and values, we can moreover assume that all agents and values appearing in this coverability witness are bounded by $f(|\mathcal{P}|)$, which bounds the size of the description of such a coverability witness by a polynomial in $f(|\mathcal{P}|)$. An algorithm for COVERconsists in enumerating all such descriptions and accepting if one finds a coverability witness. This can all be done in time exponential in $f(|\mathcal{P}|)$, thus this algorithm terminates in time $f'(|\mathcal{P}|)$ where $f' \in \mathcal{F}_{\omega|\mathcal{M}|}$. This proves that COVERlies in complexity class $F_{\omega^\omega}$. $\square$
## H Proof of Proposition 29

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

*Proof.* We present a reduction from the halting problem for Minsky machines to COVER for signature BNRA.

A Minsky Machine with two counters is a tuple $M = (\text{Loc}, \Delta, \mathbf{X}, \ell_0, \ell_f)$ where
$\text{Loc}$ is a finite set of locations, $\mathbf{X} = \{\mathbf{x}_1, \mathbf{x}_2\}$ is a set of two counters, $\Delta \subseteq \text{Loc} \times \{\mathbf{x} - , \mathbf{x} +, \mathbf{x} = 0? | \mathbf{x} \in \mathbf{X}\} \times \text{Loc}$ is a finite set of transitions, $\ell_0 \in \text{Loc}$ is an initial location and $\ell_f \in \text{Loc}$ is a final location. A configuration of a Minsky machine is a tuple $(\ell, v_1, v_2) \in \text{Loc} \times \mathbb{N} \times \mathbb{N}$ where $v_1$ (resp. $v_2$) stands for the value of the counter $\mathbf{x}_1$ (resp. $\mathbf{x}_2$). We write $(\ell, v_1, v_2) \to (\ell', v'_1, v'_2)$ if there is $\delta \in \Delta$ such that:

- $\delta = (\ell, \mathbf{x}_i +, \ell')$ and $v'_i = v_i + 1, v_{3-i} = v'_{3-i}$;

- $\delta = (\ell, \mathbf{x}_i -, \ell')$ and $v'_i = v_i - 1, v_{3-i} = v'_{3-i}$;

- $\delta = (\ell, \mathbf{x}_i = 0?, \ell')$ and $v'_i = v_i = 0, v_{3-i} = v'_{3-i}$.

An execution of the machine is a sequence $(\ell_1, v_1^{(1)}, v_2^{(1)}) \to (\ell_2, v_1^{(2)}, v_2^{(2)}) \to \dots \to (\ell_k, v_1^{(k)}, v_2^{(k)})$. The halting problem asks whether $\ell_f$ is coverable. This problem is well-known to be undecidable [19].

<figure><img src="image_14.png" /><figcaption>Fig. 11: Partial depiction of the protocol built in Proposition 29. Only one transition, which is $(\ell_0, \delta, \ell_1)$, is represented in the $\mathcal{P}_{\text{loc}}$ part above; similarly, only one increment and one decrement transitions are depicted in the $\mathcal{P}_{\text{count}}$ part below. The rebroadcast loops rebroadcast all transitions acting on $\mathbf{x}_2$ and all acknowledgements; the one on $(\mathbf{x}_1, 0)$ also rebroadcasts all transitions with $\mathbf{x}_1$ – and with zero-tests, and the one on $(\mathbf{x}_1, 1)$ rebroadcasts all transitions with $\mathbf{x}_1$ +.</figcaption></figure>

Fix a Minsky Machine $M = (\text{Loc}, \Delta, \mathbf{X}, \ell_0, \ell_f)$. We build a signature protocol $\mathcal{P}$ with a state $q_f$ such that $(\mathcal{P}, q_f)$ is a positive instance of TARGET if and
## H Proof of Proposition 29

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

*Proof.* We present a reduction from the halting problem for Minsky machines to COVER for signature BNRA.

A Minsky Machine with two counters is a tuple $M = (\text{Loc}, \Delta, \mathbf{X}, \ell_0, \ell_f)$ where $\text{Loc}$ is a finite set of locations, $\mathbf{X} = \{\mathbf{x}_1, \mathbf{x}_2\}$ is a set of two counters, $\Delta \subseteq \text{Loc} \times \{\mathbf{x} - , \mathbf{x} +, \mathbf{x} = 0? \mid \mathbf{x} \in \mathbf{X}\} \times \text{Loc}$ is a finite set of transitions, $\ell_0 \in \text{Loc}$ is an initial location and $\ell_f \in \text{Loc}$ is a final location. A configuration of a Minsky machine is a tuple $(\ell, v_1, v_2) \in \text{Loc} \times \mathbb{N} \times \mathbb{N}$ where $v_1$ (resp. $v_2$) stands for the value of the counter $\mathbf{x}_1$ (resp. $\mathbf{x}_2$). We write $(\ell, v_1, v_2) \to (\ell', v'_1, v'_2)$ if there is $\delta \in \Delta$ such that:

- $\delta = (\ell, \mathbf{x}_i +, \ell')$ and $v'_i = v_i + 1, v_{3-i} = v'_{3-i}$;

- $\delta = (\ell, \mathbf{x}_i -, \ell')$ and $v'_i = v_i - 1, v_{3-i} = v'_{3-i}$;

- $\delta = (\ell, \mathbf{x}_i = 0?, \ell')$ and $v'_i = v_i = 0, v_{3-i} = v'_{3-i}$.

An execution of the machine is a sequence $(\ell_1, v_1^{(1)}, v_2^{(1)}) \to (\ell_2, v_1^{(2)}, v_2^{(2)}) \to \dots \to (\ell_k, v_1^{(k)}, v_2^{(k)})$. The halting problem asks whether $\ell_f$ is coverable. This problem is well-known to be undecidable [19].

<figure><img src="image_13.png" /><figcaption>Fig. 11: Partial depiction of the protocol built in Proposition 29. Only one transition, which is $(\ell_0, \delta, \ell_1)$, is represented in the $P_{\text{loc}}$ part above; similarly, only one increment and one decrement transitions are depicted in the $P_{\text{count}}$ part below. The rebroadcast loops rebroadcast all transitions acting on $\mathbf{x}_2$ and all acknowledgements; the one on $(\mathbf{x}_1, 0)$ also rebroadcasts all transitions with $\mathbf{x}_1$ - and with zero-tests, and the one on $(\mathbf{x}_1, 1)$ rebroadcasts all transitions with $\mathbf{x}_1$ +.</figcaption></figure>

Fix a Minsky Machine $M = (\text{Loc}, \Delta, \mathbf{X}, \ell_0, \ell_f)$. We build a signature protocol $\mathcal{P}$ with a state $q_f$ such that $(\mathcal{P}, q_f)$ is a positive instance of TARGET if and
only if $\ell_f$ is coverable in $M$. The protocol is represented in Figure 11. As in Proposition 11, in an initial phase, each agent picks a predecessor by storing its identifier and only listens to this predecessor afterwards. We call *cycle* a sequence of agents $a_1, a_2, \dots, a_n = a_1$ where agent $a_i$ is the predecessor of $a_{i+1}$ for all $i < n$. As all agents have to reach the end state, they must all pick a predecessor. As there are finitely many agents in a run, a cycle will necessarily be formed in any run satisfying the *TARGET* requirement.

The rest of the construction aims at faithfully simulating the machine in a cycle: Agents in $\mathcal{P}_{\text{loc}}$ sends a sequence of instructions and waits after each one for a confirmation that it was executed. Agents in $\mathcal{P}_{\text{count}}$ simulate counter values. The messages circulating in a cycle contain either a transition $\delta \in \Delta$ or an acknowledgment $\bar{\delta}$ with $\delta \in \Delta$. An agent $a$ in $\mathcal{P}_{\text{count}}$ first picks a counter $\mathbf{x}_i$ it simulates, and goes to state $(\mathbf{x}_i, 0)$. If $a$ is in $(\mathbf{x}_i, 0)$ and receives $\delta$ corresponding to an increment of $\mathbf{x}_i$, it goes to $(\mathbf{x}_i, 1)$ and broadcast an acknowledgment $\bar{\delta}$, and conversely for decrements. If $\bar{\delta}$ is a zero-test $\mathbf{x}_i = 0$? and $a$ is on state $(\mathbf{x}_i, 1)$ then it stops, making the whole cycle fail. Otherwise it broadcasts the acknowledgment $\bar{\delta}$. Other messages are rebroadcast as such.

An agent $a$ in $\mathcal{P}_{\text{loc}}$ starts in state $\text{loc}(\ell_0)$. When in state $\text{loc}(\ell)$, it picks and broadcasts a transition $\delta = (\ell, \alpha, \ell') \in \Delta$, waits for the acknowledgment $\bar{\delta}$ and goes to $\text{loc}(\ell')$. In the case where $\delta$ is a zero-test, we have $\bar{\delta} = \delta$: there is no need for a distinct acknowledgment because there is no action to perform (if the test fails then no message is transmitted). When in $\text{loc}(\ell_f)$, $a$ broadcasts a special message end that propagates in the cycle and makes everyone go to $q_f$. When it receives itself the message end, it goes to $q_f$.

It is quite easy to see that, if $\ell_f$ can be covered in $M$, one can build a run of $\mathcal{P}$ where all agents end in $q_f$. Let $N$ the highest counter value in the execution of $M$ covering $q_f$. The run of $\mathcal{P}$ first puts all its agents in the same cycle; exactly one agent $a_{\text{lead}}$ goes in $\mathcal{P}_{\text{loc}}$ and $2N$ agents go in $\mathcal{P}_{\text{count}}$; half of these simulate $\mathbf{x}_1$ and half $\mathbf{x}_2$, so that the largest counter value is never exceeded. It then suffices to faithfully simulate the execution of $M$: $a_{\text{lead}}$ selects the corresponding sequence of transitions, their effect is always applied as we have enough agents simulating each counter. After each round the number of agents in state $(\mathbf{x}_i, 1)$ is exactly the value of $\mathbf{x}_i$ at this point in the run of the machine, hence zero-tests never cause failure. In the end $a_{\text{lead}}$ reaches $\text{loc}(\ell_f)$ and broadcasts end, allowing every agent in $\mathcal{P}_{\text{count}}$ to get to $q_f$.

For the converse implication, suppose that we have a run $\rho$ of $\mathcal{P}$ where all agents end in $q_f$. As mentioned before, there must be a cycle of agents $a_1, \dots, a_n$ in this run. Observe that all agents alternate between broadcasts and receptions, so that to reach $q_f$ they must all have made the same number of broadcasts and receptions. This implies that no message was lost along the cycle.

Note that there may be several agents in $\mathcal{P}_{\text{loc}}$ along the cycle; however, they must all broadcast exactly the same sequence of transitions, otherwise one of them would lack an acknowledgment and would not get to $q_f$. Let $a$ be the agent that first reaches $\text{loc}(\ell_f)$ and $a'$ the first agent in $\mathcal{P}_{\text{loc}}$ after $a$ in the cycle; there are only agents in $\mathcal{P}_{\text{count}}$ between $a$ and $a'$ in the cycle, we call these
only if $\ell_f$ is coverable in $M$. The protocol is represented in Figure 11. As in Proposition 11, in an initial phase, each agent picks a predecessor by storing its identifier and only listens to this predecessor afterwards. We call *cycle* a sequence of agents $a_1, a_2, \dots, a_n = a_1$ where agent $a_i$ is the predecessor of $a_{i+1}$ for all $i < n$. As all agents have to reach the end state, they must all pick a predecessor. As there are finitely many agents in a run, a cycle will necessarily be formed in any run satisfying the *TARGET* requirement.

The rest of the construction aims at faithfully simulating the machine in a cycle: Agents in $\mathcal{P}_{\text{loc}}$ sends a sequence of instructions and waits after each one for a confirmation that it was executed. Agents in $\mathcal{P}_{\text{count}}$ simulate counter values. The messages circulating in a cycle contain either a transition $\delta \in \Delta$ or an acknowledgment $\bar{\delta}$ with $\delta \in \Delta$. An agent $a$ in $\mathcal{P}_{\text{count}}$ first picks a counter $\mathbf{x}_i$ it simulates, and goes to state $(\mathbf{x}_i, 0)$. If $a$ is in $(\mathbf{x}_i, 0)$ and receives $\delta$ corresponding to an increment of $\mathbf{x}_i$, it goes to $(\mathbf{x}_i, 1)$ and broadcast an acknowledgment $\bar{\delta}$, and conversely for decrements. If $\bar{\delta}$ is a zero-test $\mathbf{x}_i = 0$? and $a$ is on state $(\mathbf{x}_i, 1)$ then it stops, making the whole cycle fail. Otherwise it broadcasts the acknowledgment $\bar{\delta}$. Other messages are rebroadcast as such.

An agent $a$ in $\mathcal{P}_{\text{loc}}$ starts in state $\text{loc}(\ell_0)$. When in state $\text{loc}(\ell)$, it picks and broadcasts a transition $\delta = (\ell, \alpha, \ell') \in \Delta$, waits for the acknowledgment $\bar{\delta}$ and goes to $\text{loc}(\ell')$. In the case where $\delta$ is a zero-test, we have $\bar{\delta} = \delta$: there is no need for a distinct acknowledgment because there is no action to perform (if the test fails then no message is transmitted). When in $\text{loc}(\ell_f)$, $a$ broadcasts a special message end that propagates in the cycle and makes everyone go to $q_f$. When it receives itself the message end, it goes to $q_f$.

It is quite easy to see that, if $\ell_f$ can be covered in $M$, one can build a run of $\mathcal{P}$ where all agents end in $q_f$. Let $N$ the highest counter value in the execution of $M$ covering $q_f$. The run of $\mathcal{P}$ first puts all its agents in the same cycle; exactly one agent $a_{\text{lead}}$ goes in $\mathcal{P}_{\text{loc}}$ and $2N$ agents go in $\mathcal{P}_{\text{count}}$; half of these simulate $\mathbf{x}_1$ and half $\mathbf{x}_2$, so that the largest counter value is never exceeded. It then suffices to faithfully simulate the execution of $M$: $a_{\text{lead}}$ selects the corresponding sequence of transitions, their effect is always applied as we have enough agents simulating each counter. After each round the number of agents in state $(\mathbf{x}_i, 1)$ is exactly the value of $\mathbf{x}_i$ at this point in the run of the machine, hence zero-tests never cause failure. In the end $a_{\text{lead}}$ reaches $\text{loc}(\ell_f)$ and broadcasts end, allowing every agent in $\mathcal{P}_{\text{count}}$ to get to $q_f$.

For the converse implication, suppose that we have a run $\rho$ of $\mathcal{P}$ where all agents end in $q_f$. As mentioned before, there must be a cycle of agents $a_1, \dots, a_n$ in this run. Observe that all agents alternate between broadcasts and receptions, so that to reach $q_f$ they must all have made the same number of broadcasts and receptions. This implies that no message was lost along the cycle.

Note that there may be several agents in $\mathcal{P}_{\text{loc}}$ along the cycle; however, they must all broadcast exactly the same sequence of transitions, otherwise one of them would lack an acknowledgment and would not get to $q_f$. Let $a$ be the agent that first reaches $\text{loc}(\ell_f)$ and $a'$ the first agent in $\mathcal{P}_{\text{loc}}$ after $a$ in the cycle; there are only agents in $\mathcal{P}_{\text{count}}$ between $a$ and $a'$ in the cycle, we call these
agents intermediate agents. The intermediate agents faithfully encode the two counters and all decrements and zero-tests pass, otherwise $a'$ would lack an acknowledgment. Therefore, the sequence of transitions of a defines an execution of M that covers $\ell_f$, which concludes the proof. □

# I Proofs of Section 5

In this section the register argument in receptions and broadcasts is always 1, hence we remove it. Our new set of operations is

$$ Op^M = \{ \mathbf{br}(m), \mathbf{rec}(m, *), \mathbf{rec}(m, \downarrow), \mathbf{rec}(m, =), \mathbf{rec}(m, \neq) | m \in \mathcal{M} \}. $$

Also, given a configuration $\gamma$, we write $\mathbf{data}(\gamma)(a)$ for $\mathbf{data}(\gamma)(a, 1)$.

Given a run $\rho$, we write $\mathbf{ag}(\rho)$ for its set of agents, and we define the set of states appearing in it $\mathbf{cov}(\rho) := \{q \in Q | \exists i, \exists a, \mathbf{st}(\gamma_i)(a) = q\}$ as well as its set of values $\mathbf{val}(\rho) := \{v \in N | \exists i, j, a, \mathbf{data}(\gamma_i)(a, j) = v\}$.

First, to simplify the proofs, we eliminate reception transitions with action '$\neq$'. This is feasible as we can execute several copies of a run in parallel (with distinct values) so that every broadcast is made in each copy with a different value. Hence if a agent receives a message, it can always receive it with a value different from its own, making disequality tests useless. We can thus replace them with receptions with '$*$'.

## I.1 Removing Disequality Tests

We start by formalising the intuition that a configuration contains more agents than another one up to renaming.

**Definition 42.** We define a preorder over the set of configurations as follows: $\gamma \preceq \gamma'$ if there exists an injective function $\pi: ag(\gamma) \to ag(\gamma')$ such that, for all $a \in ag(\gamma)$, $\gamma(a) = \gamma'(\pi(a))$.

**Lemma 43.** Let $(\tilde{\mathcal{P}}, q_f)$ an instance of the coverability problem. This instance is positive if and only if $(\tilde{\mathcal{P}}, q_f)$ is positive, where $\tilde{\mathcal{P}}$ is equal to $\mathcal{P}$ where every disequality test '$\neq$' is replaced by dummy action '$*$'.

*Proof.* First, if $(\tilde{\mathcal{P}}, q_f)$ is positive then so is $(\tilde{\mathcal{P}}, q_f)$, as one can easily lift any initial run in $\mathcal{P}$ to an equivalent initial run in $\tilde{\mathcal{P}}$ (transitions are less guarded in $\tilde{\mathcal{P}}$ that in $\mathcal{P}$).

Suppose now that $(\tilde{\mathcal{P}}, q_f)$ is a positive instance of the coverability problem. There exists an initial run $\tilde{\rho} : \tilde{\gamma}_0 \xrightarrow{*} \tilde{\gamma}$ in $\tilde{\mathcal{P}}$ that covers $q_f$. We prove by induction on the length of $\tilde{\rho}$ that there exists an initial run $\rho$ reaching a configuration $\gamma$ such that $\tilde{\gamma} \preceq \gamma$ (note that if $\tilde{\gamma}$ covers a state, then so does $\gamma$).

If $\tilde{\gamma} = \tilde{\gamma}_0$ then $\rho = \tilde{\rho}$ suffices. Suppose that $\tilde{\rho}$ has length $k \ge 1$, and that the result if true for runs of length $k-1$. Decompose $\tilde{\rho}$ into $\tilde{\rho}_{k-1} : \tilde{\gamma}_0 \xrightarrow{*} \tilde{\gamma}_{k-1}$ of
agents intermediate agents. The intermediate agents faithfully encode the two counters and all decrements and zero-tests pass, otherwise $a'$ would lack an acknowledgment. Therefore, the sequence of transitions of a defines an execution of M that covers $\ell_f$, which concludes the proof. □

# I Proofs of Section 5

In this section the register argument in receptions and broadcasts is always 1, hence we remove it. Our new set of operations is

$$ Op^{\mathcal{M}} = \{\mathbf{br}(m), \mathbf{rec}(m, *), \mathbf{rec}(m, \downarrow), \mathbf{rec}(m, =), \mathbf{rec}(m, \neq) | m \in \mathcal{M}\}. $$

Also, given a configuration $\gamma$, we write $\mathbf{data}(\gamma)(a)$ for $\mathbf{data}(\gamma)(a, 1)$.

Given a run $\rho$, we write $\mathbf{ag}(\rho)$ for its set of agents, and we define the set of states appearing in it $\mathbf{cov}(\rho) := \{q \in Q | \exists i, \exists a, \mathbf{st}(\gamma_i)(a) = q\}$ as well as its set of values $\mathbf{val}(\rho) := \{v \in \mathbb{N} | \exists i, j, a, \mathbf{data}(\gamma_i)(a, j) = v\}$.

First, to simplify the proofs, we eliminate reception transitions with action '$\neq$'. This is feasible as we can execute several copies of a run in parallel (with distinct values) so that every broadcast is made in each copy with a different value. Hence if a agent receives a message, it can always receive it with a value different from its own, making disequality tests useless. We can thus replace them with receptions with '$*$'.

## I.1 Removing Disequality Tests

We start by formalising the intuition that a configuration contains more agents than another one up to renaming.

**Definition 42.** We define a preorder over the set of configurations as follows: $\gamma \preceq \gamma'$ if there exists an injective function $\pi : ag(\gamma) \to ag(\gamma')$ such that, for all $a \in ag(\gamma)$, $\gamma(a) = \gamma'(\pi(a))$.

**Lemma 43.** Let $(\tilde{\mathcal{P}}, q_f)$ an instance of the coverability problem. This instance is positive if and only if $(\tilde{\mathcal{P}}, q_f)$ is positive, where $\tilde{\mathcal{P}}$ is equal to $\mathcal{P}$ where every disequality test '$\neq$' is replaced by dummy action '$*$'.

*Proof.* First, if $(\tilde{\mathcal{P}}, q_f)$ is positive then so is $(\tilde{\mathcal{P}}, q_f)$, as one can easily lift any initial run in $\mathcal{P}$ to an equivalent initial run in $\tilde{\mathcal{P}}$ (transitions are less guarded in $\tilde{\mathcal{P}}$ that in $\mathcal{P}$).

Suppose now that $(\tilde{\mathcal{P}}, q_f)$ is a positive instance of the coverability problem. There exists an initial run $\tilde{\rho} : \tilde{\gamma}_0 \xrightarrow{*} \tilde{\gamma}$ in $\tilde{\mathcal{P}}$ that covers $q_f$. We prove by induction on the length of $\tilde{\rho}$ that there exists an initial run $\rho$ reaching a configuration $\gamma$ such that $\tilde{\gamma} \preceq \gamma$ (note that if $\tilde{\gamma}$ covers a state, then so does $\gamma$).

If $\tilde{\gamma} = \tilde{\gamma}_0$ then $\rho = \tilde{\rho}$ suffices. Suppose that $\tilde{\rho}$ has length $k \ge 1$, and that the result if true for runs of length $k-1$. Decompose $\tilde{\rho}$ into $\tilde{\rho}_{k-1} : \tilde{\gamma}_0 \xrightarrow{*} \tilde{\gamma}_{k-1}$ of
length $k-1$ and a final step $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$. By induction hypothesis, there exists $\rho_{k-1}: \gamma_0 \stackrel{*}{\to} \gamma_{k-1}$ such that $\tilde{\gamma}_{k-1} \sqsubseteq \gamma_{k-1}$: there exists an injective function $\pi: \tilde{A} \to A$ such that, for all $a \in \tilde{A}$, $\tilde{\gamma}_{k-1}(a) = \gamma_{k-1}(\pi(a))$, where $\tilde{A} := ag(\tilde{\rho})$ and $A := ag(\rho)$. If $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$ involves no reception transition from $\tilde{P}$ whose corresponding transition in $\tilde{P}$ has action ‘$\neq$’, then we directly lift this step into a step appended at the end of $\rho_{k-1}$ (making $\pi(a)$ take a transition whenever $a$ does so in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$). Otherwise, write $\tilde{A}_\neq$ the subset of $\tilde{A}$ corresponding to agents taking in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$ a reception transition from $\tilde{P}$ whose corresponding transition in $\tilde{P}$ has action ‘$\neq$’. Write $(q, \mathbf{br}(m), q') \in \Delta$ the broadcast transition used in this step. Using the copycat principle, we add to $\gamma_{k-1}$ a fresh agent $a_{\text{new}}$ with state $q$ and a register value that does not appear in $\gamma_{k-1}$. We first mimic this broadcast step at the end of $\rho_{k-1}$, making any agent $\pi(a) \in \pi(\tilde{A} \setminus \tilde{A}_\neq)$ take the transition that $a$ takes in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$. We then add a new step where $a_{\text{new}}$ broadcasts using transition $(q, \mathbf{br}(m), q')$, and every agent $\pi(a) \in \pi(\tilde{A}_\neq)$ takes the transition corresponding to the transition taken by $a$ in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$. Such a transition is a reception with action ‘$\neq$’ in $\tilde{P}$; however, because $a_{\text{new}}$ does not share its register value with any process from $\tilde{A}$, all disequality conditions are satisfied and this step is valid. In the end, every agent $\pi(a) \in \pi(\tilde{A})$ has taken the transition in $\tilde{P}$ corresponding to the one $a$ took in $\tilde{P}$ in step $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$, hence the configuration $\gamma_k$ reached by the constructed run is such that $\tilde{\gamma}_k \sqsubseteq \gamma_k$. $\square$

## I.2 Abstraction

We now define our abstraction. We formalize the definition of a gang:

**Definition 44.** Let $(Q, \Delta, q_0)$ be a protocol.

A gang is a pair $G = (b, K) \in (Q \cup \{\perp\}) \times 2^Q$. The element $b$ is the boss and the set $K$ is the clique of the gang.

Let $\rho = \gamma_0 \to \gamma_1 \to \dots \to \gamma_k$ be a run and $v \in \text{val}(\rho)$. The gang of value $v$ in $\rho$, written $\text{gang}_v(\rho)$, is the gang $(b_v(\rho), K_v(\rho))$ such that,

- if there exists $a_0 \in ag(\rho)$ such that, for every $i \in [0, k]$, $\text{data}(\gamma_i)(a_0) = v$ then $b_v(\rho) := \text{st}(\gamma_k)(a_0)$, otherwise $b_v(\rho) := \perp$,

- $K_v(\rho) := \{q \in Q \mid \exists i \le k, \exists a \in \tilde{A} \setminus \{a_0\}, \gamma_i(a) = (q, v)\}$

We define abstract runs as follows:

**Definition 45.** An abstract configuration over $\tilde{A}$ is a tuple of $2^Q \times \mathcal{G}$ where $\mathcal{G}$ designates the set of all gangs. We write $\Sigma_{\tilde{A}}$ the set of abstract configurations over $\tilde{A}$ and $\Sigma := \bigcup_{\tilde{A} \subseteq \mathbb{N}_{\text{finite}}} \Sigma_{\tilde{A}}$ the set of all abstract configurations.

Given a set of states $S \subseteq Q$, a message type $m$ and a set of operations $O$, we define $S^m, \tilde{A} = \{s' \in Q \mid \exists s \in S, a \in O, (s, \text{rec}(m, a), s') \in \Delta\}$.

Given two abstract configurations $\sigma = (S, b, K)$ and $\sigma' = (S', b', K')$, there is an abstract step from $\sigma$ to $\sigma'$, denoted $\sigma \to \sigma'$, when $K' \subseteq S'$, $b' \in S' \cup \{\perp\}$ and one of the following cases is satisfied.

1. Broadcast from clique: There exists $(q_{br}, \mathbf{br}(m), q'_{br}) \in \Delta$ such that:
length $k-1$ and a final step $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$. By induction hypothesis, there exists $\rho_{k-1}: \gamma_0 \stackrel{*}{\to} \gamma_{k-1}$ such that $\tilde{\gamma}_{k-1} \sqsubseteq \gamma_{k-1}$: there exists an injective function $\pi: \tilde{A} \to A$ such that, for all $a \in \tilde{A}$, $\tilde{\gamma}_{k-1}(a) = \gamma_{k-1}(\pi(a))$, where $\tilde{A} := ag(\tilde{\rho})$ and $A := ag(\rho)$. If $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$ involves no reception transition from $\tilde{\mathcal{P}}$ whose corresponding transition in $\mathcal{P}$ has action ‘$\neq$’, then we directly lift this step into a step appended at the end of $\rho_{k-1}$ (making $\pi(a)$ take a transition whenever $a$ does so in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$). Otherwise, write $\tilde{A}_\neq$ the subset of $\tilde{A}$ corresponding to agents taking in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$ a reception transition from $\tilde{\mathcal{P}}$ whose corresponding transition in $\mathcal{P}$ has action ‘$\neq$’. Write $(q, \mathbf{br}(m), q') \in \Delta$ the broadcast transition used in this step. Using the copycat principle, we add to $\gamma_{k-1}$ a fresh agent $a_{\text{new}}$ with state $q$ and a register value that does not appear in $\gamma_{k-1}$. We first mimic this broadcast step at the end of $\rho_{k-1}$, making any agent $\pi(a) \in \pi(\tilde{A} \setminus \tilde{A}_\neq)$ take the transition that $a$ takes in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$. We then add a new step where $a_{\text{new}}$ broadcasts using transition $(q, \mathbf{br}(m), q')$, and every agent $\pi(a) \in \pi(\tilde{A}_\neq)$ takes the transition corresponding to the transition taken by $a$ in $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$. Such a transition is a reception with action ‘$\neq$’ in $\mathcal{P}$; however, because $a_{\text{new}}$ does not share its register value with any process from $\tilde{A}$, all disequality conditions are satisfied and this step is valid. In the end, every agent $\pi(a) \in \pi(\tilde{A})$ has taken the transition in $\mathcal{P}$ corresponding to the one $a$ took in $\tilde{\mathcal{P}}$ in step $\tilde{\gamma}_{k-1} \to \tilde{\gamma}_k$, hence the configuration $\gamma_k$ reached by the constructed run is such that $\tilde{\gamma}_k \sqsubseteq \gamma_k$. $\square$

## I.2 Abstraction

We now define our abstraction. We formalize the definition of a gang:

**Definition 44.** Let $(Q, \Delta, q_0)$ be a protocol.

A gang is a pair $G = (b, K) \in (Q \cup \{\perp\}) \times 2^Q$. The element $b$ is the boss and the set $K$ is the clique of the gang.

Let $\rho = \gamma_0 \to \gamma_1 \to \dots \to \gamma_k$ be a run and $v \in \text{val}(\rho)$. The gang of value $v$ in $\rho$, written $\text{gang}_v(\rho)$, is the gang $(b_v(\rho), K_v(\rho))$ such that,

- if there exists $a_0 \in ag(\rho)$ such that, for every $i \in [0, k]$, $\text{data}(\gamma_i)(a_0) = v$ then $b_v(\rho) := \text{st}(\gamma_k)(a_0)$, otherwise $b_v(\rho) := \perp$,

- $K_v(\rho) := \{q \in Q \mid \exists i \le k, \exists a \in \tilde{A} \setminus \{a_0\}, \gamma_i(a) = (q, v)\}$

We define abstract runs as follows:

**Definition 45.** An abstract configuration over $\tilde{A}$ is a tuple of $2^Q \times \mathcal{G}$ where $\mathcal{G}$ designates the set of all gangs. We write $\Sigma_{\tilde{A}}$ the set of abstract configurations over $\tilde{A}$ and $\Sigma := \bigcup_{A \subseteq N_{\text{finite}}} \Sigma_A$ the set of all abstract configurations.

Given a set of states $S \subseteq Q$, a message type $m$ and a set of operations $O$, we define $S^m, \tilde{A} = \{s' \in Q \mid \exists s \in S, a \in O, (s, \text{rec}(m, a), s') \in \Delta\}$.

Given two abstract configurations $\sigma = (S, b, K)$ and $\sigma' = (S', b', K')$, there is an abstract step from $\sigma$ to $\sigma'$, denoted $\sigma \to \sigma'$, when $K' \subseteq S'$, $b' \in S' \cup \{\perp\}$ and one of the following cases is satisfied.

1. Broadcast from clique: There exists $(q_{br}, \mathbf{br}(m), q'_{br}) \in \Delta$ such that:
(1) Either $\mathbf{b} = \mathbf{b}'$ or there exists ($\mathbf{b}, \mathbf{rec}(m, \alpha), \mathbf{b}'$) $\in \Delta$ for some action $\alpha$.

(2) $K' = K \cup \{q'_{br}\} \cup \overrightarrow{K^{m, \{=,*,\downarrow\}}} \cup \overrightarrow{S^{m, \{\downarrow\}}}$.

2. Broadcast from boss: there exists $m \in \mathcal{M}$ such that ($\mathbf{b}, \mathbf{br}(m), \mathbf{b}'$) $\in \Delta$

(1) $\mathbf{b}, \mathbf{b}' \neq \perp$ (technically implied by the existence of ($\mathbf{b}, \mathbf{br}(m), \mathbf{b}'$) but written here to match other cases)

(2) $K' = K \cup \overrightarrow{K^{m, \{=,*,\downarrow\}}} \cup \overrightarrow{S^{m, \{\downarrow\}}}$.

3. External broadcast: There exists ($q_{br}, \mathbf{br}(m), q'_{br}$) $\in \Delta$ such that

(1) Either $\mathbf{b} = \mathbf{b}'$ or:

- $\mathbf{b}' \neq \perp$ and there exists ($\mathbf{b}, \mathbf{rec}(m, *), \mathbf{b}'$) $\in \Delta$, or

- $\mathbf{b}' = \perp$ and there exists ($\mathbf{b}, \mathbf{rec}(m, \downarrow), \mathbf{b}'$) $\in \Delta$.

(2) $K' = K \cup \overrightarrow{K^{m, \{*\}}}$.

4. Gang reset: $S' = S \cup K \cup \{\mathbf{b}\}$, $K' = \emptyset$ and $\mathbf{b}' = q_0$

Given a concrete run $\rho: \gamma_0 \xrightarrow{*} \gamma_k$, we write $\text{abs}_v(\rho)$ for the abstract configuration $(S, \text{gang}_v(\rho))$ where $S$ is the set of all states appearing in $\rho$.

The initial abstract configuration is $\sigma_0 := (\{q_0\}, q_0, \emptyset)$. As in the concrete case, an abstract run is a sequence $\nu = \sigma_0, \dots, \sigma_k$ such that $\sigma_0$ is the initial configuration and, for all $i$, $\sigma_i \to \sigma_{i+1}$. We denote such a run $\sigma_0 \xrightarrow{*} \sigma_k$. Similarly, we denote by $\sigma \xrightarrow{*} \sigma'$ the existence of a sequence of steps from $\sigma$ to $\sigma'$.

The intuition is that we will keep track of one value at a time, while assuming that we have unlimited supplies of agents in the states we covered so far. We follow the gang of one value through the run, which allows us to discover new states. A gang reset lets us add those new states to the set of covered ones and switch to another value.

First of all we observe that if there is an abstract run covering a state then there is a short one.

**Lemma 46.** For every $\sigma \in \Sigma$ such that $\sigma_0 \xrightarrow{*} \sigma$, there exists an abstract run $\nu : \sigma_0 \xrightarrow{*} \sigma$ of less that $(|Q| + 2)^3$ steps.

*Proof.* Note that $S$ may never decrease along an abstract run and that $K$ may only decrease at gang resets. We can hence enforce in the abstract semantics that, at least every $|Q| + 2$ steps without reset, either $S$ or $K$ has increased. Indeed, otherwise the configuration has looped as the boss may only take $|Q| + 1$ values. We may also enforce that $S$ has strictly increased between two resets, as otherwise one may remove anything that happened between the two resets. Therefore, there are at most $|Q| - 1$ gang resets in total, and each portion of the run with no reset has at most $(|Q| + 2)(|Q| + 1)$ steps, yielding the bound. $\square$

It remains to prove that our abstraction is sound and complete.
(1) Either $\mathbf{b} = \mathbf{b}'$ or there exists ($\mathbf{b}, \mathbf{rec}(m, \alpha), \mathbf{b}'$) $\in \Delta$ for some action $\alpha$.

(2) $K' = K \cup \{q'_{br}\} \cup \overrightarrow{K^{m, \{=,*,\downarrow\}}} \cup \overrightarrow{S^{m, \{\downarrow\}}}$.

2. Broadcast from boss: there exists $m \in \mathcal{M}$ such that ($\mathbf{b}, \mathbf{br}(m), \mathbf{b}'$) $\in \Delta$

(1) $\mathbf{b}, \mathbf{b}' \neq \perp$ (technically implied by the existence of ($\mathbf{b}, \mathbf{br}(m), \mathbf{b}'$) but written here to match other cases)

(2) $K' = K \cup \overrightarrow{K^{m, \{=,*,\downarrow\}}} \cup \overrightarrow{S^{m, \{\downarrow\}}}$.

3. External broadcast: There exists ($q_{br}, \mathbf{br}(m), q'_{br}$) $\in \Delta$ such that

(1) Either $\mathbf{b} = \mathbf{b}'$ or:

- $\mathbf{b}' \neq \perp$ and there exists ($\mathbf{b}, \mathbf{rec}(m, *), \mathbf{b}'$) $\in \Delta$, or

- $\mathbf{b}' = \perp$ and there exists ($\mathbf{b}, \mathbf{rec}(m, \downarrow), \mathbf{b}'$) $\in \Delta$.

(2) $K' = K \cup \overrightarrow{K^{m, \{*\}}}$.

4. Gang reset: $S' = S \cup K \cup \{\mathbf{b}\}$, $K' = \emptyset$ and $\mathbf{b}' = q_0$

Given a concrete run $\rho: \gamma_0 \stackrel{*}{\to} \gamma_k$, we write $\text{abs}_v(\rho)$ for the abstract configuration $(S, \text{gang}_v(\rho))$ where $S$ is the set of all states appearing in $\rho$.

The initial abstract configuration is $\sigma_0 := (\{q_0\}, q_0, \emptyset)$. As in the concrete case, an abstract run is a sequence $\nu = \sigma_0, \dots, \sigma_k$ such that $\sigma_0$ is the initial configuration and, for all $i$, $\sigma_i \to \sigma_{i+1}$. We denote such a run $\sigma_0 \stackrel{*}{\to} \sigma_k$. Similarly, we denote by $\sigma \stackrel{*}{\to} \sigma'$ the existence of a sequence of steps from $\sigma$ to $\sigma'$.

The intuition is that we will keep track of one value at a time, while assuming that we have unlimited supplies of agents in the states we covered so far. We follow the gang of one value through the run, which allows us to discover new states. A gang reset lets us add those new states to the set of covered ones and switch to another value.

First of all we observe that if there is an abstract run covering a state then there is a short one.

**Lemma 46.** For every $\sigma \in \Sigma$ such that $\sigma_0 \stackrel{*}{\to} \sigma$, there exists an abstract run $\nu : \sigma_0 \stackrel{*}{\to} \sigma$ of less that $(|Q| + 2)^3$ steps.

*Proof.* Note that $S$ may never decrease along an abstract run and that $K$ may only decrease at gang resets. We can hence enforce in the abstract semantics that, at least every $|Q| + 2$ steps without reset, either $S$ or $K$ has increased. Indeed, otherwise the configuration has looped as the boss may only take $|Q| + 1$ values. We may also enforce that $S$ has strictly increased between two resets, as otherwise one may remove anything that happened between the two resets. Therefore, there are at most $|Q| - 1$ gang resets in total, and each portion of the run with no reset has at most $(|Q| + 2)(|Q| + 1)$ steps, yielding the bound. $\square$

It remains to prove that our abstraction is sound and complete.
**Completeness** In this subsection we prove Lemma 48. To do so, we take a concrete run $\rho$ in our model and any value $v$ appearing in the reached configuration. We prove that there exists an abstract run leading to the abstract configuration $(cov(\rho), gang_v(\rho))$.

To construct the abstract run, we will first show that for all $S$ such that $cov(\rho) \subseteq S$, we can keep track of the set of agents carrying a value $v$: $(S, q_0, \emptyset) \stackrel{*}{\rightarrow} (S, b_v(\rho), K)$ with $K_v(\rho) \subseteq K$. Then, it is left to show that for all concrete run $\rho$ and for all value $v$, $\sigma_0 \stackrel{*}{\rightarrow} (S, q_0, \emptyset)$ with $cov(\rho) \subseteq S$.

**Lemma 47.** For all initial runs $\rho: \gamma_0 \stackrel{*}{\rightarrow} \gamma$, $S \subseteq Q$ and $v \in val(\rho)$, if $cov(\rho) \subseteq S$ then there exists $K$ such that $(S, q_0, \emptyset) \stackrel{*}{\rightarrow} (S, b_v(\rho), K)$ and $K_v(\rho) \subseteq K$.

*Proof.* Let $\mathbb{A} = ag(\rho)$. As $v$ appears in $\rho$, it must appear in $\gamma_0$; let $a_0$ be the unique agent such that $\mathbf{data}(\gamma_0)(a_0) = v$. We write $\rho: \gamma_0 \rightarrow \gamma_1 \rightarrow \dots \rightarrow \gamma_k = \gamma$. For every $i \le k$, let $\rho_i: \gamma_0 \stackrel{*}{\rightarrow} \gamma_i$ be the prefix of $\rho$ of length $i$. We set $\sigma^0 = (S, q_0, \emptyset)$.

We construct by induction on $i$ a sequence of abstract configurations $\sigma^i = (S, b_i, K_i)$ such that $\sigma^0 \stackrel{*}{\rightarrow} \sigma^i$ and $K_v(\rho_i) \subseteq K_i$. The statement is clear for $i=0$.

Suppose now that $(S, q_0, \emptyset) \stackrel{*}{\rightarrow} \sigma^i$. If suffices to prove that $\sigma^i \rightarrow \sigma^{i+1}$. We consider the last step of $\rho_{i+1}$, which is referred to under the name $s_{i+1}$ in what follows; $s_{i+1}: \gamma_i \rightarrow \gamma_{i+1}$. Let $a_{br}$ the agent making the broadcast transition in $s_{i+1}$ and $A_{rec}$ the set of agents receiving this broadcast in $s_{i+1}$. Let $(q_{br}, \mathbf{br}(m), q'_{br}) \in \Delta$ denote the transition taken by $a_{br}$ in $s_{i+1}$.

We now make the following case distinction to determine the type of the abstract step $\sigma^i \rightarrow \sigma^{i+1}$:

1. if $\mathbf{data}(\gamma_i)(a_{br}) = v$ but there exists $j < i$ such that $\mathbf{data}(\gamma_j)(a_{br}) \neq v$ then it is a broadcast from clique,

2. if, for all $j \le i$, $\mathbf{data}(\gamma_j)(a_{br}) = v$ then it is a broadcast from boss,

3. otherwise it is an external broadcast.

Note that $a_{br}$ may not change its register value in $s_{i+1}$ hence $\mathbf{data}(\gamma_i)(a_{br}) = \mathbf{data}(\gamma_{i+1})(a_{br})$.

Let $a_{boss}$ the agent such that $\mathbf{data}(\gamma_0)(a_{boss}) = v$. In case 2, $a_{boss} = a_{br}$; in the other two cases, $a_{boss} \neq a_{br}$.

It is easy to check that in all cases, the gang given by applying the abstract semantics covers $gang_v(\rho_{i+1})$:

(1) In case 2, this condition is automatically satisfied. In the other two cases, we look at what $a_{boss}$ does in $s_{i+1}$. If it remains idle then we have $b_i = b_{i+1}$. Otherwise it takes a reception transition as $a_{br} \neq a_{boss}$. In case 1 the condition is then satisfied. In case 3, this reception cannot have action ‘=’ as the broadcast is from an agent with register value that is not $v$ ($\mathbf{data}(\gamma_i)(a_{br}) \neq v$ by hypothesis). For the same reason, if this reception has action ‘↓’ then $b_{i+1} = \bot$. If this reception has action ‘*’ and $b_i \neq \bot$ then $b_{i+1} \neq \bot$ as $a_{boss}$ keeps value $v$.
**Completeness** In this subsection we prove Lemma 48. To do so, we take a concrete run $\rho$ in our model and any value $v$ appearing in the reached configuration. We prove that there exists an abstract run leading to the abstract configuration $(cov(\rho), gang_v(\rho))$.

To construct the abstract run, we will first show that for all $S$ such that $cov(\rho) \subseteq S$, we can keep track of the set of agents carrying a value $v$: $(S, q_0, \emptyset) \stackrel{*}{\rightarrow} (S, b_v(\rho), K)$ with $K_v(\rho) \subseteq K$. Then, it is left to show that for all concrete run $\rho$ and for all value $v$, $\sigma_0 \stackrel{*}{\rightarrow} (S, q_0, \emptyset)$ with $cov(\rho) \subseteq S$.

**Lemma 47.** For all initial runs $\rho: \gamma_0 \stackrel{*}{\rightarrow} \gamma$, $S \subseteq Q$ and $v \in val(\rho)$, if $cov(\rho) \subseteq S$ then there exists $K$ such that $(S, q_0, \emptyset) \stackrel{*}{\rightarrow} (S, b_v(\rho), K)$ and $K_v(\rho) \subseteq K$.

*Proof.* Let $\mathbb{A} = ag(\rho)$. As $v$ appears in $\rho$, it must appear in $\gamma_0$; let $a_0$ be the unique agent such that $\mathbf{data}(\gamma_0)(a_0) = v$. We write $\rho: \gamma_0 \rightarrow \gamma_1 \rightarrow \dots \rightarrow \gamma_k = \gamma$. For every $i \le k$, let $\rho_i: \gamma_0 \stackrel{*}{\rightarrow} \gamma_i$ be the prefix of $\rho$ of length $i$. We set $\sigma^0 = (S, q_0, \emptyset)$.

We construct by induction on $i$ a sequence of abstract configurations $\sigma^i = (S, b_i, K_i)$ such that $\sigma^0 \stackrel{*}{\rightarrow} \sigma^i$ and $K_v(\rho_i) \subseteq K_i$. The statement is clear for $i=0$.

Suppose now that $(S, q_0, \emptyset) \stackrel{*}{\rightarrow} \sigma^i$. If suffices to prove that $\sigma^i \rightarrow \sigma^{i+1}$. We consider the last step of $\rho_{i+1}$, which is referred to under the name $s_{i+1}$ in what follows; $s_{i+1}: \gamma_i \rightarrow \gamma_{i+1}$. Let $a_{br}$ the agent making the broadcast transition in $s_{i+1}$ and $A_{rec}$ the set of agents receiving this broadcast in $s_{i+1}$. Let $(q_{br}, \mathbf{br}(m), q'_{br}) \in \Delta$ denote the transition taken by $a_{br}$ in $s_{i+1}$.

We now make the following case distinction to determine the type of the abstract step $\sigma^i \rightarrow \sigma^{i+1}$:

1. if $\mathbf{data}(\gamma_i)(a_{br}) = v$ but there exists $j < i$ such that $\mathbf{data}(\gamma_j)(a_{br}) \neq v$ then it is a broadcast from clique,

2. if, for all $j \le i$, $\mathbf{data}(\gamma_j)(a_{br}) = v$ then it is a broadcast from boss,

3. otherwise it is an external broadcast.

Note that $a_{br}$ may not change its register value in $s_{i+1}$ hence $\mathbf{data}(\gamma_i)(a_{br}) = \mathbf{data}(\gamma_{i+1})(a_{br})$.

Let $a_{boss}$ the agent such that $\mathbf{data}(\gamma_0)(a_{boss}) = v$. In case 2, $a_{boss} = a_{br}$; in the other two cases, $a_{boss} \neq a_{br}$.

It is easy to check that in all cases, the gang given by applying the abstract semantics covers $gang_v(\rho_{i+1})$:

(1) In case 2, this condition is automatically satisfied. In the other two cases, we look at what $a_{boss}$ does in $s_{i+1}$. If it remains idle then we have $b_i = b_{i+1}$. Otherwise it takes a reception transition as $a_{br} \neq a_{boss}$. In case 1 the condition is then satisfied. In case 3, this reception cannot have action ‘=’ as the broadcast is from an agent with register value that is not $v$ ($\mathbf{data}(\gamma_i)(a_{br}) \neq v$ by hypothesis). For the same reason, if this reception has action ‘↓’ then $b_{i+1} = \bot$. If this reception has action ‘*’ and $b_i \neq \bot$ then $b_{i+1} \neq \bot$ as $a_{boss}$ keeps value $v$.
(2) In all cases $K_{i+1}$ is defined by adding to $K_i$ all states reachable with value $v$ from it by receiving the broadcast message $m$ from a state of $K_i$ with value $v$ or from a state of $S$ with value $v' \neq v$ (plus $q'_{br}$ in case 1). As $K_v(\rho_i) \subseteq K_i$, necessarily $K_v(\rho_{i+1}) \subseteq K_{i+1}$

We have proven that $\sigma^i \to \sigma^{i+1}$, which concludes the induction step. Applying the result with $i=k$ proves Lemma 47. □

We may now prove completeness of the abstraction. Intuitively, we start with $S = \{q_0\}$ and we increase it in the following way: we look at the first state $q \notin S$ that is covered in $\rho$, we follow the gang associated with the value of an agent that covered $q$ until the gang covers it too (using Lemma 47), then we do a gang reset to add $q$ to $S$.

**Lemma 48.** If $\rho$ is an initial run and $v \in \text{val}(\rho)$, then there exist $S, K$ such that $\sigma_0 \xrightarrow{*} (S, b_v(\rho), K)$ and $\text{cov}(\rho) \subseteq S$ and $K_v(\rho) \subseteq K$.

*Proof.* Let $\rho$ an initial run. We construct by induction an increasing sequence of sets $C_0, \dots, C_m$ such that $C_m = \text{cov}(\rho)$ and for all $i$, $C_i \subseteq \text{cov}(\rho)$, $q_0 \in C_i$, and there exists $S_i$ such that $\sigma_0 \xrightarrow{*} (S_i, q_0, \emptyset)$ and $C_i \subseteq S_i$. First, we set $C_0 = \{q_0\}$ and the property is verified as $\sigma_0 \xrightarrow{*} (\{q_0\}, q_0, \emptyset)$.

Now suppose we constructed $C_0, \dots, C_j$. If $C_j = \text{cov}(\rho)$ we can stop. Otherwise let $\rho_p : \gamma_0 \xrightarrow{*} \gamma_p$ the longest suffix of $\rho$ such that $\text{cov}(\rho_p) \subseteq C_j$. Write $s$ the step immediately after $\rho_p$ in $\rho$. By maximality of $\rho_p$, $\rho_p \cdot s$ covers some state $q$ that is not in $C_j$. Let $a$ be an agent that is in $q$ after step $s$, let $v$ be its value at that point. We set $C_{i+1} = C_i \cup \{q\}$.

By induction hypothesis, there exist $S_j$ such that $\sigma_0 \xrightarrow{*} (S_j, q_0, \emptyset)$ and $C_j \subseteq S_j$. Furthermore, as $\text{cov}(\rho_p) \subseteq C_j$, by Lemma 47 there exists $K_j$ such that $\sigma_0 \xrightarrow{*} (S_j, b_v(\rho_p), K_j)$ and $K_v(\rho_p) \subseteq K_j$.

If $q \in K_j$ then applying a gang reset suffices. If not, we mimic step $s$ with a step in the abstract semantics, as in Lemma 47 so that $q$ is added to the clique, then apply a gang reset to reach $(S_{i+1}, q_0, \emptyset)$ with $C_{i+1} = S_i \cup \{q\} \subseteq S_{i+1}$.

This concludes our induction.

In the end, there exist $S_m$ such that $\sigma_0 \xrightarrow{*} (S_m, q_0, \emptyset)$ and $\text{cov}(\rho) \subseteq S_j$. Lemma 47 allows us to conclude the proof." □

**Soundness** It is left to prove that our abstraction is sound, which we will do by considering an abstract run $\sigma_0 \xrightarrow{*} \sigma = (S, b, K)$ and constructing a concrete run $\rho : \gamma_0 \xrightarrow{*} \gamma$ that follows the abstract run with an exponential amount of agents to make sure that we can send some of them through all possible transitions at each step and never run out.

**Lemma 49.** For all $\sigma_0 \in \Sigma_{\text{init}}$ and $\sigma = (S, b, K) \in \Sigma$ such that $\sigma_0 \xrightarrow{*} \sigma$, for all $s \in S$, there exists a reachable configuration $\gamma$ covering $s$.

We in fact prove the following stronger lemma, which directly implies Lemma 49.
(2) In all cases $K_{i+1}$ is defined by adding to $K_i$ all states reachable with value $v$ from it by receiving the broadcast message $m$ from a state of $K_i$ with value $v$ or from a state of $S$ with value $v' \neq v$ (plus $q'_{br}$ in case 1). As $K_v(\rho_i) \subseteq K_i$, necessarily $K_v(\rho_{i+1}) \subseteq K_{i+1}$

We have proven that $\sigma^i \to \sigma^{i+1}$, which concludes the induction step. Applying the result with $i=k$ proves Lemma 47. $\square$

We may now prove completeness of the abstraction. Intuitively, we start with $S = \{q_0\}$ and we increase it in the following way: we look at the first state $q \notin S$ that is covered in $\rho$, we follow the gang associated with the value of an agent that covered $q$ until the gang covers it too (using Lemma 47), then we do a gang reset to add $q$ to $S$.

**Lemma 48.** If $\rho$ is an initial run and $v \in \text{val}(\rho)$, then there exist $S, K$ such that $\sigma_0 \xrightarrow{*} (S, b_v(\rho), K)$ and $\text{cov}(\rho) \subseteq S$ and $K_v(\rho) \subseteq K$.

*Proof.* Let $\rho$ an initial run. We construct by induction an increasing sequence of sets $C_0, \dots, C_m$ such that $C_m = \text{cov}(\rho)$ and for all $i$, $C_i \subseteq \text{cov}(\rho)$, $q_0 \in C_i$, and there exists $S_i$ such that $\sigma_0 \xrightarrow{*} (S_i, q_0, \emptyset)$ and $C_i \subseteq S_i$. First, we set $C_0 = \{q_0\}$ and the property is verified as $\sigma_0 \xrightarrow{*} (\{q_0\}, q_0, \emptyset)$.

Now suppose we constructed $C_0, \dots, C_j$. If $C_j = \text{cov}(\rho)$ we can stop. Otherwise let $\rho_p : \gamma_0 \xrightarrow{*} \gamma_p$ the longest suffix of $\rho$ such that $\text{cov}(\rho_p) \subseteq C_j$. Write $s$ the step immediately after $\rho_p$ in $\rho$. By maximality of $\rho_p$, $\rho_p \cdot s$ covers some state $q$ that is not in $C_j$. Let $a$ be an agent that is in $q$ after step $s$, let $v$ be its value at that point. We set $C_{i+1} = C_i \cup \{q\}$.

By induction hypothesis, there exist $S_j$ such that $\sigma_0 \xrightarrow{*} (S_j, q_0, \emptyset)$ and $C_j \subseteq S_j$. Furthermore, as $\text{cov}(\rho_p) \subseteq C_j$, by Lemma 47 there exists $K_j$ such that $\sigma_0 \xrightarrow{*} (S_j, b_v(\rho_p), K_j)$ and $K_v(\rho_p) \subseteq K_j$.

If $q \in K_j$ then applying a gang reset suffices. If not, we mimic step $s$ with a step in the abstract semantics, as in Lemma 47 so that $q$ is added to the clique, then apply a gang reset to reach $(S_{i+1}, q_0, \emptyset)$ with $C_{i+1} = S_i \cup \{q\} \subseteq S_{i+1}$.

This concludes our induction.

In the end, there exist $S_m$ such that $\sigma_0 \xrightarrow{*} (S_m, q_0, \emptyset)$ and $\text{cov}(\rho) \subseteq S_j$. Lemma 47 allows us to conclude the proof." $\square$

**Soundness** It is left to prove that our abstraction is sound, which we will do by considering an abstract run $\sigma_0 \xrightarrow{*} \sigma = (S, b, K)$ and constructing a concrete run $\rho : \gamma_0 \xrightarrow{*} \gamma$ that follows the abstract run with an exponential amount of agents to make sure that we can send some of them through all possible transitions at each step and never run out.

**Lemma 49.** For all $\sigma_0 \in \Sigma_{\text{init}}$ and $\sigma = (S, b, K) \in \Sigma$ such that $\sigma_0 \xrightarrow{*} \sigma$, for all $s \in S$, there exists a reachable configuration $\gamma$ covering $s$.

We in fact prove the following stronger lemma, which directly implies Lemma 49.
**Lemma 50.** Let $\sigma_0 \in \Sigma_{\text{init}}$, and $\sigma_0 \to \sigma_1 \to \dots \to \sigma_n$ an abstract run. For all $i$ let $(S_i, b_i, K_i) := \sigma_i$. Let $M = |\Delta| + 1$.

For all $i$, there exist a set of agents $\mathbb{A}_i$, an initial run $\rho_i : \gamma_0 \xrightarrow{*} \gamma_i$ over $\mathbb{A}_i$, agents $a_0, \dots, a_n \in \mathbb{A}_i$ and values $v_0, \dots, v_n \in \mathbb{N}$ such that:

- for all $s \in S_i$, there are at least $M^{n-i}$ agents (different from $a_i$) in state $s$

- for all $s \in K_i$, there are at least $M^{n-i}$ agents (different from $a_i$) in state $s$ with value $v_i$

- if $b_i \neq \perp$, then $a_i$ is in state $b_i$ with value $v_i$.

*Proof.* We proceed by induction on $i$. We set $\mathbb{A}_0 = \{1, \dots, M^n\}$, and we set $\gamma_0(a) = (q_0, a)$ for all $a$. Clearly $\gamma_0$ satisfies the requirements with respect to $\sigma_0$, with $a_0 = v_0 \in \mathbb{A}$.

Now assume we constructed $\gamma_0 \xrightarrow{*} \dots \xrightarrow{*} \gamma_i$ over $\mathbb{A}_i$ satisfying the conditions of the lemma, we construct $\gamma_{i+1}$ using a case distinction on the form of the transition $\sigma_i \to \sigma_{i+1}$. For each $s \in S \setminus K$ we define $\mathbb{A}_{i,s}$ as the set of agents in state $s$ in $\gamma_i$. We have $|\mathbb{A}_{i,s}| \ge M^{n-i}$ thus we can extract $M = |\Delta| + 1$ disjoint sets of agents $(\mathbb{A}_{i,s}^d)_{d \in \Delta \cup \{\varepsilon\}}$ from it, each set having $M^{n-i-1}$ agents. Similarly, for each $s \in K$ we define $\mathbb{A}_{i,s}$ as the set of agents in state $s$ with value $v_i$ in $\gamma_i$. We have $|\mathbb{A}_{i,s}| \ge M^{n-i}$ thus we can extract $|\Delta| + 1$ disjoint sets of agents $(\mathbb{A}_{i,s}^d)_{d \in \Delta \cup \{\varepsilon\}}$ from it each set having $M^{n-i-1}$ agents.

**Case 1:** If $\sigma_i \to \sigma_{i+1}$ is a broadcast from clique $d = (q, \mathbf{br}(m), q')$ with $q \in K_i$, then we make all agents $a \in \mathbb{A}_{i,q}^d$ (which all have value $v_i$) execute that transition one by one. None of those broadcasts are received by any other agent, except for the last one: If $b \neq b'$ then there is a transition $(b, \mathbf{rec}(m, \alpha), b')$ and we make $a_i$ execute it upon receiving the broadcast. We then set $a_{i+1} = a_i$. For all $k' \in K_{i+1} \setminus (K_i \cup \{q'\})$ there exists a transition $d' = (k, \mathbf{rec}(m, \alpha), k')$ such that either $\alpha$ is $=$ or $*$ and $k \in K_i$ or $\alpha$ is $\downarrow$ and $k \in S$. In both cases we make all agents of $\mathbb{A}_{i,k'}^d$ take that transition. We set $v_{i+1} = v_i$.

**Case 2:** If $\sigma_i \to \sigma_{i+1}$ is a broadcast from boss $d = (b_i, \mathbf{br}(m), b_{i+1})$, then we make $a_i$ (which has value $v_i$) execute that transition, and we set $a_{i+1} = a_i$. The agents receiving that message are as follows:

For all $k' \in K_{i+1} \setminus K_i$ there exists a transition $d' = (k, \mathbf{rec}(m, \alpha), k')$ such that $\alpha$ is either $=$ or $*$ and $k \in K_i$ or $\alpha$ is $\downarrow$ and $k \in S$. In both cases we make all agents of $\mathbb{A}_k^d$ take that transition. By definition of an abstract run, we must have $b_i \in S_i$. Hence we can make all agents of $\mathbb{A}_{i,s}^d$ execute $d$, with no agent receiving the corresponding broadcasts. We set $v_{i+1} = v_i$.

**Case 3:** If $\sigma_i \to \sigma_{i+1}$ is an external broadcast $d = (q, \mathbf{br}(m), q')$, then we make all agents $a \in \mathbb{A}_q^d$ execute that transition one by one. None of those broadcasts are received by any other agent, except for the last one: If $b_i \neq b_{i+1}$ then there is a transition $(b_i, \mathbf{rec}(m, \alpha), b')$ and either $b_{i+1} = b'' \neq \perp$ and $\alpha = *$ or $b_{i+1} = \perp$ and $\alpha = \downarrow$. In both cases we make $a_i$ execute that transition, and we set $a_{i+1} = a_i$. For all $k' \in K_{i+1} \setminus K_i$ there exists a transition $d' = (k, \mathbf{rec}(m, *), k')$
**Lemma 50.** Let $\sigma_0 \in \Sigma_{\text{init}}$, and $\sigma_0 \to \sigma_1 \to \dots \to \sigma_n$ an abstract run. For all $i$ let $(S_i, b_i, K_i) := \sigma_i$. Let $M = |\Delta| + 1$.

For all $i$, there exist a set of agents $\mathbb{A}_i$, an initial run $\rho_i : \gamma_0 \xrightarrow{*} \gamma_i$ over $\mathbb{A}_i$, agents $a_0, \dots, a_n \in \mathbb{A}_i$ and values $v_0, \dots, v_n \in \mathbb{N}$ such that:

- for all $s \in S_i$, there are at least $M^{n-i}$ agents (different from $a_i$) in state $s$

- for all $s \in K_i$, there are at least $M^{n-i}$ agents (different from $a_i$) in state $s$ with value $v_i$

- if $b_i \neq \perp$, then $a_i$ is in state $b_i$ with value $v_i$.

*Proof.* We proceed by induction on $i$. We set $\mathbb{A}_0 = \{1, \dots, M^n\}$, and we set $\gamma_0(a) = (q_0, a)$ for all $a$. Clearly $\gamma_0$ satisfies the requirements with respect to $\sigma_0$, with $a_0 = v_0 \in \mathbb{A}$.

Now assume we constructed $\gamma_0 \xrightarrow{*} \dots \xrightarrow{*} \gamma_i$ over $\mathbb{A}_i$ satisfying the conditions of the lemma, we construct $\gamma_{i+1}$ using a case distinction on the form of the transition $\sigma_i \to \sigma_{i+1}$. For each $s \in S \setminus K$ we define $\mathbb{A}_{i,s}$ as the set of agents in state $s$ in $\gamma_i$. We have $|\mathbb{A}_{i,s}| \ge M^{n-i}$ thus we can extract $M = |\Delta| + 1$ disjoint sets of agents $(\mathbb{A}_{i,s}^d)_{d \in \Delta \cup \{\varepsilon\}}$ from it, each set having $M^{n-i-1}$ agents. Similarly, for each $s \in K$ we define $\mathbb{A}_{i,s}$ as the set of agents in state $s$ with value $v_i$ in $\gamma_i$. We have $|\mathbb{A}_{i,s}| \ge M^{n-i}$ thus we can extract $|\Delta| + 1$ disjoint sets of agents $(\mathbb{A}_{i,s}^d)_{d \in \Delta \cup \{\varepsilon\}}$ from it each set having $M^{n-i-1}$ agents.

**Case 1:** If $\sigma_i \to \sigma_{i+1}$ is a broadcast from clique $d = (q, \mathbf{br}(m), q')$ with $q \in K_i$, then we make all agents $a \in \mathbb{A}_{i,q}^d$ (which all have value $v_i$) execute that transition one by one. None of those broadcasts are received by any other agent, except for the last one: If $b \neq b'$ then there is a transition $(b, \mathbf{rec}(m, \alpha), b')$ and we make $a_i$ execute it upon receiving the broadcast. We then set $a_{i+1} = a_i$. For all $k' \in K_{i+1} \setminus (K_i \cup \{q'\})$ there exists a transition $d' = (k, \mathbf{rec}(m, \alpha), k')$ such that either $\alpha$ is $=$ or $*$ and $k \in K_i$ or $\alpha$ is $\downarrow$ and $k \in S$. In both cases we make all agents of $\mathbb{A}_{i,k'}^d$ take that transition. We set $v_{i+1} = v_i$.

**Case 2:** If $\sigma_i \to \sigma_{i+1}$ is a broadcast from boss $d = (b_i, \mathbf{br}(m), b_{i+1})$, then we make $a_i$ (which has value $v_i$) execute that transition, and we set $a_{i+1} = a_i$. The agents receiving that message are as follows:

For all $k' \in K_{i+1} \setminus K_i$ there exists a transition $d' = (k, \mathbf{rec}(m, \alpha), k')$ such that $\alpha$ is either $=$ or $*$ and $k \in K_i$ or $\alpha$ is $\downarrow$ and $k \in S$. In both cases we make all agents of $\mathbb{A}_k^d$ take that transition. By definition of an abstract run, we must have $b_i \in S_i$. Hence we can make all agents of $\mathbb{A}_{i,s}^d$ execute $d$, with no agent receiving the corresponding broadcasts. We set $v_{i+1} = v_i$.

**Case 3:** If $\sigma_i \to \sigma_{i+1}$ is an external broadcast $d = (q, \mathbf{br}(m), q')$, then we make all agents $a \in \mathbb{A}_q^d$ execute that transition one by one. None of those broadcasts are received by any other agent, except for the last one: If $b_i \neq b_{i+1}$ then there is a transition $(b_i, \mathbf{rec}(m, \alpha), b')$ and either $b_{i+1} = b'' \neq \perp$ and $\alpha = *$ or $b_{i+1} = \perp$ and $\alpha = \downarrow$. In both cases we make $a_i$ execute that transition, and we set $a_{i+1} = a_i$. For all $k' \in K_{i+1} \setminus K_i$ there exists a transition $d' = (k, \mathbf{rec}(m, *), k')$
with $k \in K_i$. We make all agents of $A_k^{d'}$ take that transition. We set $v_{i+1} = v_i$.

**Case 4:** If $\sigma_i \to \sigma_{i+1}$ is a gang reset then no agent moves and we select some $a_{i+1}$ in $A_{q_0}$ and set $v_{i+1}$ to be its value.

Throughout the case distinction we have ensured that:

- If $b_{i+1} \neq \perp$ then $a_{i+1}$ is an agent of value $v_{i+1}$.

- If the step is not a gang reset, then $v_{i+1} = v_i$ and for all $k' \in K_{i+1} \setminus K_i$, there exists $d \in \Delta$ from some $k$ to $k'$ such that all agents of $A_{i,k}^d$ take that transition. Furthermore, if $d$ is of the form $(k, \text{rec}(m, \downarrow), k')$ then the broadcasting agent has value $v_i$, thus all those agents keep value $v_i = v_{i+1}$. For all $k \in K_i$, the agents of $A_{i,k}^\epsilon$ do not move between configurations $\gamma_i$ and $\gamma_{i+1}$, hence they have state $k$ and value $v_{i+1}$ in $\gamma_{i+1}$.

- If the step is a gang reset, the conditions of the lemma hold trivially.

As a result, we have ensured that the conditions of the lemma were respected. This concludes our induction. $\square$

To obtain Lemma 49, we apply Lemma 50 to an abstract run $\sigma_0 \to \dots \to \sigma_n = \sigma$ from $\sigma_0$ to $\sigma$ by setting $i = n$.

## I.3 Conclusion

**Proposition 51.** Let $q_f$ be a state, there exists a reachable configuration covering $q_f$ if and only if there exists a reachable abstract configuration $(S, b, K)$ with $q_f \in S$.

*Proof.* The two implications follow from Lemmas 48 and 49 respectively. $\square$

**NP-hardness.** We present here a reduction from the 3SAT problem to the cover problem in 1-BNRAs.

**Proposition 52.** The cover problem is NP-hard.

*Proof.* Let $x_1, \dots, x_n$ be variables and $\phi = \bigwedge_{j=1}^m C_j$ with, for all $j$, $C_j = \ell_j^1 \lor \ell_j^2 \lor \ell_j^3$ and $\ell_j^1, \ell_j^2, \ell_j^3 \in \{x_i, \neg x_i \mid 1 \le i \le n\}$.

Consider the protocol displayed in Figure 12. Our alphabet of messages is the set of literals $\{x_i, \neg x_i \mid 1 \le i \le n\}$. Agents may either receive a message, and repeat it forever or it may broadcast one of $x_i, \neg x_i$ for each $i$ and then try to receive a message with one of $\ell_j^1, \ell_j^2, \ell_j^3$ for each $j$, with their own register value.

If $\phi$ is satisfied by some assignment $\nu$, then we construct a run where an agent $a$ broadcasts the satisfied literals while going from 0 to $N$ and other agents receive the messages and go to the corresponding states in the lower part of the protocol while storing the register value of $a$. Then for each $j$ we select some $\ell_j^p$ satisfied by $\nu$. There exists $i$ such that there is an agent in state $\ell_j^p$, which broadcasts $\ell_j^p$ along with the initial register value of $a$, allowing $a$ to go to the next state. As a result, there is a run in which an agent $a$ reaches $m'$.
with $k \in K_i$. We make all agents of $A_k^{d'}$ take that transition. We set $v_{i+1} = v_i$.

**Case 4:** If $\sigma_i \to \sigma_{i+1}$ is a gang reset then no agent moves and we select some $a_{i+1}$ in $A_{q_0}$ and set $v_{i+1}$ to be its value.

Throughout the case distinction we have ensured that:

- If $b_{i+1} \neq \perp$ then $a_{i+1}$ is an agent of value $v_{i+1}$.

- If the step is not a gang reset, then $v_{i+1} = v_i$ and for all $k' \in K_{i+1} \setminus K_i$, there exists $d \in \Delta$ from some $k$ to $k'$ such that all agents of $A_{i,k}^d$ take that transition. Furthermore, if $d$ is of the form $(k, \text{rec}(m, \downarrow), k')$ then the broadcasting agent has value $v_i$, thus all those agents keep value $v_i = v_{i+1}$. For all $k \in K_i$, the agents of $A_{i,k}^\epsilon$ do not move between configurations $\gamma_i$ and $\gamma_{i+1}$, hence they have state $k$ and value $v_{i+1}$ in $\gamma_{i+1}$.

- If the step is a gang reset, the conditions of the lemma hold trivially.

As a result, we have ensured that the conditions of the lemma were respected. This concludes our induction. $\square$

To obtain Lemma 49, we apply Lemma 50 to an abstract run $\sigma_0 \to \dots \to \sigma_n = \sigma$ from $\sigma_0$ to $\sigma$ by setting $i = n$.

## I.3 Conclusion

**Proposition 51.** Let $q_f$ be a state, there exists a reachable configuration covering $q_f$ if and only if there exists a reachable abstract configuration $(S, b, K)$ with $q_f \in S$.

*Proof.* The two implications follow from Lemmas 48 and 49 respectively. $\square$

**NP-hardness.** We present here a reduction from the 3SAT problem to the cover problem in 1-BNRAs.

**Proposition 52.** The cover problem is NP-hard.

*Proof.* Let $x_1, \dots, x_n$ be variables and $\phi = \bigwedge_{j=1}^m C_j$ with, for all $j$, $C_j = \ell_j^1 \lor \ell_j^2 \lor \ell_j^3$ and $\ell_j^1, \ell_j^2, \ell_j^3 \in \{x_i, \neg x_i \mid 1 \le i \le n\}$.

Consider the protocol displayed in Figure 12. Our alphabet of messages is the set of literals $\{x_i, \neg x_i \mid 1 \le i \le n\}$. Agents may either receive a message, and repeat it forever or it may broadcast one of $x_i, \neg x_i$ for each $i$ and then try to receive a message with one of $\ell_j^1, \ell_j^2, \ell_j^3$ for each $j$, with their own register value.

If $\phi$ is satisfied by some assignment $\nu$, then we construct a run where an agent $a$ broadcasts the satisfied literals while going from 0 to $N$ and other agents receive the messages and go to the corresponding states in the lower part of the protocol while storing the register value of $a$. Then for each $j$ we select some $\ell_j^p$ satisfied by $\nu$. There exists $i$ such that there is an agent in state $\ell_j^p$, which broadcasts $\ell_j^p$ along with the initial register value of $a$, allowing $a$ to go to the next state. As a result, there is a run in which an agent $a$ reaches $m'$.
<figure><img src="image_15.png" /><figcaption>Fig. 12: The protocol used for the NP-hardness proof.</figcaption></figure>

Now suppose there is a run $\rho$ over some set of agents $A$ such that some agent $a \in A$ is in state $m'$ in the final configuration. For each $i$, $a$ has broadcast either $x_i$ or $\neg x_i$, but not both. Let $\nu$ be the valuation assigning $\top$ to $x_i$ if and only if $a$ has broadcast it. For each $j$, $a$ has received one of $\ell_j^1, \ell_j^2, \ell_j^3$ along with its own initial register value (which we call $r$). For this to happen, $a$ must have broadcast this literal before, hence it is satisfied by $\nu$.

As a result, $\nu$ satisfies a literal of each clause of $\phi$, and thus satisfies $\phi$. This concludes our reduction. $\square$

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

*Proof.* The lower bound is given by Proposition 52. For the upper bound, say we are given a protocol $\mathcal{P} = (Q, \mathcal{M}, \Delta, q_0, r)$ and a state $q_f$. By Proposition 51, there is a reachable configuration covering $q_f$ if and only if there is an abstract run to an abstract configuration $(S, b, K)$ with $q_f \in S$. Furthermore, by Lemma 46 if there is such an abstract run then there is one with at most $(|Q| + 2)^3$ steps. Thus we can simply guess such an abstract run and verify it in polynomial time. As a result, the cover problem is in NP. $\square$
<figure><img src="image_14.png" /><figcaption>Fig. 12: The protocol used for the NP-hardness proof.</figcaption></figure>

Now suppose there is a run $\rho$ over some set of agents $A$ such that some agent $a \in A$ is in state $m'$ in the final configuration. For each $i$, $a$ has broadcast either $x_i$ or $\neg x_i$, but not both. Let $\nu$ be the valuation assigning $\top$ to $x_i$ if and only if $a$ has broadcast it. For each $j$, $a$ has received one of $\ell_j^1, \ell_j^2, \ell_j^3$ along with its own initial register value (which we call $r$). For this to happen, $a$ must have broadcast this literal before, hence it is satisfied by $\nu$.

As a result, $\nu$ satisfies a literal of each clause of $\phi$, and thus satisfies $\phi$. This concludes our reduction. $\square$

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

*Proof.* The lower bound is given by Proposition 52. For the upper bound, say we are given a protocol $\mathcal{P} = (Q, \mathcal{M}, \Delta, q_0, r)$ and a state $q_f$. By Proposition 51, there is a reachable configuration covering $q_f$ if and only if there is an abstract run to an abstract configuration $(S, b, K)$ with $q_f \in S$. Furthermore, by Lemma 46 if there is such an abstract run then there is one with at most $(|Q| + 2)^3$ steps. Thus we can simply guess such an abstract run and verify it in polynomial time. As a result, the cover problem is in NP. $\square$