11institutetext: Technical University of Munich 11email<EMAIL_ADDRESS>22institutetext: ENS Rennes 22email<EMAIL_ADDRESS>33institutetext: Technical University of Munich 33email:
<EMAIL_ADDRESS>
# Parameterized Analysis of Reconfigurable Broadcast Networks††thanks: This
project has received funding from the European Research Council (ERC) under
the European Union’s Horizon 2020 research and innovation programme under
grant agreement No 787367 (PaVeS).

A. R. Balasubramanian 11 Lucie Guillou 22 Chana Weil-Kennedy(✉) 33

###### Abstract

Reconfigurable broadcast networks (RBN) are a model of distributed computation
in which agents can broadcast messages to other agents using some underlying
communication topology which can change arbitrarily over the course of
executions. In this paper, we conduct _parameterized analysis_ of RBN. We
consider cubes, (infinite) sets of configurations in the form of lower and
upper bounds on the number of agents in each state, and we show that we can
evaluate boolean combinations over cubes and reachability sets of cubes in .
In particular, reachability from a cube to another cube is a -complete
problem.

To prove the upper bound for this parameterized analysis, we prove some
structural properties about the reachability sets and the _symbolic graph_
abstraction of RBN, which might be of independent interest. We justify this
claim by providing two applications of these results. First, we show that the
almost-sure coverability problem is -complete for RBN, thereby closing a
complexity gap from a previous paper [3]. Second, we define a computation
model using RBN, à la population protocols, called RBN protocols. We
characterize precisely the set of predicates that can be computed by such
protocols.

###### Keywords:

Broadcast networks Parameterized reachability Almost-sure coverability
Asynchronous shared-memory systems

##  1 Introduction

Reconfigurable broadcast networks (RBN) [8, 10] are a formalism for modelling
distributed systems in which a set of anonymous, finite-state agents execute
the same underlying protocol and broadcast messages to their neighbors
according to an underlying communication topology. The communication topology
is reconfigurable, meaning that the set of neighbors of an agent can change
arbitrarily over the course of an execution. Parameterized verification of
these networks concerns itself with proving that a given property is correct,
irrespective of the number of participating agents. Dually, it can be viewed
as the problem of finding an execution of some number of agents which violates
a given property. Ever since their introduction within this context [10], RBN
have been studied extensively, with various results on (parameterized)
reachability and coverability [8, 10, 3, 7], along with various extensions
using probabilities and clocks [5, 4].

In this paper, we first consider the _cube-reachability_ problem for RBN, in
which we are given two (possibly infinite) sets of configurations
$\mathcal{C}$ and $\mathcal{C}^{\prime}$ (called _cubes_), each of them
defined by lower and upper bounds on the number of agents in each state, and
we must decide if there is a configuration in $\mathcal{C}$ which can reach
some configuration in $\mathcal{C}^{\prime}$. The cube-reachability question
covers parameterized reachability and coverability problems, and as explained
in [3], also covers the parameterized reachability problem for a generalized
model of RBN called _RBN with leaders_. Moreover, a sub-problem of cube-
reachability has already been studied for RBN in [8]. The authors show that
this sub-problem is -complete. One of the results in our paper is that the
entire cube-reachability problem is -complete, hence extending the sub-problem
considered in [8], while still retaining the same complexity upper bound.

In fact, our main result, which we call the Theorem, is a more general result.
It subsumes the above result for cube-reachability and allows for more complex
parameterized analysis of RBN. The Theorem roughly states that any boolean
combination of atoms can be evaluated in , where an atom is a finite union of
cubes or the reachability set of a finite union of cubes (i.e.
$\mathit{post}^{*}$ or $\mathit{pre}^{*}$). To prove the Theorem, we first
consider the so called _symbolic graph_ of a RBN ([8], Section 5). We prove
some structural properties about these graphs, using results from [8]. Next,
using these structural properties, we show that the set of reachable
configurations of a cube $\mathcal{C}$ can be expressed as a finite union of
cubes, each having a norm exponentially bounded in the size of the given RBN
and $\mathcal{C}$. This result then allows us to give an on-the-fly
exploration algorithm for proving the Theorem.

We believe that the Theorem and the results leading to it that we have proven
in this paper have further applications to problems concerning RBN. To justify
this claim, we provide two applications. First, we show that the almost-sure
coverability problem for RBN is -complete, thereby closing a complexity gap
from a previous paper ([3], Section 5.3). Second, we define a computation
model using RBN, called RBN protocols, which is similar in spirit to the
population protocols model [1, 2]. We characterize precisely the set of
predicates that can be computed using RBN protocols. This result generalizes
the corresponding result for IO protocols, which are a sub-class of population
protocols that can be simulated by RBN protocols, as shown in ([3], Section
6.2).

Finally, by the reduction given in ([3], Section 4.2), our results on cube-
reachability and almost-sure coverability can be transferred to another model
of distributed computation called asynchronous shared memory systems (ASMS),
giving a -completeness result for both of these problems. This solves an open
problem from ([6], Section 6).

To summarize, we have shown that many important parameterized problems of RBN
can be solved in PSPACE, that the sub-problem of the cube-reachability problem
defined in [8] can be generalized while retaining the same upper bounds, and
that the almost-sure coverability problems for RBN and ASMS are -complete,
thereby solving open problems from [3, 6]. We believe that our other results
might be of independent interest, and we provide an application by introducing
RBN protocols and characterizing the set of predicates that they can compute.

The paper is organized as follows. Section 2 contains preliminaries, including
the definition of RBN. Section 3 defines the symbolic graph of a RBN, and
proves the properties of this graph needed to derive our main result. Section
4 contains the main result that a host of parameterized problems over cubes,
including cube-reachability, is -complete for RBN. Finally, Sections 5 and 6
give applications of our main results: Section 5 solves the complexity gap for
the almost-sure coverability problem, and Section 6 introduces RBN protocols
and characterizes their expressive power. Due to lack of space, full proofs of
some of the results can be found in the appendix.

##  2 Preliminaries

The definitions and notations in this section are taken from [3].

###  2.1 Multisets

A _multiset_ on a finite set $E$ is a mapping $C\colon
E\rightarrow\mathbb{N}$, i.e. for any $e\in E$, $C(e)$ denotes the number of
occurrences of element $e$ in $C$. We let $\mathbb{M}(E)$ denote the set of
all multisets on $E$. Let $\Lbag e_{1},\ldots,e_{n}\Rbag$ denote the multiset
$C$ such that $C(e)=|\\{j\mid e_{j}=e\\}|$. We sometimes write multisets using
set-like notation. For example, $\Lbag 2\cdot a,b\Rbag$ and $\Lbag a,a,b\Rbag$
denote the same multiset. Given $e\in E$, we denote by $\bm{e}$ the multiset
consisting of one occurrence of element $e$, that is $\Lbag e\Rbag$.
Operations on $\mathbb{N}$ like addition or comparison are extended to
multisets by defining them component wise on each element of $E$. Subtraction
is allowed as long as each component stays non-negative. We call
$|C|\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\sum_{e\in
E}C(e)$ the _size_ of $C$.

###  2.2 Reconfigurable Broadcast Networks

Reconfigurable broadcast networks (RBN) are networks consisting of finite-
state, anonymous agents and a communication topology which specifies for every
pair of processes, whether or not there is a communication link between them.
During a single step, a single agent can broadcast a message which is received
by all of its neighbors, after which both the agent and its neighbors change
their state according to some transition relation. Further, in between two
steps, the communication topology can change in an arbitrary manner. For the
problems that we consider in this paper, it is easier to forget the
communication topology and define the semantics of an RBN directly in terms of
collections of agents.

######  Definition 1.

A _reconfigurable broadcast network_ is a tuple
$\mathcal{R}=(Q,\Sigma,\delta)$ where $Q$ is a finite set of states, $\Sigma$
is a finite alphabet and $\delta\subseteq Q\times\left\\{!a,?a\ |\
a\in\Sigma\right\\}\times Q$ is the transition relation.

If $(p,!a,q)$ (resp. $(p,?a,q)$) is a transition in $\delta$, we will denote
it by $p\xrightarrow{!a}q$ (resp. $p\xrightarrow{?a}q$). A _configuration_ $C$
of a RBN $\mathcal{R}$ is a multiset over $Q$, which intuitively counts the
number of processes in each state. Given a letter $a\in\Sigma$ and two
configurations $C$ and $C^{\prime}$ we say that there is a _step_
$C\xrightarrow{a}C^{\prime}$ if there exists a multiset $\Lbag
t,t_{1},\ldots,t_{k}\Rbag$ of $\delta$ for some $k\geq 0$ satisfying the
following: $t=p\xrightarrow{!a}q$, each $t_{i}=p_{i}\xrightarrow{?a}q_{i}$,
$C\geq\bm{p}+\sum_{i}\bm{p_{i}}$, and
$C^{\prime}=C-\bm{p}-\sum_{i}\bm{p_{i}}+\bm{q}+\sum_{i}\bm{q_{i}}$. We
sometimes write this as $C\xrightarrow{t+t_{1},\ldots,t_{n}}C^{\prime}$ or
$C\xrightarrow{a}C^{\prime}$. Intuitively it means that a process at the state
$p$ broadcasts the message $a$ and moves to $q$, and for each $1\leq i\leq k$,
there is a process at the state $p_{i}$ which receives this message and moves
to $q_{i}$. We denote by $\xrightarrow{*}$ the reflexive and transitive
closure of the step relation. A _run_ is then a sequence of steps.

$q_{1}$$q_{2}$$q_{3}$$?a$$!b$$?b$$!a$ Figure 1: An RBN $\mathcal{R}$ with
three states.

Let $\mathcal{R}=(Q,\Sigma,\delta)$ be an RBN. Given configurations $C$ and
$C^{\prime}$, we say $C^{\prime}$ is _reachable_ from $C$ if
$C\xrightarrow{*}C^{\prime}$. We say $C^{\prime}$ is _coverable_ from $C$ if
there exists $C^{\prime\prime}$ such that $C\xrightarrow{*}C^{\prime\prime}$
and $C^{\prime\prime}\geq C^{\prime}$. The _reachability_ problem consists of
deciding, given a RBN $\mathcal{R}$ and configurations $C,C^{\prime}$, whether
$C^{\prime}$ is reachable from $C$ in $\mathcal{R}$. The _coverability_
problem consists of deciding, given a RBN $\mathcal{R}$ and configurations
$C,C^{\prime}$, whether $C^{\prime}$ is coverable from $C$ in $\mathcal{R}$.
Let $\mathcal{S}$ be a set of configurations. The _predecessor set_ of
$\mathcal{S}$ is
$\mathit{pre}^{*}(\mathcal{S})\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\\{C^{\prime}|\exists
C\in\mathcal{S}\,.\,C^{\prime}\xrightarrow{*}C\\}$, and the _successor set_ of
$\mathcal{S}$ is
$\mathit{post}^{*}(\mathcal{S})\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\\{C|\exists
C^{\prime}\in\mathcal{S}\,.\,C^{\prime}\xrightarrow{*}C\\}$.

######  Example 1.

Figure 1 illustrates a RBN $\mathcal{R}=(Q,\Sigma,\delta)$ with
$Q=\left\\{q_{1},q_{2},q_{3}\right\\}$. Configuration $\Lbag 3\cdot
q_{1}\Rbag$ can reach $\Lbag 2\cdot q_{1},q_{3}\Rbag$ in two steps. First, a
process broadcasts $a$, the two other processes receive it and move to
$q_{2}$. Then, one of the processes in $q_{2}$ broadcasts $b$ and moves to
$q_{1}$, while the other one receives $b$ and moves to $q_{3}$. Notice that
$\Lbag q_{3}\Rbag$ is only coverable from a configuration $\Lbag k\cdot
q_{1}\Rbag$ if $k\geq 3$.

###  2.3 Cubes and Counting Sets

Given a finite set $Q$, a _cube_ $\mathcal{C}$ is a subset of $\mathbb{M}(Q)$
described by a lower bound $L\colon Q\rightarrow\mathbb{N}$ and an upper bound
$U\colon Q\rightarrow\mathbb{N}\cup\\{\infty\\}$ such that
$\mathcal{C}=\\{C:L\leq C\leq U\\}$. Abusing notation, we identify the set
$\mathcal{C}$ with the pair $(L,U)$. Notice that since $U(q)$ can be $\infty$
for some state $q$, a cube can contain an infinite number of configurations.
All the results in this paper are true irrespective of whether the constants
in a given input cube are encoded in unary or binary.

A finite union of cubes $\bigcup_{i=1}^{m}(L_{i},U_{i})$ is called a _counting
constraint_ and the set of configurations $\bigcup_{i=1}^{m}\mathcal{C}_{i}$
it describes is called a _counting set_. Notice that two different counting
constraints may describe the same counting set. For example, let
$Q=\left\\{q\right\\}$ and let $(L,U)=(1,3)$, $(L^{\prime},U^{\prime})=(2,4)$,
$(L^{\prime\prime},U^{\prime\prime})=(1,4)$. The counting constraints
$(L,U)\cup(L^{\prime},U^{\prime})$ and $(L^{\prime\prime},U^{\prime\prime})$
define the same counting set. It is easy to show (see also Proposition 2 of
[12]) that counting constraints and counting sets are closed under Boolean
operations.

##### Norms.

Let $\mathcal{C}=(L,U)$ be a cube. Let $\|{\mathcal{C}}\|_{l}$ be the the sum
of the components of $L$. Let $\|{\mathcal{C}}\|_{u}$ be the sum of the finite
components of $U$ if there are any, and $0$ otherwise. The _norm_ of
$\mathcal{C}$ is the maximum of $\|{\mathcal{C}}\|_{l}$ and
$\|{\mathcal{C}}\|_{u}$, denoted by $\|{\mathcal{C}}\|$. We define the norm of
a counting constraint $\Gamma=\bigcup_{i=1}^{m}\mathcal{C}_{i}$ as
$\|{\Gamma}\|\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\displaystyle\max_{i\in[1,m]}\\{\|{\mathcal{C}_{i}}\|\\}.$
The norm of a counting set $\mathcal{S}$ is the smallest norm of a counting
constraint representing $\mathcal{S}$, that is,
$\|{\mathcal{S}}\|\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\displaystyle\min_{\mathcal{S}=\llbracket{\Gamma}\rrbracket}\\{\|{\Gamma}\|\\}$.
Proposition 5 of [12] entails the following results for the norms of the
union, intersection and complement.

######  Proposition 1.

