The key to modifying ${\mathcal{A}}$ to obtain ${\mathcal{B}}$ is to treat
edges of $P^{\multimap}$ differently based on the conditions under which they
can (or cannot) be taken infinitely often in runs of
$(P^{\multimap})^{\infty}$. In particular, one has to distinguish between
edges that can appear infinitely often on a run with finitely or infinitely
many broadcasts, and among the latter between ones that can or cannot appear
unboundedly many times between two consecutive broadcasts. Note that the fact
that an edge is only used a bounded number of times between consecutive
broadcasts can be naturally tracked by the acceptance condition of a single
counter.

The rest of this section is organized as follows. We formally present the
classification of edges along the lines outlined above, and prove a couple of
easy lemmas about this classification. We then give the definition of the
automaton ${\mathcal{B}}$ and prove the correctness of the construction.

######  Definition  (Edge Types).

An edge $e$ of $P^{\multimap}$ is

  * •

_locally-reusable_ iff it appears infinitely many times on some run of
$(P^{\multimap})^{\infty}$ with finitely many broadcasts.

  * •

green iff it appears infinitely many times on some run of
$(P^{\multimap})^{\infty}$ with infinitely many broadcasts.

  * •

light green iff it appears unboundedly many times between broadcasts on some
run $\pi=\pi_{0}\pi_{1}\ldots$ of $(P^{\multimap})^{\infty}$ with infinitely
many broadcasts, i.e., if for every $n\in\mathbb{N}$ there are
$i<j\in\mathbb{N}$ such that $\pi_{i}\dots\pi_{j}$ contains $n$ transitions
using this edge and no broadcast edges.

  * •

dark green iff it is green but not light green.

Note that:

  * •

light green edges are also green,

  * •

dark green edges are exactly those green edges which satisfy that for every
run of $(P^{\multimap})^{\infty}$ there is a bound on the number of times they
appear between any two consecutive broadcasts,

  * •

green edges only belong to components of $P^{\multimap}$ that are on the loop
of the lasso,

  * •

broadcast edges can only be dark green.

######  Example 4.

Neither edge in $P^{\multimap}$ for the template $P$ in Figure 2 is locally-
reusable or green.

On the other hand, every edge in $P^{\multimap}$ for the template $P$ in
Figure 2 is dark green (and none are locally-reusable).

It turns out that determining the type of an edge is decidable; this is a non-
trivial problem, and we dedicate Section 7 to solving it.

We now characterize the edge types in terms of witnessing cycles in
$(P^{\multimap})^{\infty}$. Recall the definition of legal configuration and
path (Definition 5).

######  Lemma .

An edge $e$ of $P^{\multimap}$ is:

  1. (1)

locally-reusable iff it appears on a legal cycle $C_{e}$ of
$(P^{\multimap})^{\infty}$ that has no broadcasts.

  2. (2)

green iff it appears on a legal cycle $C_{e}$ of $(P^{\multimap})^{\infty}$
that has broadcasts.

  3. (3)

light green iff it appears on a legal cycle $D_{e}$ of
$(P^{\multimap})^{\infty}$ that has no broadcasts, that is contained in a
legal cycle $C_{e}$ with broadcasts;

  4. (4)

dark green iff it appears on a legal cycle $C_{e}$ of
$(P^{\multimap})^{\infty}$ that has broadcasts, but not on any cycle without
broadcasts that is contained in a cycle with broadcasts.

###### Proof.

Observe that it is enough to prove the first three items.

For the ‘if’ directions, let $n\in\mathbb{N}$ be the number of processes in
$C_{e}$ (i.e., $C_{e}$ is a cycle in $(P^{\multimap})^{n}$), and recall that
since $C_{e}$ is legal, its source configuration $f$ is in
$(P^{\multimap}_{i})^{n}$ for some $i$. Hence, by Lemma 5 (Loading), a
configuration $g$ such that
${\left.\kern-1.2ptg\vphantom{\big{|}}\right|_{[n]}}=f$ (i.e., the first $n$
processes of $g$ form the configuration $f$) can be reached from an initial
configuration of $(P^{\multimap})^{\infty}$; then, for items (i) and (ii), we
can simply pump $C_{e}$ forever (with the extra processes in $g$ moving only
on broadcasts). For item (iii), $C_{e}$ is pumped in the following way: for
every $i\in\mathbb{N}$, at the $i$’th repetition of the outer cycle $C_{e}$ we
pump the inner cycle $D_{e}$ for $i$ times.

The ‘only if’ directions follow from the observation that every run in
$(P^{\multimap})^{\infty}$ involves only finitely many processes, and thus
only finitely many distinct configurations, all of which are legal (by Remark
3). ∎

Lemma 6 implies that every light green edge is locally-reusable, whereas a
dark green edge may or may not be locally-reusable.666This overlap is the
reason that we decided to use the term “locally-reusable” instead of naming
these edges by another color. The following lemma states that we can assume
that the cycles in Lemma 6 that witness broadcasts all have the same number of
broadcasts.

######  Lemma .

There is a number $K$ such that for every green, light green, or dark green
edge $e$, the cycle $C_{e}$ mentioned in items ii), iii) and iv) in Lemma 6
can be taken to contain exactly $K$ broadcasts.

###### Proof.

Apply Lemma 6 to all the relevant edges in $P^{\multimap}$ and obtain cycles,
say $C_{e_{1}},C_{e_{2}},\cdots,C_{e_{l}}$. Suppose $C_{e_{i}}$ has $k_{i}$
broadcasts. Let $K$ be the least-common-multiple of the $k_{i}$s. By repeating
cycle $C_{e_{i}}$ for $K/k_{i}$ times, we obtain a witnessing cycle with
exactly $K$ broadcasts. ∎

We now informally describe the structure of the automaton ${\mathcal{B}}$. It
is made up of three copies of ${\mathcal{A}}$ (called
${{\mathcal{B}}^{init}}$, ${{\mathcal{B}}^{grn}}$, ${{\mathcal{B}}^{loc}}$) as
follows: ${\mathcal{B}}^{init}$ is an exact copy of ${\mathcal{A}}$; the copy
${\mathcal{B}}^{grn}$ has only the green edges left; and ${\mathcal{B}}^{loc}$
has only the locally-reusable edges left (and in particular has no broadcast
edges). Furthermore, for every edge $(s,\sigma,s^{\prime})$ in
${{\mathcal{B}}^{init}}$ we add two new edges, both with the same source as
the original edge, but one going to the copy of $s^{\prime}$ in
${\mathcal{B}}^{grn}$, and one to the copy of $s^{\prime}$ in
${\mathcal{B}}^{loc}$. The initial states of ${\mathcal{B}}$ are the initial
states of ${\mathcal{B}}^{init}$. The single counter increments at every
transition in ${\mathcal{B}}^{init}$ and at every dark green rendezvous edge
in ${\mathcal{B}}^{grn}$, and resets at every broadcast edge in
${\mathcal{B}}^{grn}$. In other words, the acceptance condition will enforce
that the run eventually leaves ${\mathcal{B}}^{init}$, and that boundedly many
dark green rendezvous edges are taken between broadcasts in
${\mathcal{B}}^{grn}$.

Here is the formal definition.

######  Definition  (B-Automaton ${\mathcal{B}}$).

Let

$P=\left\langle{\textit{AP},\Sigma_{\textsf{rdz}}\cup\\{\mathfrak{b}\\},S,I,R,\lambda}\right\rangle$

be a process template, and let
$P^{\multimap}=\left\langle{AP,\Sigma_{\textsf{rdz}}\cup\\{\mathfrak{b}\\},S^{\multimap},I^{\multimap},R^{\multimap},\lambda^{\multimap}}\right\rangle$
be its unwinding. Define the B-automaton
${\mathcal{B}}=\left\langle{\Sigma,S^{\prime},I^{\prime},R^{\prime},G,cc}\right\rangle$
as follows:

  * •

$\Sigma=2^{AP}$,

  * •

$S^{\prime}=\\{{init},{grn},{loc}\\}\times S^{\multimap}$,

  * •

$G=S^{\prime}$, i.e., the Büchi condition is always satisfied,

  * •

$I^{\prime}=\\{{init}\\}\times I^{\multimap}$,

  * •

The transition relation $R^{\prime}$ is
$\delta_{{init}}\cup\delta_{grn}\cup\delta_{loc}$ and the counter function
$cc$ are defined as follows. For every transition $e=(s,\sigma,t)\in
R^{\multimap}$

    1. (1)

$\delta_{{init}}$ contains the transitions
$\tau=((init,s),\lambda^{\multimap}(s),(i,t))$ for every
$i\in\\{{init},{grn},{loc}\\}$; and $cc(\tau)=\mathsf{inc}$.

    2. (2)

$\delta_{grn}$ contains the transition
$\tau=(({grn},s),\lambda^{\multimap}(s),({grn},t))$ only if $e$ is green;
$cc(\tau)=\mathsf{inc}$ if $e$ is a dark green rendezvous edge,
$cc(\tau)=\mathsf{reset}$ if $e$ is a broadcast edge, and otherwise
$cc(\tau)=\mathsf{skip}$;

    3. (3)

$\delta_{loc}$ contains the transition
$\tau=(({loc},s),\lambda^{\multimap}(s),({loc},t))$ only if $e$ is locally-
reusable; $cc(\tau)=\mathsf{skip}$.

Since transitions of ${\mathcal{B}}$ are induced by transitions of
$P^{\multimap}$, we call transitions of ${\mathcal{B}}$ broadcast, light
green, etc., based on the classification of the corresponding transition of
$P^{\multimap}$.

The rest of this section is concerned with proving that the construction is
correct:

######  Theorem .

For every RB-template $P$ the language of the B-automaton ${\mathcal{B}}$ is
$\textsc{exec-inf}({{P}^{\infty}})$.

#### Right-to-left direction.

Take $\alpha\in\textsc{exec-inf}({{P}^{\infty}})$. By Corollary 5 we have that
$\textsc{exec}({{{P}^{\infty}}})=\textsc{exec}({(P^{\multimap})^{\infty}})$.
Thus, there is some $\pi\in P^{\multimap}$ such that
$\alpha=\lambda^{\multimap}(\pi)$. We now show that there is an accepting run
of ${\mathcal{B}}$ on $\alpha$. First note that by Definition 5 and
Proposition 5, for every prefix of $\alpha$ there is a finite run on that
prefix that remains in ${\mathcal{B}}^{init}$. There are two cases: either
$\pi$ contains infinitely many broadcast transitions or not. If it does not,
then from some point on all edges on $\pi$ are locally-reusable. Thus, at that
point, the automaton can move from ${\mathcal{B}}^{init}$ to
${\mathcal{B}}^{loc}$. The resulting run is accepting since the counter is
never incremented in ${\mathcal{B}}^{loc}$. On the other hand, if $\pi$ has
infinitely many broadcast transitions, then from some point on, all its edges
are green. Thus, at that point, the automaton can move from
${\mathcal{B}}^{init}$ to ${\mathcal{B}}^{grn}$. Observe that the counter is
reset on every broadcast edge and it is only incremented on dark green edges,
which by Def. 6, appear only boundedly many times between broadcasts.

#### Outline of left-to-right direction.

Let $\Omega$ be an accepting run in ${\mathcal{B}}$ on input $\alpha$. By
Corollary 5 it is enough to construct a run $\pi$ in
$(P^{\multimap})^{\infty}$ whose projection on process $1$ has labeling
$\alpha$. Let $\beta$ be the run in $P^{\multimap}$ induced by $\Omega$
(recall that every transition of the automaton is induced by a transition of
$P^{\multimap}$). The construction of $\pi$ is guided by having process $1$
trace $\beta$. We decompose $\beta=\beta^{\prime}\cdot\beta^{\prime\prime}$
where $\beta^{\prime}$ corresponds to the finite prefix of the run $\Omega$
that stays in ${\mathcal{B}}^{init}$.

In order to trace $\beta^{\prime}$, we use the techniques in Section 5 for
finite traces. This leaves us with the task of tracing $\beta^{\prime\prime}$
which contains either only locally reusable edges or only green edges. First,
observe that tracing a broadcast edge is easy since we can simply append a
global broadcast transition to the run $\pi$ being constructed. On the other
hand, for each rendezvous edge $e$ we will assign multiple groups of processes
to help process $1$ traverse $e$ (the number of groups is discussed later).
Each group associated with $e$ has the property that it can trace a _cycle_
$C_{e}$ in which edge $e$ is taken at some point, say by process $p_{e}$. So,
if $e$ is the next edge that process $1$ should take, we progress some group
along the cycle $C_{e}$ to the point where $e$ should be taken, then process
$1$ swaps places with process $p_{e}$ (this is virtual, and merely re-assigns
process ids); and then the group takes the next transition along the cycle
$C_{e}$, and so process $1$ takes $e$. Note that in order for a group to be
available to assist process $1$ again in the future, it has to be ‘reset’,
i.e., put back to the same position just before the edge $e$ was taken. This
is done differently, depending on the type of $e$. If $e$ is locally-reusable,
then so are all subsequent edges $f,g,\dots$ that process $1$ should take; so,
since $C_{e},C_{f},C_{g},\dots$ contain no broadcasts, the group can simply
loop around $C_{e}$ immediately after process $1$ leaves $C_{e}$; when process
$1$ does leave $C_{e}$, it swaps with $p_{f}$ in $C_{f}$, and so on. If $e$ is
light green, then it is on an inner cycle $D_{e}$, without broadcasts, of
$C_{e}$ (Lemma 6), so the group can loop around $D_{e}$ after process $1$
swaps out — we call this _recharging_ — thus enabling it to help process $1$
again even though it has not yet completed the outer cycle $C_{e}$. Finally,
if $e$ is dark green, this group will only be ready again after the whole
cycle $C_{e}$ is looped once more, which requires waiting for $K$ broadcasts.
Thus, until that happens, if process $1$ needs to trace $e$ it will need the
help of another group associated with $e$. The key observation is that the
number of these groups is bounded. The reason for this is that $\Omega$ is an
accepting run, and thus one can deduce that there is a bound on the number of
times a dark green edge is used until the $K$ broadcasts needed to complete
the cycle $C_{e}$ are taken.