Let $\mathcal{S}_{1},\mathcal{S}_{2}$ be counting sets. The norms of the
union, intersection and complement satisfy:
$\|{\mathcal{S}_{1}\cup\mathcal{S}_{2}}\|\leq\max\\{\|{\mathcal{S}_{1}}\|,\|{\mathcal{S}_{2}}\|\\},\|{\mathcal{S}_{1}\cap\mathcal{S}_{2}}\|\leq\|{\mathcal{S}_{1}}\|+\|{\mathcal{S}_{2}}\|$,
and $\|{\overline{\mathcal{S}_{1}}}\|\leq|Q|\cdot\|{\mathcal{S}_{1}}\|+|Q|.$

##### Reachability.

The reachability problem can be generalized to the _cube-reachability_ problem
which consists of deciding, given an RBN $\mathcal{R}$ and two cubes
$\mathcal{C},\mathcal{C}^{\prime}$, whether there exists configurations
$C\in\mathcal{C}$ and $C^{\prime}\in\mathcal{C}^{\prime}$ such that
$C^{\prime}$ is reachable from $C$ in $\mathcal{R}$. If this is the case, we
say $\mathcal{C}^{\prime}$ is reachable from $\mathcal{C}$. The _counting set-
reachability_ problem asks, given an RBN $\mathcal{R}$ and two counting sets
$\mathcal{S},\mathcal{S}^{\prime}$, whether there exists cubes
$\mathcal{C}\in\mathcal{S}$ and $\mathcal{C}^{\prime}\in\mathcal{S}^{\prime}$
such that $\mathcal{C}^{\prime}$ is reachable from $\mathcal{C}$ in
$\mathcal{R}$. We define _cube-coverability_ and _counting set-coverability_
in an analoguous way.

######  Remark 1.

In the paper [8], the authors define a sub-class of the cube-reachability
problem, which is called the _unbounded initial cube-reachability_ problem in
[3]. More precisely, the sub-class considered in [8] is the following: We are
given an RBN and two cubes $\mathcal{C}=(L,U)$ and
$\mathcal{C}^{\prime}=(L^{\prime},U^{\prime})$ with the special property that
$L(q)=0$ and $U(q)\in\\{0,\infty\\}$ for every state $q$. We then have to
decide if $\mathcal{C}$ can reach $\mathcal{C}^{\prime}$. This problem was
shown to be -complete ([8], Theorem 5.5), whenever the numbers in the input
are given in unary. As we shall show later in this paper, the cube-
reachability problem itself is in , even when the input numbers are encoded in
binary, thereby generalizing the upper bound results given in that paper.

##  3 Reachability sets of counting sets

In this section, we set the stage for proving the main result of this paper.
This main result is given in two stages: First, we show that given a RBN with
state set $Q$ and a counting set $\mathcal{S}$, the set
$\mathit{post}^{*}(\mathcal{S})$ is also a counting set and
$\|{\mathit{post}^{*}(\mathcal{S})}\|\leq 2^{p(\|{\mathcal{S}}\|\cdot|Q|)}$
where $p$ is some fixed polynomial. Using this, we then prove that a host of
cube-parameterized problems for RBN can be solved in .

The rest of this section is organized as follows: To prove the first result,
we recall the notion of a _symbolic graph_ of a RBN from [8]. In the symbolic
graph, each node is a _symbolic configuration_ of the RBN, which intuitively
represents an infinite set of configurations in which the number of agents is
fixed in some states, and arbitrarily big in the others. Next, by exploiting
the special structure of the symbolic graph, we prove some properties which
allow us to show that whenever two nodes in this graph are reachable, they are
reachable by a path having a special structure. Finally, using these
properties and the connection between symbolic configurations and
configurations of the RBN, we prove the desired first result. Once we have
shown the first result, we then show how the Theorem can be obtained from it.

Throughout this section, we fix an RBN $\mathcal{R}=(Q,\Sigma,\delta)$.

###  3.1 Symbolic graph

In this subsection, we recall the notion of a _symbolic graph_ of an RBN from
[8]. Here, for the sake of convenience, we define it in a slightly different
way, but the underlying notion is the same as [8]. Throughout this subsection
and the next, we fix a number $k\in\mathbb{N}$.

The _symbolic graph of index_ $k$ associated with the RBN $\mathcal{R}$ is an
edge-labelled graph $\mathcal{G}_{k}=(N,E,L)$ where $N=\mathbb{M}_{k}(Q)\times
2^{Q}$ is the set of nodes. Here $\mathbb{M}_{k}(Q)$ denotes the set of
multisets on $Q$ of size at most $k$. $E$ is the set of edges and
$L:E\to\Sigma$ is the labelling function. Each node of $\mathcal{G}_{k}$ is
also called a _symbolic configuration_. Intuitively, in each symbolic
configuration $(v,S)$, the multiset $v$ (called the _concrete part_) is used
to keep track of a fixed set of at most $k$ agents, and the subset $S$ (called
the _abstract part_) is used to keep track of the _support_ of the remaining
agents.

Let $\theta=(v,S)$ and $\theta^{\prime}=(v^{\prime},S^{\prime})$ be two
symbolic configurations. There is an edge labelled by $a$ between $\theta$ and
$\theta^{\prime}$ if and only if the following is satisfied: There exists a
transition $(q,!a,q^{\prime})\in\delta$ such that at least one of the
following two conditions holds

  * •

(Broadcast from $v$) There exists a multiset of transitions
$\Lbag(p_{1},?a,p_{1}^{\prime}),\dots,\allowbreak(p_{l},?a,p_{l}^{\prime})\Rbag$
such that
$v^{\prime}=v-\sum_{i}\bm{p_{i}}+\sum_{i}\bm{p_{i}^{\prime}}-\bm{q}+\bm{q^{\prime}}$,
and for each $q_{s}\in Q$:

    * –

If $q_{s}\in S^{\prime}\setminus S$ then there exists $q^{\prime}_{s}\in S$
and $(q^{\prime}_{s},?a,q_{s})\in R$,

    * –

If $q_{s}\in S\setminus S^{\prime}$ then there exists $q^{\prime}_{s}\in
S^{\prime}$ and $(q_{s},?a,q^{\prime}_{s})\in R$.

  * •

(Broadcast from $S$) There exists a multiset of transitions
$\Lbag(p_{1},?a,p_{1}^{\prime}),\dots,\allowbreak(p_{l},?a,p_{l}^{\prime})\Rbag$
such that $v^{\prime}=v-\sum_{i}\bm{p_{i}}+\sum_{i}\bm{p_{i}^{\prime}}$, $q\in
S,q^{\prime}\in S^{\prime}$, and for each $q_{s}\in
Q\setminus\\{q,q^{\prime}\\}$:

    * –

if $q_{s}\in S^{\prime}\setminus S$ then there exists $q^{\prime}_{s}\in S$
and $(q^{\prime}_{s},?a,q_{s})\in R$,

    * –

if $q_{s}\in S\setminus S^{\prime}$ then there exists $q^{\prime}_{s}\in
S^{\prime}$ and $(q_{s},?a,q^{\prime}_{s})\in R$.

An edge labelled by $a$ between $\theta$ and $\theta^{\prime}$ is denoted by
$\theta\rightsquigarrow^{a}_{\mathcal{G}_{k}}\theta^{\prime}$. The relation
$\rightsquigarrow^{*}_{\mathcal{G}_{k}}$ is the reflexive and transitive
closure of
$\rightsquigarrow_{\mathcal{G}_{k}}:=\cup_{a\in\Sigma}\rightsquigarrow^{a}_{\mathcal{G}_{k}}$.
Whenever the index $k$ is clear, we will drop the subscript $\mathcal{G}_{k}$
from these notations.

######  Remark 2.

Let $\theta=(v,S),\theta^{\prime}=(v^{\prime},S^{\prime})$ be two symbolic
configurations. By construction, $\theta$ can only reach $\theta^{\prime}$ if
$|v|=|v^{\prime}|$.

To give an intuition behind the edges in $\mathcal{G}_{k}$, recall the
intuition that in a symbolic configuration, the concrete part is used to keep
track of a fixed set of at most $k$ processes and the abstract part is used to
keep track of the support of the remaining processes. The first condition for
the existence of an edge asserts the following: 1) In the concrete part, some
process broadcasts the message $a$ and some subset of processes receive $a$,
2) In the abstract part, any new state added or any old state deleted comes
because of receiving $a$. The second condition asserts exactly the same,
except we now require the process broadcasting the message $a$ to be from the
abstract part.

The symbolic graph of index $k$ can be thought of as an abstraction of the set
of configurations of $\mathcal{R}$, where only a fixed number of processes are
explicitly represented and the rest are abstracted by means of their support
alone. To formalize this, given a symbolic configuration $\theta=(v,S)$, we
let ${\llbracket\theta\rrbracket}$ denote the following (infinite) set of
configurations: $C\in{\llbracket\theta\rrbracket}$ if and only if $C(q)=v(q)$
for $q\notin S$ and $C(q)\geq v(q)$ for $q\in S$.

$\left\\{q_{1}\right\\}$$\left\\{q_{1},q_{2}\right\\}$$\left\\{q_{1},q_{2},q_{3}\right\\}$$\left\\{q_{2}\right\\}$$\left\\{q_{1},q_{3}\right\\}$$\left\\{q_{2},q_{3}\right\\}$$\left\\{q_{3}\right\\}$$a$$a$$b$$b$$b$$b$$a,b$$b$$b$$a$$a$$b$$b$
Figure 2: Symbolic graph $\mathcal{G}_{0}$ of index $0$ of the RBN of Example
1.

######  Example 2.

The symbolic graph $\mathcal{G}_{0}$ of index $0$ of the RBN of Example 1 is
illustrated in Figure 2. At this index, the graph only keeps track of a subset
$S\subseteq Q$, and the edges correspond to broadcasts from $S$. Consider the
edges from $\left\\{q_{1}\right\\}$. The self-loop corresponds to a broadcast
of $a$ that is not received. The edge to $\left\\{q_{1},q_{2}\right\\}$
corresponds to a broadcast of $a$ received by at least one process in $q_{1}$.
There is no edge from $\left\\{q_{3}\right\\}$ because there is no broadcast
transition from $q_{3}$.

We then have the following lemma, which asserts that runs between two
configurations in an RBN induce corresponding runs in the symbolic graph. The
proof of the lemma is easily obtained from the definition of the symbolic
graph.

######  Lemma 1 ().

Let $C,C^{\prime}$ be two configurations of $\mathcal{R}$ such that
$C\xrightarrow{a}C^{\prime}$. Then, for every $\theta$ such that
$C\in{\llbracket\theta\rrbracket}$, there exists $\theta^{\prime}$ such that
$C^{\prime}\in{\llbracket\theta^{\prime}\rrbracket}$ and
$\theta\rightsquigarrow^{a}\theta^{\prime}$.

###  3.2 Properties of the symbolic graph

In this subsection, we prove some properties of the symbolic graph (of any
index $k$). The first two properties that we prove exhibit some structural
properties on the paths of the symbolic graph. The next two properties relate
paths over the symbolic graph to runs over the configurations of the given
RBN. These four properties will ultimately lead us to prove our two main
contributions in the next section.

#### First property: Monotonicity.

Let $k\in\mathbb{N}$ and let $\mathcal{G}_{k}$ be the symbolic graph of index
$k$ associated with $\mathcal{R}$. The first key property of $\mathcal{G}_{k}$
is the following property, which we call _monotonicity_.

######  Proposition 2.

Let $\theta=(v,S)$ and $\theta^{\prime}=(v^{\prime},S^{\prime})$ be symbolic
configurations of $\mathcal{G}_{k}$. Then the following are true:

  * •

If $Z\subseteq S$ and $\theta\rightsquigarrow^{a}\theta^{\prime}$, then
$(v,S)\rightsquigarrow^{a}(v^{\prime},Z\cup S^{\prime})$.

  * •

If $Z\subseteq Q$ and $\theta\rightsquigarrow^{a}\theta^{\prime}$, then
$(v,Z\cup S)\rightsquigarrow^{a}(v^{\prime},Z\cup S^{\prime})$.

###### Proof.

The two points follow immediately from the definition of
$\rightsquigarrow^{a}$. ∎

#### Second property: Normal Form.

To state the second property, we first need a small definition.

######  Definition 2.

Let $(v_{0},S_{0})\rightsquigarrow\cdots\rightsquigarrow(v_{m},S_{m})$ a path
in $\mathcal{G}_{k}$. A pair of indices $0\leq i<j\leq m$ is called a _bad
pair_ if $(S_{i}\setminus S_{i+1})\cap S_{j}\neq\emptyset$. A path is said to
be in _normal form_ if it contains no bad pairs, i.e., for all $0\leq i<m$ and
any $j>i$, $(S_{i}\setminus S_{i+1})\cap S_{j}=\emptyset$.

Intuitively, a path is in normal form if during each step, the states that
disappear from the abstract part never reappear again. The following lemma
asserts that whenever there is a path between two symbolic configurations,
then there is a path between them that is in normal form.

######  Lemma 2 ().

Let $\theta,\theta^{\prime}$ be symbolic configurations of $\mathcal{G}_{k}$
such that there is a path between $\theta$ and $\theta^{\prime}$ of length
$m$. Then, there is a path in normal form between $\theta$ and
$\theta^{\prime}$ of length $m$.

###### Proof Sketch.

Let
$\theta=\theta_{0}\rightsquigarrow\theta_{1}\rightsquigarrow\theta_{2}\rightsquigarrow\dots\theta_{m-1}\rightsquigarrow\theta_{m}=\theta^{\prime}$
be the path between $\theta$ and $\theta^{\prime}$. We proceed by induction on
$m$. The claim is clearly true for $m=0$. Suppose $m>0$ and the claim is true
for $m-1$. By induction hypothesis, we can assume that the path
$\theta_{0}\rightsquigarrow\theta_{1}\rightsquigarrow\dots\rightsquigarrow\theta_{m-1}$
is already in normal form.

Let each $\theta_{i}=(v_{i},S_{i})$. Let $l$ be the number of bad pairs in the
path between $\theta_{0}$ and $\theta_{m}$. If $l=0$, then the path is already
in normal form and we are done. Suppose $l>0$ and let $(w,w^{\prime})$ be a
bad pair. Since the path between $\theta_{0}$ and $\theta_{m-1}$ is already in
normal form, it has to be the case that $w^{\prime}=m$. Hence, we have
$Z:=(S_{w}\setminus S_{w+1})\cap S_{m}\neq\emptyset$.

By Proposition 2, the following is a valid path:
$(v_{w},S_{w})\rightsquigarrow(v_{w+1},S_{w+1}\cup
Z)\rightsquigarrow(v_{w+2},S_{w+2}\cup Z)\dots(v_{m-1},S_{m-1}\cup
Z)\rightsquigarrow(v_{m},S_{m}\cup Z)=(v_{m},S_{m})$. Let
$\theta^{\prime}_{j}:=\theta_{j}$ if $j\leq w$ and $(v_{j},S_{j}\cup Z)$
otherwise. Hence, we get a path
$\theta^{\prime}_{0}\rightsquigarrow\theta^{\prime}_{1}\rightsquigarrow\dots\theta^{\prime}_{m-1}\rightsquigarrow\theta^{\prime}_{m}$.

Let each $\theta^{\prime}_{e}=(v_{e}^{\prime},S_{e}^{\prime})$ and let $0\leq
i<j\leq m-1$. By a case analysis on where $i$ and $j$ are relative to the
index $w$, we can prove that $(S_{i}^{\prime}\setminus S_{i+1}^{\prime})\cap
S_{j}^{\prime}=\emptyset$. Having proved this, it is then clear by
construction, that this new path from $\theta^{\prime}_{0}:=\theta_{0}$ to
$\theta^{\prime}_{m}:=\theta_{m}$ has at most $l-1$ bad pairs only. Hence, we
now have a path from $\theta_{0}$ to $\theta_{m}$ such that the prefix of
length $m-1$ is in normal form and the number of bad pairs has been strictly
reduced to $l-1$. Repeatedly applying this procedure leads to a path in normal
form between $\theta_{0}$ and $\theta_{m}$. ∎

#### Third property: Refinement.

Before we state the third property, we need a small definition. Recall that,
given a symbolic configuration $\theta=(v,S)$, the set
${\llbracket\theta\rrbracket}$ denotes the set of configurations $C$ such that
$C(q)=v(q)$ if $q\notin S$ and $C(q)\geq v(q)$ otherwise. The following
definition refines the set ${\llbracket\theta\rrbracket}$.

######  Definition 3.

Given a symbolic configuration $\theta=(v,S)$ and a number $N\in\mathbb{N}$,
let ${\llbracket\theta\rrbracket}_{N}$ denote the set of configurations $C$
such that $C(q)=v(q)$ if $q\notin S$ and $C(q)\geq v(q)+N$ otherwise. Note
that ${\llbracket\theta\rrbracket}={\llbracket\theta\rrbracket}_{0}$.

This definition along with the above two properties now enable us to prove the
third property. It roughly states that if a symbolic configuration
$\theta^{\prime}$ can be reached from another symbolic configuration $\theta$,
then there is a “small” $N$ such that any configuration in
${\llbracket\theta^{\prime}\rrbracket}_{N}$ can be reached from some
configuration in ${\llbracket\theta\rrbracket}$.

######  Theorem 3.1 ().

Let $\theta,\theta^{\prime}$ be symbolic configurations of $\mathcal{G}_{k}$
such that $\theta\rightsquigarrow^{*}\theta^{\prime}$. Then there exists
$N\leq k\times(2k)^{|Q|}\times(|Q|+1)^{|Q|+1}+1$ such that for all
$C^{\prime}\in{\llbracket\theta^{\prime}\rrbracket}_{N}$, there exists
$C\in{\llbracket\theta\rrbracket}$ such that $C\xrightarrow{*}C^{\prime}$.

###### Proof Sketch.

Suppose $\theta\rightsquigarrow^{*}\theta^{\prime}$. If the length of the path
is 0, then there is nothing to prove. Hence, we restrict ourselves to the case
when the length of the path is bigger than 0. By Lemma 2, there is a path in
normal from from $\theta$ to $\theta^{\prime}$ (say)
$\theta=\theta_{0}\rightsquigarrow\theta_{1}\rightsquigarrow\theta_{2}\dots\theta_{m-1}\rightsquigarrow\theta_{m}=\theta^{\prime}$
with each $\theta_{i}:=(v_{i},S_{i})$.

Let $N_{0}=0$ and let $N_{i}=(N_{i-1}+1)\cdot(|S_{i-1}\setminus S_{i}|+1)$ for
every $1\leq i\leq m$. In Lemma 5.3 of [8] (more precisely in its proof, in
Lemma 6 of the long version [9]), the following fact has been proved:

> For every $1\leq i\leq m$ and for every
> $C^{\prime}\in{\llbracket\theta_{i}\rrbracket}_{N_{i}+1}$, there exists
> $C\in{\llbracket\theta_{i-1}\rrbracket}_{N_{i-1}+1}$ such that
> $C\xrightarrow{*}C^{\prime}$.

This immediately proves that for all
$C^{\prime}\in{\llbracket\theta^{\prime}\rrbracket}_{N_{m}+1}$, there exists
$C\in{\llbracket\theta\rrbracket}$ such that $C\xrightarrow{*}C^{\prime}$. If
we prove $N_{m}\leq k\times(2k)^{|Q|}\times(|Q|+1)^{|Q|+1}$, then the proof of
the theorem will be complete.

Notice that if $(v,\emptyset)\rightsquigarrow(v^{\prime},S^{\prime})$ is an
edge in $\mathcal{G}_{k}$ then $S^{\prime}=\emptyset$. This fact, along with
the definition of a path in normal form, allows us to easily conclude that the
number of indices $i$ such that $|S_{i-1}\setminus S_{i}|>0$ is at most $|Q|$.
It then follows that except for at most $|Q|$ indices, each index $N_{i}$ is
obtained from $N_{i-1}$ by simply adding 1 and in the remaining indices,
$N_{i}$ is obtained from $N_{i-1}$ by adding 1 and then multiplying by a
number which is at most $|Q|+1$. Using this, we can deduce that the maximum
value for $N_{m}$ is at most $(m-|Q|+1)|Q|(|Q|+1)^{|Q|}$. Since $m$ is itself
the length of the path between $\theta_{0}$ and $\theta_{m}$, $m$ is upper
bounded by the number of symbolic configurations in $\mathcal{G}_{k}$ which is
at most $k\times k^{|Q|}\times 2^{|Q|}$. Overall we get that $N_{m}\leq
k\times(2k)^{|Q|}\times(|Q|+1)^{|Q|+1}$. ∎

######  Remark 3.

A similar result was proved in Lemma 5.3 of [8], but there it was just stated
that there exists an $N$ satisfying this property. Moreover from the proof of
that lemma, only a doubly exponential bound on $N$ could be inferred.

#### Fourth property: Compatibility.

To describe the fourth property, we need the following notion of order on
configurations, _relative_ to a given symbolic configuration.

######  Definition 4.

Let $\theta=(v,S)$ be a symbolic configuration, and let $C,C^{\prime}$ be two
configurations of $\mathcal{R}$. We define an order $\preceq_{\theta}$ such
that $C\preceq_{\theta}C^{\prime}$ if and only if
$C,C^{\prime}\in[\\![\theta]\\!]$, and $\forall q\in S$, $C(q)\leq
C^{\prime}(q)$.

This definition enables us to state our next property, which we dub
_compatibility_. It intuitively says that the order that we have defined is,
in some sense, compatible with the edges of the symbolic configurations.

######  Lemma 3.

Let $\theta$ be a symbolic configuration of $\mathcal{G}_{k}$, and let
$C,C^{\prime}$ be two configurations of $\mathcal{R}$. If
$C\in[\\![\theta]\\!]$ and $C\xrightarrow{*}C^{\prime}$, then there exists a
symbolic configuration $\theta^{\prime}$ such that 1)
$C^{\prime}\in[\\![\theta^{\prime}]\\!]$, 2)
$\theta\rightsquigarrow^{*}\theta^{\prime}$ and 3) for all $C^{\prime}_{1}$
such that $C^{\prime}_{1}\succeq_{\theta^{\prime}}C^{\prime}$, there exists
$C_{1}\in[\\![\theta]\\!]$ such that $C_{1}\xrightarrow{*}C^{\prime}_{1}$.

###### Proof.

Let $\theta$ be a symbolic configuration and $C,C^{\prime}$ be configurations
such that $C\in[\\![\theta]\\!]$ and $C\xrightarrow{*}C^{\prime}$. Let
$C=C_{0}\xrightarrow{}\cdots\xrightarrow{}C_{m-1}\xrightarrow{}C_{m}=C^{\prime}$
denote the run between $C$ and $C^{\prime}$. We prove the property by
induction on $m$. For $m=0$, we have $C=C^{\prime}$. The property is easily
seen to hold with $\theta^{\prime}=\theta$.

Suppose now that $m\geq 1$, and that the property holds for all $n\leq m$. By
induction hypothesis, for the configuration $C_{m-1}$, there exists a symbolic
configuration $\theta_{m-1}$ satisfying the property, in particular
$\theta\rightsquigarrow^{*}\theta_{m-1}$. Since $C_{m-1}\xrightarrow{a}C_{m}$
for some $a\in\Sigma$, by Lemma 1, there exists a symbolic configuration
$\theta_{m}$ such that $C_{m}\in[\\![\theta_{m}]\\!]$, and
$\theta_{m-1}\rightsquigarrow^{a}\theta_{m}$. Using
$\theta\rightsquigarrow^{*}\theta_{m-1}$, we obtain that
$\theta\rightsquigarrow^{*}\theta_{m}$.

Let $\theta_{m-1}=(v_{m-1},S_{m-1})$ and $\theta_{m}=(v_{m},S_{m})$. Let
$C^{\prime}_{m}\in[\\![\theta_{m}]\\!]$ be such that
$C^{\prime}_{m}\succeq_{\theta_{m}}C_{m}$. We will construct a configuration
$C^{\prime}_{m-1}\in[\\![\theta_{m-1}]\\!]$ such that
$C^{\prime}_{m-1}\succeq_{\theta_{m-1}}C_{m-1}$ and
$C^{\prime}_{m-1}\xrightarrow{*}C^{\prime}_{m}$. If we construct such a
configuration, then by induction hypothesis, there is a
$C_{1}\in[\\![\theta]\\!]$ such that
$C_{1}\xrightarrow{*}C^{\prime}_{m-1}\xrightarrow{*}C^{\prime}_{m}$, which
will conclude the proof.

Let $C^{\prime}_{m-1}(q)=C_{m-1}(q)$ for all $q\not\in S_{m-1}$. To define
$C^{\prime}_{m-1}$ on $S_{m-1}$, we first define a mapping pred from states in
$S_{m}$ to states of $S_{m-1}\cup\overline{S_{m-1}}=Q$ as follows. Given
$q^{\prime}\in S_{m}$:

  * •

If $q^{\prime}\in S_{m-1}$, $\emph{pred}(q^{\prime})=q^{\prime}$;

  * •

If $q^{\prime}\not\in S_{m-1}$, by definition of edges in the symbolic graph,
there exists $q\in S_{m-1}$ such that $(q,?a,q^{\prime})$ is a transition.
Then $\emph{pred}(q^{\prime})=q$ for one (arbitrary but fixed) such $q$.

By definition, $C^{\prime}_{m}(q)=C_{m}(q)$ for all $q\not\in S_{m}$. For all
$q\in S_{m}$, let $n_{q}=C^{\prime}_{m}(q)-C_{m}(q)$. Intuitively, we want to
place these $n_{q}$ processes in the right places of $C^{\prime}_{m-1}$ so
that $C^{\prime}_{m-1}\xrightarrow{}C^{\prime}_{m}$. For all $q\in S_{m-1}$,
let $C^{\prime}_{m-1}(q)=C_{m-1}(q)+\sum_{q^{\prime}\in
S_{m},\emph{pred}(q^{\prime})=q}n_{q^{\prime}}$. By definition,
$C^{\prime}_{m-1}\succeq_{\theta_{m-1}}C_{m-1}$. So all that remains is to
prove that $C^{\prime}_{m-1}\xrightarrow{*}C^{\prime}_{m}$.

Let $C_{m-1}\xrightarrow{t+t_{1},\dots,t_{n}}C_{m}$ where
$t=(p,!a,p^{\prime})$ and each $t_{i}=(p_{i},?a,p_{i}^{\prime})$. If we let
$S_{m}\setminus S_{m-1}=\\{q_{1}^{\prime},\dots,q_{w}^{\prime}\\}$, then by
definition there is a transition
$t_{i}^{\prime}:=(pred(q_{i}^{\prime}),?a,q_{i}^{\prime})$ for each $i$.
Additionally, $C^{\prime}_{m-1}(pred(q_{i}^{\prime}))\geq
C_{m-1}(pred(q_{i}^{\prime}))+n_{q_{i}^{\prime}}$. This allows us to do
$C^{\prime}_{m-1}\xrightarrow{t+t_{1},\dots,t_{n},n_{q_{1}^{\prime}}\cdot
t_{1}^{\prime},n_{q_{2}^{\prime}}\cdot
t_{2}^{\prime},\dots,n_{q_{w}^{\prime}}\cdot t_{w}^{\prime}}C^{\prime}_{m}$,
which concludes the proof.

∎

##  4 The Theorem

In this section, we prove our two main contributions. First, we show that
given a cube $\mathcal{C}$, $\mathit{post}^{*}(\mathcal{C})$ is a counting set
of bounded size. Using this, we show our main result: any boolean combination
of atoms can be evaluated in , where an atom is a counting set or the
reachability set of a counting set. We call this the _Theorem_. The intuition
behind the Theorem is that the norms of the counting sets obtained by such
combinations are “small”, and so we only need to examine small configurations
to verify them, thus yielding a algorithm for checking correctness. In
particular, the Theorem will show that the cube-reachability problem is in .
We fix an arbitrary RBN $\mathcal{R}=(Q,\Sigma,\delta)$ for the rest of the
section.

We start by drawing links between cubes and symbolic configurations.

  * •

Given a symbolic configuration $\theta=(v,S)$, we let $\mathcal{C}_{\theta}$
be the cube $(L,U)$ where $L=v$, and $U(q)=v(q)$ if $q\notin S$ and
$U(q)=\infty$ otherwise. Then $\mathcal{C}_{\theta}=[\\![\theta]\\!]$.

  * •

Given a cube $\mathcal{C}=(L,U)$, we define $\Delta_{\mathcal{C}}$ to be the
set of symbolic configurations $\theta=(v,S)$ with $S=\left\\{q\ |\
U(q)=\infty\right\\}$ and $L(q)\leq v(q)\leq U(q)$ if $q\notin S$ and
$v(q)=L(q)$ otherwise. Then $[\\![\Delta_{\mathcal{C}}]\\!]=\mathcal{C}$.