#### Detailed proof of left-to-right direction.

Let $\Omega$ be an accepting run in ${\mathcal{B}}$ on input $\alpha$. Since
every transition in ${\mathcal{B}}$ corresponds to a transition in
$P^{\multimap}$, let $\beta$ be the corresponding run in $P^{\multimap}$.
Since $\Omega$ is an accepting run, it either gets trapped in
${\mathcal{B}}^{grn}$ or it gets trapped in ${\mathcal{B}}^{loc}$. Decompose
$\Omega=\Omega^{\prime}\cdot\Omega^{\prime\prime}$ accordingly, i.e., the
prefix $\Omega^{\prime}$ corresponds to the run until it first enters
${\mathcal{B}}^{loc}$ or ${\mathcal{B}}^{grn}$. Decompose
$\alpha=\alpha^{\prime}\cdot\alpha^{\prime\prime}$ and
$\beta=\beta^{\prime}\cdot\beta^{\prime\prime}$ accordingly.

We are required to construct a run of ${{P}^{\infty}}$ whose projection on
process $1$ is labeled $\alpha$. By Corollary 5 it is enough to construct a
run $\pi$ of $(P^{\multimap})^{\infty}$ whose projection onto process $1$ is
labeled $\alpha$. We first construct a finite run $\rho^{\prime}$ of
$(P^{\multimap})^{\infty}$ whose projection on process $1$ is
$\beta^{\prime}$. Since $\Omega^{\prime}$ stays inside ${\mathcal{B}}^{init}$
it is actually also an accepting run of ${\mathcal{A}}$ on $\alpha^{\prime}$.
Thus, by Corollary 5, $\alpha^{\prime}\in\textsc{exec-fin}({{P}^{\infty}})$.
By Corollary 5 it is also in $\textsc{exec-fin}((P^{\multimap})^{\infty})$,
i.e., there is a run $\rho^{\prime}$ of $(P^{\multimap})^{t}$ for some number
$t$ of processes whose projection onto process $1$ is $\alpha^{\prime}$. Let
$P^{\multimap}_{l}$ be the component that the run $\rho^{\prime}$ ends in.

To complete the proof, we will construct an infinite path
$\rho^{\prime\prime}$ of $(P^{\multimap})^{n}$ for some number $n$ of
processes, satisfying the following: 1) its projection on process $1$ is
$\beta^{\prime\prime}$ (note that this implies that $\rho^{\prime\prime}$
starts in a configuration where process $1$ is in the same state as when it
ended $\rho^{\prime}$), and 2) it starts in a configuration in
$P^{\multimap}_{l}$. To see why this is enough to complete the proof, proceed
as follows in order to compose $\rho^{\prime}$ and $\rho^{\prime\prime}$.
Apply Lemma 5 (Loading) to get a finite run $\rho$ in
$(P^{\multimap})^{\infty}$ that has the same number of broadcasts as
$\rho^{\prime}$, and ends in a configuration that, when restricted to the
first $n$ processes, is the starting configuration of $\rho^{\prime\prime}$.
Note that $\rho^{\prime}$ may use $m>n$ processes in order to achieve that. By
Lemma 3.6, we can simultaneously simulate both $\rho$ and $\rho^{\prime}$ in a
run $\pi^{\prime}$ of $(P^{\multimap})^{t+m}$. Assume w.l.o.g. that the first
$t$ processes are simulating $\rho^{\prime}$, and that the next $n$ processes
are simulating the first $n$ processes of $\rho$. Thus, at the final
configuration of $\pi^{\prime}$, these $n$ processes are exactly in the states
needed to start simulating $\rho^{\prime\prime}$, and processes $1$ and $t+1$
are in the same state. Thus, we can extend the simulation by letting process
$1$ exchange roles with process $t+1$ and having processes $1,t+2,\dots t+n$
simulate $\rho^{\prime\prime}$ (with all other processes doing nothing except
responding to broadcasts). The resulting run $\pi$ has the property that its
projection onto process $1$ is labeled $\alpha$, as promised.

#### Constructing $\rho^{\prime\prime}$

First, assume w.l.o.g. that $P$ (and thus also $P^{\multimap}$) has no self
loops 777A template can be transformed, in linear time, to one without self
loops (and the same set of executions) as follows: for every state $s$ that
has a self loop, add a new state $\hat{s}$ with the same labeling, replace
every self loop $(s,\sigma,s)$ with $(s,\sigma,\hat{s})$, and for every
outgoing transition $(s,\sigma^{\prime},t)$, including self-loops, add the
transition $(\hat{s},\sigma^{\prime},t)$. — this is not essential, but
simplifies some technicalities in the construction. Second, we differentiate
between two cases, depending in which component $\Omega^{\prime\prime}$ is
trapped. We treat the case that $\Omega^{\prime\prime}$ is trapped in
${\mathcal{B}}^{grn}$ (the case that $\Omega^{\prime\prime}$ is trapped in
${\mathcal{B}}^{loc}$ is simpler, and does not use any new ideas). Note that
we will ignore the technicality of keeping track of process numbers, as we
find it distracts, rather then helps one understand the proof.

Let $E_{\textsf{light green}}$ (resp. $E_{\textsf{dark green}}$) be the set of
light green (resp. dark green) edges that appear on $\beta^{\prime\prime}$,
and note that these are the only edges that appear on it (by the fact that
${\mathcal{B}}^{grn}$ contains only green edges). For every edge $e\in
E_{\textsf{dark green}}$ (resp. $e\in E_{\textsf{light green}}$), let $C_{e}$
(resp. $C_{e},D_{e}$) be the witnessing cycle(s) with exactly $K$ broadcasts
(for some fixed $K$) from Lemma 6, and assume w.l.o.g. that (a) every such
cycle $C_{e}$ starts in a configuration in the component $P^{\multimap}_{l}$
in which $\rho^{\prime}$ ends, and (b) that if $e^{\prime}$ is the first edge
on $\beta^{\prime\prime}$, then $e^{\prime}$ appears in the first transition
taken in the cycle $C_{e^{\prime}}$. To see how to achieve (a) note that if
$e^{\prime}$ and each subsequent edge is locally-reusable, then because each
$C_{e}$ contains no broadcasts, each $C_{e}$ is contained in
$P^{\multimap}_{l}$. On the other hand, if the edges $e$ are green, then $e$
must be on the loop of the lasso, and so $P^{\multimap}_{l}$ is on the loop of
the lasso (since $e^{\prime}$ is), and so since $C_{e}$ contains at least one
broadcast, it must go through $P^{\multimap}_{l}$. Since $\Omega$ is an
accepting run, the counter is bounded on it. Thus, since in
${\mathcal{B}}^{grn}$ we increment the counter when reading a dark green edge,
and reset it when reading a broadcast edge, we can pick
$\mathfrak{m}\in\mathbb{N}$ such that every dark green edge appears at most
$\mathfrak{m}$ times on any section of $\beta$ that contains $K$ broadcasts.

Let the _designated occurrence_ of $e$ on $C_{e}$ be defined as follows: if
$e$ is dark green then it is the first transition in $C_{e}$ in which $e$
occurs, and if $e$ is light green then it is the first transition of $C_{e}$,
that is also on the nested cycle $D_{e}$, in which $e$ occurs. For every
$h\in[K]$, let $C_{e}(h)$ denote the portion of $C_{e}$ just after the $h-1$
broadcast up to (and including) the $h$ broadcast. For $h$ such that
$C_{e}(h)$ contains the designated occurrence of $e$ we divide $C_{e}(h)$
further into three pieces: $C_{e}(h,1)$ is the part up to the designated
occurrence, $C_{e}(h,2)$ is the designated occurrence, and $C_{e}(h,3)$ is the
remainder.

Take exactly enough processes to assign them to one copy $G_{e}^{1}$ of
$C_{e}$ for every $e\in E_{\textsf{light green}}$, and $\mathfrak{m}$ copies
$G_{e}^{1},\dots G_{e}^{\mathfrak{m}}$ of $C_{e}$ for every $e\in
E_{\textsf{dark green}}$.

Given a group of processes $G_{e}^{i}$, for some $i$ and $e$, we define the
following operations:

  * •

flush: $G_{e}^{i}$ simulates (using Lemma 3.6) the portion of $C_{e}(h)$ which
it has not yet simulated, up to but not including the broadcast;

  * •

load: in case $C_{e}(h)$ contains the designated occurrence of $e$, then
$G_{e}^{i}$ simulates (using Lemma 3.6) the path $C_{e}(h,1)$;

  * •

swap: we say that we _swap_ process $1$ into $G_{e}^{i}$ to mean that process
$1$ and process $j$ in $G_{e}^{i}$ (where $j$ is a process that will take the
edge $e$ the next time the designated transition will be reached by
$G_{e}^{i}$) exchange their group associations. I.e., process $1$ joins
$G_{e}^{i}$, and process $j$ takes its place in the former group of process
$1$;

  * •

recharge: if $e$ is light green, we say that we _recharge_ $C_{e}$ to mean
that the group $G_{e}^{i}$ simulates (using Lemma 3.6) tracing $D_{e}$ until
reaching (but not executing) the designated occurrence of $e$.

  * •

mark: if $e$ is dark green, we may mark a group $G_{e}^{i}$ as used or fresh
by setting or resetting a virtual flag.

Obviously (except for flush and mark), not every operation above can be taken
at any time. For example, a swap is allowed only at a time process $1$ and $j$
are in the same state (e.g., just after $G_{e}^{i}$ is loaded).

We are now ready to construct $\rho^{\prime\prime}$. The initial configuration
of $\rho^{\prime\prime}$ is obtained by having all processes at the beginning
of the cycles they were assigned to, and process $1$ assigned to the group
$G^{1}_{e^{\prime}}$ where $e^{\prime}$ is the first edge on
$\beta^{\prime\prime}$ (this can be done because $e^{\prime}$ appears in the
first transition taken in the cycle $C_{e^{\prime}}$). Note that this
satisfies the requirement that $\rho^{\prime\prime}$ starts in a configuration
in $P^{\multimap}_{l}$. The rest is done in blocks, where in the $i$’th block
we extend $\rho^{\prime\prime}$ with a path $\xi_{i}$ containing $K$
broadcasts and whose projection on process $1$ is the portion of
$\beta^{\prime\prime}$ after the $(i-1)K$ broadcast up to and including the
$iK$ broadcast — which we call $\beta^{\prime\prime}_{i}$. The construction
will ensure that $\xi^{\prime}$, defined as the concatenation of the
$\xi_{i}$s, weakly-simulates all the cycles of all the groups, and thus by
Remark 1, will maintain the following invariant $(\dagger)$: at the
configuration $f$ at the start of each block, the processes in every group of
the form $G_{e}^{i}$ are in states corresponding to the initial configuration
$g$ of $C_{e}$ (i.e.,
${\left.\kern-1.2ptf\vphantom{\big{|}}\right|_{G_{e}^{i}}}=g$). The invariant
obviously holds for the first block by our choice of the initial configuration
of $\rho^{\prime\prime}$.

For $i\in\mathbb{N}$, assume that blocks $<i$ have been constructed. We now
describe how to build block $i$. First, mark all the groups as _fresh_ , then
proceed in $K$ rounds by repeating the following algorithm for every $1\leq
h\leq K$. Let $e_{1},\dots e_{x}$ be the prefix of $\beta^{\prime\prime}_{i}$
not yet traced by process $1$, up to and including the next broadcast
(obviously, the length $x$ of this prefix depends on $h$). For every
$j\in[x]$, if $e_{j}$ is light green pick the group $G_{e_{j}}^{1}$; and if it
is dark green pick the first _fresh_ group from among the yet unpicked groups
in $G_{e_{j}}^{1},\dots G_{e_{j}}^{\mathfrak{m}}$, and mark this group as
_used_ (we can always pick a fresh group since — by our choice of
$\mathfrak{m}$, and since $\beta^{\prime\prime}_{i}$ has exactly $K$
broadcasts — there are at most $\mathfrak{m}$ occurrences of $e_{j}$ in
$\beta^{\prime\prime}_{i}$). Denote the group thus picked by
$\mathbb{G}_{e_{j}}$, and let $\mathbb{G}_{e_{0}}$ denote whatever group
process $1$ is in at the beginning of the round.

  1. (1)

For $1\leq j\leq x$ repeat:

    1. (a)

Load the group $\mathbb{G}_{e_{j}}$ and Swap process $1$ into it;

    2. (b)

if $j<x$ then have group $\mathbb{G}_{e_{j}}$ simulate the transition
$C_{e_{j}}(h,2)$, with process $1$ taking the edge $e_{j}$.

    3. (c)

If $j>1$, and $e_{j-1}$ is a light green edge, then recharge
$\mathbb{G}_{e_{j-1}}$.

  2. (2)

Flush all groups except $\mathbb{G}_{e_{x}}$ (that process $1$ is currently
in). Note that since $e_{x}$ is a broadcast, the loading of
$\mathbb{G}_{e_{x}}$ already put it in a flushed condition.

  3. (3)

Perform a broadcast (with process $1$ taking the broadcast edge $e_{x}$).

Since the invariant $(\dagger)$ holds at the start of each block, it is easy
to see that the algorithm can actually be executed. Indeed, the invariant
ensures that the algorithm can load when needed (and thus, swap and recharge
when needed). It is not hard to see that, as promised, the resulting path
$\xi_{i}$ weakly-simulates all the cycles of all the groups. To see that the
projection of $\xi_{i}$ on process $1$ is $\beta^{\prime\prime}_{i}$, observe
that the moves performed by process $1$ in lines $1(b)$ and $3$ of the
algorithm trace exactly $\beta^{\prime\prime}_{i}$. Furthermore, process $1$
is moved only in these lines since, by our assumption that $P^{\multimap}$
contains no self loops, every edge in $\beta^{\prime\prime}$ is different than
the edge just before and just after it and thus, process $1$ is never in a
group when it is being loaded (except at the very beginning of the first
block, in which case the load in line $1(a)$ of the algorithm does nothing
since this group is already in a loaded position in the initial configuration
of $\rho^{\prime\prime}$).

This completes the proof of Theorem 6.