Notice that the set $\Delta_{\mathcal{C}}$ is included in the symbolic graph
of index $2\|{\mathcal{C}}\|$. Indeed, if $\mathcal{C}=(L,U)$ and
$(v,S)\in\Delta_{\mathcal{C}}$, then $|v|\leq|L|+|U_{f}|$ where $U_{f}(q)=0$
if $U(q)=\infty$ and $U_{f}(q)=U(q)$ otherwise. Since
$\|{\mathcal{C}}\|=\max(|L|,|U_{f}|)$, we have the desired result. By Remark
2, we know that symbolic configurations in the graph of index
$2\|{\mathcal{C}}\|$ can only reach symbolic configurations which are also in
the graph of index $2\|{\mathcal{C}}\|$.

######  Lemma 4.

Given a cube $\mathcal{C}$, the sets $\Delta_{\mathcal{C}}$ and
$\mathit{post}^{*}(\Delta_{\mathcal{C}})$ are included in the symbolic graph
of index $2\|{\mathcal{C}}\|$.

There are only a finite number of symbolic configurations in the graph of a
given index. Therefore $\mathit{post}^{*}(\Delta_{\mathcal{C}})$ is a finite
set of symbolic configurations $\theta$. It follows that
$[\\![\mathit{post}^{*}(\Delta_{\mathcal{C}})]\\!]$ is the finite union of the
cubes $\mathcal{C}_{\theta}$, and thus a counting set.

Unfortunately, it is in general not the case that
$\mathit{post}^{*}(\mathcal{C})=[\\![\mathit{post}^{*}(\Delta_{\mathcal{C}})]\\!]$,
which would close our argument. However, we will show that for each symbolic
configuration $\theta$ in $\mathit{post}^{*}(\Delta_{\mathcal{C}})$, there is
a counting set $\mathcal{S}_{\theta}\subseteq[\\![\theta]\\!]$ such that the
finite union of these counting sets is equal to
$\mathit{post}^{*}(\mathcal{C})$. This will then show our first important
result, namely that the reachability set of a counting set is also a counting
set with “small” norm.

######  Theorem 4.1.

Let $\mathcal{C}$ be a cube. color=green!30]how detailed do we want this
bound? Then $\mathit{post}^{*}(\mathcal{C})$ is a counting set and

$\|{\mathit{post}^{*}(\mathcal{C})}\|\in
O((\|{\mathcal{C}}\|\cdot|Q|)^{|Q|+2})$

The same holds for $\mathit{pre}^{*}$ by using the given RBN with reversed
transitions.

###### Proof.

We start by defining a counting set $\mathcal{M}$ of configurations, which we
will then prove to be equal to
$\mathit{post}^{*}(\mathcal{C})$.color=blue!30]Check my
changescolor=green!30]done, some typos corrected Given a symbolic
configuration $\theta$ of $\mathit{post}^{*}(\Delta_{\mathcal{C}})$, we define
the set $\min(\theta,\mathcal{C})$ to be the set of configurations
$C\in[\\![\theta]\\!]$ such that $C$ is minimal for the order
$\preceq_{\theta}$ over the configurations of
$\mathit{post}^{*}(\mathcal{C})$, i.e.

$\min(\theta,\mathcal{C})=\min_{\preceq_{\theta}}\left\\{C\in[\\![\theta]\\!]\
|\ C\in\mathit{post}^{*}(\mathcal{C})\right\\}$

We can now define $\mathcal{M}$ to be the following set

$\mathcal{M}=\bigcup_{\theta\in\mathit{post}^{*}(\Delta_{\mathcal{C}})}\
\bigcup_{C\in\min(\theta,\mathcal{C})}\mathcal{C}_{C}^{\theta},$

where $\mathcal{C}_{C}^{\theta}$ is the cube $\mathcal{C}_{(C,S)}$ for $S$
such that $\theta=(v,S)$. Since $\mathcal{M}$ is a finite union of cubes, it
is a counting set.

We show that $\mathit{post}^{*}(\mathcal{C})\subseteq\mathcal{M}$. Let
$C\in\mathit{post}^{*}(\mathcal{C})$. There exists $C_{0}\in\mathcal{C}$ such
that $C_{0}\xrightarrow{*}C$, and there exists
$\theta_{0}\in\Delta_{\mathcal{C}}$ such that $C_{0}\in[\\![\theta_{0}]\\!]$.
Applying Lemma 1, we obtain the existence of
$\theta\in\mathit{post}^{*}(\theta_{0})\subseteq\mathit{post}^{*}(\Delta_{\mathcal{C}})$
such that $C\in[\\![\theta]\\!]$. Now, there exists a configuration
$C^{\prime}\in\min(\theta,\mathcal{C})$ such that
$C^{\prime}\preceq_{\theta}C$. By definition of
$\mathcal{C}_{C^{\prime}}^{\theta}$, $C$ is in
$\mathcal{C}_{C^{\prime}}^{\theta}$ and thus in $\mathcal{M}$.

Now we show that $\mathcal{M}\subseteq\mathit{post}^{*}(\mathcal{C})$. Let
$C\in\mathcal{M}$. By definition, there must be a symbolic configuration
$\theta\in\mathit{post}^{*}(\Delta_{\mathcal{C}})$ and a configuration
$C^{\prime}\in\mathit{post}^{*}(\mathcal{C})$ such that
$C^{\prime}\preceq_{\theta}C$. By the Compatibility Lemma (Lemma 3), $C$ is in
$\mathit{post}^{*}(\mathcal{C})$ as well.

All that remains is to bound the norm of $\mathcal{M}$. To do this, let
$\theta=(v,S)\in\mathit{post}^{*}(\Delta_{\mathcal{C}})$ and let
$C\in\min(\theta,\mathcal{C})$. If we bound the norm of
$\mathcal{C}_{C}^{\theta}$ by the desired quantity, then the proof will be
complete. Noticing that $\|{\mathcal{C}_{C}^{\theta}}\|=|C|$, it suffices to
bound $|C|$ by the desired quantity, which is what we shall do now.

By Theorem 3.1 and Lemma 4, there exists an $N\leq
2\|{\mathcal{C}}\|\times(4\|{\mathcal{C}}\|)^{|Q|}\times(|Q|+1)^{|Q|+1}$ such
that
$[\\![\mathit{post}^{*}(\Delta_{\mathcal{C}})]\\!]_{N}\subseteq\mathit{post}^{*}([\\![\Delta_{\mathcal{C}}]\\!])=\mathit{post}^{*}(\mathcal{C})$.
By definition of $C$, there must be a smallest $N^{\prime}$ such that
$C(q)\leq v(q)+N^{\prime}$ for every state $q$. If $N^{\prime}>N$, then let
$C_{N}$ be the configuration given by $C_{N}(q)=\min(C(q),v(q)+N)$. We get
that
$C_{N}\in[\\![\theta]\\!]_{N}\subseteq[\\![\mathit{post}^{*}(\Delta_{\mathcal{C}})]\\!]_{N}\subseteq\mathit{post}^{*}(\mathcal{C})$,
and so $C_{N}\preceq_{\theta}C$ and $C_{N}\in\mathit{post}^{*}(\mathcal{C})$,
which is a contradiction to the minimality of $C$. Hence $N^{\prime}\leq N$
and so $|C|\leq|v|+|Q|\cdot N$. Since $\theta=(v,S)$ is in
$\mathit{post}^{*}(\Delta_{\mathcal{C}})$, by Lemma 4, we have that $|v|\leq
2\|{\mathcal{C}}\|$. Substituting the upper bounds for $|v|$ and $N$ in the
inequality $|C|\leq|v|+|Q|\cdot N$ then gives the required upper bound for
$|C|$, thereby finishing the proof.

This result also holds for $\mathit{pre}^{*}(\mathcal{C})$. If
$\mathcal{R}=(Q,\Sigma,R)$ is the given RBN, consider the “reverse” RBN
$\mathcal{R}_{r}$, defined as $\mathcal{R}=(Q,\Sigma,R_{r})$ where $R_{r}$ has
a transition $(q,\star a,q^{\prime})$ for $\star\in\left\\{!,?\right\\}$ iff
$R_{r}$ has a transition $(q^{\prime},\star a,q)$. Notice that
$\mathcal{R}_{r}$ is still an RBN and that $\mathit{post}^{*}(\mathcal{C})$ in
$\mathcal{R}$ is equal to $\mathit{pre}^{*}(\mathcal{C})$ in
$\mathcal{R}_{r}$. ∎

Recall that counting sets are closed under boolean operations. With the above
theorem, plus the fact that counting sets are finite unions of cubes, we
obtain the following closure result.

######  Corollary 1 (Closure).

Counting sets are closed under $\mathit{post}^{*}$, $\mathit{pre}^{*}$ and
boolean operations.

We are now ready to show our main result, the Theorem. We show that there
exist algorithms to evaluate boolean combinations over counting sets and
reachability set of counting sets. This result and its proof are adapted from
a similar result for population protocols in [13].

Given a counting constraint $\Gamma$, we let $[\Gamma]$ denote the counting
set described by $\Gamma$. To state our result, we first define some “nice”
expressions.

######  Definition 5.

A _nice_ expression is any expression that is constructed by the following
syntax:

$E:=\Gamma\ |\ \mathit{post}^{*}(\Gamma)\ |\ \mathit{pre}^{*}(\Gamma)\ |\
E\cap E\ |\ E\cup E\ |\ \overline{E}$

where $\Gamma$ is any counting constraint.

If $E$ is a nice expression, then the _size_ of $E$, denoted by $|E|$, is
defined as follows:

  * •

If $E=\Gamma$ or $\mathit{post}^{*}(\Gamma)$ or $\mathit{pre}^{*}(\Gamma)$,
then $|E|=1$;

  * •

If $E=E_{1}\cup E_{2}$ or $E=E_{1}\cap E_{2}$, then $|E|=|E_{1}|+|E_{2}|$;

  * •

If $E=\overline{E_{1}}$, then $|E|=|E_{1}|+1$.

The set of configurations that is described by a nice expression $E$ can be
defined in a straightforward manner, and is denoted as $[E]$.

Notice that any nice expression $E$ is a counting constraint, and $[E]$ is a
counting set, by the Closure Corollary 1.

######  Theorem 4.2 ( Theorem).

Let $E$ be a nice expression and let $N$ be the maximum norm of the counting
constraints appearing in $E$. Then $[E]$ is a counting set of norm at most
exponential in $N,|E|$ and $|Q|$. Further, the membership and emptiness
problems for $[E]$ are in .

###### Proof.

Recall that $[E]$ is a counting set , by the Closure Corollary (Corollary 1).
The exponential bounds for the norms follow immediately from Proposition 1 and
Theorem 4.1. The membership complexity for union, intersection and complement
is easy to see. Without loss of generality it suffices to prove that
membership in $\mathit{post}^{*}(\Gamma)$ is in , where $\Gamma$ is a counting
constraint.

By Savitch’s Theorem =, so we provide a nondeterministic algorithm. Given
$(C,\Gamma)$, we want to decide whether $C\in\mathit{post}^{*}(\Gamma)$. The
algorithm first guesses a configuration $C_{0}\in\Gamma$ of the same size as
$C$, verifies that $C_{0}$ belongs to $\Gamma$, and then simply guesses an
execution starting at $C_{0}$, step by step. The algorithm stops if either the
configuration reached at some step is $C$, or if it has guessed more steps
than the number of configurations of size $|C|$. This concludes the discussion
regarding the membership complexity.

To see that checking emptiness of $E$ is in , notice that if $E$ is nonempty,
then it has an element of size at most $\|{E}\|$. We can guess such an element
$C$ in polynomial space (by representing each coefficient in binary), and
verify that $C$ is indeed in $E$ by means of the membership algorithm. ∎

This result is a powerful tool which can be used to prove that a host of
problems are in for RBN. For instance, the cube-reachability problem for cubes
$\mathcal{C}$ and $\mathcal{C}^{\prime}$ is just checking if
$\mathit{post}^{*}(\mathcal{C})\cap\mathcal{C}^{\prime}$ is empty, which by
the Theorem can be done in . Combining this with Remark 1, we obtain the
following result.

######  Theorem 4.3.

Cube-reachability is -complete for RBN.

By the reduction given in Section 4.2 of [3], this result also proves that
cube-reachability is -complete for asynchronous shared-memory systems (ASMS),
which is another model of distributed computation where agents communicate by
a shared register. Due to lack of space, we defer a discussion of this result
to the appendix.

We will demonstrate further applications of the Theorem in the next section.

##  5 Application 1: Almost-sure coverability

Having presented our Theorem and the closure property for reachability sets of
counting sets, we now provide two applications. For the first one, we consider
the _almost-sure coverability_ problem for RBN. Using our new results, we
prove that this problem is -complete.

The rest of the section is as follows: We first recall the definition of the
almost-sure coverability problem, give a characterization of it in terms of
counting sets and then prove -completeness. Throughout this section, we fix a
RBN $\mathcal{R}=(Q,\Sigma,\delta)$ with two special states
$\mathit{init},\mathit{fin}\in Q$, which will respectively be called the
initial and final states.

###  5.1 The almost-sure coverability problem

Let $\uparrow\mathit{fin}$ denote the set of all configurations $C$ of
$\mathcal{R}$ such that $C(\mathit{fin})\geq 1$. For any $k\geq 1$, we say
that the configuration $\Lbag k\cdot\mathit{init}\Rbag$ _almost-surely covers_
$\mathit{fin}$ if and only if $\mathit{post}^{*}(\Lbag
k\cdot\mathit{init}\Rbag)\subseteq\mathit{pre}^{*}(\uparrow\mathit{fin})$. The
reason behind calling this the almost-sure coverability relation is that the
definition given here is equivalent to covering the state $\mathit{fin}$ from
$\Lbag k\cdot\mathit{init}\Rbag$ with probability 1 under a probabilistic
scheduler which picks agents uniformly at random at each step.

The number $k$ is called a _cut-off_ if one of the following is true: Either,
1) for all $h\geq k$, the configuration $\Lbag h\cdot\mathit{init}\Rbag$
almost-surely covers $\mathit{fin}$, in which case $k$ is called a _positive_
cut-off; or, 2) for all $h\geq k$, the configuration $\Lbag
h\cdot\mathit{init}\Rbag$ does not almost-surely cover $\mathit{fin}$, in
which case $k$ is called a _negative_ cut-off. The following was proved in
Theorem 9 of [3].

######  Theorem 5.1.

Given an RBN with two states $\mathit{init},\mathit{fin}$, a cut-off always
exists. Whether the cut-off is positive or negative can be decided in .

Our main result of this section is that

######  Theorem 5.2.

Deciding whether the cut-off of a given RBN is positive or negative is
-complete. Moreover, a given RBN always has a cut-off which is at most
exponential in its number of states.

###  5.2 A characterization of almost-sure coverability