In Section 7 we will show how to decide the type of the edges in
$P^{\multimap}$ (Theorem 7) in polynomial time in the size of $P^{\multimap}$.
Thus, we can build the B-automaton ${\mathcal{B}}$ in exponential time in the
size of $P$. Combining this with Theorem 6 we get Theorem 3 that says that the
PMCP for NBW/LTL specifications of RB-systems can be solved in exptime.

###### Proof of Theorem 3.

We reduce the PMCP problem to the emptiness problem for B-automata.

Given a process template $P$, and the corresponding B-automaton
${\mathcal{B}}$ (whose Büchi set is trivial), suppose the specification is
given as an LTL formula $\varphi$ (the case of NBW is given afterwards). Let
$L({\mathcal{B}})$ denote the language of ${\mathcal{B}}$, and let
$L(\lnot\varphi)$ denote the set of models of $\lnot\varphi$. Then, every
execution in $\textsc{exec-inf}({{P}^{\infty}})$ satisfies $\varphi$ if and
only if $L({\mathcal{B}})\cap L(\lnot\varphi)=\emptyset$. Using Theorem 2.3,
let ${\mathcal{A}}_{\lnot\varphi}$ be an NBW accepting all models of
$\lnot\varphi$, and denote its states by $Q$ and its Büchi set by $G$. Build
the synchronous product of ${\mathcal{A}}_{\lnot\varphi}$ and ${\mathcal{B}}$
to get an NBW with one counter, call it $M$, whose language is equal to
$L({\mathcal{B}})\cap L({\mathcal{A}}_{\lnot\varphi})$. By Lemma 2.2, one can
test whether $L(M)$ is empty in ptime. Thus, this PMCP algorithm is
exponential in the size of the template $P$ (since computing ${\mathcal{B}}$
can be done in time exponential in the size of $P$) and exponential in the
size of $\varphi$ (since computing ${\mathcal{A}}_{\lnot\varphi}$ can be done
in time exponential in the size of $\varphi$).

For the case that the specification is an NBW ${\mathcal{A}}$, we proceed in a
similar way by noting that we can build an NBW ${\mathcal{A}}^{\prime}$ for
the complement of $L({\mathcal{A}})$ in time exponential in the size of
${\mathcal{A}}$ (see for example [Saf88]).

∎

##  7\. Deciding Edge Types

This section is dedicated to proving the following result:

######  Theorem .

Given a reachability-unwinding $P^{\multimap}$ of a process template $P$, the
type (light green, dark green, and locally-reusable) of each edge $e$ in
$P^{\multimap}$ can be decided in ptime (in the size of $P^{\multimap}$).

We will develop the proof of Theorem 7 in several steps:

1. The starting point for the proof of Theorem 7 is the characterization of edge types in Lemma 6 through the existence (or lack thereof) of suitable cycles in $(P^{\multimap})^{\infty}$. In Subsection 7.1, we weaken this characterization using the notion of _pseudo-cycles_. Pseudo cycles are paths that start and end in configurations that are identical up to the renaming of processes, i.e., there are exactly the same number of processes in every state, though the identities of the processes in each of the states may differ. Pseudo-cycles can always be pumped to a cycle by iterating the pseudo-cycle until the initial configuration is reached again. Hence, pseudo-cycles can be seen as more compact representations of cycles. Importantly, we are able to obtain a bound on the number of broadcasts in pseudo-cycles, which we need for deciding edge types.

2. In order to be able to conveniently reason about pseudo-cycles we will work with counter abstractions of R-Systems: In Subsection 7.2, we define vector rendezvous systems (VRS) and their continuous relaxation, called continuous vector rendezvous systems (CVRS). The notions of VRSs and CVRS are inspired by the notion of Vector Addition Systems (VAS) [HP79], where configurations only store the number of processes for every process state but not the identity of the processes. VRSs are counter abstractions of R-Systems; in particular, pseudo-cycles of R-Systems correspond to cycles in VRSs and vice versa. CVRSs are a continuous relaxation of VRSs in which steps can be taken by a rational fraction. CVRSs have the advantage that we can characterize reachability and the existence of cycles in them by solving linear programming problems over the rationals. We will be able to work with CVRs instead of VRSs because we will show that we can scale a CVRSs cycle to a VRS cycle (as we are interested in the parameterized verification problem we can always scale the number of processes). We then reduce the existence of witnessing pseudo-cycles for the type of an edge to corresponding reachability statements for CVRSs, as outlined below.

3. In Subsection 7.3, we develop a characterization of reachability for CVRSs. This characterization will give rise to an equation system and a fixed point algorithm, which is the basis for our edge type computation procedure. The results in this subsection already allow us to compute the locally-reusable edges and the light green edges (under the assumption that the green edges are already known; the computation of the green edges is, however, only done in the next subsection).

4. In Subsection 7.4, we show how to decide whether an edge of $P^{\multimap}$ is green. This problem represents the main difficulty in deciding the type of an edge. We give an algorithm that computes all green edge of $P^{\multimap}$ and prove its correctness. We further remark that, though not actually needed, one can derive a pseudo-cycle that contains all green edges from our procedure.

###  7.1. Pseudo-cycles

######  Definition .

Let $P$ be an RB-template with state set $S$, and let $n\in\mathbb{N}$. Two
configurations $f,f^{\prime}$ of ${{P}^{n}}$ are called _twins_ if every state
is covered by the same number of processes in $f$ and $f^{\prime}$, i.e.
$|f^{-1}(q)|=|f^{\prime-1}(q)|$ for every $q\in S$.

Let $g\circ h$ denote the composition $g(h(\cdot))$. Observe that
$f,f^{\prime}$ are twins if and only if there is a (not necessarily unique)
permutation $\theta:[n]\to[n]$ such that $f^{\prime}=f\circ\theta$.
Intuitively, $\theta$ maps each process in $f^{\prime}$ to a matching process
in $f$ (i.e., one in the same state). Thus, given a transition
$f\xrightarrow{{\sigma}}g$, say $t$, in ${{P}^{n}}$, we denote by $t[\theta]$
the transition $f\circ\theta\xrightarrow{{\sigma^{\prime}}}g\circ\theta$
resulting from replacing process $i$ with process $\theta(i)$ in $t$; and
having $\sigma^{\prime}=\mathfrak{b}$ if $\sigma=\mathfrak{b}$, and
$\sigma^{\prime}=((\theta^{-1}(i_{1}),{a}_{1}),\dots,(\theta^{-1}(i_{k}),{a}_{k}))$
if $\sigma=((i_{1},{a}_{1}),\dots,(i_{k},{a}_{k}))$. Note that the rendezvous
or broadcast action of the transition taken in $t$ and $t[\theta]$ are the
same — it is only the identities of the processes involved that are different.
Extend $\theta$ to paths point-wise, i.e., if $\pi=t_{1}t_{2}\ldots$ is a path
then define $\pi[\theta]=t_{1}[\theta]t_{2}[\theta]\ldots$.

######  Definition .

A finite path $\pi$ of an RB-system ${{P}^{n}}$ is a pseudo-cycle if
$\textsf{src}(\pi)$ and $\textsf{dst}(\pi)$ are twins.

Obviously, every cycle is also a pseudo-cycle, but not vice-versa. For
example, for $P$ in Figure 7, the following path in ${{P}^{4}}$ is a pseudo-
cycle that is not a cycle:
$(p,q,q,r)\xrightarrow{((3,{c}_{1}),(4,{c}_{2}))}(p,q,r,p)\xrightarrow{((2,{c}_{1}),(3,{c}_{2}))}(p,r,p,p)\xrightarrow{((3,{a}_{1}),(4,{a}_{2}))}(p,r,q,q)$.

$p$start$q$$r$start${a}_{1}$${a}_{2}$${c}_{2}$${c}_{1}$

Figure 6. R-template.

$p$start$q$${a}_{1}$$\mathfrak{b}$${a}_{2}$$\mathfrak{b}$

Figure 7. RB-template.

######  Remark 6.

Similar to cycles, for which one can chose any point on the cycle as its start
(and end) point, one can chose any point along a pseudo-cycle as the start
point. Indeed, if $C$ is a pseudo-cycle that starts in a configuration $f$ and
ends in a twin $f^{\prime}$, then given any configuration $g$ along $C$ we can
obtain a new pseudo-cycle, that uses exactly the same edges (but with possibly
different processes taking these edges) as follows: start in $g$ and traverse
the suffix of $C$ until $f^{\prime}$, reassign process id’s according to the
permutation transforming $f$ to $f^{\prime}$ and traverse the prefix of $C$
from $f$ to $g$ using these reassigned processes to reach a twin $g^{\prime}$
of $g$.

The following immediate lemma states that every pseudo-cycle $\pi$ can be
pumped to a cycle.

######  Lemma .

Given a pseudo-cycle (resp. legal pseudo-cycle) $\pi$ in ${{P}^{n}}$, and a
permutation $\theta$ such that
$\textsf{dst}(\pi)=\textsf{src}(\pi)\circ\theta$, then there is a $z\geq 1$
such that

$\pi[\theta^{0}]\pi[\theta^{1}]\pi[\theta^{2}]\ldots\pi[\theta^{z-1}],$

is a cycle (resp. legal cycle) in ${{P}^{n}}$, where $\theta^{j}$ denotes the
composition of $\theta$ with itself $j$ times.

###### Proof.

We can choose $z$ such that the permutation $\theta^{z}$ is the identity
(recall that the set of permutations of a finite set forms a finite group, and
that the order of every element in a finite group is finite, i.e., there is
some $z\in\mathbb{N}$ such that $\theta^{z}$ is the identity permutation). We
observe that
$\textsf{dst}(\pi[\theta^{0}]\pi[\theta^{1}]\pi[\theta^{2}]\ldots\pi[\theta^{z-1}])=\textsf{src}(\pi)\circ\theta^{z}=\textsf{src}(\pi)$,
and thus it is a cycle. ∎

Recall that $n,r$ denote the prefix-length and period of $P^{\multimap}$,
respectively. The following lemma states that we can assume that if an edge of
$P^{\multimap}$ appears on a pseudo-cycle with broadcasts then it also appears
on one with exactly $r$ broadcasts. Knowing this bound will be crucial for
decidability of edge types (in contrast, Lemma 6 only says that a bound
exists), as well as for obtaining good complexity for deciding PMCP.

######  Lemma  (Spiral).

An edge $e$ appears on a legal pseudo-cycle $D$ in $(P^{\multimap})^{\infty}$,
which contains broadcasts, iff it appears on a legal pseudo cycle $C$ of
$(P^{\multimap})^{\infty}$, containing exactly $r$ broadcasts and starting in
a configuration in $P^{\multimap}_{n}$.

###### Proof.

Assume $D$ is a legal pseudo-cycle in $(P^{\multimap})^{m}$, for some
$m\in\mathbb{N}$. By Remark 6 we can assume w.l.o.g. that $D$ starts and ends
in a configuration in $P^{\multimap}_{n}$. Observe that (by the lasso
structure of $P^{\multimap}$) $D$ must have $lr$ broadcast transitions for
some $l\in\mathbb{N}$, and that after every $r$ broadcasts all processes are
in $P^{\multimap}_{n}$. Let $f_{0}$ be the initial configuration on $D$. For
every $i\in[l]$, let $f_{i}$ be the configuration in $D$ just after $ir$
broadcasts, and let $\rho_{i}$ be the portion of $D$ from $f_{i-1}$ to
$f_{i}$. Observe that $\rho_{i}$ contains exactly $r$ broadcasts. By Lemma
3.6, we can compose the paths $\rho_{1},\dots\rho_{l}$ into a single path $C$
in the system $(P^{\multimap})^{ml}$ with $ml$ processes. It is not hard to
see that $C$ is a legal pseudo-cycle. Indeed, after $r$ broadcasts the
processes that were simulating $\rho_{i}$ are in states that match the
configuration $f_{(i+1)\bmod l}$, i.e., the configuration that the processes
that simulate $\rho_{(i+1)\bmod l}$ started in. Obviously, $e$ appears on $C$,
which completes the proof. ∎

We now use the notion of a pseudo-cycle to give a characterization of the
edges types that is easier to detect than the one given in Section 6:

######  Lemma .

An edge $e$ of $P^{\multimap}$ is:

  1. (1)

locally-reusable iff it appears on a legal pseudo-cycle $C_{e}$ of
$(P^{\multimap})^{\infty}$ without broadcasts.

  2. (2)

green iff it appears on a legal pseudo-cycle $C_{e}$ of
$(P^{\multimap})^{\infty}$ with $r$ broadcasts.

  3. (3)

light green iff it appears on a legal pseudo-cycle $C_{e}$ of
$(P^{\multimap})^{\infty}$ without broadcasts that only uses green edges;

  4. (4)

dark green iff it is green and does not appear on a legal pseudo-cycle $C_{e}$
of $(P^{\multimap})^{\infty}$ without broadcasts that only uses green edges.

###### Proof.

Item 4 follows from item 3 since green edges are partitioned to light green
and dark green edges.

Items 1 and 2 follow immediately from Lemmas 6 and 7.1 and the fact that every
cycle is also a pseudo-cycle (for the ‘only if’ direction of item 2 use Lemma
7.1 to obtain a pseudo-cycle with exactly $r$ broadcasts). The same fact,
combined with Lemma 6, gives the ’only if’ direction of item 3.

For the ‘if’ direction of item 3, we claim that it is enough to show that:
($\dagger$) there is a configuration $f$ of $(P^{\multimap})^{\infty}$ and two
pseudo-cycles $C,D$ starting in $f$, such that $D$ contains broadcasts, and
$C$ contains the edge $e$ and no broadcasts. Indeed, by Lemma 7.1, one can
pump $C,D$ to obtain cycles $C^{\prime},D^{\prime}$ starting and ending in
$f$, and the ‘figure-eight’ cycle obtained by concatenating $C^{\prime}$ to
$D^{\prime}$ is (according to Lemma 6) a cycle witnessing that the edge $e$ is
light green.