We now rewrite the definition of almost-sure coverability in terms of counting
sets. Let $[\mathit{init}]$ be the cube such that $L(q)=U(q)=0$ if
$q\neq\mathit{init}$ and $L(\mathit{init})=0,U(\mathit{init})=\infty$. Notice
that by definition, $\uparrow\mathit{fin}$ is a cube. We now consider the set
of configurations defined by
$\mathcal{S}:=\mathit{post}^{*}([\mathit{init}])\cap\overline{\mathit{pre}^{*}(\uparrow\mathit{fin})}$.
By our Theorem 4.2, $\mathcal{S}$ is a counting set such that the norm of
$\mathcal{S}$ is at most $2^{p(|Q|)}$ for some fixed polynomial $p$. We now
claim the following.

######  Theorem 5.3.

$\mathcal{R}$ has a positive cut-off if and only if $\mathcal{S}$ is finite.
Moreover, $|Q|\cdot|\mathcal{S}|$ is an upper bound on the size of the cut-off
for $\mathcal{R}$ and so $\mathcal{R}$ has a cut-off which is exponential in
its number of states.

###### Proof.

Let $N$ be the norm of $\mathcal{S}$. Suppose $\mathcal{S}$ is finite. If
$C\in\mathcal{S}$, then $\sum_{q\in Q}C(q)\leq|Q|\cdot N$. So, if $C$ is any
configuration of size $h>|Q|\cdot N$ such that $C\in\mathit{post}^{*}(\Lbag
h\cdot\mathit{init}\Rbag)$ then $C\in\mathit{pre}^{*}(\uparrow\mathit{fin})$.
Hence, $|Q|\cdot N$ is a positive cut-off for $\mathcal{R}$.

Suppose $\mathcal{S}$ is infinite, and let $\cup_{i}\mathcal{C}_{i}$ be a
counting constraint for $\mathcal{S}$ whose norm is $N$. Then there must exist
an index $i$ with $\mathcal{C}_{i}:=(L,U)$ and a state $p$ such that
$U(p)=\infty$. For each $h\geq N$, consider the configuration $C_{h}$ given by
$C_{h}(q)=L(q)$ if $q\neq p$ and $C_{h}(p)=h$. Notice that
$C_{h}\in\mathcal{S}$ and so
$C_{h}\in\mathit{post}^{*}([\mathit{init}])\cap\overline{\mathit{pre}^{*}(\uparrow\mathit{fin})}$.
Hence, for every $h\geq|Q|\cdot N$, we have exhibited a configuration of size
$h$, reachable from $(\Lbag h\cdot\mathit{init}\Rbag$ but from which
$\mathit{fin}$ is not coverable. Thus $N$ is a negative cut-off for
$\mathcal{R}$. ∎

######  Remark 4.

Notice that we have shown that if $\mathcal{S}$ is finite, then $\mathcal{R}$
has a positive cut-off and if $\mathcal{S}$ is infinite, then $\mathcal{R}$
has a negative cut-off. This gives an alternative proof of the fact that a
cut-off always exists for a given RBN.

###  5.3 -completeness of the almost-sure coverability problem

Because of Theorem 5.3, we now have the following result.

######  Lemma 5 ().

Deciding whether the cut-off of a given RBN is positive or negative can be
done in .

###### Proof Sketch.

By Theorem 5.3, it follows that a given RBN has a negative cut-off iff
$\mathcal{S}=\mathit{post}^{*}([\mathit{init}])\cap\overline{\mathit{pre}^{*}(\uparrow\mathit{fin})}$
is infinite. We have already seen that $\mathcal{S}$ is a counting set such
that the norm of $\mathcal{S}$ is at most $N:=2^{p(|Q|)}$ for some fixed
polynomial $p$.

Let $\cup_{i}\mathcal{C}_{i}$ be a counting constraint for $\mathcal{S}$ which
minimizes its norm and let each $\mathcal{C}_{i}=(L_{i},U_{i})$. Hence,
$L_{i}(q)\leq N$ for every state $q$. Further, $\mathcal{S}$ is infinite iff
there is an index $i$ and a state $q$ such that $U_{i}(q)=\infty$. Using these
two facts, we can then show that $\mathcal{S}$ is infinite iff there is a
state $q$ and a configuration $C\in\mathcal{S}$ such that $C(q^{\prime})\leq
N$ for every $q^{\prime}\neq q$ and $C(q)=N+1$.

Hence, to check if $\mathcal{S}$ is infinite, we just have to guess a state
$q$ and a configuration $C$ such that $C(q^{\prime})\leq N$ for every
$q^{\prime}\neq q$ and $C(q)=N+1$ and check if $C\in\mathcal{S}$. Since
guessing $C$ can be done in polynomial space (by representing every number in
binary), by the Theorem (Theorem 4.2), we can check if $C\in\mathcal{S}$ in
polynomial space as well, which concludes the proof of the theorem. ∎

We also have the accompanying hardness result.

######  Lemma 6 ().

Deciding whether the cut-off of a given RBN is positive or negative is -hard.

Similar to the cube-reachability problem, our result on almost-sure
coverability also applies to the related model of ASMS. This solves an open
problem from [6]. For lack of space, we once again defer this discussion to
the appendix.

##  6 Application 2: Computation by RBN

In this section we give another application of our results. We introduce a
model of computation using RBN called _RBN protocols_. We take inspiration
from the extensively-studied model of population protocols [1, 2, 13]. The
reader can consult the above references for more details on population
protocols.

In our model, reconfigurable networks of identical, anonymous agents interact
to compute a predicate
$\varphi:\mathbb{N}^{k}\rightarrow\left\\{0,1\right\\}$. We show that RBN
protocols compute exactly the threshold predicates, which we will define more
formally below.

###  6.1 RBN Protocols

We introduce our computation model. The notation mimics that of [14].
color=blue!30]By PN19, did you mean Petri Nets 19?

######  Definition 6.

An _RBN protocol_ is a tuple $\mathcal{P}=(Q,\Sigma,\delta,I,O)$ where
$(Q,\Sigma,\delta)$ is an RBN, $I=\left\\{q_{1},\ldots,q_{k}\right\\}$ is a
set of _input states_ , and $O:Q\rightarrow\left\\{0,1\right\\}$ is an _output
function_.

_Configurations_ and _runs_ of $\mathcal{P}$ are the same as that of the
underlying RBN. A configuration $C$ is called a _0-consensus_ (respectively a
_1-consensus_) if $C(q)>0$ implies $O(q)=0$ (respectively $O(q)=1$). For
$b\in\\{0,1\\}$, a $b$-consensus $C$ is _stable_ if every configuration
reachable from $C$ is also a $b$-consensus. A run
$C_{0}\xrightarrow{}C_{1}\xrightarrow{}C_{2}\cdots$ of $\mathcal{P}$ is _fair_
if it is finite and cannot be extended by any stepcolor=green!30]same as in
PN19, stronger or same than in DC (could change to DC) , or if it is infinite
and the following condition holds for all configurations $C,C^{\prime}$: if
$C\xrightarrow{}C^{\prime}$ and $C=C_{i}$ for infinitely many $i\geq 0$, then
the step $C\xrightarrow{}C^{\prime}$ appears infinitely along the run. In
other words, if a fair run reaches a configuration infinitely often, then all
the configurations reachable in a step from that configuration will be reached
infinitely often from it.

A fair run $C_{0}\xrightarrow{}C_{1}\xrightarrow{}\dots$ _converges to $b$_ if
there is $i\geq 0$ such that $C_{j}$ is a $b$-consensus for every $j\geq i$.
For every $\bm{v}\in\mathbb{N}^{k}$, let $C_{\bm{v}}$ be the configuration
given by $C_{\bm{v}}(q_{i})=\bm{v}_{i}$ for every $q_{i}\in I$, and
$C_{\bm{v}}(q)=0$ for every $q\in Q\setminus I$. We call $C_{\bm{v}}$ the
_initial configuration for input $\bm{v}$_. The protocol $\mathcal{P}$
_computes the predicate_ $\varphi\colon\mathbb{N}^{k}\rightarrow\\{0,1\\}$, if
for every $\bm{v}\in\mathbb{N}^{k}$, every fair run starting at $C_{\bm{v}}$
converges to $\varphi(\bm{v})$.

$q_{1}$$q_{2}$$q_{3}$$?a$$!b$$?b$$!a$$?b$$!b$ Figure 3: An RBN protocol
$\mathcal{P}$.

######  Example 3.

Adding the dashed line transitions to the RBN of Example 1 yields the RBN
protocol $\mathcal{P}=(Q,\Sigma,\delta,I,O)$ illustrated in Figure 3. The
initial state is $q_{1}$, i.e. $I=\left\\{q_{1}\right\\}$, and the output
function is defined such that $O(q_{1})=O(q_{2})=0$ and $O(q_{3})=1$. If there
is a process in $q_{3}$, it can “attract” the rest of the processes there
using the new dashed transitions. As with the RBN of Example 1, a process can
be put in $q_{3}$ starting from the initial configuration $\Lbag k\cdot
q_{1}\Rbag$ if and only if $k\geq 3$. This RBN protocol computes the predicate
$x\geq 3$: if there are less than $3$ processes originally in $q_{1}$ then
they stay in states with output $0$, and if there are more, then in a fair run
a process eventually enters $q_{3}$, and eventually the others follow, thus
converging to $1$.

###  6.2 Expressivity

In this section, we show that RBN protocols compute exactly the predicates
definable by counting sets. A predicate
$\varphi:\mathbb{N}^{k}\rightarrow\left\\{0,1\right\\}$ is _definable by
counting sets_ if for every $b\in\\{0,1\\}$, the sets $\left\\{\bm{v}\ |\
\varphi(\bm{v})=b\right\\}$ are counting sets.

For $b\in\left\\{0,1\right\\}$, define the following sets of configurations:

  * •

Let $\mathcal{C}_{b}$ be the set of $b$-consensus configurations.

  * •

Let $\mathcal{ST}_{b}$ be the set
$\overline{\mathit{pre}^{*}\left(\overline{\mathcal{C}_{b}}\right)}$ of stable
$b$-consensuses. These are the configurations from which one can reach only
$b$-consensuses.

  * •

Let $\mathcal{I}_{b}$ be the set of initial configurations $C_{\bm{v}}$ for
inputs $\bm{v}$ such that $\varphi(\bm{v})=b$.

The next lemma states that every predicate computed by a protocol is definable
by counting sets.

######  Lemma 7 ().

Let $\mathcal{P}$ be a RBN protocol that computes the predicate
$\varphi:\mathbb{N}^{k}\rightarrow\left\\{0,1\right\\}$. Then for every
$b\in\\{0,1\\}$, the sets $\mathcal{I}_{b},\mathcal{C}_{b}$ and
$\mathcal{ST}_{b}$ are all counting sets. This entails that $\varphi$ is
definable by counting sets.

###### Proof Sketch.

Fix a $b\in\\{0,1\\}$. It is easy to see that $\mathcal{C}_{b}$ is a cube.
Unraveling the definitions of $\mathcal{I}_{b}$ and $\mathcal{ST}_{b}$, we can
express them in terms of $\mathcal{C}_{b}$ by using boolean operations and
$\mathit{pre}^{*}$. By the Closure Corollary (Corollary 1), they are counting
sets. Set $\left\\{\bm{v}\ |\ \varphi(\bm{v})=b\right\\}$ is simply
$\mathcal{I}_{b}$ restricted to $I$, and so we are done. ∎

The next lemma states the converse result. It essentially uses the fact that
there is a sub-class of population protocols called IO protocols which compute
exactly the predicates definable by counting sets (Theorem 7 and Theorem 39 of
[2, 14]), and that IO protocols are a sub-class of RBN (Section 6.2 of [3]).

######  Lemma 8 ().

Let $\varphi:\mathbb{N}^{k}\rightarrow\left\\{0,1\right\\}$ be a predicate
definable by counting sets. Then there exists a RBN protocol computing
$\varphi$.

By Lemma 7 and Lemma 8, we get our result.

######  Theorem 6.1.

RBN protocols compute exactly the predicates definable by counting sets.

## Acknowledgements

We thank Nathalie Bertrand and Javier Esparza for many helpful discussions.

## References

  * [1] Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. Distributed Comput. 18(4), 235–253 (2006). https://doi.org/10.1007/s00446-005-0138-3, https://doi.org/10.1007/s00446-005-0138-3
  * [2] Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The computational power of population protocols. Distributed Comput. 20(4), 279–304 (2007). https://doi.org/10.1007/s00446-007-0040-2, https://doi.org/10.1007/s00446-007-0040-2
  * [3] Balasubramanian, A.R., Weil-Kennedy, C.: Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent. In: Ganty, P., Bresolin, D. (eds.) Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2021, Padua, Italy, 20-22 September 2021. EPTCS, vol. 346, pp. 18–34 (2021). https://doi.org/10.4204/EPTCS.346.2, https://doi.org/10.4204/EPTCS.346.2
  * [4] Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS. pp. 501–513 (2013). https://doi.org/10.4230/LIPIcs.FSTTCS.2013.501
  * [5] Bertrand, N., Fournier, P., Sangnier, A.: Playing with probabilities in reconfigurable broadcast networks. In: Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS. pp. 134–148 (2014). https://doi.org/10.1007/978-3-642-54830-7_9
  * [6] Bouyer, P., Markey, N., Randour, M., Sangnier, A., Stan, D.: Reachability in networks of register protocols under stochastic schedulers. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy. LIPIcs, vol. 55, pp. 106:1–106:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPIcs.ICALP.2016.106, https://doi.org/10.4230/LIPIcs.ICALP.2016.106
  * [7] Chini, P., Meyer, R., Saivasan, P.: Liveness in broadcast networks. In: Atig, M.F., Schwarzmann, A.A. (eds.) Networked Systems - 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19-21, 2019, Revised Selected Papers. Lecture Notes in Computer Science, vol. 11704, pp. 52–66. Springer (2019). https://doi.org/10.1007/978-3-030-31277-0_4, https://doi.org/10.1007/978-3-030-31277-0_4
  * [8] Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012), https://doi.org/10.4230/LIPIcs.FSTTCS.2012.289
  * [9] Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. _Long version_ (2012), https://www.irif.fr/~sangnier/publis/DSTZ-FSTTCS12-long.pdf
  * [10] Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6269, pp. 313–327. Springer (2010). https://doi.org/10.1007/978-3-642-15375-4_22, https://doi.org/10.1007/978-3-642-15375-4_22
  * [11] Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. J. ACM 63(1), 10:1–10:48 (2016). https://doi.org/10.1145/2842603, https://doi.org/10.1145/2842603
  * [12] Esparza, J., Ganty, P., Majumdar, R., Weil-Kennedy, C.: Verification of immediate observation population protocols. In: CONCUR. LIPIcs, vol. 118, pp. 31:1–31:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)
  * [13] Esparza, J., Jaax, S., Raskin, M.A., Weil-Kennedy, C.: The complexity of verifying population protocols. Distributed Comput. 34(2), 133–177 (2021). https://doi.org/10.1007/s00446-021-00390-x, https://doi.org/10.1007/s00446-021-00390-x
  * [14] Esparza, J., Raskin, M.A., Weil-Kennedy, C.: Parameterized analysis of immediate observation petri nets. In: Donatelli, S., Haar, S. (eds.) Application and Theory of Petri Nets and Concurrency - 40th International Conference, PETRI NETS 2019, Aachen, Germany, June 23-28, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11522, pp. 365–385. Springer (2019). https://doi.org/10.1007/978-3-030-21571-2_20, https://doi.org/10.1007/978-3-030-21571-2_20
  * [15] Hague, M.: Parameterised pushdown systems with non-atomic writes. In: Chakraborty, S., Kumar, A. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India. LIPIcs, vol. 13, pp. 457–468. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011). https://doi.org/10.4230/LIPIcs.FSTTCS.2011.457, https://doi.org/10.4230/LIPIcs.FSTTCS.2011.457

##  Appendix 0.A Proofs for section 3

See 1

###### Proof.

color=blue!30]Can you check if this proof is okay and elaborate if
needed?color=green!30]done Let $C\xrightarrow{t+t_{1},\dots,t_{n}}C^{\prime}$,
where $t=(p,!a,p^{\prime})$ and each $t_{i}=(p_{i},?a,p_{i}^{\prime})$. Let
$\theta=(v,S)$ such that $C\in{\llbracket\theta\rrbracket}$. Let
$t_{1},\ldots,t_{k}$ be the subset of receive transitions such that
$p_{1},\ldots,p_{k}\notin S$, and let $t_{k+1},\ldots,t_{n}$ be the subset of
receive transitions such that $p_{k+1},\ldots,p_{n}\in S$. We have two cases.

  * •

If $p\notin S$, then we perform a “broadcast from $v$”. Let
$v^{\prime}=v-\sum_{i}\bm{p_{i}}+\sum_{i=1}^{k}\bm{p_{i}^{\prime}}-\bm{p}+\bm{p^{\prime}}$.
Let
$S^{\prime}=S\cup\left\\{p_{i}^{\prime}|i\in\left\\{k+1,n\right\\}\right\\}$.

  * •

If $p\in S$, then we perform a “broadcast from $S$”. Let
$v^{\prime}=v-\sum_{i}\bm{p_{i}}+\sum_{i=k+1}^{n}\bm{p_{i}^{\prime}}$. Let
$S^{\prime}=S\cup\left\\{p^{\prime}\right\\}\cup\left\\{p_{i}^{\prime}|i\in\left\\{k+1,n\right\\}\right\\}$.

Since $C\xrightarrow{t+t_{1},\dots,t_{n}}C^{\prime}$, $C(q)>0$ for
$q\in\left\\{p,p_{1},\ldots,p_{n}\right\\}$ and thus $v^{\prime}$ is well-
defined. Let $\theta^{\prime}$ be $(v^{\prime},S^{\prime})$. By our definition
of $v^{\prime},S^{\prime}$, there is an edge
$\theta\rightsquigarrow^{a}\theta^{\prime}$ in the symbolic graph. ∎

See 2

###### Proof.

Let
$\theta=\theta_{0}\rightsquigarrow\theta_{1}\rightsquigarrow\theta_{2}\rightsquigarrow\dots\theta_{m-1}\rightsquigarrow\theta_{m}=\theta^{\prime}$
be the path between $\theta$ and $\theta^{\prime}$. We proceed by induction on
$m$. The claim is clearly true for $m=0$. Suppose $m>0$ and the claim is true
for $m-1$. By induction hypothesis, we can assume that the path
$\theta_{0}\rightsquigarrow\theta_{1}\rightsquigarrow\dots\rightsquigarrow\theta_{m-1}$
is already in normal form.

Let each $\theta_{i}=(v_{i},S_{i})$. Let $l$ be the number of bad pairs in the
path between $\theta_{0}$ and $\theta_{m}$. If $l=0$, then the path is already
in normal form and we are done. Suppose $l>0$ and let $(w,w^{\prime})$ be a
bad pair. Since the path between $\theta_{0}$ and $\theta_{m-1}$ is already in
normal form, it has to be the case that $w^{\prime}=m$. Hence, we have
$Z:=(S_{w}\setminus S_{w+1})\cap S_{m}\neq\emptyset$.

By Proposition 2, the following is a valid path:
$(v_{w},S_{w})\rightsquigarrow(v_{w+1},S_{w+1}\cup
Z)\rightsquigarrow(v_{w+2},S_{w+2}\cup Z)\dots(v_{m-1},S_{m-1}\cup
Z)\rightsquigarrow(v_{m},S_{m}\cup Z)=(v_{m},S_{m})$. Let
$\theta^{\prime}_{j}:=\theta_{j}$ if $j\leq w$ and $(v_{j},S_{j}\cup Z)$
otherwise. Hence, we get a path
$\theta^{\prime}_{0}\rightsquigarrow\theta^{\prime}_{1}\rightsquigarrow\dots\theta^{\prime}_{m-1}\rightsquigarrow\theta^{\prime}_{m}$.

Let each $\theta^{\prime}_{i}=(v_{i}^{\prime},S_{i}^{\prime})$. We first claim
that the path between $\theta^{\prime}_{0}$ and $\theta^{\prime}_{m-1}$ is in
normal form. Indeed, suppose there exists $0\leq i<j\leq m-1$ such that
$(S_{i}^{\prime}\setminus S_{i+1}^{\prime})\cap S_{j}^{\prime}\neq\emptyset$.
There are four cases:

  * •

$i\leq w$ and $j\leq w$ : In this case $S_{i}^{\prime}\setminus
S_{i+1}^{\prime}=S_{i}\setminus S_{i+1}$ and $S_{j}^{\prime}=S_{j}$, and since
the path between $\theta_{0}$ and $\theta_{m-1}$ is in normal form, this case
cannot happen.

  * •

$w<i$ and $w<j$: In this case $S_{i}^{\prime}\setminus
S_{i+1}^{\prime}=S_{i}\setminus S_{i+1}$ and $S_{j}^{\prime}=S_{j}\cup Z$.
Since the path between $\theta_{0}$ and $\theta_{m-1}$ is in normal form, this
should then imply that $(S_{i}\setminus S_{i+1})\cap Z\neq\emptyset$. By
definition this means that $(S_{w}\setminus S_{w+1})\cap S_{i}\neq\emptyset$
which contradicts the fact that the path between $\theta_{0}$ and
$\theta_{m-1}$ is in normal form.

  * •

$i<w$ and $w<j$: Similar to the case before, this should then imply that
$(S_{i}\setminus S_{i+1})\cap Z\neq\emptyset$. By definition this means that
$(S_{i}\setminus S_{i+1})\cap S_{w}\neq\emptyset$ which contradicts the fact
that the path between $\theta_{0}$ and $\theta_{m-1}$ is in normal form.

  * •

$i=w$ and $w<j$: In this case $S_{i}^{\prime}\setminus
S_{i+1}^{\prime}=S_{i}\setminus(S_{i+1}\cup Z)$ and $S_{j}^{\prime}=S_{j}\cup
Z$. This would then imply that $(S_{i}\setminus S_{i+1})\cap
S_{j}\neq\emptyset$ which contradicts the fact that the path between
$\theta_{0}$ and $\theta_{m-1}$ is in normal form.

It is then clear by construction, that this new path from
$\theta^{\prime}_{0}:=\theta_{0}$ to $\theta^{\prime}_{m}:=\theta_{m}$ has at
most $l-1$ bad pairs only. Hence, we now have a path from $\theta_{0}$ to
$\theta_{m}$ such that the prefix of length $m-1$ is in normal form and the
number of bad pairs has been strictly reduced to $l-1$. Repeatedly applying
this procedure, leads to a path in normal form between $\theta_{0}$ and
$\theta_{m}$. ∎

See 3.1

###### Proof.

Suppose $\theta\rightsquigarrow^{*}\theta^{\prime}$. If the length of the path
is 0, then there is nothing to prove. Hence, we restrict ourselves to the case
when the length of the path is bigger than 0. By Lemma 2, there is a path in
normal from from $\theta$ to $\theta^{\prime}$ (say)
$\theta=\theta_{0}\rightsquigarrow\theta_{1}\rightsquigarrow\theta_{2}\dots\theta_{m-1}\rightsquigarrow\theta_{m}=\theta^{\prime}$
with each $\theta_{i}:=(v_{i},S_{i})$.

Let $N_{0}=0$ and let $N_{i}=(N_{i-1}+1)\cdot(|S_{i-1}\setminus S_{i}|+1)$ for
every $1\leq i\leq m$. In Lemma 6 of [8], the following fact has been proved:

> For every $1\leq i\leq m$ and for every
> $C^{\prime}\in{\llbracket\theta_{i}\rrbracket}_{N_{i}+1}$, there exists
> $C\in{\llbracket\theta_{i-1}\rrbracket}_{N_{i-1}+1}$ such that
> $C\xrightarrow{*}C^{\prime}$.

This immediately proves that for all
$C^{\prime}\in{\llbracket\theta^{\prime}\rrbracket}_{N_{m}+1}$, there exists
$C\in{\llbracket\theta\rrbracket}$ such that $C\xrightarrow{*}C^{\prime}$. If
we prove $N_{m}\leq k\times(2k)^{|Q|}\times(|Q|+1)^{|Q|+1}$, then the proof of
the theorem will be complete.

Notice that since the path between $\theta_{0}$ and $\theta_{m}$ is in normal
form, the number of indices $i$ such that $|S_{i-1}\setminus S_{i}|>0$ is at
most $|Q|$. Indeed, suppose $q\in S_{i-1}\setminus S_{i}$ for some $i$. Then
by the normal form property, $q\notin S_{j}$ for any $j\geq i$. Hence, in the
rest of the path $q$ does not appear in the abstract part at all. By
definition of the edges in the symbolic graph, if
$(v,\emptyset)\rightsquigarrow(v^{\prime},S^{\prime})$ is an edge, then
$S^{\prime}=\emptyset$. These two facts then imply that the number of indices
$i$ such that $|S_{i-1}\setminus S_{i}|>0$ is at most $|Q|$.

It then follows that except for at most $|Q|$ indices, each index $N_{i}$ is
obtained from $N_{i-1}$ by simply adding 1 and in the remaining indices,
$N_{i}$ is obtained from $N_{i-1}$ by adding 1 and then multiplying by a
number which is at most $|Q|+1$. The way to maximize $N_{m}$ by this procedure
is by letting $N_{i}=N_{i-1}+1$ for every $1\leq i\leq m-|Q|$ and then letting
$N_{i}=(N_{i-1}+1)\cdot(|Q|+1)$ for every $m-|Q|<i\leq m$. This gives an upper
bound of $(m-|Q|+1)|Q|(|Q|+1)^{|Q|}$ for $N_{m}$. Since $m$ is itself the
length of the path between $\theta_{0}$ and $\theta_{m}$, $m$ is upper bounded
by the number of symbolic configurations in $\mathcal{G}_{k}$ which is at most
$|\mathbb{N}_{k}^{Q}|\times 2^{|Q|}\leq k\times k^{|Q|}\times 2^{|Q|}$.
Overall we get that $N_{m}\leq k\times(2k)^{|Q|}\times(|Q|+1)^{|Q|+1}$. ∎

##  Appendix 0.B Proofs for Section 5

See 5

###### Proof.

By Theorem 5.3, it follows that a given RBN has a negative cut-off iff
$\mathcal{S}=\mathit{post}^{*}([\mathit{init}])\cap\overline{\mathit{pre}^{*}(\uparrow\mathit{fin})}$
is infinite. We have already seen that $\mathcal{S}$ is a counting set such
that the norm of $\mathcal{S}$ is at most $N:=2^{p(|Q|)}$ for some fixed
polynomial $p$.

Let $\cup_{i}\mathcal{C}_{i}$ be a counting constraint for $\mathcal{S}$ which
minimizes its norm and let each $\mathcal{C}_{i}=(L_{i},U_{i})$. Hence,
$L_{i}(q)\leq N$ for every state $q$. Further, $\mathcal{S}$ is infinite iff
there is an index $i$ and a state $q$ such that $U_{i}(q)=\infty$.

Using these two facts, we claim that $\mathcal{S}$ is infinite iff there is a
state $q$ and a configuration $C\in\mathcal{S}$ such that $C(q^{\prime})\leq
N$ for every $q^{\prime}\neq q$ and $C(q)=N+1$. Indeed, if $\mathcal{S}$ is
infinite, then there is an $i$ and a $q$ such that $U_{i}(q)=\infty$. If we
let $C$ be such that $C(q^{\prime})=L(q^{\prime})\leq N$ for every
$q^{\prime}\neq q$ and $C(q)=N+1$ then $C\in\mathcal{C}_{i}\in\mathcal{S}$.

For the other direction, suppose such a state $q$ and a configuration $C$
exists. Since $C\in\mathcal{S}$ we have that $C\in\mathcal{C}_{i}$ for some
$i$. Now, since $C(q)=N+1$ and the norm of $\mathcal{C}_{i}$ is at most $N$,
it must be the case that $U_{i}(q)=\infty$. This then proves that
$\mathcal{S}$ is infinite.

Hence, to check if $\mathcal{S}$ is infinite, we just have to guess a state
$q$ and a configuration $C$ such that $C(q^{\prime})\leq N$ for every
$q^{\prime}\neq q$ and $C(q)=N+1$ and check if $C\in\mathcal{S}$. Since
guessing $C$ can be done in polynomial space (by representing every number in
binary), by the Theorem (Theorem 4.2), we can check if $C\in\mathcal{S}$ in
polynomial space as well, which concludes the proof of the theorem. ∎

See 6

###### Proof.

We reduce from the fixed-configuration almost-sure coverability problem for
RBN. In this problem, we are given a RBN $\mathcal{R}=(Q,\Sigma,\delta)$, a
configuration $C$ of $\mathcal{R}$ such that $2\leq|C|\leq|Q|$ and a state
$q_{f}\in Q$ and we are asked to decide if $C$ can almost-surely cover
$q_{f}$, i.e., if $\mathit{post}^{*}(C)\subseteq\mathit{pre}^{*}(\uparrow
q_{f})$. This problem is -hard and the proof is as follows: In Theorem 4 of
[14], the authors give a reduction from the acceptance problem for linear-
space bounded Turing machines to the problem of covering a state $q_{f}$ from
a given initial configuration $C$ for a subclass of RBN called IO nets which
have the following property: Starting from the initial configuration of the IO
net, there is exactly one execution which is possible. It then follows that
the covering the state $q_{f}$ from $C$ is equivalent to almost-surely
covering $q_{f}$ from $C$. Since IO nets are a subclass of RBN (Section 6.2 of
[3]), it follows that the fixed-configuration almost-sure coverability problem
for RBN is -hard.