We now show that if $e$ appears on a pseudo-cycle $C_{e}$ satisfying item 3
then $(\dagger)$ holds. Let $g$ be the initial configuration of $C_{e}$ and
let $H:=\\{s\mid g(s)>0\\}$ be the set of states of $P^{\multimap}$ for which
there is some process in that state in $g$. Assume w.l.o.g. that there is no
process that does not move on $C_{e}$ (such processes can simply be removed),
and for every $s\in H$, let $e^{s}$ be some edge in $P^{\multimap}$ appearing
in $C_{e}$ whose source is $s$. Observe that by item 3 the edge $e^{s}$ is
green, and apply Lemma 6 to obtain a witnessing cycle $C_{e^{s}}$ starting
with some process in $s$. By Lemma 6, we can assume that the cycles
$C_{e^{s}}$ thus obtained for all states in $H$ have the same number of
broadcasts. Hence, by Lemma 3.6, we can run together $g(s)$ copies of
$C_{e^{s}}$, for all $s$ in $H$, in one cycle $D$. Let $f$ be the starting
configuration of $D$. Note that $f(s)\geq g(s)$ for every state $s$ in
$P^{\multimap}$, and obtain a pseudo-cycle $C$ starting in $f$ which simulates
$C_{e}$ (since $C_{e}$ has no broadcasts, processes that $f$ has in excess of
$g$ can simply not move). The proof is complete by noting that $f,C$ and $D$
satisfy $\dagger$. ∎

###  7.2. Vector Rendezvous Systems

We now formally introduce VRSs and CVRSs. We recall that $k$ denotes the
number of processes participating in a rendezvous, $\Sigma_{\textsf{actn}}$
denotes a finite set of rendezvous actions, and
$\Sigma_{\textsf{rdz}}=\cup_{{a}\in\Sigma_{\textsf{actn}}}\\{{a}_{1},\dots,{a}_{k}\\}$
denotes the _rendezvous alphabet_.

Given a finite set $S$, we can think of $\mathbb{Q}^{S}$ as the set of
rational vectors of dimension $|S|$, and we use the elements of $S$ as indices
into these vectors. We also use the standard operations of vector addition and
scalar multiplication. Finally, we compare vectors point-wise, i.e., given
$c,c^{\prime}\in\mathbb{Q}^{S}$ we say that $c\leq c^{\prime}$ iff $c(s)\leq
c^{\prime}(s)$ for all $s\in S$.