We now give a reduction from the fixed-configuration almost-sure coverability
problem for RBN to the problem of checking if a given RBN has a positive cut-
off. Let $(\mathcal{R},C,q_{f})$ be an instance of the fixed-configuration
almost-sure coverability problem for RBN such that
$\mathcal{R}=(Q,\Sigma,\delta)$ and $C=\Lbag q_{1},\dots,q_{n}\Rbag$. The
required reduction proceeds in three stages.

First stage:  We construct a new RBN
$\mathcal{R}_{1}=(Q_{1},\Sigma_{1},\delta_{1})$ as follows:
$Q_{1}=Q\times\\{1,2,\dots,n\\}\cup\\{\mathit{fin}\\}$ where $\mathit{fin}$ is
a new state, $\Sigma_{1}=\Sigma\cup\\{@\\}$ where $@$ is a new letter and
$\delta_{1}=\\{(p,i)\xrightarrow{!a}(q,i):p\xrightarrow{!a}q\in\delta\\}\cup\\{(p,i)\xrightarrow{?a}(q,i):p\xrightarrow{?a}q\in\delta\\}\cup\\{(q_{f},i)\xrightarrow{!@}\mathit{fin}\\}$.
For each $i$, the set $Q\times\\{i\\}$, will be called the $i^{th}$ copy of
$\mathcal{R}$.

Intuitively, $\mathcal{R}_{1}$ contains $n$ copies of $\mathcal{R}$ along with
a new state $\mathit{fin}$ such that it is always possible to move from any
copy of the state $q_{f}$ to the new state $\mathit{fin}$. Note that since
$n=|C|\leq|Q|$, this construction takes polynomial time.

Let $D:=\\{(q_{1},1),(q_{2},2),\dots,(q_{n},n)\\}$. It is straightforward to
verify that $C$ can almost-surely cover $q_{f}$ in $\mathcal{R}$ iff $D$ can
almost-surely cover $\mathit{fin}$ in $\mathcal{R}_{1}$.

Second stage:  We now construct a second RBN
$\mathcal{R}_{2}=(Q_{2},\Sigma_{2},\delta_{2})$ as follows:
$Q_{2}=Q_{1}\cup\\{\mathit{init}\\}$ where $\mathit{init}$ is a new state,
$\Sigma_{2}=\Sigma_{1}\cup\\{\\#\\}\cup\\{\$_{1},\dots,\$_{n}\\}$ where
$\\#,\$_{1},\dots,\$_{n}$ are $n+1$ new letters and $\delta_{2}$ contains all
the transitions in $\delta_{1}$ and also the following transitions:

  * •

Type 1 transitions: $\mathit{init}\xrightarrow{!\\#}(q_{i},i)$ and for each
$1\leq i\leq n$.

  * •

Type 2 transitions: For every $p\in Q$ and $1\leq i\leq n$, we have the
transitions $(p,i)\xrightarrow{!\$_{i}}(p,i)$ and
$(p,i)\xrightarrow{?\$_{i}}\mathit{fin}$.

By combining the Type 1 and Type 2 transitions, it is very easy to verify the
following facts:

  * •

Fact 1: If $C^{\prime}\geq\Lbag(p,i),(q,i)\Rbag$ for some $i$ and some $p,q$,
then $C^{\prime}$ can cover $\mathit{fin}$.

  * •

Fact 2: If $C^{\prime}\geq\Lbag 2\cdot\mathit{init}\Rbag$ or
$C\geq\Lbag\mathit{init},(p,i)\Rbag$ for some $i$ and some $p$, then
$C^{\prime}$ can cover $\mathit{fin}$.

  * •

Fact 3: $n+1$ is a positive cut-off for $\mathcal{R}_{2}$.

  * •

Fact 4: If $C^{\prime}\xrightarrow[\mathcal{R}_{2}]{*}C^{\prime\prime}$ is a
run such that $C^{\prime}(\mathit{init})=0$ and $C^{\prime}$ does not contain
two processes in the same copy of $\mathcal{R}$, then no transitions of type 1
or type 2 could have been fired along this run. Consequently, we have
$C^{\prime}\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime\prime}$.

We now claim that

> $\Lbag n\cdot\mathit{init}\Rbag$ can almost-surely cover $\mathit{fin}$ in
> $\mathcal{R}_{2}$ iff $D$ can almost-surely cover $\mathit{fin}$ in
> $\mathcal{R}_{1}$.

Suppose $\Lbag n\cdot\mathit{init}\Rbag$ can almost-surely cover
$\mathit{fin}$ in $\mathcal{R}_{2}$. We want to show that $D$ can almost-
surely cover $\mathit{fin}$ in $\mathcal{R}_{1}$. To do this, we have to show
that if $D\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime}$, then $C^{\prime}$ can
cover $\mathit{fin}$ in $\mathcal{R}_{1}$. Notice that
$C^{\prime}(\mathit{init})=0$ and $C^{\prime}$ does not contain two processes
in the same copy of $\mathcal{R}$.

Notice that, by using the type 1 transitions, we have $\Lbag
n\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{2}]{*}D$ and so we have
$\Lbag
n\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{2}]{*}D\xrightarrow[\mathcal{R}_{2}]{*}C^{\prime}$.
By assumption, this means that
$C^{\prime}\xrightarrow[\mathcal{R}_{2}]{*}C^{\prime\prime}$ with
$C^{\prime\prime}(\mathit{fin})>0$. By Fact 4, we have
$C^{\prime}\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime\prime}$ and so
$C^{\prime}$ can cover $\mathit{fin}$ in $\mathcal{R}_{1}$.

Suppose $D$ can almost-surely cover $\mathit{fin}$ in $\mathcal{R}_{1}$. We
want to show that $\Lbag n\cdot\mathit{init}\Rbag$ can almost-surely cover
$\mathit{fin}$ in $\mathcal{R}_{2}$. To do so, we have to show that if $\Lbag
n\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{2}]{*}C^{\prime}$, then
$C^{\prime}$ can cover $\mathit{fin}$ in $\mathcal{R}_{2}$. By means of Fact 1
and Fact 2, it suffices to show that this is the case when $C^{\prime}$
contains exactly one process in each copy of $\mathcal{R}$. In this case, we
will prove that $D\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime}$ and so by
assumption, this means that $C^{\prime}$ can cover $\mathit{fin}$ in
$\mathcal{R}_{1}$ and hence in $\mathcal{R}_{2}$ as well.

All that remains to show that is that
$D\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime}$, which is what we do now.
Consider the run $\Lbag
n\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{2}]{}C_{1}\xrightarrow[\mathcal{R}_{2}]{}C_{2}\dots
C_{k}\xrightarrow[\mathcal{R}_{2}]{}C^{\prime}$. Since $C^{\prime}$ has
exactly one process in each copy of $\mathcal{R}$, it must be the case that
along this run, no type 2 transitions were fired, and each type 1 transition
was fired exactly once, i.e., for each $1\leq i\leq n$, the transition
$\mathit{init}\xrightarrow{!\\#}(q_{i},i)$ occured exactly once along this
run. Notice that if for some $j$, we have
$C_{j}\xrightarrow[\mathcal{R}_{2}]{r_{j}+r^{1}_{j},\dots,r^{l_{j}}_{j}}C_{j+1}\xrightarrow[\mathcal{R}_{2}]{r_{j+1}+r^{1}_{j+1},\dots,r^{l_{j+1}}_{j+1}}C_{j+2}$
where $r_{j}$ is not a type 1 transition and $r_{j+1}$ is a type 1 transition,
then
$C_{j}\xrightarrow[\mathcal{R}_{2}]{r_{j+1}+r^{1}_{j+1},\dots,r^{l_{j+1}}_{j+1}}C^{\prime\prime}\xrightarrow[\mathcal{R}_{2}]{r_{j}+r^{1}_{j},\dots,r^{l_{j}}_{j}}C_{j+2}$.
This means that we can push all the occurences of type 1 transitions along
this run to the beginning. But then notice that after the first $n$ steps we
would have reached the configuration $D$ from $\Lbag
n\cdot\mathit{init}\Rbag$. This means that
$D\xrightarrow[\mathcal{R}_{2}]{*}C^{\prime}$ and by Fact 4, we have
$D\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime}$, which finishes the proof.

Notice that by Fact 3, we have actually shown the following

> Fact 5: $D$ can almost-surely cover $\mathit{fin}$ in $\mathcal{R}_{1}$ iff
> $\Lbag n\cdot\mathit{init}\Rbag$ can almost-surely cover $\mathit{fin}$ in
> $\mathcal{R}_{2}$ iff $n$ is a positive cut-off for $\mathcal{R}_{2}$.

Third stage:  We now construct our final RBN
$\mathcal{R}_{3}=(Q_{3},\Sigma_{3},\delta_{3})$ as follows:
$Q_{3}=Q_{2}\cup\\{s_{1},s_{2},\dots,s_{n}\\}$ where $s_{1},\dots,s_{n}$ are
$n$ new states, $\Sigma_{3}=\Sigma_{2}\cup\\{a_{1},\dots,a_{n},b\\}$ where
$a_{1},\dots,a_{n},b$ are $n+1$ new letters and $\delta_{3}$ contains all the
transitions in $\delta_{2}$ and also the following transitions:

  * •

Type 3 transitions: For each $i\in\\{1,\dots,n\\}$, we have
$(q_{i},i)\xrightarrow{!a_{i}}(q_{i},i)$ and
$s_{i-1}\xrightarrow{?a_{i}}s_{i}$. (Here and in the sequel, $s_{0}$ is taken
to be $\mathit{init}$).

  * •

Type 4 transitions: For each $i\in\\{1,\dots,n-1\\}$, we have
$s_{i}\xrightarrow{!b}\mathit{init}$.

Since $s_{n}$ is a sink state which does not broadcast anything and since the
only way to reach $s_{n}$ is through $s_{n-1}$, it is easy to verify the
following:

  * •

Fact 6: Suppose $C^{\prime}\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime\prime}$
such that $C^{\prime}(s_{n})=i_{n}$ and $C^{\prime\prime}(s_{n})=j_{n}$. Then
$i_{n}\leq j_{n}$ and $C^{\prime}-i_{n}\cdot
s_{n}\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime\prime}-j_{n}\cdot
s_{n}+(j_{n}-i_{n})\cdot
s_{n-1}\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime\prime}-j_{n}\cdot
s_{n}+(j_{n}-i_{n})\cdot\mathit{init}$.

We now claim that

> There is a positive cut-off for $\mathcal{R}_{3}$ iff $n$ is a positive cut-
> off for $\mathcal{R}_{2}$.

Suppose $n$ is a positive cut-off for $\mathcal{R}_{2}$. We claim that $n$ is
also a positive cut-off for $\mathcal{R}_{3}$. To show this, we have to prove
that for all $h\geq n$, if $\Lbag
h\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime}$, then
$C^{\prime}$ can cover $\mathit{fin}$ in $\mathcal{R}_{3}$. Let
$C^{\prime}(s_{l})=i_{l}$ for every $1\leq l\leq n$ and let $i=\sum_{1\leq
l\leq n}i_{l}$. We consider two cases:

  * •

Case 1: $C^{\prime}(s_{n})=0$. Let $\tilde{C}=C^{\prime}-(\sum_{1\leq l\leq
n}i_{l}\cdot s_{l})+i\cdot\mathit{init}$. Notice that $\tilde{C}$ can be
reached from $\Lbag h\cdot\mathit{init}\Rbag$ in $\mathcal{R}_{2}$ \- Simply
use the same run from $\Lbag h\cdot\mathit{init}\Rbag$ to $C^{\prime}$, but
remove all the type 3 and type 4 transitions. By assumption then, $\tilde{C}$
can cover $\mathit{fin}$ in $\mathcal{R}_{2}$ and so in $\mathcal{R}_{3}$ as
well.

Further, notice that $C^{\prime}$ can reach $\tilde{C}$ in $\mathcal{R}_{3}$
means of type 4 transitions. This means that $C^{\prime}$ can also cover
$\mathit{fin}$ in $\mathcal{R}_{3}$.

  * •

Case 2: $C^{\prime}(s_{n})>0$. Let $h^{\prime}=h-i_{n}$. By Fact 6, we have
$\Lbag
h^{\prime}\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime}-i_{n}\cdot
s_{n}$. If we show that $h^{\prime}\geq n$, then we can apply the same
argument as Case 1 to finish this case as well. Indeed, for a process to reach
the state $s_{n}$, it is easy to see by construction that, in $C^{\prime}$,
there should be at least one process in each copy of $\mathcal{R}$. Hence,
there are at least $n$ processes in $C^{\prime}$ which are not in $s_{n}$ and
so $h^{\prime}\geq n$.

Suppose there is a positive cut-off for $\mathcal{R}_{3}$. We need to show
that $n$ is a positive cut-off for $\mathcal{R}_{2}$. By Fact 5, it suffices
to show that $D$ can almost-surely cover $\mathit{fin}$ in $\mathcal{R}_{1}$.
To show this, we need to show that if
$D\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime}$ then $C^{\prime}$ can cover
$\mathit{fin}$ in $\mathcal{R}_{1}$.

Let $N$ be the positive cut-off for $\mathcal{R}_{3}$ and let
$h\geq\max\\{n,N\\}$. By assumption $\Lbag h\cdot\mathit{init}\Rbag$ can
almost-surely cover $\mathit{fin}$ in $\mathcal{R}_{3}$. By using Type 1 and
Type 3 transitions, it is easy to see that, $\Lbag
h\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{3}]{*}D+(h-n)\cdot s_{n}$
and so $\Lbag
h\cdot\mathit{init}\Rbag\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime}+(h-n)\cdot
s_{n}$. By assumption, $C^{\prime}+(h-n)\cdot s_{n}$ can cover $\mathit{fin}$
in $\mathcal{R}_{3}$ and so we have a run $C^{\prime}+(h-n)\cdot
s_{n}\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime\prime}$ with
$C^{\prime\prime}(\mathit{fin})>0$. By induction on the run, it is easy to
prove that along this run, all the configurations $\tilde{C^{\prime\prime}}$
satisfy $\tilde{C^{\prime\prime}}(s_{n})=h-n$ and
$\tilde{C^{\prime\prime}}(s_{i})=0$ for every $0\leq i\leq n-1$. Hence, by
Fact 6, we have
$C^{\prime}\xrightarrow[\mathcal{R}_{3}]{*}C^{\prime\prime}-(h-n)\cdot s_{n}$.
Notice that along this run, there is no possibility of firing any transition
of type 1, 2 or 4. Further, if a transition of type 3, i.e., a transition of
the form $(q_{i},i)\xrightarrow{!a_{i}}(q_{i},i)$ is fired, then there could
have been no process which received that message. It follows that transitions
of type 3 do not change the configuration along this run. Hence, we can assume
that no transitions belonging to type 3 are fired along this run. This then
implies that
$C^{\prime}\xrightarrow[\mathcal{R}_{1}]{*}C^{\prime\prime}-(h-n)\cdot s_{n}$
and so $C^{\prime}$ can cover $\mathit{fin}$ in $\mathcal{R}_{1}$.