Continuous Vector Rendezvous System (CVRS). A _continuous vector rendezvous
system_ (CVRS) is a tuple
${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$, where
$S$ is a finite set of states and $R\subseteq
S\times\Sigma_{\textsf{rdz}}\times S$ is a finite set of _transitions_. The
_configurations_ of ${\mathcal{V}}$ are the vectors $\mathbb{Q}_{\geq 0}^{S}$.
For a transition $t=(p,\sigma,q)$, we denote by $\textsf{rdz}(t)=\sigma$ its
rendezvous symbol, by $\textsf{src}(t)=p$ the _source_ state of $t$, and by
$\textsf{dst}(t)=q$ the _destination_ state of $t$. Also, we denote by
$\textsf{out}(t)\in\\{0,1\\}^{S}$ the vector that has a $1$ entry at index $p$
and zero entries otherwise, and by $\textsf{in}(t)\in\\{0,1\\}^{S}$ the vector
that has a $1$ entry at index $q$ and zero entries otherwise. We now define
what it means for a CVRS to take a step.

######  Definition  (Step of a CVRS).

Given a $k$-tuple $\mathbf{\mathfrak{t}}=(t_{1},\ldots,t_{k})$ of transitions
in $R$, the CVRS ${\mathcal{V}}$ can _step_ with _multiplicity_
$\alpha\in\mathbb{Q}_{>0}$ from a configuration $c$ to a configuration
$c^{\prime}$ using transitions $\mathbf{\mathfrak{t}}=(t_{1},\ldots,t_{k})$,
denoted $c\xrightarrow{t_{1},\ldots,t_{k}:\alpha}c^{\prime}$, or
$c\xrightarrow{\mathbf{\mathfrak{t}}:\alpha}c^{\prime}$, if:

  1. (1)

there is an action ${a}\in\Sigma_{\textsf{actn}}$ such that
$\textsf{rdz}(t_{i})={a}_{i}$ for all $i\in[k]$,

  2. (2)

$c\geq\alpha\sum_{i=1}^{k}\textsf{out}(t_{i})$, and

  3. (3)

$c^{\prime}=c+\alpha\sum_{i=1}^{k}\left(\textsf{in}(t_{i})-\textsf{out}(t_{i})\right)$.

A step is said to _synchronize_ on ${a}$. We say that a transition $t\in R$
_participates_ in a step $c\xrightarrow{t_{1},\ldots,t_{k}:\alpha}c^{\prime}$
if $t=t_{i}$ for some $i\in[k]$.

A _trace_ of ${\mathcal{V}}$ is a sequence of steps
$c_{1}\xrightarrow{\mathbf{\mathfrak{t}}_{1}:\alpha_{1}}c_{2}\xrightarrow{\mathbf{\mathfrak{t}}_{2}:\alpha_{2}}\cdots
c_{n}$. We say that a configuration $c^{\prime}$ is _reachable_ from
configuration $c$, denoted $c\rightarrow^{\star}c^{\prime}$, if there is a
trace
$c_{1}\xrightarrow{\mathbf{\mathfrak{t}}_{1}:\alpha_{1}}c_{2}\xrightarrow{\mathbf{\mathfrak{t}}_{2}:\alpha_{2}}\cdots
c_{n}$, with $c=c_{1}$ and $c^{\prime}=c_{n}$.

Vector Rendezvous System (VRS). A _vector rendezvous system (VRS)_ , is a
restriction of a CVRS, where the set of configurations is $\mathbb{N}_{0}^{S}$
and all steps are restricted to have multiplicity $\alpha=1$. Given any VRS
${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$, the
_relaxation_ of ${\mathcal{V}}$ is the same tuple interpreted as a CVRS. Since
a natural number is also rational, it is obvious that any VRS
${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ is also a
CVRS.

Note that every trace of a VRS is also a trace of its relaxation, and that the
relaxation has more traces than the VRS since every rational multiple of a
step in the VRS is a step in its relaxation.

######  Remark 7.

Every R-template
$P=\left\langle{\textit{AP},\Sigma_{\textsf{rdz}},S,I,R,\lambda}\right\rangle$
defines a VRS
${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ with the
same set of rendezvous alphabet, states, and transitions. These two systems
are closely related. Intuitively, ${\mathcal{V}}$ is an abstraction of
${{P}^{\infty}}$ in the sense that it does not keep track of the state of
every individual process, but only keeps track of the number of processes in
every state. More formally, every configuration $f\in{{P}^{\infty}}$ induces a
configuration $c$ of ${\mathcal{V}}$, called its _counter representation_ ,
defined as $c(s):=|f^{-1}|(s)$ for $s\in S$, i.e., $c(s)$ is the number of
processes of $f$ that are in state $s$. Furthermore,
$c\xrightarrow{t_{1},\cdots,t_{k}}c^{\prime}$ is a step of ${\mathcal{V}}$ if
and only if there is a global transition $(f,\sigma,f^{\prime})$ in
${{P}^{\infty}}$ such that $c$ and $c^{\prime}$ are the counter
representations of $f$ and $f^{\prime}$ respectively, and $t_{1},\cdots,t_{k}$
are exactly the rendezvous edges taken by the $k$ active processes in the
transition $(f,\sigma,f^{\prime})$.

We now define operations for manipulating traces. Given a trace
$\xi:=c_{1}\xrightarrow{\mathbf{\mathfrak{t}}_{1}:\alpha_{1}}c_{2}\xrightarrow{\mathbf{\mathfrak{t}}_{2}:\alpha_{2}}\cdots
c_{n}$ of a CVRS ${\mathcal{V}}$, we define the following two operations:

  1. (1)

Multiplication by a scalar $0<\gamma$: Let $\gamma\otimes\xi$ be the trace
$\gamma c_{1}\xrightarrow{\mathbf{\mathfrak{t}}_{1}:\gamma\alpha_{1}}\gamma
c_{2}\xrightarrow{\mathbf{\mathfrak{t}}_{2}:\gamma\alpha_{2}}\cdots\gamma
c_{n}$.

  2. (2)

Addition of a constant configuration $c$: let $c\oplus\xi$ be the trace
$c+c_{1}\xrightarrow{\mathbf{\mathfrak{t}}_{1}:\alpha_{1}}c+c_{2}\xrightarrow{\mathbf{\mathfrak{t}}_{2}:\alpha_{2}}\cdots
c+c_{n}$.

It is not hard to see, by consulting the definition of a step, that
$\gamma\otimes\xi$ and $c\oplus\xi$, are indeed traces of ${\mathcal{V}}$.
Note, however, that multiplying by a scalar $\gamma<0$ would not yield a
trace, and that adding a vector $c$ that is not a configuration (i.e., which
has negative coordinates) may sometimes also not yield a trace — either
because intermediate points may not be configurations (due to having some
negative coordinates), or since condition (ii) in the definition of a step
(Definition 7.2) is violated. Finally, traces in CVRSs have a _convexity
property_ that states that by taking a fraction $0<\gamma<1$ of each step of a
trace $c\rightarrow^{\star}c^{\prime}$ one obtains a trace from $c$ to the
convex combination $(1-\gamma)c+\gamma c^{\prime}$:

######  Proposition  (convexity).

Let
$\xi:=c_{1}\xrightarrow{\mathbf{\mathfrak{t}}_{1}:\alpha_{1}}c_{2}\xrightarrow{\mathbf{\mathfrak{t}}_{2}:\alpha_{2}}\cdots
c_{n}$ be a trace of a CVRS ${\mathcal{V}}$, and let $0<\gamma<1$ be rational.
Define configurations $c_{i}^{\prime}:=\gamma c_{i}+(1-\gamma)c_{1}$ for
$1<i\leq n$. Then
$\xi^{\prime}:=c_{1}\xrightarrow{\mathbf{\mathfrak{t}}_{1}:\gamma\alpha_{1}}c_{2}^{\prime}\xrightarrow{\mathbf{\mathfrak{t}}_{2}:\gamma\alpha_{2}}\cdots
c_{n}^{\prime}$ is a trace of ${\mathcal{V}}$.

###### Proof.

Simply observe that $\xi^{\prime}$ is the trace
$((1-\gamma)c_{1})\oplus(\gamma\otimes\xi)$. ∎

In the following two lemmas we combine Remark 7 with Lemma 7.1 in order to
rephrase the characterization of edge types in terms of the existence of
certain CVRSs traces. We begin by characterizing the locally-reusable edges
and the light green edges (relative to green edges):

######  Lemma .

An edge $e$ of $P^{\multimap}$ is locally-reusable iff $e$ participates in a
step of a cyclic trace of some component $P^{\multimap}_{i}$ considered as
CVRS, i.e., iff $e$ participates in a step of a trace
$\xi:=c\rightarrow^{\star}c$ of CVRS $P^{\multimap}_{i}$. Moreover, $e$ is
light green iff $\xi$ uses only green edges.

###### Proof.

We start with the ‘only if’ direction. By Lemma 7.1 there is a legal pseudo-
cycle $C$, which contains $e$, and which does not contain broadcasts. Because
$C$ does not contain broadcasts, we have that all configurations of $C$ are in
some component $P^{\multimap}_{i}$ of $P^{\multimap}$. Let $f$ be the initial
configuration of $C$, and let $c$ be its counter representation. By Remark 7,
$C$ induces a trace $\xi:=c\rightarrow^{\star}c$ in the VRS corresponding to
$P^{\multimap}_{i}$, and $e$ participates in a step of $\xi$. As every VRS is
a CVRS the claim follows.

For the other direction, let $e$ participate in a step of some trace
$\xi:=c\rightarrow^{\star}c$ of the CVRS corresponding to $P^{\multimap}_{i}$.
Let $x$ be the least common multiple of all the denominators that appear in
the multiplicities of any step, or any coordinate of any configuration of
$\xi$. Consider the trace $x\otimes\xi:=xc\rightarrow^{\star}xc$. Observe that
all configurations on this trace are in $\mathbb{N}_{0}^{S_{i}}$, and that all
steps on it are taken with an integer multiplicity. By replacing every step
that uses a multiplicity $y\in\mathbb{N}$ with $y$ consecutive steps each with
multiplicity $1$, we obtain a trace
$\varrho:=xc_{i}\rightarrow^{\star}xc^{\prime}_{i}$ in $P^{\multimap}_{i}$
considered as VRS. By Remark 7, there is a corresponding pseudo-cycle $C$ of
$P^{\multimap}_{i}$, and $e$ appears on $C$. The claim then follows from Lemma
7.1. ∎

We now turn to characterizing the green edges.

For the statement of the lemma, recall (see Section 5) that the template
$P^{\multimap}$ is built from component templates arranged in a lasso
structure. Let $\mathcal{I}:=\\{n,n+1,\ldots,n+r-1=m\\}$ be the set of indices
of the components on the noose of $P^{\multimap}$, and for every
$i\in\mathcal{I}$ define $next(i)$ (resp. ${\rm Phys.~{}Rev.~{}E}{i}$) to be
the component number immediately following $i$ (resp. preceding $i$) along the
noose. Note that, in particular, $next(n+r-1)=n$ and ${\rm
Phys.~{}Rev.~{}E}{n}=n+r-1$.

######  Lemma .

An edge $e$ of $P^{\multimap}$ is green iff, for every $i\in\mathcal{I}$: (i)
there is a subset ${\mathcal{T}}_{i}$ of the transitions of
$P^{\multimap}_{i}$, and a subset $B_{i}$ of the broadcast transitions from
$P^{\multimap}_{i}$ to $P^{\multimap}_{next(i)}$; (ii) there are coefficients
$\alpha_{t}\in\mathbb{Q}_{>0}$ for every $t\in B_{i}$; and (iii) there is a
trace $\xi_{i}:=c_{i}\rightarrow^{\star}c_{i}^{\prime}$ of the CVRS of
$P^{\multimap}_{i}$ using exactly the transitions ${\mathcal{T}}_{i}$; such
that: $e\in\cup_{i\in\mathcal{I}}(B_{i}\cup{\mathcal{T}}_{i}$), and for all
$q\in S^{\multimap}_{i}$ the following holds:

  1. (1)

$c_{i}(q)=\sum_{t\in B_{{\rm
Phys.~{}Rev.~{}E}{i}},\textsf{dst}(t)=q}\alpha_{t}$.

  2. (2)

$c^{\prime}_{i}(q)=\sum_{t\in B_{i},\textsf{src}(t)=q}\alpha_{t}$.

###### Proof.

By Lemma 7.1, it is enough to show that $e$ appears on a pseudo-cycle $C$,
with $r$ broadcasts, of $(P^{\multimap})^{\infty}$ iff the conditions of the
lemma hold. First, assume that such a pseudo-cycle $C$ exists. For every $i\in
I$, let $f_{i}$ (resp. $f^{\prime}_{i}$) be the configurations of $C$ in
$P^{\multimap}_{i}$ just after (resp. just before) a broadcast, let $C_{i}$ be
the sub-path of $C$ from $f_{i}$ to $f^{\prime}_{i}$, let ${\mathcal{T}}_{i}$
be the process transitions appearing on $C_{i}$. By Remark 7, $C_{i}$ induces
a trace $\xi_{i}:=c_{i}\rightarrow^{\star}c_{i}^{\prime}$ of the CVRS of
$P^{\multimap}_{i}$, using exactly the transitions in ${\mathcal{T}}_{i}$,
where $c_{i},c^{\prime}_{i}$ are the counter representations of
$f_{i},f^{\prime}_{i}$. Consider now the global broadcast transition of $C$
from $f^{\prime}_{i}$ to $f_{next(i)}$, let $B_{i}$ be the set of local
broadcast transitions that participate in it, and for every $t\in B_{i}$ let
$\alpha_{t}$ to be the number of processes in $f^{\prime}_{i}$ that take $t$.
It is easy to see that the conditions of the lemma are satisfied.

For the other direction, assume that sets ${\mathcal{T}}_{i}$ and $B_{i}$,
coefficients $\alpha_{t}$, and traces $\xi_{i}$ satisfying the conditions of
the lemma exist. Using the same argument as in the proof of Lemma 7.2 — by
taking $x$ to be the least common multiple of all the denominators that appear
in the multiplicities of any step or any coordinate of any configuration of
these traces, as well as any of the coefficients $\alpha_{t}$ — we can obtain
from each trace $\xi_{i}$ a trace
$\varrho_{i}:=xc_{i}\rightarrow^{\star}xc^{\prime}_{i}$ in the VRS
corresponding to $P^{\multimap}_{i}$. We can now build the required pseudo-
cycle $C$ in $r$ rounds. We start by (arbitrarily) picking some
$i_{i}\in\mathcal{I}$, and a configuration $f_{i_{1}}$ whose counter
representations is $xc_{i_{1}}$. At each round $j$, we extend $C$ by
concatenating a path (obtained from $\varrho_{i_{j}}$ by Remark 7) from
$f_{i_{j}}$ to a configuration $f^{\prime}_{i_{j}}$ whose counter
representation is $xc^{\prime}_{i_{j}}$; we then append a global broadcast
transition in which each edge $t\in B_{i_{j}}$ is taken by exactly
$x\alpha_{t}$ processes, resulting in a configuration $f_{i_{j+1}}$ whose
counter representation is $xc_{next(i_{j})}$ (this is possible by equations
(1) and (2) in the conditions of the lemma).

It follows that, at the end of the last round, $C$ is a path in
$(P^{\multimap})^{\infty}$ from $f_{i_{1}}$ to $f_{i_{r+1}}$, whose counter
representations are $xc_{i_{1}}$ and $xc_{next^{r}(i_{1})}=xc_{i_{1}}$,
respectively. Thus, $C$ is a pseudo-cycle. ∎

In Lemmas 7.2 and 7.2 we have related edge-types to the existence of certain
CVRS traces. Developing a criterion for the existence of CVRS traces is the
subject of the next subsection. Having developed this characterization, we can
replace the existence of CVRS traces with this criterion in the two lemmas
mentioned. This will then allow us to present our algorithms for deciding
edge-types using linear programming.

###  7.3. Characterization of Reachability in CVRSs

Our aim in this section is to develop a characterization of the existence of a
trace between two configurations $c,c^{\prime}$ in a CVRS which can be used as
a basis for an efficient algorithm. Looking at Definition 7.2 of a step, one
can see that the task is very simple if $c^{\prime}$ is reachable from $c$ in
one step. However, in the general case, a trace from $c$ to $c^{\prime}$ may
have a very large number of steps, so we have to find a way to avoid reasoning
about each step individually. The following proposition is our starting point
for summarizing a large number of steps by equations, and it follows
immediately from the definitions of a step and a trace:

######  Proposition .

Let ${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ be a
CVRS, and let $\xi:=c\rightarrow^{\star}c^{\prime}$ be a trace in it. For
every $t\in R$, let $\alpha_{t}\in\mathbb{Q}_{\geq 0}$ be the sum of the
multiplicities of all the steps in $\xi$ in which $t$ participates. Then:

  1. (1)

$c^{\prime}=c+\sum_{t\in
R}\alpha_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$;

  2. (2)

For every rendezvous action ${a}\in\Sigma_{\textsf{actn}}$, and every
$i,j\in[k]$, we have that $\sum_{t\in
R,\textsf{rdz}(t)={a}_{i}}\alpha_{t}=\sum_{t\in
R,\textsf{rdz}(t)={a}_{j}}\alpha_{t}$.

We will see that the inverse of Proposition 7.3 also holds, provided one adds
some suitable conditions, as follows. The equations of Proposition 7.3 ensure
that the ‘accounting’ in a trace is done correctly, i.e., that the transitions
can be allocated to steps — item 2, corresponding to requirement (i) in
Definition 7.2 — and that added to the vector $c$ they yield the vector
$c^{\prime}$ — item 1, corresponding to requirement (iii) in that definition.
In order to extend Proposition 7.3 to a full characterization of reachability,
we need to address the last element in the definition of a step (requirement
(ii)) which states, for every state $s$, that $c(s)$ is at least the
multiplicity of the step times the number of transitions that participate in
the step whose source is $s$. Observe that if $c(s)>0$ this condition can
always be satisfied if $\alpha$ is small enough; however, if $c(s)=0$, and
there is some $i\in[k]$ such that $\textsf{src}(t_{i})=s$, then the condition
is necessarily violated. The characterization we now develop will thus make a
distinction between those states for which $c(s)>0$ and those for which
$c(s)=0$.

We will use the following terminology: For a vector $c\in\mathbb{Q}_{\geq
0}^{S}$, let the _support_ of $c$ be the set $(c)^{\neq 0}:=\\{s\in S\mid
c(s)>0\\}$. We will also make use of the following notation: for a set of
transitions $R$, we lift src and dst as follows:
$\textsf{src}(R)=\\{\textsf{src}(t)\mid t\in R\\}$ and
$\textsf{dst}(R)=\\{\textsf{dst}(t)\mid t\in R\\}$.

The following lemma states that we can summarize a large number of steps
between two configurations in case the support of the two configurations is
the same and no step increases the support:

######  Lemma .

Let ${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ be a
CVRS. Let $c,c^{\prime}\in\mathbb{Q}_{\geq 0}^{S}$ be configurations and let
$\alpha_{t}\in\mathbb{Q}_{\geq 0}$ be coefficients for every $t\in R$ such
that:

  1. (1)

$c^{\prime}=c+\sum_{t\in
R}\alpha_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$;

  2. (2)

For every rendezvous action ${a}\in\Sigma_{\textsf{actn}}$, and every
$i,j\in[k]$, we have that $\sum_{t\in
R,\textsf{rdz}(t)={a}_{i}}\alpha_{t}=\sum_{t\in
R,\textsf{rdz}(t)={a}_{j}}\alpha_{t}$;

  3. (3)

$(c)^{\neq 0}=(c^{\prime})^{\neq 0}$;

  4. (4)

For $R^{\prime}:=\\{t\in R\mid\alpha_{t}>0\\}$ we have
$\textsf{src}(R^{\prime})\subseteq(c^{\prime})^{\neq 0}$ and
$\textsf{dst}(R^{\prime})\subseteq(c)^{\neq 0}$.

Then, we have $c\rightarrow^{\star}c^{\prime}$ and all transitions in
$R^{\prime}$ participate in some step of this trace.

###### Proof.

Equations (1) and (2) give us a good starting point for showing the existence
of a trace from $c$ to $c^{\prime}$. Indeed, (2) allows us to group the
transitions in $R^{\prime}$ into steps such that each transition $t\in
R^{\prime}$ is taken with a combined multiplicity of $\alpha_{t}$; and (1)
guarantees that concatenating all these steps will take us from $c$ to
$c^{\prime}$. It remains to find a way to make sure each of these steps
satisfies requirement $(ii)$ in the definition of a step (Definition 7.2). We
begin, however, by ignoring this problem. That is, we will consider _quasi-
steps_ and _quasi-traces_. Formally, quasi-steps are like steps except that
they are between arbitrary vectors in $\mathbb{Q}^{S}$ (as opposed to steps
which were defined only for vectors in $\mathbb{Q}_{\geq 0}^{S}$), and that
they do not have to satisfy requirement $(ii)$ of Definition 7.2. We will
denote quasi-steps using $\xLongrightarrow{}$. A quasi-trace is simply a
sequence of quasi-steps where the destination of each quasi-step in the
sequence is the source of the next one. We complete the proof by first
constructing a quasi-trace $\varrho$ from $c$ to $c^{\prime}$, and then
showing how to turn $\varrho$ into a trace.

We construct $\varrho$ using the following algorithm. If $c=c^{\prime}$ then
we are done. Otherwise, at round $0$, set $\varrho$ to the empty quasi-trace,
and $v_{1}:=c$ be the source of the first quasi-step to be constructed. At
round $\geq 1$, do the following:

  1. (1)

pick a transition $t$ whose $\alpha_{t}$ is minimal among all edges in
$R^{\prime}$; let ${a}_{i}$ be $\textsf{rdz}(t)$;

  2. (2)

let $t_{i}:=t$, and for every $j\in[k]\setminus\\{i\\}$ pick some $t_{j}\in
R^{\prime}$ with $\textsf{rdz}(t_{j})={a}_{j}$;

  3. (3)

extend $\varrho$ with the quasi-step
$v_{i}\xLongrightarrow{t_{1},\ldots,t_{k}:\alpha_{t}}v_{i+1}$;

  4. (4)

for every $j\in[k]$, subtract $\alpha_{t}$ from $\alpha_{t_{j}}$, and if the
resulting $\alpha_{t_{j}}$ is zero then remove $t_{j}$ from $R^{\prime}$. If
$R^{\prime}=\emptyset$ stop and output $\varrho$.

Since at least one transition (namely the transition $t$ picked in step $1$)
is removed at the end of each round, the algorithm stops after at most
$|R^{\prime}|$ rounds. It is also easy to see that item (2) of the lemma is an
invariant of the algorithm (i.e., it holds using the updated values at the end
of each round). This, together with our choice of $t$, ensures that we are
always able to find the required transitions in the second step of every
round. Finally, observe that the resulting final quasi-trace $\varrho$ uses
every transition $t$ in (the initial) $R^{\prime}$ with a combined
multiplicity which is exactly $\alpha_{t}$ and thus, by item (1) of the lemma,
we have that $\varrho$ ends in $c^{\prime}$ as promised. It remains to show
how to derive from $\varrho$ a trace from $c$ to $c^{\prime}$.

$c$$c^{\prime}$ Figure 8.  A graphical representation in two dimensions of the
replacement of quasi-steps (in dotted arrows) by steps (in dashed arrows). In
this example $h=3$ and $m=2$.

Let $m$ be the number of quasi-steps in $\varrho$. For $j\in[m]$, denote the
transitions used in the $j$-th quasi-step of $\varrho$ by
$t^{j}_{1},\ldots,t^{j}_{k}$, denote the multiplicity used by $\alpha^{j}$,
and the destination reached by $v_{j}$ (also set $v_{0}:=c$). Consider
$c=v_{0},v_{1},\ldots,v_{m}=c^{\prime}$ as points in the $|S|$-dimensional
Euclidean space. Let $H:=(c)^{\neq 0}=(c^{\prime})^{\neq 0}$ (by item (3) of
the lemma). We note that every point on the line segment $L$ between $c$ and
$c^{\prime}$ also has support $H$ (being a convex combination of $c$ and
$c^{\prime}$). It follows that $L$ does not touch any of the hyperplanes
corresponding to the states in $H$ (i.e., the hyperplanes defined by the
equations $v(s)=0$, for $s\in H$). Let $x>0$ be the minimum of the Euclidean
distances between $L$ and any of these hyperplanes888Recall that in a
Euclidean space the distance between a hyperplane and a line-segment, that
does not touch it, is positive., let $y$ be the maximum over $j\in{m}$ of the
multiplicities $\alpha^{j}$, and let $h\in\mathbb{N}$ be large enough to
satisfy $\frac{myk}{h}\leq x$.

Construct a new quasi-trace $\varrho^{\prime}$ from $c$ to $c^{\prime}$ by
starting at $c$, and repeating $h$ times the following: for $j=1,\dots,m$,
extend $\varrho^{\prime}$ by taking a quasi-step using the transitions
$t^{j}_{1},\ldots,t^{j}_{k}$ with multiplicity $\alpha^{j}/h$. This
construction is illustrated in Figure 8. We claim that $\varrho^{\prime}$ is
actually a trace, i.e., that for every $s\in S$, and every point $v_{lm+j}$ on
$\varrho^{\prime}$ (where $0\leq l<h$, and $0\leq j<m$) we have that condition
(ii) in Definition 7.2 is satisfied, namely, that $v_{lm+j}(s)\geq
o_{lm+j}(s)$, where $o_{lm+j}$ is the vector
$\frac{\alpha^{j}}{h}\sum_{i=1}^{k}\textsf{out}(t^{j}_{i})$. Observe that this
not only guarantees that each quasi-step is a step, but also that all points
on $\varrho^{\prime}$ are configurations (i.e., have no negative coordinates).
Consider first the case of $s\in S\setminus H$. By item (4) of the lemma,
$\textsf{src}(R^{\prime})\subseteq H$ and $\textsf{dst}(R^{\prime})\subseteq
H$, and thus $v_{lm+j}(s)=c(s)=0=o_{lm+j}(s)$. For $s\in H$, note that
$o_{lm+j}(s)\leq\frac{yk}{h}$, and thus it is enough to show that
$v_{lm+j}(s)-\frac{yk}{h}\geq 0$. Observe that, for every $0\leq l<h$, the
point reached after taking $lm$ quasi-steps of $\varrho^{\prime}$ is
$c+\frac{l}{h}(c^{\prime}-c)$, which is a point on $L$. Hence, by our choice
of $x$, we have that $v_{lm}(s)\geq x$. Also note that each quasi-step on
$\varrho^{\prime}$ can decrease $v_{lm}(s)$ by at most $\frac{yk}{h}$, thus,
for every $0\leq j<m$, we have that $v_{lm+j}(s)-\frac{yk}{h}\geq
v_{lm}(s)-\frac{myk}{h}\geq x-x=0$. ∎

The above lemma already allows us to characterize the locally-reusable edges,
as well as the light green edges (relative to green edges):

######  Lemma .

Given a component $P^{\multimap}_{i}$ of $P^{\multimap}$, an edge $e$ of
$P^{\multimap}_{i}$ is locally-reusable iff there are coefficients
$\alpha_{t}\in\mathbb{Q}_{\geq 0}$ for every $t\in R^{\multimap}_{i}$, such
that:

  1. (1)

$0=\sum_{t\in
R^{\multimap}_{i}}\alpha_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$;

  2. (2)

For every rendezvous action ${a}\in\Sigma_{\textsf{actn}}$, and every
$j,h\in[k]$, we have that $\sum_{t\in
R^{\multimap}_{i},\textsf{rdz}(t)={a}_{j}}\alpha_{t}=\sum_{t\in
R^{\multimap}_{i},\textsf{rdz}(t)={a}_{h}}\alpha_{t}$;

  3. (3)

$\alpha_{e}>0$.

Moreover, $e$ is light green iff we further require that the set $\\{t\in
R_{i}\mid\alpha_{t}>0\\}$ only contains green edges.

###### Proof.

For the ‘only if’ direction, we observe that by Lemma 7.2 there is a trace
$\xi:=c\rightarrow^{\star}c$ of the CVRS $P^{\multimap}_{i}$ such that $e$
participates in a step of $\xi$. Moreover, $\xi$ uses only green edges in case
$e$ is light green. By Proposition 7.3, we can derive coefficients
$\alpha_{t}\in\mathbb{Q}_{\geq 0}$ that satisfy the conditions of the lemma.

For the ‘if’ direction, let $R^{\prime}=\\{t\in R_{i}\mid\alpha_{t}>0\\}$ and
$H=\textsf{src}(R^{\prime})\cup\textsf{dst}(R^{\prime})$. Set
$c\in\mathbb{Q}_{\geq 0}^{S_{i}}$ to the configuration defined by $c(q)=1$, if
$q\in H$, and $c(q)=0$, otherwise. Then, apply Lemma 7.3 and obtain a trace
$\xi:=c\rightarrow^{\star}c$ of the CVRS $P^{\multimap}_{i}$, such that $e$
participates in a step of $\xi$. By Lemma 7.2, the type (locally-reusable, or
light green) of $e$ follows. ∎

Lemma 7.3 gives rise to a ptime algorithm for computing the locally-reusable
and light green edges (in case we already know the green edges):

######  Corollary .

Let $e$ be an edge of $P^{\multimap}$. We can decide in ptime (in the size of
$P^{\multimap}$), whether $e$ is locally-reusable, and whether $e$ is light
green (assuming we already know which edges are green).

###### Proof.

For every edge $e$ of $P^{\multimap}$, we need to find a solution that
satisfies the equations of Lemma 7.3. Such a solution can be found by linear
programming over the rationals, which is in ptime. ∎

The rest of this section will be dedicated to addressing the problem of
deciding whether an edge is green or not. Observe that — unlike locally-
reusable and light green edges for which a witnessing pseudo-cycle is
characterized by Lemma 7.2 using a cyclic trace in a single CVRS — the
characterization of the witnessing pseudo-cycle for a green edge in terms of
CVRS traces (as given by Lemma 7.2) involves non-cyclic traces in multiple
different CVRSs. Hence, our first step is to develop a general
characterization of reachability in CVRS which extends the characterization
given in Lemma 7.3 to the case of traces whose source and destination
configurations may have a different support. We begin with the following
property of the support:

######  Lemma .

Let ${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ be a
CVRS and let $c,c_{1},c_{2}\in\mathbb{Q}_{\geq 0}^{S}$ be configurations of
it. Then:

  1. (1)

If $c\rightarrow^{\star}c_{1}$ and $c\rightarrow^{\star}c_{2}$ then there is a
trace $c\rightarrow^{\star}c_{3}$ with $(c_{3})^{\neq 0}=(c_{1})^{\neq
0}\cup(c_{2})^{\neq 0}$;

  2. (2)

If $c_{1}\rightarrow^{\star}c$ and $c_{2}\rightarrow^{\star}c$ then there is a
trace $c_{3}\rightarrow^{\star}c$ with $(c_{3})^{\neq 0}=(c_{1})^{\neq
0}\cup(c_{2})^{\neq 0}$.

###### Proof.

Let $c_{3}=\frac{1}{2}c_{1}+\frac{1}{2}c_{2}$, and observe that $(c_{3})^{\neq
0}=(c_{1})^{\neq 0}\cup(c_{2})^{\neq 0}$. It remains to show the desired
traces between $c$ and $c_{3}$. For the first item, let
$\xi_{1}:=c\rightarrow^{\star}c_{1}$, and
$\xi_{2}:=c\rightarrow^{\star}c_{2}$. A trace from $c$ to $c_{3}$ is obtained
by concatenating $\frac{1}{2}c\oplus(\frac{1}{2}\otimes\xi_{1})$ and
$\frac{1}{2}c_{1}\oplus(\frac{1}{2}\otimes\xi_{2})$. For the second item, let
$\xi_{1}:=c_{1}\rightarrow^{\star}c$, and
$\xi_{2}:=c_{2}\rightarrow^{\star}c$. A trace from $c_{3}$ to $c$ is obtained
by concatenating $\frac{1}{2}c_{1}\oplus(\frac{1}{2}\otimes\xi_{2})$ and
$\frac{1}{2}c\oplus(\frac{1}{2}\otimes\xi_{1})$. ∎

Let ${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ be a
CVRS, let $R^{\prime}\subseteq R$, and let $c\in\mathbb{Q}_{\geq 0}^{S}$ be a
configuration. We say that a set $H\subseteq S$ is _forward (resp. backward)
$R^{\prime}$-accessible from $c$_ if there is a trace
$c\rightarrow^{\star}c^{\prime}$ (resp. $c^{\prime}\rightarrow^{\star}c$),
with all of it’s steps using only transitions from $R^{\prime}$, such that
$(c^{\prime})^{\neq 0}=H$. We define $\textsf{forw}(c,R^{\prime})$ (resp.
$\textsf{back}(c,R^{\prime})$) to be the union of all sets $H\subseteq S$ that
are forward (resp. backward) $R^{\prime}$-accessible from $c$.

######  Remark 8.

Observe that Lemma 7.3 implies that $\textsf{forw}(c,R^{\prime})$ is forward
$R^{\prime}$-accessible from $c$, and that $\textsf{back}(c,R^{\prime})$ is
backward $R^{\prime}$-accessible from $c$. It follows that
$\textsf{forw}(c,R^{\prime})$ (resp. $\textsf{back}(c,R^{\prime})$) is the
maximal subset of $S$ that is forward (resp. backward) $R^{\prime}$-accessible
from $c$.

######  Proposition .

Given a CVRS
${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$, a subset
$R^{\prime}\subseteq R$, and a configuration $c$, the sets
$\textsf{forw}(c,R^{\prime})$ and $\textsf{back}(c,R^{\prime})$ can be
computed in ptime.

###### Proof.

We present a fixed point algorithm for computing
$\textsf{forw}(c,R^{\prime})$; computing $\textsf{back}(c,R^{\prime})$ is done
in a symmetric fashion. Construct an increasing chain $H_{0}\subsetneq
H_{1}\subsetneq\cdots$ of sets $H_{i}\subseteq S$, until a larger set cannot
be found, as follows. Let $H_{0}:=(c)^{\neq 0}$. For each $i$, we check if
there is an action ${a}\in\Sigma_{\textsf{actn}}$, and there are transitions
$t_{1},\ldots,t_{k}\in R^{\prime}$ with $\textsf{rdz}(t_{j})={a}_{j}$ for all
$j\in[k]$, such that $\textsf{src}(\\{t_{1},\ldots,t_{k}\\})\subseteq H_{i}$
and $\textsf{dst}(\\{t_{1},\ldots,t_{k}\\})\not\subseteq H_{i}$. In case there
are such transitions, we set
$H_{i+1}:=H_{i}\cup\textsf{dst}(\\{t_{1},\ldots,t_{k}\\})$; otherwise, we are
done and have $H_{i}=\textsf{forw}(c,R^{\prime})$.

The correctness of the algorithm is demonstrated as follows. First, to see
that for every round $i$, the set $H_{i}$ is contained in
$\textsf{forw}(c,R^{\prime})$, proceed by induction on $i$. Note that, by the
induction hypothesis, there is a trace $\xi:=c\rightarrow^{\star}c_{i}$ with
$(c_{i})^{\neq 0}=H_{i}$, and that this trace can be extended to a trace
$\xi^{\prime}:=c\rightarrow^{\star}c_{i}\xrightarrow{t_{1},\ldots,t_{k}:\alpha}c_{i+1}$,
with $(c_{i+1})^{\neq 0}=\textsf{dst}(\\{t_{1},\ldots,t_{k}\\})\cup
H_{i}=H_{i+1}$, by choosing $0<\alpha<\frac{1}{k}\cdot\min_{q\in(c_{i})^{\neq
0}}\\{c_{i}(q)$}. To see that the algorithm outputs
$\textsf{forw}(c,R^{\prime})$, and not a proper subset of it, let
$\xi:=c\rightarrow^{\star}c^{\prime}$ be a trace such that $(c^{\prime})^{\neq
0}=\textsf{forw}(c,R^{\prime})$. Assume by way of contradiction that the
support of some configuration along $\xi$ is not contained in the output of
the algorithm, and let $c_{i+1}$ be the first such configuration on $\xi$.
Consider the step $c_{i}\xrightarrow{t_{1},\cdots,t_{k}:\alpha_{i}}c_{i+1}$
and note that $\textsf{src}(\\{t_{1},\ldots,t_{k}\\})\subseteq(c_{i})^{\neq
0}$. Let $P_{0},P_{1},P_{2},\cdots,P_{n}$ be the sequence of sets computed by
the algorithm. By minimality of $i$, there is a $j$ such that $(c_{i})^{\neq
0}\subseteq P_{j}\subseteq P_{n}$. Thus,
$\textsf{src}(\\{t_{1},\ldots,t_{k}\\})\subseteq P_{n}$ and
$\textsf{dst}(\\{t_{1},\ldots,t_{k}\\})\not\subseteq P_{n}$. But this
contradicts the termination condition of the algorithm. ∎

The following simple property of the operators forw and back will be useful:

######  Proposition .

Let ${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ be a
CVRS and let $\xi:=c\rightarrow^{\star}c^{\prime}$ be a trace of
${\mathcal{V}}$. Let $R^{\prime}$ be the set of transitions that participate
in steps of $\xi$, and let $\mathit{Configs}$ be the set of configurations
that appear in $\xi$. Then,
$\textsf{forw}(c,R^{\prime})=\textsf{back}(c^{\prime},R^{\prime})=\bigcup_{c^{\circ}\in\mathit{Configs}}(c^{\circ})^{\neq
0}=(c)^{\neq 0}\cup\textsf{dst}(R^{\prime})=(c^{\prime})^{\neq
0}\cup\textsf{src}(R^{\prime})$.

###### Proof.

For every configuration $c^{\circ}$ that appears on $\xi$, the prefix
$c\rightarrow^{\star}c^{\circ}$ of $\xi$, and the suffix
$c^{\circ}\rightarrow^{\star}c^{\prime}$ of $\xi$, obviously only use
transitions from $R^{\prime}$. Hence,
$\bigcup_{c^{\circ}\in\mathit{Configs}}(c^{\circ})^{\neq
0}\subseteq\textsf{forw}(c,R^{\prime})$ and
$\bigcup_{c^{\circ}\in\mathit{Configs}}(c^{\circ})^{\neq
0}\subseteq\textsf{back}(c^{\prime},R^{\prime})$; as well as
$\bigcup_{c^{\circ}\in\mathit{Configs}}(c^{\circ})^{\neq 0}\subseteq(c)^{\neq
0}\cup\textsf{dst}(R^{\prime})$ and
$\bigcup_{c^{\circ}\in\mathit{Configs}}(c^{\circ})^{\neq
0}\subseteq(c^{\prime})^{\neq 0}\cup\textsf{src}(R^{\prime})$. For the other
direction, observe that $\textsf{forw}(c,R^{\prime})\subseteq(c)^{\neq
0}\cup\textsf{dst}(R^{\prime})\subseteq\bigcup_{c^{\circ}\in\mathit{Configs}}(c^{\circ})^{\neq
0}$ and, similarly,
$\textsf{back}(c^{\prime},R^{\prime})\subseteq(c^{\prime})^{\neq
0}\cup\textsf{src}(R^{\prime})\subseteq\bigcup_{c^{\circ}\in\mathit{Configs}}(c^{\circ})^{\neq
0}$. ∎

######  Remark 9.

It is worth noting that for every configuration $c$ and set of transitions
$R^{\prime}$, we have that $\textsf{forw}(c,R^{\prime})\subseteq(c)^{\neq
0}\cup\textsf{dst}(R^{\prime})$ (resp.
$\textsf{back}(c,R^{\prime})\subseteq(c)^{\neq
0}\cup\textsf{src}(R^{\prime})$); however, only in case there is a path from
$c$ (resp. to $c$), that uses exactly the transitions in $R^{\prime}$, do the
reverse inclusions also hold.

We are now ready to state a full characterization of reachability in CVRSs:

######  Theorem .

Let ${\mathcal{V}}=\left\langle{\Sigma_{\textsf{rdz}},S,R}\right\rangle$ be a
CVRS. A configuration $c^{\prime}\in\mathbb{Q}_{\geq 0}^{S}$ is reachable from
a configuration $c\in\mathbb{Q}_{\geq 0}^{S}$ iff there are coefficients
$\alpha_{t}\in\mathbb{Q}_{\geq 0}$ for every $t\in R$ such that:

  1. (1)

$c^{\prime}=c+\sum_{t\in
R}\alpha_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$;

  2. (2)

For every rendezvous action ${a}\in\Sigma_{\textsf{actn}}$, and every
$i,j\in[k]$, we have that $\sum_{t\in
R,\textsf{rdz}(t)={a}_{i}}\alpha_{t}=\sum_{t\in
R,\textsf{rdz}(t)={a}_{j}}\alpha_{t}$;

  3. (3)

For $R^{\prime}:=\\{t\in R\mid\alpha_{t}>0\\}$ we have that
$\textsf{src}(R^{\prime})\subseteq\textsf{back}(c^{\prime},R^{\prime})$,
$\textsf{dst}(R^{\prime})\subseteq\textsf{forw}(c,R^{\prime})$, and
$\textsf{forw}(c,R^{\prime})=\textsf{back}(c^{\prime},R^{\prime})$.

###### Proof.

For the forward direction, take a trace $\xi:=c\rightarrow^{\star}c^{\prime}$.
For every $t\in R$, let $\alpha_{t}$ be the sum of the multiplicities of the
steps of $\xi$ in which $t$ participates. By Proposition 7.3, we have that
condition (1) and (2) of the lemma are satisfied. Condition (3) holds by
applying Proposition 7.3 to $\xi$.

For the reverse direction, assume that there are coefficients $\alpha_{t}$
such that conditions (1)-(3) are satisfied. Let
$H:=\textsf{forw}(c,R^{\prime})=\textsf{back}(c^{\prime},R^{\prime})$. By
Remark 8, we can obtain traces $\xi_{1}:=c\rightarrow^{\star}c_{1}$ and
$\xi_{2}:=c_{2}\rightarrow^{\star}c^{\prime}$, using only transitions from
$R^{\prime}$, such that $(c_{1})^{\neq 0}=H=(c_{2})^{\neq 0}$. It remains to
show that $c_{2}$ is reachable from $c_{1}$. For every transition $t\in R$,
let $\alpha^{1}_{t}$ (resp. $\alpha^{2}_{t}$) be the sum of the multiplicities
of the steps of $\xi_{1}$ (resp. $\xi_{2}$) in which $t$ participates, and let
$\gamma_{t}=\alpha_{t}-\alpha^{1}_{t}-\alpha^{2}_{t}$. By the convexity
property (Proposition 7.2) we can assume w.l.o.g. that: ($\S$)
$\alpha^{1}_{t}$ and $\alpha^{2}_{t}$ are small enough such that
$\gamma_{t}>0$ for all $t\in R^{\prime}$ (simply apply the convexity property
to $\xi_{1}$ and $\xi_{2}$ with a small enough $\gamma$ to obtain, if needed,
replacement $\xi_{1},\xi_{2},c_{1},c_{2}$). By Proposition 7.3, we get that
$c_{1}=c+\sum_{t\in
R^{\prime}}\alpha^{1}_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$, and
$c^{\prime}=c_{2}+\sum_{t\in
R^{\prime}}\alpha^{2}_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$.
Combining the last two equalities with condition (1) of the Lemma, and
rearranging terms, we get:

$c_{2}=c_{1}+\sum_{t\in
R^{\prime}}\gamma_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$ ($\dagger$)

Again, by Proposition 7.3, we have for every $l\in\\{1,2\\}$:

$\forall{a}\in\Sigma_{\textsf{actn}},i,j\in[k]:\sum_{t\in
R^{\prime},\textsf{rdz}(t)={a}_{i}}\alpha^{l}_{t}=\sum_{t\in
R^{\prime},\textsf{rdz}(t)={a}_{j}}\alpha^{l}_{t},$

Together with condition (2) we thus get that:

$\forall{a}\in\Sigma_{\textsf{actn}},i,j\in[k]:\sum_{t\in
R^{\prime},\textsf{rdz}(t)={a}_{i}}\gamma_{t}=\sum_{t\in
R^{\prime},\textsf{rdz}(t)={a}_{j}}\gamma_{t}$ (${\ddagger}$)

By $(\dagger)$ and $({\ddagger})$, and our choice of $c_{1},c_{2}$, the
requirements of Lemma 7.3 are satisfied for $c_{1},c_{2}$ and coefficients
$\gamma_{t}$. Hence, $c_{2}$ is reachable from $c_{1}$. ∎

######  Remark 10.

The characterization in Theorem 7.3 is an adaptation of the characterization
of reachability in continuous vector addition systems from [FH15]; for our
characterization result we had to redevelop the theory of [FH15] for CVRSs.

###  7.4. An Algorithm for Finding the green Edges

In this section we present a ptime algorithm for deciding the existence of
pseudo-cycles with $r$ broadcasts in $(P^{\multimap})^{\infty}$. The algorithm
will be developed based on the following characterization which is an
immediate consequence of Lemma 7.2, using Theorem 7.3 to characterize the
traces $\xi_{i}$ of this lemma. Recall that $\mathcal{I}$ is the set of
indices of the components on the noose of $P^{\multimap}$.

######  Corollary .

An edge $e$ of $P^{\multimap}$ is green iff, for every $i\in\mathcal{I}$: (i)
there is a subset ${\mathcal{T}}_{i}$ of the transitions of
$P^{\multimap}_{i}$, and a subset $B_{i}$ of the broadcast transitions from
$P^{\multimap}_{i}$ to $P^{\multimap}_{next(i)}$, with
$e\in\cup_{i\in\mathcal{I}}(B_{i}\cup{\mathcal{T}}_{i}$); (ii) there are
coefficients $\alpha_{t}\in\mathbb{Q}_{>0}$ for every
$t\in{\mathcal{T}}_{i}\cup B_{i}$; such that:

  1. (1)

$c^{\prime}_{i}=c_{i}+\sum_{t\in{\mathcal{T}}_{i}}\alpha_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$,
where $c_{i},c^{\prime}_{i}$ are defined, for every $q\in S^{\multimap}_{i}$,
by: $c_{i}(q):=\sum_{t\in B_{{\rm
Phys.~{}Rev.~{}E}{i}},\textsf{dst}(t)=q}\alpha_{t}$, and
$c^{\prime}_{i}(q):=\sum_{t\in B_{i},\textsf{src}(t)=q}\alpha_{t}$;

  2. (2)

for every rendezvous action ${a}\in\Sigma_{\textsf{actn}}$, and every
$j,h\in[k]$, we have that
$\sum_{t\in{\mathcal{T}}_{i},\textsf{rdz}(t)={a}_{j}}\alpha_{t}=\sum_{t\in{\mathcal{T}}_{i},\textsf{rdz}(t)={a}_{h}}\alpha_{t}$;

  3. (3)

$\textsf{dst}({\mathcal{T}}_{i})\subseteq\textsf{forw}(c_{i},{\mathcal{T}}_{i})$,
$\textsf{src}({\mathcal{T}}_{i})\subseteq\textsf{back}(c_{i}^{\prime},{\mathcal{T}}_{i})$,
and
$\textsf{forw}(c_{i},{\mathcal{T}}_{i})=\textsf{back}(c_{i}^{\prime},{\mathcal{T}}_{i})$.

Corollary 7.4 gives rise to Algorithm 1 for computing the set of green edges
of $P^{\multimap}$.

We remark that the algorithm presented here for computing green edges differs
from our original algorithm in [ARZS15]. Here, we use an algorithm that is
inspired by, and extends, Algorithm $2$ in [FH15] for deciding the
reachability of a target configuration from an initial configuration in
continuous vector addition systems. The extension is in two ways: first from
vector addition systems to CVRSs, and second by adding machinery for handling
broadcasts.

Input: $P^{\multimap}$.

Initialize — for every $i\in\mathcal{I}$ do:

${\mathcal{T}}_{i}$ := all rendezvous transitions of $P^{\multimap}_{i}$;

$B_{i}$ := all broadcast transitions from $P^{\multimap}_{i}$ to
$P^{\multimap}_{next(i)}$;

Repeat: For every $i\in\mathcal{I}$: take variables
$c_{i}(q),c^{\prime}_{i}(q)$ for every $q\in S^{\multimap}_{i}$, and
$\alpha_{t}$ for every $t\in{\mathcal{T}}_{i}\cup B_{i}$.

Find a solution to the following constraint system, such that the number of
non-zero variables $\alpha_{t}$ is maximal:

  * $\bullet$

$\alpha_{t}\geq 0$ for every $t\in{\mathcal{T}}_{i}\cup B_{i}$;

  * $\bullet$

$c_{i}(q)=\sum_{t\in B_{{\rm
Phys.~{}Rev.~{}E}{i}},\textsf{dst}(t)=q}\alpha_{t}$, for every $q\in
S^{\multimap}_{i}$;

  * $\bullet$

$c^{\prime}_{i}(q)=\sum_{t\in B_{i},\textsf{src}(t)=q}\alpha_{t}$, for every
$q\in S^{\multimap}_{i}$;

  * $\bullet$

$c_{i}^{\prime}=c_{i}+\sum_{t\in{\mathcal{T}}_{i}}\alpha_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$;

  * $\bullet$

$\sum_{t\in{\mathcal{T}}_{i},\textsf{rdz}(t)={a}_{j}}\alpha_{t}=\sum_{t\in{\mathcal{T}}_{i},\textsf{rdz}(t)={a}_{h}}\alpha_{t}$
for every ${a}\in\Sigma_{\textsf{actn}}$ and $j,h\in[k]$.

Let
$H_{i}:=\textsf{forw}(c_{i},{\mathcal{T}}_{i})\cap\textsf{back}(c^{\prime}_{i},{\mathcal{T}}_{i})$;

Let ${\mathcal{T}}_{i}$ :=
$\\{t\in{\mathcal{T}}_{i}\mid\alpha_{t}>0\\}\cap\\{t\in{\mathcal{T}}_{i}\mid\textsf{src}(t)\in
H_{i}\wedge\textsf{dst}(t)\in H_{i}\\}$;

Let $B_{i}$ := $\\{t\in B_{i}\mid\alpha_{t}>0\\}$;

Until neither ${\mathcal{T}}_{i}$ nor $B_{i}$ change, for any
$i\in\mathcal{I}$.

Output: $\bigcup_{i\in\mathcal{I}}B_{i}\cup{\mathcal{T}}_{i}$

Algorithm 1 Algorithm for computing all edges of $P^{\multimap}$ that can
appear in a pseudo-cycle with broadcasts of $(P^{\multimap})^{\infty}$.

######  Theorem .

Deciding if an edge of $P^{\multimap}$ is green can be done in ptime.

###### Proof.

We begin by making a couple of important observations. In each iteration of
the main loop of the algorithm we need to find a solution to a constraint
system forming a linear programming problem over the rationals, with no
objective function, whose canonical form is: $Ax=0,x\geq 0$ (for some matrix
$A$ and vector $x$ of variables), such that the solution is maximal with
respect to the number of non-zero variables $\alpha_{t}$. Given that linear
programs of this canonical form have the property that the sum of any two
solutions is itself a solution, we have that: ($\dagger$) one can find a
maximal solution $x$ by looking, for every $t\in{\mathcal{T}}_{i}\cup B_{i}$,
for a solution to the system $Ax=0,x\geq 0,\alpha_{t}>0$, and adding together
all the solutions that were found; ($\ddagger$) for every variable
$\alpha_{t}$ of the system $Ax=0,x\geq 0$, if there is a solution in which
$\alpha_{t}>0$, then $\alpha_{t}>0$ in every maximal solution.

We now show that Algorithm 1 outputs exactly the set of green edges of
$P^{\multimap}$.

To see that every edge output by the algorithm is green, we will apply
Corollary 7.4 (direction ‘if’) to the sets ${\mathcal{T}}_{i}$ and $B_{i}$ and
the coefficients $\alpha_{t}$ from the solution obtained in the last iteration
of the algorithm. Observe that at this last iteration all the sets have
reached a fixed point. Hence, in particular, for every
$t\in{\mathcal{T}}_{i}\cup B_{i}$ we have that $\alpha_{t}>0$, and (§)
$\textsf{dst}({\mathcal{T}}_{i})\subseteq H_{i}$,
$\textsf{src}({\mathcal{T}}_{i})\subseteq H_{i}$. Since the constraint system
in the algorithm exactly matches requirements (1) and (2) in Corollary 7.4,
the only thing we have to show before we can apply this corollary is that also
condition (3) holds. Observe that, by $\S$, it is enough to show that at the
last iteration $\textsf{forw}(c_{i},{\mathcal{T}}_{i})=H_{i}$ and
$\textsf{back}(c_{i}^{\prime},{\mathcal{T}}_{i})=H_{i}$. We will show the
first equality, the second is shown in a symmetric way. Consider the following
chain of inequalities:
$H_{i}\subseteq\textsf{forw}(c_{i},{\mathcal{T}}_{i})\subseteq(c_{i})^{\neq
0}\cup\textsf{dst}({\mathcal{T}}_{i})\subseteq(c_{i})^{\neq 0}\cup
H_{i}\subseteq H_{i}$. The first containment is by the definition of $H_{i}$,
the second by Remark 9, the third by $\S$, and the last by the following
argument: for $q\in(c_{i})^{\neq 0}$, if
$q\in\textsf{src}({\mathcal{T}}_{i})\cup\textsf{dst}({\mathcal{T}}_{i})$ then
$q\in H_{i}$ by $\S$; otherwise, $q\in(c^{\prime}_{i})^{\neq 0}$ (by the
constraint
$c_{i}^{\prime}=c_{i}+\sum_{t\in{\mathcal{T}}_{i}}\alpha_{t}\left(\textsf{in}(t)-\textsf{out}(t)\right)$),
and since by definition $(c_{i})^{\neq
0}\subseteq\textsf{forw}(c_{i},{\mathcal{T}}_{i})$ and $(c^{\prime}_{i})^{\neq
0}\subseteq\textsf{back}(c^{\prime}_{i},{\mathcal{T}}_{i})$, we have that
$q\in\textsf{forw}(c_{i},{\mathcal{T}}_{i})\cap\textsf{back}(c^{\prime}_{i},{\mathcal{T}}_{i})=H_{i}$.

To see that every green edge $e$ of $P^{\multimap}$ is output by the
algorithm, apply Corollary 7.4 (direction ‘only if’) to $e$ to obtain sets
$\tilde{{\mathcal{T}}}_{i}$ and $\tilde{B}_{i}$, and coefficients
$\tilde{\alpha}_{t}>0$, satisfying the conditions of the corollary. We claim
that if
$\tilde{{\mathcal{T}}}_{i}\cup\tilde{B}_{i}\subseteq{\mathcal{T}}_{i}\cup
B_{i}$ holds, for every $i\in\mathcal{I}$, at the beginning of an iteration
(which is the case at initialization), then it also does at its end. Note that
this would conclude the proof since
$e\in\cup_{i\in\mathcal{I}}(\tilde{B}_{i}\cup\tilde{{\mathcal{T}}}_{i}$) by
condition (i) of the corollary. To prove the claim, note that if
$\tilde{{\mathcal{T}}}_{i}\cup\tilde{B}_{i}\subseteq{\mathcal{T}}_{i}\cup
B_{i}$, for every $i\in\mathcal{I}$, then the coefficients
$\tilde{\alpha}_{t}$ induce a (not necessarily maximal) solution to the
constraint system. Hence, by observation ($\ddagger$) at the beginning of the
proof, every maximal solution $\alpha_{t},c,c^{\prime}$ of this system will
have $\alpha_{t}>0$ for every
$t\in\tilde{{\mathcal{T}}}_{i}\cup\tilde{B}_{i}$. The claim follows by showing
that
$\textsf{src}(\tilde{{\mathcal{T}}}_{i})\cup\textsf{dst}(\tilde{{\mathcal{T}}}_{i})\subseteq
H_{i}$. To see this, observe that $\alpha_{t}>0$ for every $t\in\tilde{B}_{i}$
implies (by the definition of $c_{i}$ and $c_{i}^{\prime}$ in condition (1) of
the corollary, and the corresponding constraint in the algorithm) that
$(\tilde{c}_{i})^{\neq 0}\subseteq(c_{i})^{\neq 0}$ and
$(\tilde{c}_{i}^{\prime})^{\neq 0}\subseteq(c_{i}^{\prime})^{\neq 0}$. Hence,
$\textsf{forw}(\tilde{c}_{i},\tilde{{\mathcal{T}}}_{i})\subseteq\textsf{forw}(c_{i},{\mathcal{T}}_{i})$
and
$\textsf{back}(\tilde{c}_{i}^{\prime},\tilde{{\mathcal{T}}}_{i})\subseteq\textsf{back}(c_{i}^{\prime},{\mathcal{T}}_{i})$.
Since, by condition (3) of the corollary,
$\textsf{src}(\tilde{{\mathcal{T}}}_{i})\cup\textsf{dst}(\tilde{{\mathcal{T}}}_{i})\subseteq\textsf{forw}(\tilde{c_{i}},\tilde{{\mathcal{T}}}_{i})=\textsf{back}(\tilde{c}_{i}^{\prime},\tilde{{\mathcal{T}}}_{i})$
we are done.

It remains to show that the algorithm runs in polynomial time. Since in every
round at least one transition is removed from either ${\mathcal{T}}_{i}$ or
$B_{i}$, for some $i$, the main loop repeats linearly many times in the size
of $P^{\multimap}$. By observation ($\dagger$) at the beginning of the proof,
finding a maximal solution to the constraint system of each iteration can be
done by solving a linear number of linear programming problems (of polynomial
size) over the rationals, which is in ptime. Since, by Proposition 7.3,
calculating $\textsf{forw}(c_{i},{\mathcal{T}}_{i})$ and
$\textsf{back}(c^{\prime}_{i},{\mathcal{T}}_{i})$ is also in ptime, we
conclude that the whole algorithm runs in polynomial time. ∎

Theorem 7.4, together with Corollary 7.3, yield the promised proof to the main
theorem (Theorem 7) of this section.

##  8\. Conclusion

We have established the decidability and complexity of the PMCP for safety and
liveness properties of RB-systems, which are polynomially inter-reducible with
discrete-timed networks. The lower and upper complexity bounds for safety
properties are tight. We leave open the problem of whether our exptime upper-
bound for liveness properties is tight. We note that the pspace lower bound
for safety properties also implies a pspace lower bound for liveness
properties. The exptime upper bound is established by (repeatedly) solving an
exponentially sized linear program. As linear programming is known to be
ptime-complete, it seems unlikely that our techniques can be improved to show
a pspace upper bound.

A further direction for future research concerns whether our results for the
discrete-time model can be lifted to the continuous-time model without a
distinguished controller (note that PMCP for continuous time networks with a
distinguished controller is undecidable [AJ03]). For example, time-bounded
invariance and time-bounded response properties (expressed as MTL formulae)
hold on the discrete-time model iff they hold with the continuous-time model
[HMP92], whereas [OW03] establish several results on to the use of
digitization techniques for timed automata.

##  9\. Acknowledgments

This work is partially supported by the Austrian Science Fund (FWF): P 32021,
the Austrian National Research Network S11403-N23 (RiSE) of the Austrian
Science Fund (FWF), and by the Vienna Science and Technology Fund (WWTF)
through grant ICT12-059.

## References

  * [AAC+18] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke.  Universal safety for timed petri nets is pspace-complete.  In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 6:1–6:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.  doi:10.4230/LIPIcs.CONCUR.2018.6.
  * [ADM04] Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata.  Multi-clock timed networks.  In Harald Ganzinger, editor, LICS, pages 345–354, July 2004.
  * [ADR+16] Parosh Aziz Abdulla, Giorgio Delzanno, Othmane Rezine, Arnaud Sangnier, and Riccardo Traverso.  Parameterized verification of time-sensitive models of ad hoc network protocols.  Theoretical Computer Science, 612:1–22, 2016.
  * [AJ03] Parosh Aziz Abdulla and Bengt Jonsson.  Model checking of systems with many identical timed processes.  TCS, 290(1):241–264, 2003.
  * [AJKR14] B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin.  Parameterized model checking of token-passing systems.  In VMCAI, pages 262–281. Springer, 2014.
  * [AKR+18] Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, and Helmut Veith.  Parameterized model checking of rendezvous systems.  Distributed Computing, 31(3):187–222, 2018.
  * [Alu99] Rajeev Alur.  Timed automata.  In CAV, pages 8–22. Springer, 1999.
  * [AMRZ22] Benjamin Aminof, Aniello Murano, Sasha Rubin, and Florian Zuleger.  Verification of agent navigation in partially-known environments.  Artif. Intell., 308:103724, 2022.  doi:10.1016/j.artint.2022.103724.
  * [AR16] Benjamin Aminof and Sasha Rubin.  Model checking parameterised multi-token systems via the composition method.  In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, volume 9706 of Lecture Notes in Computer Science, pages 499–515. Springer, 2016.  doi:10.1007/978-3-319-40229-1\\_34.
  * [ARZ15] Benjamin Aminof, Sasha Rubin, and Florian Zuleger.  On the expressive power of communication primitives in parameterised systems.  In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 313–328. Springer, 2015.  doi:10.1007/978-3-662-48899-7\\_22.
  * [ARZS15] Benjamin Aminof, Sasha Rubin, Florian Zuleger, and Francesco Spegni.  Liveness of parameterized timed networks.  In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 375–387. Springer, 2015.
  * [AST18] Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur.  Model checking parameterized systems.  In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 685–725. Springer, 2018\.  doi:10.1007/978-3-319-10575-8\\_21.
  * [BF13] Nathalie Bertrand and Paulin Fournier.  Parameterized verification of many identical probabilistic timed processes.  In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2013.
  * [BJK+15] Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder.  Decidability of Parameterized Verification.  Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.
  * [BK00] F. Bacchus and F. Kabanza.  Using temporal logics to express search control knowledge for planning.  Artif. Intell., 116(1-2), 2000.
  * [BM06] Jorge A. Baier and Sheila A. McIlraith.  Planning with first-order temporally extended goals using heuristic search.  In AAAI, 2006.
  * [Boj10] Mikolaj Bojanczyk.  Beyond $\omega$-regular languages.  In STACS 2010, pages 11–16, 2010.
  * [BT18] Clark Barrett and Cesare Tinelli.  Satisfiability Modulo Theories, pages 305–343.  Springer International Publishing, Cham, 2018.  doi:10.1007/978-3-319-10575-8_11.
  * [CETFX09] Remy Chevallier, Emmanuelle Encrenaz-Tiphene, Laurent Fribourg, and Weiwen Xu.  Timed verification of the generic architecture of a memory circuit using parametric timed automata.  Formal Methods in System Design, 34(1):59–81, 2009.
  * [CTV08] Edmund Clarke, Murali Talupur, and Helmut Veith.  Proving ptolemy right: The environment abstraction framework for model checking concurrent systems.  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 33–47. Springer, 2008.
  * [DGV13] Giuseppe De Giacomo and Moshe Y. Vardi.  Linear temporal logic and linear dynamic logic on finite traces.  In IJCAI, 2013.
  * [DSZ10] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro.  Parameterized verification of ad hoc networks.  In International Conference on Concurrency Theory, pages 313–327. Springer, 2010.
  * [EFM99] Javier Esparza, Alain Finkel, and Richard Mayr.  On the verification of broadcast protocols.  In LICS, pages 352–359, 1999.
  * [EL87] E. Allen Emerson and Chin-Laung Lei.  Modalities for model checking: Branching time logic strikes back.  Sci. Comput. Program., 8(3):275–306, 1987.
  * [FH15] Estíbaliz Fraca and Serge Haddad.  Complexity analysis of continuous petri nets.  Fundam. Inform., 137(1):1–28, 2015.
  * [GJ79] M. R. Garey and David S. Johnson.  Computers and Intractability: A Guide to the Theory of NP-Completeness.  W. H. Freeman, 1979.
  * [GS92] Steven M German and A Prasad Sistla.  Reasoning about systems with many processes.  JACM, 39(3):675–735, 1992.
  * [HMP92] Thomas A Henzinger, Zohar Manna, and Amir Pnueli.  What good are digital clocks?  In Automata, Languages and Programming, pages 545–558. Springer, 1992.
  * [HP79] John E. Hopcroft and Jean-Jacques Pansiot.  On the reachability problem for 5-dimensional vector addition systems.  Theor. Comput. Sci., 8:135–159, 1979.
  * [Ise17] Tobias Isenberg.  Incremental inductive verification of parameterized timed systems.  ACM Transactions on Embedded Computing Systems (TECS), 16(2):1–24, 2017.
  * [Jon97] Neil D. Jones.  Computability and complexity - from a programming perspective.  Foundations of computing series. MIT Press, 1997.
  * [JS18] Swen Jacobs and Mouhammad Sakr.  Analyzing guarded protocols: Better cutoffs, more systems, more expressivity.  In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 247–268. Springer, 2018.
  * [KKW14] Alexander Kaiser, Daniel Kroening, and Thomas Wahl.  A widening approach to multithreaded program verification.  ACM Trans. Program. Lang. Syst., 36(4):14:1–14:29, 2014.  doi:10.1145/2629608.
  * [KL16] Panagiotis Kouvaros and Alessio Lomuscio.  Parameterised verification for multi-agent systems.  Artif. Intell., 234:152–189, 2016.  doi:10.1016/j.artint.2016.01.008.
  * [LP22] Alessio Lomuscio and Edoardo Pirovano.  A counter abstraction technique for verifying properties of probabilistic swarm systems.  Artif. Intell., 305:103666, 2022.  doi:10.1016/j.artint.2022.103666.
  * [McM01] Kenneth L. McMillan.  Parameterized verification of the FLASH cache coherence protocol by compositional model checking.  In Tiziana Margaria and Thomas F. Melham, editors, Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings, volume 2144 of Lecture Notes in Computer Science, pages 179–195. Springer, 2001.  doi:10.1007/3-540-44798-9\\_17.
  * [OW03] Joël Ouaknine and James Worrell.  Revisiting digitization, robustness, and decidability for timed automata.  In LICS, pages 198–207, 2003.
  * [Saf88] Shmuel Safra.  On the complexity of omega-automata.  In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 319–327. IEEE Computer Society, 1988.  doi:10.1109/SFCS.1988.21948.
  * [SS13] Sylvain Schmitz and Philippe Schnoebelen.  The power of well-structured systems.  In Pedro R. D’Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 5–24. Springer, 2013.  doi:10.1007/978-3-642-40184-8\\_2.
  * [SS20] Luca Spalazzi and Francesco Spegni.  Parameterized model checking of networks of timed automata with boolean guards.  Theoretical Computer Science, 813:248–269, 2020.
  * [Suz88] Ichiro Suzuki.  Proving properties of a ring of finite-state machines.  Inf. Process. Lett., 28(4):213–214, 1988.
  * [Var95] Moshe Y. Vardi.  An automata-theoretic approach to linear temporal logic.  In Faron Moller and Graham M. Birtwistle, editors, Logics for Concurrency - Structure versus Automata, volume 1043 of LNCS, 1995.  doi:10.1007/3-540-60915-6_6.
  * [ZP04] Lenore D. Zuck and Amir Pnueli.  Model checking and abstraction to the aid of parameterized systems (a survey).  Comput. Lang. Syst. Struct., 30(3-4):139–169, 2004.  doi:10.1016/j.cl.2004.02.006.