This chain of constructions then proves the desired result. ∎

##  Appendix 0.C Proof for section 6

See 7

###### Proof.

Let $\mathcal{P}=(Q,\Sigma,\delta,I,O)$ be a RBN protocol computing $\varphi$
and let $b\in\\{0,1\\}$. First we show that $\mathcal{ST}_{b}$ is a counting
set. The set $\mathcal{C}_{b}$ is equal to the cube such that there are 0
processes in states $q$ with $O(q)=1-b$ (i.e. an upper and a lower bound of
$0$), and an arbitrary number of processes elsewhere (i.e. an upper bound of
$\infty$ and a lower bound of $0$). By the Closure Corollary 1,
$\mathcal{ST}_{b}=\overline{\mathit{pre}^{*}\left(\overline{\mathcal{C}_{b}}\right)}$
is a counting set.

Let $\mathcal{I}$ be the counting set of initial configurations defined by the
cube which puts an arbitrary number of processes in initial states of $I$, and
$0$ elsewhere. The set
$\mathcal{I}\cap\overline{\mathit{pre}^{*}(\overline{\mathit{pre}^{*}(\mathcal{ST}_{b})})}$
is the set of initial configurations from which all runs of $\mathcal{P}$
converge to $b$. By the Closure Corollary 1, it is a counting set. Since
$\mathcal{P}$ computes $\varphi$, by definition
$\mathcal{I}_{b}=\mathcal{I}\cap\overline{\mathit{pre}^{*}(\overline{\mathit{pre}^{*}(\mathcal{ST}_{b})})}$.
The set $\left\\{\bm{v}\ |\ \varphi(\bm{v})=b\right\\}$ is equal to
$\mathcal{I}_{b}$ restricted to the initial states $I$, and so we are done. ∎

See 8

###### Proof.

To prove this, we first need the notion of an immediate observation net. An
immediate observation (IO) net is a tuple $\mathcal{N}=(Q,\delta)$ where $Q$
is a finite set of states and $\delta\subseteq Q\times Q\times Q$ is the
transition relation. A configuration of $\mathcal{N}$ is a multiset over $Q$,
and there is a step between two configurations $C,C^{\prime}$ if there exists
$(p,q,p^{\prime})\in\delta$ such that $C\geq\Lbag p,q\Rbag$ and
$C^{\prime}=C-\bm{p}+\bm{p^{\prime}}$.

In Section 6.2 of [3], it is shown that RBN can simulate IO nets. More
specifically, given an IO net $\mathcal{N}=(Q,\delta)$, Section 6.2 of [3]
shows that we can compute in polynomial time, a RBN
$\mathcal{R}=(Q,\Sigma,\delta^{\prime})$ with the same set of states such that
$C\xrightarrow{*}C^{\prime}$ in $\mathcal{N}$ if and only if
$C\xrightarrow{*}C^{\prime}$ in $\mathcal{R}$ for any two configurations
$C,C^{\prime}$. This implies that for any two subsets of configurations
$\mathcal{C},\mathcal{C}^{\prime}$,
$\mathit{post}^{*}(\mathcal{C})\subseteq\mathit{pre}^{*}(\mathcal{C}^{\prime})$
in $\mathcal{N}$ if and only if
$\mathit{post}^{*}(\mathcal{C})\subseteq\mathit{pre}^{*}(\mathcal{C}^{\prime})$
in $\mathcal{R}$.

Given an IO net $\mathcal{N}=(Q,\delta)$, a subset $I\subseteq Q$ and an
output function $O:Q\to\\{0,1\\}$, the tuple $(\mathcal{N},I,O)$ defines an
immediate observation (IO) population protocol, a subclass of population
protocols introduced in [2]. Similar to the definition of RBN protocols, we
can define the notion of an IO protocol computing a predicate and Theorem 7
and Theorem 39 of [2] shows that IO population protocols compute exactly the
predicates definable by counting sets.

Proposition 2.12 of [13] entails that an IO protocol computes a predicate
$\varphi$ if and only if
$\mathit{post}^{*}(\mathcal{I}_{b})\subseteq\mathit{pre}^{*}(\mathcal{ST}_{b})$
for every $b\in\\{0,1\\}$. This is also true for RBN. Indeed Proposition 2.12
of [13] states the above result for “well-behaved generalized protocols”
(Definition 2.1 of [13]). Fix an arbitrary RBN protocol $\mathcal{P}$. By
definition 2.1 of [13], it is a generalized protocol by setting $Conf$ to be
the set of configurations of $\mathcal{P}$, $\Sigma$ to be its set of states,
and $Step$ to be the step relation of the underlying RBN. By definition 2.8 of
[13], it is well-behaved, i.e., every fair execution eventually ends up in a
bottom strongly connected component of the reachability graph. This is because
the number of processes does not change along a run, so the reachability graph
from any configuration is finite.

Since RBN can simulate IO nets, it follows that RBN protocols can compute any
predicate computable by IO protocols and this concludes the proof.

∎

##  Appendix 0.D Asynchronous shared-memory systems

We now consider another model of distributed computation called asynhcronous
shared-memory systems (ASMS) [15, 11]. Here, we have a set of finite-state,
anonymous agents which can communicate by means of a single shared register,
i.e., agents can either write a value to the register or read the value
currently written on the register. The definitions and notations in this
section are taken from [3].

######  Definition 7.

An asynchronous shared-memory system (ASMS) is a tuple
$\mathcal{P}=(Q,\Sigma,\delta)$ where $Q$ is a finite set of states, $\Sigma$
is a finite alphabet, and $\delta\subseteq Q\times\\{R,W\\}\times\Sigma\times
Q$ is the set of transitions. Here $R$ stands for _read_ , and $W$ stands for
_write_.

We use $p\xrightarrow{R(d)}q$ (resp. $p\xrightarrow{W(d)}q$) to denote that
$(p,R,d,q)\in\delta$ (resp. $(p,W,d,q)\in\delta$). A configuration $C$ of an
ASMS is a multiset over $Q\cup\Sigma$ such that $\sum_{d\in\Sigma}C(d)=1$,
i.e., $C$ contains exactly one element from the set $\Sigma$. Hence, we
sometimes denote a configuration $C$ as $(M,d)$ where $M$ is a multiset over
$Q$ (which counts the number of processes in each state) and $d\in\Sigma$
(which denotes the content of the shared register). The value $d$ will be
denoted by $\textit{data}(C)$.

A _step_ between configurations $C=(M,d)$ and
$C^{\prime}=(M^{\prime},d^{\prime})$ exists if there is
$t=(p,\mathtt{op},d^{\prime\prime},q)\in\delta$ such that $M(p)>0$,
$M^{\prime}=M-\bm{p}+\bm{q}$ and either $\mathtt{op}=R$ and
$d=d^{\prime}=d^{\prime\prime}$ or $\mathtt{op}=W$ and
$d^{\prime}=d^{\prime\prime}$. If such a step exists, we denote it by
$C\xrightarrow{t}C^{\prime}$ and we let $\xrightarrow{*}$ denote the reflexive
transitive closure of the step relation. A _run_ is then a sequence of steps.

A cube $\mathcal{C}=(L,U)$ of an ASMS $\mathcal{P}=(Q,\Sigma,\delta)$ is
defined to be a cube over $Q\cup\Sigma$ satisfying the following property :
There exists $d\in\Sigma$ such that $L(d)=U(d)=1$ and
$L(d^{\prime})=U(d^{\prime})=0$ for every other $d^{\prime}\in\Sigma$. Hence,
we sometimes denote a cube $\mathcal{C}$ as $(L,U,d)$ where $(L,U)$ is a cube
over $Q$ and $d\in\Sigma$. Membership of a configuration $C$ in a cube
$\mathcal{C}$ is then defined in a straightforward manner.

The cube-reachability problem for ASMS is then to decide, given $\mathcal{P}$
and two cubes $\mathcal{C},\mathcal{C}^{\prime}$, whether $\mathcal{C}$ can
reach $\mathcal{C}^{\prime}$, i.e., whether there are configurations
$C\in\mathcal{C},C^{\prime}\in\mathcal{C}^{\prime}$ such that
$C\xrightarrow{*}C^{\prime}$. In Section 4 of [3], it was shown that the cube-
reachability problems for RBN and ASMS are polynomial-time equivalent. By
Theorem 4.3, we get

######  Theorem 0.D.1.

The cube-reachability problem for ASMS is -complete.

### The almost-sure coverability problem

Similar to RBN, we can define the almost-sure coverability problem for ASMS.
Let $\mathcal{P}=(Q,\Sigma,\delta)$ be an ASMS with two special states
$\mathit{init}$ and $\mathit{fin}$ and a special initial letter
$\\#\in\Sigma$. Let $\uparrow\mathit{fin}$ denote the set of all
configurations $C$ with $C(\mathit{fin})\geq 1$. For any $k\geq 1$, we say
that the configuration $(\Lbag k\cdot\mathit{init}\Rbag,\\#)$ almost-surely
covers $\mathit{fin}$ iff $\mathit{post}^{*}(\Lbag
k\cdot\mathit{init}\Rbag,\\#)\subseteq\mathit{pre}^{*}(\uparrow\mathit{fin})$.
Now, similar to RBN, it is easy to define the notion of a cut-off for ASMS.
The following fact is known (Theorem 3 of [6]).

######  Theorem 0.D.2.

Given an ASMS $\mathcal{P}$ with two state $\mathit{init},\mathit{fin}$ and a
letter $\\#$, a cut-off always exists. Whether the cut-off is positive or
negative can be decided in and -hard.

The main result of this subsection is that

######  Theorem 0.D.3.

Deciding whether the cut-off of a given ASMS is positive or negative is in
-complete.

Note that it suffices only to prove the upper bound, since the lower bound is
already known. Let $\mathcal{P}=(Q,\Sigma,\delta)$ be a fixed ASMS with
$\mathit{init},\mathit{fin}\in Q$ and $\\#\in\Sigma$. Let
$([\mathit{init}],\\#)$ denote the cube which has an arbitrary number of
agents in the state $\mathit{init}$ and 0 elsewhere. Similar to the model of
RBN, we first show that,

######  Theorem 0.D.4.

$\mathcal{P}$ has a positive cut-off iff
$\mathcal{S}:=\mathit{post}^{*}(([\mathit{init}],\\#))\cap\overline{\mathit{pre}^{*}(\uparrow\mathit{fin})}$
is finite.

###### Proof.

Suppose $\mathcal{S}$ is finite. Let $N$ be the largest value appearing in any
of the configurations of $\mathcal{S}$. It is easy to see that if $h>|Q|\cdot
N$, then any configuration of size $h$ does not belong in $\mathcal{S}$. It
follows that if $h>|Q|\cdot N$ and $C\in\mathit{post}^{*}((\Lbag
h\cdot\mathit{init}\Rbag,\\#))$ then
$C\in\mathit{pre}^{*}(\uparrow\mathit{fin})$ and so we have a positive cut-
off.

Suppose $\mathcal{S}$ is infinite. Then there must be an infinite set of
configurations which belong to $\mathit{post}^{*}(([\mathit{init}],\\#))$ but
not in $\mathit{pre}^{*}(\uparrow\mathit{fin})$. This means that for
infinitely many numbers $h$, there is a configuration
$C_{h}\in\mathit{post}^{*}((\Lbag h\cdot\mathit{init}\Rbag,\\#))$ but
$C_{h}\notin\mathit{pre}^{*}(\uparrow\mathit{fin})$. This then implies that
$\mathcal{P}$ cannot have a positive cut-off. ∎

Hence, checking whether $\mathcal{P}$ has a positive cut-off is equivalent to
deciding if $\mathcal{S}$ is finite. We shall now show that this is decidable
in . To show this, we recall the connection established between RBN and ASMS
in Section 4 of [3].

Given an ASMS $\mathcal{P}=(Q,\Sigma,\delta)$, in section 4.2 of [3], it is
shown that in polynomial time we can come up with an RBN
$\mathcal{R}=(Q\cup\Sigma\cup Q^{\prime},\Sigma^{\prime},\delta^{\prime})$
which has a copy of $Q$ and $\Sigma$ as its states and which has the following
properties:

  * •

A good configuration of $\mathcal{R}$ is a configuration $C$ such that
$\sum_{a\in\Sigma}C(a)=1$ and $C(q)=0$ if $q\notin Q\cup\Sigma$. Notice that
there is a natural bijection between configurations of $\mathcal{P}$ and good
configurations of $\mathcal{R}$.

  * •

A configuration $C$ of $\mathcal{P}$ can reach a configuration $C^{\prime}$ of
$\mathcal{P}$ iff $\hat{C}$ can reach $\hat{C^{\prime}}$ in $\mathcal{R}$,
where $\hat{C}$ and $\hat{C^{\prime}}$ are the corresponding good
configurations of $C$ and $C^{\prime}$ respectively.

Let $\mathcal{I}$ denote the set of all good configurations of $\mathcal{R}$
and let $\mathcal{C}$ denote the set of all good configurations of
$\mathcal{R}$ which puts an arbitrary number of agents in $\mathit{init}$,
exactly one agent in $\\#$ and zero agents elsewhere.

It then follows that the set
$\mathcal{S}:=\mathit{post}^{*}(([\mathit{init}],\\#))\cap\overline{\mathit{pre}^{*}(\uparrow\mathit{fin})}$
over $\mathcal{P}$ is finite iff the set
$\mathcal{S}^{\prime}:=(\mathit{post}^{*}(\mathcal{C})\cap\mathcal{I})\cap\overline{\mathit{pre}^{*}(\uparrow\mathit{fin})\cap\mathcal{I}}$
over $\mathcal{R}$ is finite. Similar to the proof of Lemma 5, we can decide
if this set is finite or not in . This gives the required upper bound.