decproblem  Input: Question:

11institutetext: IRIF, CNRS, Université Paris Cité, France
22institutetext: DIBRIS, Università di Genova, Italy
33institutetext: LIP6, CNRS, Sorbonne Université, France

# Safety Verification of Wait-Only Non-Blocking Broadcast Protocols

Lucie Guillou 11 Arnaud Sangnier 22 Nathalie Sznajder 33

###### Abstract

We study networks of processes that all execute the same finite protocol and
communicate synchronously in two different ways: a process can broadcast one
message to all other processes or send it to at most one other process. In
both cases, if no process can receive the message, it will still be sent. We
establish a precise complexity class for two coverability problems with a
parameterised number of processes: the state coverability problem and the
configuration coverability problem. It is already known that these problems
are Ackermann-hard (but decidable) in the general case. We show that when the
protocol is _Wait-Only_ , i.e., it has no state from which a process can send
and receive messages, the complexity drops to P and PSpace, respectively.

###### Keywords:

Parameterised Networks Broadcast Verification

##  1 Introduction

#### Verification of distributed systems.

The ubiquity of distributed and concurrent systems in nowadays applications
leads to an increasing need to ensure their correct behaviour. Over the last
two decades, the verification of such systems has become a crucial research
direction in the field of computer science. Indeed, analysing distributed
systems has proven to be challenging. One difficulty is due to the numerous
interleavings caused by the concurrent behaviour of the system entities, that
make the design and modelling of these systems very complex. Moreover, the
number of agents is often not known a priori; in that case, verifying all
possible behaviours of such a system amounts to analyse it for any number of
agents, i.e. an infinite number of times. The unpredictability of the number
of participants in a system makes classical techniques such as model-checking
impractical and requires some new techniques.

#### Parameterised verification.

Addressing the challenge of unbounded entities involves designing schematic
programs or protocols intended for implementation by multiple identical
processes and parameterised by the number of entities. While in general
parameterised verification is undecidable [AK86], several realistic
restrictions enable automatic verification. Among them, one can highlight
systems where entities have no identity, and systems with simple communication
mechanism. Several papers have considered synchronous communication means, as
rendez-vous [GS92, DRB02, HS20, BER21, GSS23] and broadcast [EFM99, DSTZ12].
Note that, surprisingly, parameterised verification, when decidable, is
sometimes significantly easier than the same problem with a fixed number of
entities [DEGM17]. In all those models, all the entities execute the same
program which is modelled as a finite-state automaton.

#### Wait-Only Non-Blocking Broadcast protocols

In [GSS23], the authors have studied the complexity of several parameterised
verification problems in the context of non-blocking rendez-vous. This
communication mechanism, motivated by Java Threads programming, involves at
most two processes: when a process sends a message, it is received by at most
one process ready to receive the message, and both processes jointly change
their local state. However, when no process is ready to receive the message,
the message is sent anyway and lost, and only the sender changes its local
state. This is in contrast with classical rendez-vous as studied for instance
in [GS92], where a sender is prevented to send a message if no process can
receive it. The model proposed in [GSS23] allows to capture some behaviour of
the Threads: when a Thread is suspended in a waiting state, it can be woken up
upon the reception of a notify message sent by another Thread, but the sender
is not blocked if no Thread is suspended; it simply continues its execution
and the notify message is lost. However, this fails to capture the behaviour
of what occurs when a Thread sends a notifyAll message that will be received
by all the suspended Threads waiting for that message. This, as already
highlighted in [DRB02], is modelled by the broadcast mechanism, in which a
message sent by a process will be received by all the processes ready to
receive it. Observe that broadcast is also a non-blocking means of
communication. In this work we consider Non-Blocking Broadcast protocols, that
allow for both broadcast and non-blocking rendez-vous. One important problem
in parameterised verification is the coverability problem: is it possible
that, starting from an initial configuration, (at least) one process reaches a
bad state? With classical rendez-vous mechanism, this problem is in P [GS92],
while with non-blocking rendez-vous, it is Expspace-complete [GSS23]. For
protocols enabling both broadcast and non-blocking rendez-vous, the problem is
decidable [EK03] and Ackermann-hard [SS13, EFM99, ARZ15]. In this work we
study the coverability problem for a syntactic restriction of the protocols,
introduced in [GSS23], namely Wait-Only protocols, in which there is no state
from which a process can both send and receive a message. In this context,
when processes communicate with non-blocking rendez-vous only, the
coverability problem is in P [GSS23].

#### Our contributions.

We show that the coverability problem for Wait-Only Non-Blocking Broadcast
protocols is P-complete, and that the _configuration coverability problem_ is
PSpace-complete. This last problem asks whether it is possible to cover a
given configuration (and not simply a bad state) from an initial state. Note
that both problems are in P when forbidding broadcasts [GSS23], however, in
this work, the P-membership proof is less involved and the PSpace-membership
proof uses a different technique.

##  2 Model and verification problems

We denote by $\mathbb{N}$ the set of natural numbers. For a finite set $E$,
the set $\mathbb{N}^{E}$ represents the multisets over $E$. For two elements
$s,s^{\prime}\in\mathbb{N}^{E}$, we denote by $s+s^{\prime}$ the multiset such
that $(s+s^{\prime})(e)=s(e)+s^{\prime}(e)$ for all $e\in E$. We say that
$s^{\prime}$ is bigger than $s$, denoted $s\preceq s^{\prime}$ if and only if
$s(e)\leq s^{\prime}(e)$ for all $e\in E$. If $s\preceq s^{\prime}$, then
$s^{\prime}-s$ is the multiset such that
$(s^{\prime}-s)(e)=s^{\prime}(e)-s(e)$ for all $e\in E$. Given a subset
$E^{\prime}\subseteq E$ and $s\in\mathbb{N}^{E}$, we denote by
$||s||_{E^{\prime}}$ the sum $\Sigma_{e\in E^{\prime}}s(e)$ of elements of
$E^{\prime}$ present in $s$. The size of a multiset $s$ is given by
$||s||=||s||_{E}$. For $e\in E$, we use sometimes the notation $e$ for the
multiset $s$ verifying $s(e)=1$ and $s(e^{\prime})=0$ for all $e^{\prime}\in
E\setminus\\{e\\}$ and, to represent for instance the multiset with four
elements $a,b,b$ and $c$, we will also use the notations $\Lbag a,b,b,c\Rbag$
or $\Lbag a,2\cdot b,c\Rbag$.

###  2.1 Networks of Processes using Rendez-Vous and Broadcast

We now present the model under study in this work. We consider networks of
processes where each entity executes the same protocol given by a finite state
automaton. Given a finite alphabet $\Sigma$ of messages, the transitions of a
protocol are labelled with four types of actions that can be executed by the
processes of the network. For $m\in\Sigma$ a process can (1) send a (non-
blocking) rendez-vous over the message $m$ with $!m$, (2) send a broadcast
over $m$ with $!!m$, (3) receive a rendez-vous or a broadcast over $m$ with
$?m$ and (4) perform an internal action with $\tau$ (assuming
$\tau\not\in\Sigma$). In order to refer to these different actions, we denote
by $!\Sigma$ the set $\\{!m\mid m\in\Sigma\\}$, by $!!\Sigma$ the set
$\\{!!m\mid m\in\Sigma\\}$ and by $?\Sigma$ the set $\\{?m\mid m\in\Sigma\\}$.
Finally, we use the notation $\mathsf{Op}_{\Sigma}$ to represent the set of
labels $!!\Sigma\cup!\Sigma\cup?\Sigma\cup\\{\tau\\}$ and
$\mathsf{Act}_{\Sigma}$ to represent the set of actions
$!!\Sigma\cup!\Sigma\cup\\{\tau\\}$.

###### Definition 1

A _Non-Blocking Broadcast protocol_ $P$ (NB-Broadcast protocol) is a tuple
$(Q,\Sigma,q_{\textit{in}},T)$ such that $Q$ is a finite set of states,
$\Sigma$ is a finite alphabet, $q_{\textit{in}}$ is an initial state, and
$T\subseteq Q\times\mathsf{Op}_{\Sigma}\times Q$ is the transition relation.

In this work, we are in particular interested in studying some syntactical
restrictions on such protocols. We say that a protocol is _Wait-Only_ when for
all $q\in Q$, either $\\{q^{\prime}\mid(q,\alpha,q^{\prime})\in T\mbox{ with
}\alpha\in?\Sigma\\}=\emptyset$, or $\\{q^{\prime}\mid(q,\alpha,q^{\prime})\in
T\mbox{ with }\alpha\in!!\Sigma\cup!\Sigma\cup\\{\tau\\}\\}=\emptyset$. We
call a state respecting the first or both conditions an _active_ state and a
state respecting the second condition a _waiting_ state. In the following, we
denote by $Q_{A}$ the set of active states of $P$ and $Q_{W}$ its set of
waiting states.

If the protocol does not contain any broadcast transition of the form
$(q,!!m,q^{\prime})$, we call it a _Non-Blocking Rendez-vous protocol_ (NB-
Rendez-vous protocol).

$q_{\textit{in}}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$q_{6}$$!b$$!!a$$?a$$?b$$?a$$!!c$$?c$$!!a$
Figure 1: Example of a protocol denoted $P_{\mathsf{dashed}}$ (we note $P$ the
protocol $P_{\mathsf{dashed}}$ without the dashed arrow between $q_{2}$ and
$q_{3}$)

###### Example 1

An example of protocol is depicted on Figure 1. We name $P$ the protocol drawn
without the dashed arrow between $q_{2}$ and $q_{3}$, and
$P_{\mathsf{dashed}}$ the complete protocol. Note that $P$ is a _Wait-Only_
protocol, indeed each state is either an active state
($q_{\textit{in}},q_{2},q_{3},q_{5}$ and $q_{6}$), or a waiting state,
($q_{1}$ and $q_{4}$). However, $P_{\mathsf{dashed}}$ is not a Wait-Only
protocol, since $q_{2}$ is neither an active state nor a waiting state as it
has an outgoing transition labelled with an action $!!c$, and an outgoing
transition labelled with an action $?a$.

We shall now present the semantics associated to protocols. Intuitively, we
consider networks of processes, each process being in a state of the protocol
and changing its state according to the transitions of the protocol with the
following assumptions. A process can perform on its own an internal action
$\tau$ and this does not change the state of the other processes. When a
process sends a broadcast with the action $!!m$, then all the processes in the
network which are in a state from which the message $m$ can be received (i.e.
with an outgoing transition labelled by $?m$) have to take such a transition.
And when a process sends a rendez-vous with the action $!m$, then _at most_
one process receives it: in fact, if there is at least one process in a state
from which the message $m$ can be received, then exactly one of these
processes has to change its state, along with the receiver (while the other
processes do not move), but if no process can receive the message $m$, only
the sender performs the action $!m$. This is why we call this communication
mechanism a _non-blocking_ rendez-vous.

We move now to the formal definition of the semantics. Let
$P=(Q,\Sigma,q_{\textit{in}},T)$ be a protocol.

A _configuration_ $C$ over $P$ is a non-empty multiset over $Q$, it is
_initial_ whenever $C(q)=0$ for all $q\in Q\setminus\\{q_{\textit{in}}\\}$. We
note $\mathcal{C}$ the set of all configurations over $P$, and $\mathcal{I}$
the set of all initial configurations over $P$.

For $q\in Q$, we denote by $R(q)$ the set $\\{m\in\Sigma\mid\textrm{there
exists }q^{\prime}\in Q,(q,?m,q^{\prime})\in T\\}$ of messages that can be
received when in the state $q$. Given a transition $t=(q,\alpha,q^{\prime})\in
T$, we define the relation
$\xrightarrow{t}\subseteq\mathcal{C}\times\mathcal{C}$ as follows: for two
configurations $C,C^{\prime}$ we have $C\xrightarrow{t}C^{\prime}$ iff one of
the following conditions holds:

  * (a)

$\alpha=\tau$, and $C(q)>0$ and $C^{\prime}=C-\Lbag q\Rbag+\Lbag
q^{\prime}\Rbag$;

  * (b)

$\alpha=!!m$, and $C=\Lbag q_{1},q_{2},\dots,q_{n},q\Rbag$ for some
$n\in\mathbb{N}$, and $C^{\prime}=\Lbag
q^{\prime}_{1},q^{\prime}_{2},\dots,q^{\prime}_{n},q^{\prime}\Rbag$ where for
all $1\leq i\leq n$, either $m\nin R(q_{i})$ and $q^{\prime}_{i}=q_{i}$, or
$(q_{i},?m,q^{\prime}_{i})\in T$;

  * (c)

$\alpha=!m$, and $C(q)>0$, and $(C-\Lbag q\Rbag)(p)=0$ for all $p\in Q$ such
that $m\in R(p)$, and $C^{\prime}=C-\Lbag q\Rbag+\Lbag q^{\prime}\Rbag$;

  * (d)

$\alpha=!m$ and $C(q)>0$ and there exists $p\in Q$ such that $(C-\Lbag
q\Rbag)(p)>0$ and $(p,?m,p^{\prime})\in T$ for some $p^{\prime}\in Q$, and
$C^{\prime}=C-\Lbag p,q\Rbag+\Lbag q^{\prime},p^{\prime}\Rbag$.

Observe that when $C\xrightarrow{t}C^{\prime}$, we necessarily have
$||C||=||C^{\prime}||$.

The case (a) corresponds to the internal action of a single process, the case
(b) to the emission of a broadcast hence all the processes that can receive
the message have to receive it. The case (c) corresponds to the case where a
process sends a rendez-vous and there is no process to answer to it, hence
only the sender changes its state. The case (d) corresponds to a classical
rendez-vous where a process sends a rendez-vous and another process receives
it. Note that for both the broadcast and the rendez-vous, the absence of a
receiver does not prevent a sender from its action. We call non-blocking our
semantics because of the case (c), which contrasts with the broadcast model of
[EFM99] for instance, where this case is not possible.

We write $C\rightarrow C^{\prime}$ whenever there exists $t\in T$ such that
$C\xrightarrow{t}C^{\prime}$, and denote by $\rightarrow^{\ast}$ [resp.
$\rightarrow^{+}$] the reflexive and transitive [resp. transitive] closure of
$\rightarrow$. An execution $\rho$ is then a finite sequence of the form
$C_{0}\xrightarrow{t_{1}}C_{1}\xrightarrow{t_{2}}\ldots\xrightarrow{t_{n}}C_{n}$,
it is said to be initialized when $C_{0}$ is an initial configuration in
$\mathcal{I}$.

###### Example 2

We consider the protocol $P$ of Figure 1. We have then the following execution
starting at the initial configuration $\Lbag
q_{\textit{in}},q_{\textit{in}},q_{\textit{in}}\Rbag$ with three processes:

$\begin{array}[]{l}\Lbag
q_{\textit{in}},q_{\textit{in}},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!!a,q_{1})}\Lbag
q_{1},q_{\textit{in}},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!b,q_{4})}\Lbag
q_{2},q_{4},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!b,q_{4})}\Lbag
q_{2},q_{4},q_{4}\Rbag\\\ \xrightarrow{(q_{2},!!c,q_{1})}\Lbag
q_{1},q_{5},q_{5}\Rbag\xrightarrow{(q_{5},!!a,q_{6})}\Lbag
q_{3},q_{6},q_{5}\Rbag.\end{array}$

It corresponds to the following sequence of events: one of the agents
broadcasts message $a$ (not received by anyone), then another agent sends
message $b$ which leads to a rendez-vous with the first agent on $q_{1}$, the
last agent sends message $b$ which is not received by anyone (the sending is
possible thanks to the non-blocking semantics), the agent in state $q_{2}$
broadcasts message $c$ which is received by the two other agents, and finally,
one of the agents in $q_{5}$ broadcasts letter $a$ which is received by the
process on $q_{1}$.

###### Remark 1

Observe that internal transitions labelled by $\tau$ can be replaced by
broadcast transitions of the form $!!\tau$. Since no transition is labelled by
$?\tau$, when $\tau$ is broadcasted, no process is ready to receive it and the
semantics is equivalent to the one of an internal transition. Observe also
that since $\tau\in\mathsf{Act}_{\Sigma}$, transforming internal transitions
into broadcasts keeps a protocol Wait-Only.

Following this remark, we will omit internal transitions in the rest of this
work.

###  2.2 Verification Problems

We present now the verification problems we are interested in. Both these
problems consist in ensuring a safety property: we want to check that, no
matter the number of processes in the network, a configuration exhibiting a
specific pattern can never be reached. If the answer to the problem is
positive, it means in our context that the protocol is not safe.

The state coverability problem StateCover is stated as follows:

When the answer is positive, we say that $q_{f}$ is _coverable_ by $P$. The
second problem, called the configuration coverability problem ConfCover, is a
generalisation of the first one where we look for a multi-set to be covered.

###### Remark 2

Note that if $P$ is a Wait-Only protocol and its initial state
$q_{\textit{in}}$ is a waiting state, then no state besides $q_{\textit{in}}$
is coverable and the only coverable configurations are the initial ones.
Hence, when talking about Wait-Only protocols, we assume in the rest of this
work that the initial state $q_{\textit{in}}$ is always an _active state_.

###### Example 3

In the protocol $P$ of Figure 1, configuration $\Lbag q_{3},q_{6}\Rbag$ is
coverable as $\Lbag
q_{\textit{in}},q_{\textit{in}},q_{\textit{in}}\Rbag\rightarrow^{\ast}\Lbag
q_{3},q_{6},q_{5}\Rbag$ (see Example 2) and $\Lbag
q_{3},q_{6}\Rbag\preceq\Lbag q_{3},q_{6},q_{5}\Rbag$.

#### Results.

We summarize in Table 1 the results on NB-Broadcast protocols, where our
results appear in red. Note that for what concerns the lower bounds for NB-
Broadcast protocols, they have been proved in [SS13][Fact16, Remark 17] for
Broadcast protocols with a classical “blocking” rendez-vous semantics, i.e.
where a process requesting a rendez-vous cannot take the transition if no
process answers the rendez-vous. However, it is possible to retrieve the lower
bound for NB-Broadcast protocols without rendez-vous by using the fact that
“blocking” rendez-vous can be simulated by broadcast as shown in [EFM99,
ARZ15].

Type of protocols |  StateCover | ConfCover
---|---|---
NB-Broadcast | Decidable[EK03] and Ackermann-hard [SS13, ARZ15, EFM99]
NB-Rendez-vous |  ExpSpace-complete [GSS23]
Wait-Only NB-Rendez-vous | in P [GSS23], P-hard
Wait-Only NB-Broadcast | P-complete | PSpace-complete
Table 1: Coverability in NB-Broadcast protocols

In the rest of this work, we will focus on Wait-Only NB-Broadcast protocols
which we name Wait-Only protocols for ease of notation.

##  3 Preliminaries properties

Wait-Only protocols enjoy a nice property on coverable states. The property
makes a distinction between active states and waiting states. First, we show
that when an active state is coverable, then it is coverable by a number of
processes as big as one wants, whereas this is not true for a waiting state.
Indeed, it is possible that a waiting state can be covered by exactly one
process at a time, and no more. However, we show that if two active states, or
if an active state and a waiting state are coverable, then there is an
execution that reaches a configuration where they are both covered.

This property relies on the fact that once the active state has been covered
in an execution, it will not be emptied while performing the sequence of
actions allowing to cover the second (waiting state), since no reception of
message can happen in such a state. As we will see, this phenomenon can be
generalised to a subset of active states.

###### Example 4

Going back to the protocol $P$ of Figure 1, consider the active state $q_{2}$.
It is coverable as shown by the execution $\Lbag
q_{\textit{in}},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!!a,q_{1})}\Lbag
q_{1},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!b,q_{4})}\Lbag
q_{2},q_{4}\Rbag$. From this execution, for any integer $n\in\mathbb{N}$, one
can build an execution leading to a configuration covering $\Lbag n\cdot
q_{2}\Rbag$. For instance, for $n=2$, we build the following execution:

$\displaystyle\Lbag
q_{\textit{in}},q_{\textit{in}},q_{\textit{in}},q_{\textit{in}}\Rbag$
$\displaystyle\xrightarrow{(q_{\textit{in}},!!a,q_{1})}\Lbag
q_{1},q_{\textit{in}},q_{\textit{in}},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!b,q_{4})}\Lbag
q_{2},q_{4},q_{\textit{in}},q_{\textit{in}}\Rbag$
$\displaystyle\xrightarrow{(q_{\textit{in}},!!a,q_{1})}\Lbag
q_{2},q_{4},q_{1},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!b,q_{4})}\Lbag
q_{2},q_{4},q_{2},q_{4}\Rbag.$

Furthermore each coverable waiting state is coverable by a configuration that
also contains $q_{2}$. For instance, $\Lbag q_{2},q_{4}\Rbag$ is coverable as
shown by the above execution.

Note that when considering $P_{\mathsf{dashed}}$, which is not Wait-Only, such
an execution is not possible as the second broadcast of $a$ should be received
by the process on $q_{2}$. In fact, $q_{2}$ is coverable by only one process
and no more. This is because $q_{1}$ is coverable by at most one process at a
time; every new process arriving in state $q_{1}$ will do so by broadcasting
$a$, message that will be received by the process already in $q_{1}$. Then any
attempt to send two processes in $q_{2}$ requires a broadcast of $a$, hence
the reception of $a$ by the process already in $q_{2}$. For the same reason,
in $P_{\mathsf{dashed}}$, $\Lbag q_{1},q_{2}\Rbag$ is not coverable whereas
$q_{1}$ is a coverable waiting state and $q_{2}$ a coverable active state.

Before stating the main lemma of this section (Lemma 1), we need an additional
definition. For each _coverable_ state $q\in Q$, let $\textsf{min}_{q}$ be the
minimal number of processes needed to cover $q$. More formally,
$\textsf{min}_{q}=\min\\{n\mid n\in\mathbb{N},\textrm{ there exists
}C\in\mathcal{C}\text{ s. t. }\Lbag
n.q_{\textit{in}}\Rbag\rightarrow^{\ast}C\text{ and }C(q)>0\\}$. Note that
$\textsf{min}_{q}$ is defined only when $q$ is coverable.

###### Lemma 1

Let $P=(Q,\Sigma,q_{\textit{in}},T)$ be a Wait-Only protocol,
$A=\\{q_{1},\dots,q_{n}\\}\subseteq Q_{A}$ a subset of coverable _active_
states and $p\in Q_{W}$ a coverable _waiting_ state. Then, for all
$N\in\mathbb{N}$, there exists an execution $C_{0}\rightarrow^{\ast}C_{m}$
such that $C_{0}\in\mathcal{I}$, and $\\{N\cdot q_{1},\dots,N\cdot
q_{n},p\\}\preceq C_{m}$. Moreover,
$||C_{0}||=N.\sum^{n}_{i=1}\textsf{min}_{q_{i}}+\textsf{min}_{p}$.

The proof of this lemma relies on the two following properties on executions
of Wait-Only protocols:

###### Lemma 2

Given an initialized execution
$C_{0}\xrightarrow{t_{1}}C_{1}\xrightarrow{t_{2}}\dots...\xrightarrow{t_{k}}C_{k}$
and another initial configuration $C^{\prime}_{0}$, we can build an execution
$\widehat{C_{0}}\xrightarrow{t_{1}}\widehat{C_{1}}\xrightarrow{t_{2}}\dots...\xrightarrow{t_{k}}\widehat{C_{k}}$
with $\widehat{C_{0}}=C_{0}+C^{\prime}_{0}$. For all $0\leq i\leq k$,
$\widehat{C_{i}}(q)=C_{i}(q)$ for all $q\in Q\setminus\\{q_{\textit{in}}\\}$,
and
$\widehat{C_{i}}(q_{\textit{in}})=C_{i}(q_{\textit{in}})+C^{\prime}_{0}(q_{\textit{in}})$.

This property comes from the fact that $q_{\textit{in}}$ is an active state.
Hence, if we start from a bigger configuration, we can take exactly the same
transitions as in the initial execution, the additional processes will stay in
the initial state.

###### Lemma 3

Given an initialized execution
$C_{0}\xrightarrow{t_{1}}C_{1}\xrightarrow{t_{2}}\dots...\xrightarrow{t_{k}}C_{k}$,
given some $M\geq 1$, for all configurations (not necessarily initial)
$\widetilde{C}_{0}$ such that $\widetilde{C}_{0}(q_{\textit{in}})\geq
M.C_{0}(q_{\textit{in}})$, we have the execution
$\widetilde{C}_{0}\xrightarrow{t_{1}}\dots\xrightarrow{t_{k}}\widetilde{C}_{k}$
in which, for all $0\leq i\leq k$:
$\widetilde{C}_{i}(q)\geq\widetilde{C}_{0}(q)+C_{i}(q)$ for all $q\in
Q_{A}\setminus\\{q_{\textit{in}}\\}$, $\widetilde{C}_{i}(q)\geq C_{i}(q)$ for
all $q\in Q_{W}$ and
$\widetilde{C}_{i}(q_{\textit{in}})\geq(M-1).C_{0}(q_{\textit{in}})+C_{i}(q_{\textit{in}})$.

This last property states that, if one mimicks an initialized execution from
another (non initial) configuration, the processes already present in _active_
states (different from the initial state) will not move during the execution.

Proof of Lemma 1. Let $N\in\mathbb{N}$. Using these two properties, we can now
prove the lemma. We start by proving that there exists an execution
$C_{0}\rightarrow^{\ast}C_{m}$ such that for all $q\in A$, $C_{m}(q)\geq N$
and $||C_{0}||=N.\sum_{i=1}^{n}\textsf{min}_{q_{i}}$. We prove it by induction
on the size of $A$. If $A=\emptyset$, the property is trivially true. Let
$n\in\mathbb{N}$, and assume the property to hold for all subsets $A\subseteq
Q_{A}$ of size $n$. Take $A=\\{q_{1},q_{2},\dots,q_{n+1}\\}\subseteq Q_{A}$ of
size $n+1$ such that all states $q\in A$ are coverable and let
$A^{\prime}=A\setminus\\{q_{1}\\}$. Let
$C_{0}\xrightarrow{t_{1}}C_{1}\xrightarrow{t_{2}}\dots...\xrightarrow{t_{k}}C_{k}$
be an execution covering $q_{1}$ with $||C_{0}||=\textsf{min}_{q_{1}}$. Let
$C^{\prime}_{0}\xrightarrow{t^{\prime}_{1}}C^{\prime}_{1}\xrightarrow{t^{\prime}_{2}}\dots\xrightarrow{t^{\prime}_{m}}C^{\prime}_{m}$
be an execution such that for all $q^{\prime}\in A^{\prime}$,
$C^{\prime}_{m}(q^{\prime})\geq N$ and
$||C^{\prime}_{0}||=N.\sum_{i=2}^{n+1}\textsf{min}_{q_{i}}$ (it exists by
induction hypothesis). We let $C_{0}^{N}=\Lbag(N.\textsf{min}_{q_{1}})\cdot
q_{\textit{in}}\Rbag$ and $C^{\prime\prime}_{0}=C^{\prime}_{0}+C_{0}^{N}$.
Thanks to Lemma 2, we can build an execution
$C^{\prime\prime}_{0}\xrightarrow{t^{\prime}_{1}}C^{\prime\prime}_{1}\xrightarrow{t^{\prime}_{2}}\dots\xrightarrow{t^{\prime}_{m}}C^{\prime\prime}_{m}$,
with $C^{\prime\prime}_{m}(q)=C^{\prime}_{m}(q)$ for all $q\in
Q\setminus\\{q_{\textit{in}}\\}$ and
$C^{\prime\prime}_{m}(q_{\textit{in}})=C^{\prime}_{m}(q_{\textit{in}})+C_{0}^{N}(q_{\textit{in}})=C^{\prime}_{m}(q_{\textit{in}})+N.\textsf{min}_{q_{1}}$.
So, for all $q^{\prime}\in A^{\prime}$,
$C^{\prime\prime}_{m}(q^{\prime})=C^{\prime}_{m}(q^{\prime})\geq N$ and
$||C^{\prime\prime}_{0}||=||C^{\prime}_{0}||+||C_{0}^{N}||=N.\sum_{i=2}^{n+1}\textsf{min}_{q_{i}}+N.\textsf{min}_{q_{1}}$.

Now that we have shown how to build an execution that leads to a configuration
with more than $N$ processes on all states in $A^{\prime}$ and enough
processes in the initial state, we show that mimicking $N$ times the execution
allowing to cover $q_{1}$ allows to obtain the desired result. Let
$C_{0,1}=C^{\prime\prime}_{m}$. We know that for all $q^{\prime}\in
A^{\prime}$, $C_{0,1}(q^{\prime})\geq N$, and $C_{0,1}(q_{\textit{in}})\geq
N.\textsf{min}_{q_{1}}$. Since $||C_{0}||=\textsf{min}_{q_{1}}$, using Lemma
3, we can build the execution
$C_{0,1}\xrightarrow{t_{1}}\dots\xrightarrow{t_{k}}C_{k,1}$ with
$C_{k,1}(q_{\textit{in}})\geq(N-1).\textsf{min}_{q_{1}}$,
$C_{k,1}(q^{\prime})\geq C_{0,k}(q^{\prime})+C_{k}(q^{\prime})\geq N$ for all
$q^{\prime}\in A^{\prime}$ and $C_{k,1}(q_{1})\geq
C_{0,k}(q_{1})+C_{k}(q_{1})\geq 1$. Iterating this construction and applying
each time Lemma 3, we obtain that there is an execution
$C_{0,1}\xrightarrow{t_{1}}\dots\xrightarrow{t_{k}}C_{k,1}\xrightarrow{t_{1}}\dots\xrightarrow{t_{k}}C_{k,2}\dots\xrightarrow{t_{1}}\dots\xrightarrow{t_{k}}C_{k,N-1}\xrightarrow{t_{1}}\dots\xrightarrow{t_{k}}C_{k,N}$
with $C_{k,i}(q_{\textit{in}})\geq(N-i).\textsf{min}_{q_{1}}$,
$C_{k,i}(q^{\prime})\geq N$ for all $q^{\prime}\in A^{\prime}$ and
$C_{k,i}(q_{1})\geq C_{k,i-1}(q_{1})+1\geq i$. Observe that to obtain that
$C_{k,i}(q_{1})\geq i$ from Lemma 3, we use the fact that $q_{1}\in Q_{A}$.
Hence, $C_{k,N}(q_{1})\geq N$ and $C_{k,N}(q^{\prime})\geq N$ for all
$q^{\prime}\in A^{\prime}$ and we have build an execution where
$C_{k,N}(q)\geq N$ for all $q\in A$ and
$||C_{k,N}||=||C^{\prime\prime}_{0}||=N.\sum_{i=1}^{|A|}\textsf{min}_{q_{i}}$,
as expected.

At last, take a subset $A=\\{q_{1},\dots,q_{n}\\}\subseteq Q_{A}$ of coverable
active states. Let $C_{0}\rightarrow^{\ast}C_{m}$ be an execution such that
$C_{m}(q)\geq N$ for all $q\in A$ and
$||C_{0}||=N.\sum_{i=1}^{n}\textsf{min}_{q_{i}}$. Let $p\in Q_{W}$ a coverable
state and $C^{\prime}_{0}\rightarrow^{\ast}C^{\prime}_{k}$ such that
$C^{\prime}_{k}(p)\geq 1$ and $||C^{\prime}_{0}||=\textsf{min}_{p}$. By Lemma
2, we let $\widehat{C}_{0}=C_{0}+C^{\prime}_{0}$ and we have an execution
$\widehat{C}_{0}\rightarrow^{\ast}\widehat{C}_{m}$ with
$\widehat{C}_{m}(q)=C_{m}(q)$ for all $q\in Q\setminus\\{q_{\textit{in}}\\}$,
and
$\widehat{C}_{m}(q_{\textit{in}})=C_{m}(q_{\textit{in}})+C^{\prime}_{0}(q_{\textit{in}})$.
Hence, $\widehat{C}_{m}(q)\geq N$ for all $q\in A$ and
$\widehat{C}_{m}(q_{\textit{in}})\geq C^{\prime}_{0}(q_{\textit{in}})$, and
note that
$||\widehat{C}_{m}||=||\widehat{C}_{0}||=||C_{0}||+||C^{\prime}_{0}||=N.\sum_{i=1}^{n}\textsf{min}_{q_{i}}+\textsf{min}_{p}$.
Then, with $\widetilde{C}_{0}=\widehat{C}_{m}$, by Lemma 3, we have an
execution $\widetilde{C}_{0}\rightarrow^{\ast}\widetilde{C}_{k}$ with
$\widetilde{C}_{k}(q)\geq\widetilde{C}_{0}(q)+C_{k}(q)\geq\widetilde{C}_{0}(q)\geq
N$ for all $q\in A$, and $\widetilde{C}_{k}(p)\geq C_{k}(p)\geq 1$, and
$||\widetilde{C}_{0}||=||\widehat{C}_{0}||=N.\sum_{i=1}^{n}\textsf{min}_{q_{i}}+\textsf{min}_{p}$.

$\square$

##  4 StateCover for Wait-Only protocols is P-complete

###  4.1 Upper bound

We present here a polynomial time algorithm to solve the state coverability
problem when the considered protocol is Wait-Only. Our algorithm computes in a
greedy manner the set of coverable states using Lemma 1.

Given a Wait-Only protocol $P=(Q,\Sigma,q_{\textit{in}},T)$, we compute
iteratively a set of states $S\subseteq Q$ containing all the states that are
coverable by $P$, by relying on a family $(S_{i})_{i\in\mathbb{N}}$ of subsets
of $Q$ formally defined as follows (we recall that
$\mathsf{Act}_{\Sigma}=!!\Sigma\cup!\Sigma$):

$\displaystyle S_{0}=\\{q_{\textit{in}}\\}$ $\displaystyle S_{i+1}=S_{i}\
\cup\ \\{q\mid\textrm{there exists }q^{\prime}\in
S_{i},(q^{\prime},\alpha,q)~\in T,\alpha\in\mathsf{Act}_{\Sigma}\\}$
$\displaystyle\cup\\{q^{\prime}_{2}\mid\textrm{there exist }q_{1},q_{2}\in
S_{i},q^{\prime}_{1}\in Q,a\in\Sigma\textrm{ s. t.
}(q_{1},!a,q^{\prime}_{1})\in T\textrm{ and~}(q_{2},?a,q^{\prime}_{2})\in
T\\}$ $\displaystyle\cup\\{q^{\prime}_{2}\mid\textrm{there
exist~}q_{1},q_{2}\in S_{i},q^{\prime}_{1}\in Q,a\in\Sigma\textrm{ s. t.
}(q_{1},!!a,q^{\prime}_{1})\in T\textrm{ and~}(q_{2},?a,q^{\prime}_{2})\in
T\\}$

Intuitively at each iteration, we add some control states to $S_{i+1}$ either
if they can be reached from a transition labelled with an action (in
$\mathsf{Act}_{\Sigma}$) starting at a state in $S_{i}$ or if they can be
reached by two transitions corresponding to a communication by broadcast or by
rendez-vous starting from states in $S_{i}$. We then define
$S=\bigcup_{n\in\mathbb{N}}S_{n}$. Observe that $(S_{i})_{i\in\mathbb{N}}$ is
an increasing sequence such that $|S_{i}|\leq|Q|$ for all $i\in\mathbb{N}$.
Then we reach a fixpoint $M\leq|Q|$ such that $S_{M}=S_{M+1}=S$. Hence $S$ can
be computed in polynomial time.

The two following lemmas show correctness of this algorithm. We first prove
that any state $q\in S$ is indeed coverable by $P$. Moreover, we show that
$\textsf{min}_{q}$ the minimal number of processes necessary to cover $q\in Q$
is smaller than $2^{|Q|}$.

###### Lemma 4

If $q\in S$, then there exists $C\in\mathcal{I}$ and
$C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$,
$C^{\prime}(q)>0$ and $||C||\leq 2^{|Q|}$.

###### Proof

Let $M\in\mathbb{N}$ be the first natural such that $S_{M}=S_{M+1}$. We have
then $S_{M}=S$ and $M\leq|Q|$. We prove by induction that for all $0\leq i\leq
M$, for all $q\in S_{i}$, there exists $C\in\mathcal{I}$ and
$C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$,
$C^{\prime}(q)>0$ and $||C||\leq 2^{i}$.

As $S_{0}=\\{q_{\textit{in}}\\}$, the property trivially holds for $i=0$,
since $\Lbag q_{\textit{in}}\Rbag\in\mathcal{I}$ and $\Lbag
q_{\textit{in}}\Rbag(q_{\textit{in}})>0$.

Assume now the property to be true for $i<M$ and let $q\in S_{i+1}$. If $q\in
S_{i}$, then by induction hypothesis, we have that there exists
$C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$ such that
$C\rightarrow^{\ast}C^{\prime}$, $C^{\prime}(q)>0$ and $||C||\leq
2^{i}<2^{i+1}$. We suppose that $q\notin S_{i}$ and proceed by a case analysis
on the way $q$ has been added to $S_{i+1}$.

  1. 1.

there exists $q^{\prime}\in S_{i}$ and $t=(q^{\prime},\alpha,q)\in T$ with
$\alpha\in\mathsf{Act}_{\Sigma}$. By induction hypothesis, there exists an
execution $C\rightarrow^{\ast}C^{\prime}$ such that $C^{\prime}(q^{\prime})>0$
and $||C||\leq 2^{i}$. But we have then
$C^{\prime}\xrightarrow{t}C^{\prime\prime}$ with $C^{\prime\prime}(q)>0$, and
consequently as well $C\rightarrow^{\ast}C^{\prime\prime}$. This is true
because of the “non-blocking” nature of both broadcast and rendez-vous message
in this model. Hence there is no need to check for a process to receive the
message to ensure the execution $C\rightarrow^{\ast}C^{\prime\prime}$.

  2. 2.

there exist $q_{1},q_{2}\in S_{i}$ and $q^{\prime}_{1}\in Q$ and there exists
$a\in\Sigma$ such that $(q_{1},!a,q^{\prime}_{1}),(q_{2},\linebreak[0]?a,q)\in
T$. By induction hypothesis, we have that there exists
$C_{1},C_{2}\in\mathcal{I}$ and $C^{\prime}_{1},C^{\prime}_{2}\in\mathcal{C}$
such that $C_{1}\rightarrow^{\ast}C^{\prime}_{1}$ and
$C_{2}\rightarrow^{\ast}C^{\prime}_{2}$ and $C^{\prime}_{1}(q_{1})>0$ and
$C^{\prime}_{2}(q_{2})>0$ and $||C_{1}||\leq 2^{i}$ and $||C_{2}||\leq 2^{i}$.
Note furthermore that by definition $q_{1}$ is in $Q_{A}$ and as
$(q_{2},?a,q)\in T$, $q_{2}$ do not belong to $Q_{A}$. Hence $q_{1}\neq
q_{2}$. By Lemma 1, we know that there exist $C\in\mathcal{I}$ and
$C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ and
$C^{\prime}(q_{1})>0$ and $C^{\prime}(q_{2})>0$. Furthermore, recall that
$\textsf{min}_{q_{i}}$ for $i\in\\{1,2\\}$ is the minimal number of processes
needed to cover $q_{i}$, by Lemma 1,
$||C||\leq\textsf{min}_{q_{1}}+\textsf{min}_{q_{2}}$. By induction hypothesis,
$\textsf{min}_{q_{1}}+\textsf{min}_{q_{2}}\leq 2^{i}+2^{i}$, hence $||C||\leq
2^{i+1}$.

We then have
$C^{\prime}\xrightarrow{(q_{1},!a,q^{\prime}_{1})}C^{\prime\prime}$ with
$C^{\prime\prime}=C^{\prime}-\Lbag q_{1},q_{2}\Rbag+\Lbag
q^{\prime}_{1},q\Rbag$. Hence $C\rightarrow^{\ast}C^{\prime\prime}$ with
$C^{\prime\prime}(q)>0$.

  3. 3.

there exist $q_{1},q_{2}\in S_{i}$ and $q^{\prime}_{1}\in Q$ and there is some
$a\in\Sigma$ such that
$(q_{1},!!a,q^{\prime}_{1}),(q_{2},\linebreak[0]?a,q)\in T$. As above, we
obtain the existence of an execution $C\rightarrow^{\ast}C^{\prime}$ with
$C^{\prime}(q_{1})>0$ and $C^{\prime}(q_{2})>0$, and $||C||\leq 2^{i+1}$. Then
$C^{\prime}=\Lbag q_{1},q_{2},\dots,q_{k}\Rbag$ and
$C^{\prime}\xrightarrow{(q_{1},!!a,q^{\prime}_{1})}C^{\prime\prime}$ with
$C^{\prime\prime}=\Lbag q^{\prime}_{1},q,\dots,q^{\prime}_{k}\Rbag$ with, for
all $3\leq j\leq k$, either $a\notin R(q_{j})$ and $q_{j}=q^{\prime}_{j}$ or
$(q_{j},?a,q^{\prime}_{j})\in T$. In any case, we have
$C\rightarrow^{\ast}C^{\prime\prime}$ with $C^{\prime\prime}(q)>0$.

So, for any $q\in S$, $q\in S_{M}$ and we have an execution
$C\rightarrow^{\ast}C^{\prime}$ with $C\in\mathcal{I}$ such that
$C^{\prime}(q)>0$ and $||C||\leq 2^{M}\leq 2^{|Q|}$. ∎

We now prove the completeness of our algorithm by showing that every state
coverable by $P$ belongs to $S$.

###### Lemma 5

If there exists $C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$ such that
$C\rightarrow^{\ast}C^{\prime}$ and $C^{\prime}(q)>0$, then $q\in S$.

###### Proof

We consider the initialized execution
$C_{0}\xrightarrow{t_{1}}C_{1}\xrightarrow{t_{2}}\ldots\xrightarrow{t_{n}}C_{n}$
with $C=C_{0}$ and $C_{n}=C^{\prime}$. We will prove by induction on $0\leq
i\leq n$ that for all $q$ such that $C_{i}(q)>0$, we have $q\in S_{i}$.

For $i=0$, we have $C_{0}=\Lbag||C||\cdot q_{\textit{in}}\Rbag$, and
$S_{0}=\\{q_{0}\\}$. Hence the property holds.

Assume the property to be true for $i<n$, and let $q\in Q$ such that
$C_{i+1}(q)>0$. If $C_{i}(q)>0$, then by induction hypothesis we have $q\in
S_{i}$ and since $S_{i}\subseteq S_{i+1}$, we deduce that $q\in S_{i+1}$.
Assume now that $C_{i}(q)=0$. We proceed by a case analysis.

  1. 1.

$t_{i+1}=(q^{\prime},!a,q)$ or $t_{i+1}=(q^{\prime},!!a,q)$ for some
$a\in\Sigma$ and $q^{\prime}\in Q$. Since $C_{i}\xrightarrow{t_{i+1}}C_{i+1}$,
we have necessarily $C_{i}(q^{\prime})>0$. By induction hypothesis,
$q^{\prime}\in S_{i}$, and by construction of $S_{i+1}$, we deduce that
$q^{\prime}\in S_{i+1}$.

  2. 2.

$t_{i+1}=(q_{1},!a,q^{\prime}_{1})$ or $t_{i+1}=(q_{1},!!a,q^{\prime}_{1})$
with $q^{\prime}_{1}\neq q$. Since $C_{i}(q)=0$ and $C_{i+1}(q)>0$, there
exists a transition of the form $(q_{2},?a,q)$ with $q_{1}\neq q_{2}$ (because
$q_{1}\in Q_{A}$ and $(q_{2},?a,q)\in T$ hence $q_{2}\nin Q_{W}$).
Consequently, we know that we have $C_{i}(q_{1})>0$ and $C_{i}(q_{2})>0$. By
induction hypothesis $q_{1},q_{2}$ belong to $S_{i}$ and by construction of
$S_{i+1}$ we deduce that $q\in S_{i+1}$.

∎

The two previous lemmas show the soundness and completeness of our algorithm
to solve StateCover based on the computation of the set $S$. Since this set of
states can be computed in polynomial time, we obtain the following result.

###### Theorem 4.1

StateCover is in P for Wait-Only protocols.

Furthermore, completeness of the algorithm along with the bound on the number
of processes established in Lemma 4 gives the following result.

###### Corollary 1

Given a Wait-Only protocol $P=(Q,\Sigma,q_{\textit{in}},T)$, for all $q\in Q$
coverable by $P$, then $\textsf{min}_{q}$ the minimal number of processes
necessary to cover $q$ is at most $2^{|Q|}$.

###  4.2 Lower Bound

We show that StateCover for Wait-Only protocols is P-hard. For this, we
provide a reduction from the Circuit Value Problem (CVP) which is known to be
P-complete [Lad75]. CVP is defined as follows: given an acyclic Boolean
circuit with $n$ input variables, one output variable, $m$ boolean gates of
type _and_ , _or_ , _not_ , and a truth assignment for the input variables, is
the value of the output equal to a given boolean value? Given an instance of
the CVP, we build a protocol in which the processes broadcast variables (input
ones or associated with gates) along with their boolean values. These
broadcasts will be received by other processes that will use them to compute
boolean value of their corresponding gate, and broadcast the obtained value.
Hence, different values are propagated through the protocol representing the
circuit, until the state representing the output variable value we look for is
covered.

Take for example a CVP instance $C$ with two variables $v_{1},v_{2}$, and two
gates: one _not_ gate on variable $v_{1}$ denoted $g_{1}(v_{1},\lnot,o_{1})$
(where $o_{1}$ stands for the output variable of $g_{1}$), and one _or_ gate
on variable $v_{2}$ and $o_{1}$ denoted $g_{2}(o_{1},v_{2},\lor,o_{2})$ (where
$o_{2}$ stands for the output variable of gate $g_{2}$). Assume the input
boolean value for $v_{1}$ [resp. $v_{2}$] is $\top$ [resp. $\bot$]. The
protocol associated to $C$ is displayed on Figure 2. Assume the output value
of $C$ is $o_{2}$, we will show that $q_{\top}^{2}$ [resp. $q_{\bot}^{2}$] is
coverable if and only if $o_{2}$ evaluates to $\top$ [resp. $\bot$]. Note that
with the truth assignment depicted earlier, $o_{2}$ evaluates to $\bot$, and
indeed one can build an execution covering $q_{\bot}^{2}$ with three
processes:

$\displaystyle\Lbag 3.q_{\textit{in}}\Rbag\rightarrow\Lbag
2.q_{\textit{in}},q_{0}^{2}\Rbag\rightarrow\Lbag
q_{\textit{in}},q_{0}^{1},q_{0}^{2}\Rbag\xrightarrow{(q_{\textit{in}},!!(v_{1},\top),q_{\textit{in}})}\Lbag
q_{\textit{in}},q_{\bot}^{1},q_{0}^{2}\Rbag$
$\displaystyle\xrightarrow{(q_{\bot}^{1},!!(o_{1},\bot),q_{\bot}^{1})}\Lbag
q_{\textit{in}},q_{\bot}^{1},q_{1}^{2}\Rbag\xrightarrow{(q_{\textit{in}},!!(v_{2},\bot),q_{\textit{in}})}\Lbag
q_{\textit{in}},q_{\bot}^{1},q_{\bot}^{2}\Rbag$

$q_{\textit{in}}$$q_{0}^{1}$$q_{\top}^{1}$$q_{\bot}^{1}$$q_{0}^{2}$$q_{\top}^{2}$$q_{1}^{2}$$q_{\bot}^{2}$$!!\tau$$!!\tau$
$!!(v_{1},\top)$
---
$!!(v_{2},\bot)$
$?(v_{1},\bot)$$?(v_{1},\top)$$!!(o_{1},\bot)$$!!(o_{1},\top)$$?(o_{1},\top)$$?(v_{2},\top)$$?(o_{1},\bot)$$!!(o_{2},\top)$$?(v_{2},\bot)$$!!(o_{2},\bot)$
Figure 2: Protocol for a CVP instance with two variables $v_{1},v_{2}$, two
gates $g_{1}(\lnot,v_{1},o_{1})$ and $g_{2}(\vee,o_{1},v_{2},o_{2})$, and
input $\top$ for $v_{1}$ and $\bot$ for $v_{2}$ and output variable $o_{2}$.
Depending on the truth value of $o_{2}$ to test, the state we ask to cover can
be $q_{\bot}^{2}$ or $q_{\top}^{2}$.

Formal proofs of the reduction are given in Appendix 0.B. Together with
Theorem 4.1, we get the following theorem.

###### Theorem 4.2

StateCover for Wait-Only protocols is P-complete.

This reduction can be adapted to Wait-Only NB-Rendez-vous protocols, which
leads to the following theorem, proving that the upper bound presented in
[GSS23] is tight.

###### Theorem 4.3

StateCover for Wait-Only NB-Rendez-vous protocols is P-hard.

##  5 ConfCover for Wait-Only protocols is PSpace-complete

We present here an algorithm to solve the configuration coverability problem
for Wait-Only protocols in polynomial space.

###  5.1 Main ideas

For the remaining of the section, we fix a Wait-Only protocol
$P=(Q,\Sigma,q_{\textit{in}},T)$ and a configuration $C_{f}\in\mathcal{C}$ to
cover, and we let $K=||C_{f}||$. The intuition is the following: we (only)
keep track of the $K$ processes that will cover $C_{f}$. Of course, they might
need other processes to reach the desired configuration, if they need to
receive messages. That is why we also maintain the set of reachable states
along the execution. An abstract configuration will then be a multiset of $K$
states (concrete part of the configuration) and a set of all the reachable
states (abstract part of the configuration). Lemma 1 ensures that it is enough
to know which active states are reachable to ensure that both the concrete
part and the active states of the abstract part are coverable at the same
time. However, there is a case where this abstraction would not be enough:
assume that one of the $K$ processes has to send a message, and this message
_should not_ be received by the other $K-1$ processes. This can happen when
the message is received by a process in the part of the configuration that we
have abstracted away. In that case, even if the (waiting) state is present in
the set of reachable states, Lemma 1 does not guarantee that the entire
configuration is reachable, so the transition to an abstract configuration
where none of the $K-1$ processes has received the message might be erroneous.
This is why in that case we need to precisely keep track of the process that
will receive the message, even if in the end it will not participate in the
covering of $C_{f}$. This leads to the definition of the
$\Rightarrow_{\textsf{switch}}$ transition below.

This proof is structured as follows: we present the formal definitions of the
abstract configurations and semantics in Section 5.2. In Section 5.3, we
present the completeness proof, Section 5.4 is devoted to prove the soundness
of the construction. In the latter, we also give some ingredients to prove an
upper bound on the number of processes needed to cover the configuration. In
Section 5.5 one can find the main theorem of this section: it states that the
ConfCover problem is in PSpace and if the configuration is indeed coverable,
it presents an upper bound on the number of processes needed to cover it. In
Section 5.6, we prove that this lower bound is tight as the problem is PSpace-
hard.

###  5.2 Reasoning with Abstract Configurations

We present the abstract configurations we rely on. Let us fix $K=||C_{f}||$.
An _abstract configuration_ $\gamma$ is a pair $(M,S)$ where $M$ is a
configuration in $\mathcal{C}$ such that $||M||=K$ and $S\subseteq Q$ is a
subset of control states such that $\\{q\in Q\mid M(q)>0\\}\subseteq S$. We
call $M$ the $M$-part of $\gamma$ and $S$ its $S$-part. We denote by $\Gamma$
the set of abstract configurations and by $\gamma_{\textit{in}}$ the initial
abstract configuration $\gamma_{\textit{in}}=(\Lbag K\cdot
q_{\textit{in}}\Rbag,\\{q_{\textit{in}}\\})$. An abstract configuration
$\gamma=(M,S)$ represents a set of configurations
$\llbracket\gamma\rrbracket=\\{C\in\mathcal{C}\mid M\preceq C\mbox{ and
}C(q)>0\mbox{ implies }q\in S\\}$. Hence in $\llbracket\gamma\rrbracket$, we
have all the configurations $C$ that are bigger than $M$ as long as the states
holding processes in $C$ are stored in $S$ (observe that this implies that all
the states in $M$ appear in $S$).

We now define an abstract transition relation for abstract configurations. For
this matter, we define three transition relations
$\Rightarrow_{\textsf{step}}$,$\Rightarrow_{\textsf{ext}}$ and
$\Rightarrow_{\textsf{switch}}$ and let $\Rightarrow$ be defined by
$\Rightarrow_{\textsf{step}}\cup\Rightarrow_{\textsf{ext}}\cup\Rightarrow_{\textsf{switch}}$.
Let $\gamma=(M,S)$ and $\gamma^{\prime}=(M^{\prime},S^{\prime})$ be two
abstract configurations and $t=(q,\alpha,q^{\prime})$ be a transition in $T$
with $\alpha=!a$ or $\alpha=!!a$. For
$\kappa\in\\{\textsf{step},\textsf{ext},\textsf{switch}\\}$, we have
$\gamma\overset{t}{\Rightarrow}_{\kappa}\gamma^{\prime}$ iff all the following
conditions hold:

  * •

$S\subseteq S^{\prime}$, and,

  * •

for all $p\in S^{\prime}\setminus S$, either $p=q^{\prime}$ or there exist
$p^{\prime}\in S$ and $(p^{\prime},?a,p)$ in $T$, and,

  * •

one of the following cases is true:

    * –

$\kappa=\textsf{step}$ and $M\xrightarrow{t}M^{\prime}$. This relation
describes a message emitted from the $M$-part of the configuration;

    * –

$\kappa=\textsf{ext}$ and $q\in S$ and $M+\Lbag
q\Rbag\xrightarrow{t}M^{\prime}+\Lbag q^{\prime}\Rbag$;

    * –

$\kappa=\textsf{ext}$ and there exists $(p,?a,p^{\prime})$ in $T$ such that
$q,p\in S$ and $M+\Lbag q,p\Rbag\xrightarrow{t}M+\Lbag
q^{\prime},p^{\prime}\Rbag$ (note that in that case $M=M^{\prime}$). The
relation ext hence describes a message emitted from the $S$-part of the
configuration;

    * –

$\kappa=\textsf{switch}$ and $q\in S$ and $\alpha=!a$ and there exists
$t^{\prime}=(p,?a,p^{\prime})\in T$ such that $\Lbag p\Rbag\preceq M$ and
$\Lbag q^{\prime}\Rbag\preceq M^{\prime}$ and $M-\Lbag p\Rbag=M^{\prime}-\Lbag
q^{\prime}\Rbag$ and $M+\Lbag q\Rbag\xrightarrow{t}M^{\prime}+\Lbag
p^{\prime}\Rbag$. This relation describes a sending from a state in the
$S$-part of the abstract configuration leading to a rendez-vous with one
process in the $M$-part, and a "switch" of processes: we remove the receiver
process of the $M$-part and replace it by the sender.

Note that in any case, $q$, the state from which the message is sent, belongs
to $S$. We then write $\gamma\xRightarrow{t}\gamma^{\prime}$ whenever
$\gamma\overset{t}{\Rightarrow}_{\kappa}\gamma^{\prime}$ for
$\kappa\in\\{\textsf{step},\textsf{ext},\textsf{switch}\\}$ and we do not
always specify the used transition $t$ (when omitted, it means that there
exists a transitions allowing the transition). We denote by
$\Rightarrow^{\ast}$ the reflexive and transitive closure of $\Rightarrow$.

$q_{\textit{in}}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$q_{6}$$q_{7}$$!!\tau$$!!a$$?c$$!b$$?b$$?a$$!!c$$?b$
Figure 3: A Wait-Only protocol $P^{\prime}$.

###### Example 5

We consider the Wait-Only protocol $P^{\prime}$ depicted on Figure 3 with set
of states $Q^{\prime}$. We want to cover $C_{f}=\Lbag q_{3},q_{3},q_{6}\Rbag$
(hence $K=3$). In this example, the abstract configuration $\gamma=(\Lbag
q_{2},q_{2},q_{4}\Rbag,\\{q_{\textit{in}},q_{1},\linebreak[0]q_{2},q_{4},q_{5},q_{6}\\})$
represents all the configurations of $P^{\prime}$ with at least two processes
on $q_{2}$ and one on $q_{4}$, and no process on $q_{3}$ nor $q_{7}$.

Considering the following abstract execution, we can cover $C_{f}$:

$\displaystyle\gamma_{\textit{in}}\xRightarrow{(q_{\textit{in}},!!\tau,q_{4})}_{\textsf{step}}(\Lbag
q_{4},q_{\textit{in}},q_{\textit{in}}\Rbag,\\{q_{\textit{in}},q_{4}\\})\xRightarrow{(q_{\textit{in}},!!\tau,q_{4})}_{\textsf{step}}(\Lbag
q_{4},q_{4},q_{\textit{in}}\Rbag,\\{q_{\textit{in}},q_{4}\\})$
$\displaystyle\xRightarrow{(q_{\textit{in}},!!a,q_{1})}_{\textsf{step}}(\Lbag
q_{5},q_{5},q_{1}\Rbag,\\{q_{\textit{in}},q_{1},q_{4},q_{5}\\})\xRightarrow{(q_{5},!!c,q_{6})}_{\textsf{ext}}(\Lbag
q_{5},q_{5},q_{2}\Rbag,Q^{\prime}\setminus\\{q_{3},q_{7}\\})$
$\displaystyle\xRightarrow{(q_{2},!b,q_{3})}_{\textsf{step}}(\Lbag
q_{5},q_{5},q_{3}\Rbag,Q^{\prime})\xRightarrow{(q_{5},!!c,q_{6})}_{\textsf{step}}(\Lbag
q_{6},q_{5},q_{3}\Rbag,Q^{\prime})$
$\displaystyle\xRightarrow{(q_{2},!b,q_{3})}_{\textsf{switch}}(\Lbag
q_{3},q_{5},q_{3}\Rbag,Q^{\prime})\xRightarrow{(q_{5},!!c,q_{6})}_{\textsf{step}}(\Lbag
q_{3},q_{6},q_{3}\Rbag,Q^{\prime})$

It corresponds for instance to the following concrete execution:

$\displaystyle\Lbag q_{\textit{in}},q_{\textit{in}},q_{\textit{in}}\Rbag+\Lbag
q_{\textit{in}},q_{\textit{in}}\Rbag\rightarrow^{+}\Lbag
q_{4},q_{4},q_{\textit{in}}\Rbag+\Lbag
q_{4},q_{\textit{in}}\Rbag\xrightarrow{(q_{\textit{in}},!!a,q_{1})}\Lbag
q_{5},q_{5},q_{1}\Rbag+\Lbag q_{5},q_{\textit{in}}\Rbag$
$\displaystyle\xrightarrow{(q_{\textit{in}},!!a,q_{1})}\Lbag
q_{5},q_{5},q_{1}\Rbag+\Lbag
q_{5},q_{1}\Rbag\xrightarrow{(q_{5},!!c,q_{6})}\Lbag
q_{5},q_{5},q_{2}\Rbag+\Lbag q_{6},q_{1}\Rbag$
$\displaystyle\xrightarrow{(q_{2},!b,q_{3})}\Lbag q_{5},q_{5},q_{3}\Rbag+\Lbag
q_{7},q_{1}\Rbag\xrightarrow{(q_{5},!!c,q_{6})}\Lbag
q_{6},q_{5},q_{3}\Rbag+\Lbag q_{7},q_{2}\Rbag$
$\displaystyle\xrightarrow{(q_{2},!b,q_{3})}\Lbag q_{3},q_{5},q_{3}\Rbag+\Lbag
q_{7},q_{7}\Rbag\xrightarrow{(q_{5},!!c,q_{6})}\Lbag
q_{3},q_{6},q_{3}\Rbag+\Lbag q_{7},q_{7}\Rbag$

The $M$-part of our abstract configuration $\Lbag q_{6},q_{5},q_{3}\Rbag$
reached just before the $\Rightarrow_{\textsf{switch}}$ transition does not
correspond to the set of processes that finally cover $C_{f}$, at this point
of time, the processes that will finally cover $C_{f}$ are in states $q_{2}$,
$q_{5}$, and $q_{3}$. But here we ensure that the process on $q_{6}$ will
actually receive the $b$ sent by the process on $q_{2}$, leaving the process
on $q_{3}$ in its state. Once this has been ensured, process on $q_{6}$ is not
useful anymore, and instead we follow the process that was on $q_{2}$ before
the sending, hence the $\Rightarrow_{\textsf{switch}}$ transition.

The algorithm used to solve ConfCover, is then to seek in the directed graph
$(\Gamma,\Rightarrow)$ if a vertex of the form $(C_{f},S)$ is reachable from
$\gamma_{\textit{in}}$.

Before proving that this algorithm is correct, we establish the following
property.

###### Lemma 6

Let $(M,S)$ and $(M^{\prime},S^{\prime})$ be two abstract configurations and
$\widetilde{S}\subseteq Q$ such that $S\subseteq\widetilde{S}$. We have:

  1. 1.

$\llbracket(M,S)\rrbracket\subseteq\llbracket(M,\widetilde{S})\rrbracket$.

  2. 2.

If $(M,S)\Rightarrow(M^{\prime},S^{\prime})$ then there exists
$S^{\prime\prime}\subseteq Q$ such that
$(M,\widetilde{S})\Rightarrow(M^{\prime},S^{\prime\prime})$ and
$S^{\prime}\subseteq S^{\prime\prime}$.

###### Proof

The first point is a direct consequence of the definition of
$\llbracket\rrbracket$. For the second point, it is enough to take
$S^{\prime\prime}=S^{\prime}\cup\widetilde{S}$ and apply the definition of
$\Rightarrow$. ∎

###  5.3 Completeness of the algorithm

In this subsection we show that if $C_{f}$ can be covered then there exists an
abstract configuration $\gamma=(C_{f},S)$ such that
$\gamma_{\textit{in}}\Rightarrow^{\ast}\gamma$. We use $\mathcal{C}_{\geq K}$
to represent the set $\\{C\in\mathcal{C}\mid||C||\geq K\\}$ of configurations
with at least $K$ processes and $\mathcal{C}_{=K}$ the set
$\\{C\in\mathcal{C}\mid||C||=K\\}$ of configurations with exactly $K$
processes. This first lemma shows the completeness for a single step of our
abstract transition relation (note that we focus on the $M$-part, as it is the
one witnessing $C_{f}$ in the end).

###### Lemma 7

Let $C,C^{\prime}\in\mathcal{C}_{\geq K}$ and $t\in T$ such that
$C\xrightarrow{t}C^{\prime}$. Then for all $M^{\prime}\in\mathcal{C}_{=K}$
such that $M^{\prime}\preceq C^{\prime}$, there exists $M\in\mathcal{C}_{=K}$
and $S^{\prime}\subseteq Q$ such that
$(M,S)\Rightarrow(M^{\prime},S^{\prime})$ with $S=\\{q\in Q\mid C(q)>0\\}$,
$C\in\llbracket(M,S)\rrbracket$ and
$C^{\prime}\in\llbracket(M^{\prime},S^{\prime})\rrbracket$.

###### Proof

Let $M^{\prime}\in\mathcal{C}_{=K}$ such that $M^{\prime}\preceq C^{\prime}$.
We assume that $t=(q,\alpha,q^{\prime})$ with $\alpha\in\\{!a,!!a\\}$. We let
$S=\\{p\in Q\mid C(p)>0\\}$ and $S^{\prime}=S\cup\\{p\in Q\mid
C^{\prime}(p)>0\\}$. By definition of $S$ and $S^{\prime}$, for all $p\in
S^{\prime}\setminus S$, either $p=q^{\prime}$ or there exists $p^{\prime}\in
S$ and $(p^{\prime},?a,p)$ in $T$. In fact, let $p\in S^{\prime}\setminus S$
such that $p\neq q^{\prime}$. Since $C\xrightarrow{t}C^{\prime}$, we have
necessarily that there exist $p^{\prime}\in Q$ such that $C(p^{\prime})>0$
(hence $p^{\prime}\in S$), and $(p^{\prime},?a,p)$ in $T$. We now reason by a
case analysis to determine $M\in\mathcal{C}_{=K}$ such that
$(M,S)\Rightarrow(M^{\prime},S^{\prime})$ and $C\in\llbracket(M,S)\rrbracket$.
The different cases are: (i) $\alpha=!!a$, (ii) $\alpha=!a$ and the message is
_not received_ , (iii) $\alpha=!a$ and the message is received by a process.
Because of space constraints, we present here only case (iii) as it exhibits
the most different abstract behaviours. The two other cases can be found on
Section 0.C.1.

  1. (iii)

if $\alpha=!a$ and the message is received by a process (i.e. it is a rendez-
vous), denote by $(p,?a,p^{\prime})$ the reception transition issued between
$C$ and $C^{\prime}$. Using the definition of $\rightarrow$, we get
$C^{\prime}=C-\Lbag q,p\Rbag+\Lbag q^{\prime},p^{\prime}\Rbag$. We consider
the four following disjoint cases:

     * •

$M^{\prime}(q^{\prime})=0$ and $M^{\prime}(p^{\prime})=0$. Since $\Lbag
q^{\prime},p^{\prime}\Rbag\preceq C^{\prime}$ and $M^{\prime}\preceq
C^{\prime}$, we get that $C^{\prime}=M^{\prime}+\Lbag
q^{\prime},p^{\prime}\Rbag+M_{2}$ for some multiset $M_{2}$. We deduce that
$C=M^{\prime}+\Lbag q,p\Rbag+M_{2}$. This allows us to deduce that
$M^{\prime}\preceq C$ and consequently
$C\in\llbracket(M^{\prime},S)\rrbracket$. Moreover, $M^{\prime}+\Lbag
p,q\Rbag\xrightarrow{t}M^{\prime}+\Lbag q^{\prime},p^{\prime}\Rbag$ and
$q,p\in S$. Hence
$(M^{\prime},S)\overset{t}{\Rightarrow}_{\textsf{ext}}(M^{\prime},S^{\prime})$.

     * •

$M^{\prime}(q^{\prime})=0$ and $M^{\prime}(p^{\prime})>0$. In that case
$C^{\prime}=M^{\prime}+\Lbag q^{\prime}\Rbag+M_{2}$ for some multiset $M_{2}$.
Let $M=M^{\prime}-\Lbag p^{\prime}\Rbag+\Lbag p\Rbag$. We have then
$C=C^{\prime}+\Lbag q,p\Rbag-\Lbag q^{\prime},p^{\prime}\Rbag=M^{\prime}+\Lbag
q^{\prime}\Rbag+M_{2}+\Lbag q,p\Rbag-\Lbag
q^{\prime},p^{\prime}\Rbag=M^{\prime}+M_{2}-\Lbag p^{\prime}\Rbag+\Lbag
p\Rbag+\Lbag q\Rbag=M+\Lbag q\Rbag+M_{2}$. This allows us to deduce that
$M\preceq C$ and consequently $C\in\llbracket(M,S)\rrbracket$. Furthermore
$q\in S$ and $M+\Lbag q\Rbag\xrightarrow{t}M^{\prime}+\Lbag q^{\prime}\Rbag$.
Hence $(M,S)\overset{t}{\Rightarrow}_{\textsf{ext}}(M,S^{\prime})$.

     * •

$M^{\prime}(q^{\prime})>0$ and $M^{\prime}(p^{\prime})=0$. In that case
$C^{\prime}=M^{\prime}+\Lbag p^{\prime}\Rbag+M_{2}$ for some multiset $M_{2}$.
Let $M=M^{\prime}-\Lbag q^{\prime}\Rbag+\Lbag p\Rbag$. We have then
$C=C^{\prime}+\Lbag q,p\Rbag-\Lbag q^{\prime},p^{\prime}\Rbag=M^{\prime}+\Lbag
p^{\prime}\Rbag+M_{2}+\Lbag q,p\Rbag-\Lbag
q^{\prime},p^{\prime}\Rbag=M^{\prime}+M_{2}-\Lbag q^{\prime}\Rbag+\Lbag
p\Rbag+\Lbag q\Rbag=M+\Lbag q\Rbag+M_{2}$. This allows us to deduce that $q\in
S$ and $M\preceq C$ and consequently $C\in\llbracket(M,S)\rrbracket$. We also
have $\Lbag p\Rbag\preceq M$ and $\Lbag q^{\prime}\Rbag\preceq M^{\prime}$ and
$M-\Lbag p\Rbag=M^{\prime}-\Lbag q^{\prime}\Rbag$ and $M+\Lbag
q\Rbag\xrightarrow{t}M^{\prime}+\Lbag p^{\prime}\Rbag$. Hence
$(M,S)\overset{t}{\Rightarrow}_{\textsf{switch}}(M^{\prime},S^{\prime})$.
Observe that we need to use the $\Rightarrow_{\textsf{switch}}$ transition
relation in this case. Assume that $C(s)>0$ for some state $s\in S$ such that
$(s,?a,s^{\prime})\in T$, and that any configuration in $\mathcal{C}_{=K}$
such that $M\preceq C$ contains such state $s$. Then, applying
$\Rightarrow_{\textsf{step}}$ to such a multiset $M$ will take away the
process on state $s$ and will lead to an abstract configuration with
$M^{\prime}\not\preceq C^{\prime}$.

     * •

$M^{\prime}(q^{\prime})>0$ and $M^{\prime}(p^{\prime})>0$. In that case
$C^{\prime}=M^{\prime}+M_{2}$ for some multiset $M_{2}$. Let
$M=M^{\prime}-\Lbag p^{\prime},q^{\prime}\Rbag+\Lbag p,q\Rbag$. We have then
$C=C^{\prime}+\Lbag q,p\Rbag-\Lbag q^{\prime},p^{\prime}\Rbag=M+M_{2}$. This
allows us to deduce that $M\preceq C$ and consequently
$C\in\llbracket(M,S)\rrbracket$ and that $M\xrightarrow{t}M^{\prime}$. Hence
$(M,S)\overset{t}{\Rightarrow}_{\textsf{step}}(M^{\prime},S^{\prime})$.∎

The two previous lemmas allow us to establish completeness of the
construction, by a simple induction on the length of the considered execution.
The proof can be found on Section 0.C.1.

###### Lemma 8

Let $C_{\textit{in}}\in\mathcal{I}$ and $C\in\mathcal{C}_{\geq K}$ such that
$C_{\textit{in}}\rightarrow^{\ast}C$. For all $M\in\mathcal{C}_{=K}$ such that
$M\preceq C$ there exists $S\subseteq Q$ such that
$C\in\llbracket(M,S)\rrbracket$ and
$\gamma_{\textit{in}}\Rightarrow^{\ast}(M,S)$.

###  5.4 Soundness of the algorithm

We now prove that if we have $\gamma_{\textit{in}}\Rightarrow^{\ast}(M,S)$
then the configuration $M$ can be covered. We first establish that the
$S$-part of a reachable abstract configuration stores only states that are
reachable in a concrete execution.

###### Lemma 9

If $\gamma=(M,S)$ is an abstract configuration such that
$\gamma_{\textit{in}}\Rightarrow^{\ast}\gamma$, then all states $q\in S$ are
coverable.

###### Proof

We suppose that we have
$\gamma_{in}=\gamma_{0}\Rightarrow\gamma_{1}\Rightarrow\ldots\Rightarrow\gamma_{n}=(M,S)$
and we prove this lemma by induction on $n$, the length of the abstract
execution.

Case $n=0$: In that case $(M,S)=\gamma_{0}=(K\cdot\Lbag
q_{\textit{in}}\Rbag,\\{q_{\textit{in}}\\})$, as $q_{\textit{in}}$ is
trivially coverable, the property holds.

Case $n>0$: We assume that the property holds for all $0\leq m<n$ and consider
the abstract execution
$\gamma_{0}\xRightarrow{t_{1}}\gamma_{1}\xRightarrow{t_{2}}\ldots\xRightarrow{t_{n}}\gamma_{n}$
where $\gamma_{0}=\gamma_{\textit{in}}$ and $\gamma_{i}=(M_{i},S_{i})$ for all
$0\leq i\leq n$. Let $p\in S_{n}$. If $p\in S_{n-1}$, then by induction
hypothesis, $p$ is coverable. Otherwise, $p\in S_{n}\setminus S_{n-1}$, and
let $t_{n}=(q,\alpha,q^{\prime})$ with $\alpha\in\\{!a,!!a\mid a\in\Sigma\\}$.
By definition of $\Rightarrow$, $q\in S_{n-1}$ and

  * •

either $q^{\prime}=p$, and by induction hypothesis, there exists an
initialized execution $C_{0}\rightarrow^{\ast}C$ with $C(q)>0$ and in that
case, $C_{0}\rightarrow^{\ast}C\xrightarrow{t}C^{\prime}$ for a configuration
$C^{\prime}$ such that $C^{\prime}(p)>0$ and $p$ is coverable.

  * •

or $\alpha\in\\{!a,!!a\\}$ for some $a\in\Sigma$ and $(p^{\prime},?a,p)\in T$,
with $p^{\prime}\in S_{n-1}$. By induction hypothesis, both $q$ and
$p^{\prime}$ are coverable, with $q\in Q_{A}$ and $p\in Q_{W}$. By Lemma 1,
there exists an execution $C_{0}\rightarrow^{\ast}C$ such that $C(q)\geq 1$
and $C(p^{\prime})\geq 1$. We then have $C\xrightarrow{t_{n}}C^{\prime}$ with
$C^{\prime}(p)>0$ (if $\alpha=!a$ then the process on $p^{\prime}$ can receive
the message $a$ and move to $p$, and if $\alpha=!!a$ then the process on
$p^{\prime}$ will necessary receive the broadcast and move to $p$), and $p$ is
coverable.

∎

The next lemma establishes soundness of the algorithm. Moreover, it gives an
upper bound on the minimal number of processes needed to cover a
configuration.

###### Lemma 10

Let $(M,S)$ be an abstract configuration such that
$\gamma_{\textit{in}}\Rightarrow\gamma_{1}\Rightarrow\ldots\Rightarrow\gamma_{n}=(M,S)$.
Then, there exist $C_{\textit{in}}\in\mathcal{I}$, $C\in\mathcal{C}$ such that
$M\preceq C$ and $C_{\textit{in}}\rightarrow^{\ast}C$. Moreover,
$||C_{\textit{in}}||=||C||\leq K+2^{|Q|}\times n$.

###### Proof

We reason by induction on $n$, the length of the abstract execution.

Case $n=0$: The property trivially holds for $C=\Lbag K\cdot
q_{\textit{in}}\Rbag$.

Case $n>0$: We assume that the property holds for all $0\leq m<n$ and consider
the abstract execution
$\gamma_{0}\xRightarrow{t_{1}}\gamma_{1}\xRightarrow{t_{2}}\ldots\xRightarrow{t_{n}}\gamma_{n}$
where $\gamma_{0}=\gamma_{\textit{in}}$ and $\gamma_{i}=(M_{i},S_{i})$ for all
$0\leq i\leq n$. By induction hypothesis, we know that there exist
$C_{\textit{in}}\in\mathcal{I}$, $C_{n-1}\in\mathcal{C}$ such that
$M_{n-1}\preceq C_{n-1}$ and $C_{\textit{in}}\rightarrow^{\ast}C_{n-1}$ and
$||C_{\textit{in}}||=||C_{n-1}||\leq K+2^{|Q|}\times(n-1)$. If $M_{n}=M_{n-1}$
then the property holds. Assume now that $M_{n}\neq M_{n-1}$. We let
$t_{n}=(q,\alpha,q^{\prime})$ with $\alpha=!a$ or $\alpha=!!a$. By definition
of $\Rightarrow$, we know that $S_{n-1}\subseteq S_{n}$ and that $q\in
S_{n-1}$. Thanks to Lemma 9, $q$ is coverable. We now perform a case analysis:

  * •

Assume $\gamma_{n-1}\overset{t_{n}}{\Rightarrow}_{\textsf{step}}\gamma_{n}$.
Then $M_{n-1}\xrightarrow{t_{n}}M_{n}$, and since $M_{n-1}\preceq C_{n-1}$, we
have $C_{n-1}=M_{n-1}+M$ for some multiset $M$.

    * –

If $\alpha=!!a$, then $M_{n-1}+M=\Lbag q_{1},\dots q_{K-1},q\Rbag+\Lbag
p_{1},\dots,p_{L}\Rbag$ and $M_{n}=\Lbag q^{\prime}_{1},\dots
q^{\prime}_{K-1},q^{\prime}\Rbag$ where for all $1\leq i\leq K-1$, either
$(q_{i},?a,q^{\prime}_{i})\in T$ or $a\nin R(q_{i})$ and
$q_{i}=q^{\prime}_{i}$. For each $1\leq i\leq L$, define $p^{\prime}_{i}$ as
$p^{\prime}_{i}=p_{i}$ if $a\nin R(p_{i})$ or $p^{\prime}_{i}$ is such that
$(p_{i},?a,p^{\prime}_{i})\in T$. If we let $M^{\prime}=\Lbag
p^{\prime}_{1},\dots,p^{\prime}_{L}\Rbag$ and $C_{n}=M_{n}+M^{\prime}$, we
have by definition that $C_{n-1}\xrightarrow{t_{n}}C_{n}$ with $M_{n}\preceq
C_{n}$.

    * –

If $\alpha=!a$ and $(M_{n-1}-\Lbag q\Rbag)(p)>0$ for some $p\in Q$ such that
$(p,?a,p^{\prime})\in T$ (i.e., a rendez-vous occurred), it holds that
$M_{n-1}+M\xrightarrow{t}M_{n}+M$ and we choose $C_{n}=M_{n}+M$.

    * –

If $\alpha=!a$ and $(M_{n-1}-\Lbag q\Rbag)(p)=0$ for all $p\in Q$ such that
$a\in R(p)$ (i.e. it was a non-blocking sending of a message), then either
there exists $(p,?a,p^{\prime})\in T$ such that $M(p)>0$, either for all $p\in
Q$ such that $M(p)>0$, $a\nin R(p)$. In the first case, a rendez-vous will
occur in the execution of $t_{n}$ over $C_{n-1}$, and we have
$M_{n-1}+M\xrightarrow{t_{n}}M_{n}+M-\Lbag p\Rbag+\Lbag p^{\prime}\Rbag$. We
then let $C_{n}=M_{n}+M-\Lbag p\Rbag+\Lbag p^{\prime}\Rbag$. In the latter
case, $M_{n-1}+M\xrightarrow{t_{n}}M_{n}+M$ and with $C_{n}=M_{n}+M$. In both
cases, we have , $C_{n-1}\xrightarrow{t}C_{n}$ and $M_{n}\preceq C_{n}$.

In all cases, we have $C_{in}\rightarrow^{\ast}C_{n-1}\rightarrow C_{n}$ and
$||C_{in}||=||C_{n}||=||C_{n-1}||\leq K+2^{|Q|}\times(n-1)\leq K+2^{|Q|}\times
n$.

  * •

Assume $\gamma_{n-1}\overset{t_{n}}{\Rightarrow}_{\textsf{ext}}\gamma_{n}$ or
$\gamma_{n-1}\overset{t_{n}}{\Rightarrow}_{\textsf{switch}}\gamma_{n}$. As $q$
is coverable, from Corollary 1, there exists an execution
$C^{q}_{\textit{in}}\rightarrow^{\ast}C^{q}$ such that
$C^{q}_{\textit{in}}\in\mathcal{I}$ and $C^{q}(q)>0$ and
$||C^{q}_{\textit{in}}||\leq 2^{|Q|}$. From Lemma 2, we have the following
execution:
$C_{\textit{in}}+C^{q}_{\textit{in}}\rightarrow^{\ast}C_{\textit{in}}+C^{q}$.
Next, from Lemma 3, by taking $M=1$ and $\tilde{C}_{0}=C_{\textit{in}}+C^{q}$,
we have an execution $C_{in}+C^{q}\rightarrow^{\ast}C_{n-1}+C^{\prime q}$
where $C^{\prime q}(q)>0$. We deduce that $C_{n-1}+C^{\prime q}=M_{n-1}+\Lbag
q\Rbag+M$ for some multiset $M$. We now proceed with a case analysis:

    * –

Case $\gamma_{n-1}\overset{t_{n}}{\Rightarrow}_{\textsf{ext}}\gamma_{n}$ where
$M_{n-1}+\Lbag q\Rbag\xrightarrow{t_{n}}M_{n}+\Lbag q^{\prime}\Rbag$. By
definition of $\rightarrow$, we also have $M_{n-1}+\Lbag q\Rbag+M\rightarrow
M_{n}+\Lbag q^{\prime}\Rbag+M^{\prime}$ for some multiset $M^{\prime}$.
Letting $C_{n}=M_{n}+\Lbag q^{\prime}\Rbag+M^{\prime}$ gives us that that
$C_{in}+C^{q}_{in}\rightarrow^{\ast}M_{n-1}+\Lbag q\Rbag+M\rightarrow C_{n}$.

    * –

Case $\gamma_{n-1}\overset{t_{n}}{\Rightarrow}_{\textsf{switch}}\gamma_{n}$:
by definition of $\Rightarrow_{\textsf{switch}}$, we know that there exists
$(p,?a,p^{\prime})\in T$ with $p\in S_{n-1}$ such that
$M_{n-1}=M^{\prime}+\Lbag p\Rbag$ and that $M^{\prime}+\Lbag p\Rbag+\Lbag
q\Rbag\xrightarrow{t_{n}}M^{\prime}+\Lbag q^{\prime}\Rbag+\Lbag
p^{\prime}\Rbag$ and $M_{n}=M^{\prime}+\Lbag q^{\prime}\Rbag$. Furthermore, by
definition of $\rightarrow$, we have $M^{\prime}+\Lbag p,q\Rbag+M\rightarrow
M^{\prime}+\Lbag p^{\prime},q^{\prime}\Rbag+M$. Hence setting
$C_{n}=M^{\prime}+\Lbag p^{\prime},q^{\prime}\Rbag+M=M_{n}+\Lbag
p^{\prime}\Rbag+M$ gives us that that
$C_{in}+C^{q}_{in}\rightarrow^{\ast}M_{n-1}+\Lbag q\Rbag+M\rightarrow C_{n}$,
with $M_{n}\preceq C_{n}$.

In both cases, we have shown that there exists $C_{n}$ such that $M_{n}\preceq
C_{n}$ and $C_{in}+C^{q}_{in}\rightarrow^{\ast}C_{n}$. Furthermore we have
that $||C_{n}||=||C_{in}+C^{q}_{in}||\leq K+2^{|Q|}\times(n-1)+2^{|Q|}\leq
K+2^{|Q|}\times n$. ∎

###  5.5 Upper Bound

Using Lemmas 8 and 10, we know that there exists $C\in\mathcal{I}$ and
$C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ and
$C_{f}\preceq C^{\prime}$ iff there exists an abstract execution
$\gamma_{\textit{in}}\Rightarrow\gamma_{1}\Rightarrow\cdots\Rightarrow\gamma_{n}$
with $\gamma_{n}=(C_{f},S)$ for some $S\subseteq Q$, hence the algorithm
consisting in deciding reachability of a vertex of the form $(C_{f},S)$ from
$\gamma_{\textit{in}}$ in the finite graph $(\Gamma,\Rightarrow)$ is correct.
Note furthermore that the number of abstract configurations $|\Gamma|$ is
bounded by $|Q|^{||C_{f}||}\times 2^{|Q|}$. As the reachability of a vertex in
a graph is NL-complete, this gives us a NPSpace procedure, which leads to a
Pspace procedure thanks to Savitch’s theorem.

###### Theorem 5.1

ConfCover is in PSpace.

###### Remark 3

Thanks to Lemma 10, we know that
$\gamma_{in}\Rightarrow\gamma_{1}\Rightarrow\cdots\Rightarrow\gamma_{n}$ with
$\gamma_{n}=(C_{f},S)$ iff there exists $C_{in}\in\mathcal{I}$,
$C\in\mathcal{C}$ such that $C_{f}\preceq C$ and $C_{in}\rightarrow^{\ast}C$
and $||C_{in}||=||C||\leq K+2^{|Q|}\times n$. But due to the number of
abstract configurations, we can assume that $n\leq
2^{|Q|}\times|Q|^{||C_{f}||}$ as it is unnecessary in the abstract execution
$\gamma_{in}\Rightarrow\gamma_{1}\Rightarrow\cdots\Rightarrow\gamma_{n}$ to
visit twice the same abstract configuration. Hence the configuration $C_{f}$
is coverable iff there is $C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$
such $C\rightarrow^{\ast}C^{\prime}$ and $C_{f}\preceq C^{\prime}$ and
$||C||=||C^{\prime}||\leq K+2^{|Q|}\times 2^{|Q|}\times|Q|^{||C_{f}||}$.

###  5.6 Lower Bound

To prove PSpace-hardness of the ConfCover problem for Wait-Only protocols, we
reduce the intersection non-emptiness problem for deterministic finite
automata, which is known to be PSpace-complete [Koz77]. The PSpace-hardness in
fact holds when considering Wait-Only protocols without any (non-blocking)
rendez-vous transitions, i.e. transitions of the form $(q,!a,q^{\prime})$.

Let $\mathcal{A}_{1},\dots,\mathcal{A}_{n}$ be a list of deterministic finite
and _complete_ automata with
$\mathcal{A}_{i}=(\Sigma,Q_{i},q_{i}^{0},\\{q_{i}^{f}\\},\Delta_{i})$ for all
$1\leq i\leq n$. Observe that we restrict our reduction to automata with a
unique accepting state, which does not change the complexity of the problem.
We note $\Sigma^{\ast}$ the set of words over the finite alphabet $\Sigma$ and
$\Delta^{\ast}_{i}$ the function extending $\Delta_{i}$ to $\Sigma^{\ast}$,
i.e, for all $q\in Q_{i}$, $\Delta_{i}^{\ast}(q,\varepsilon)=q$, and for all
$w\in\Sigma^{\ast}$ and $a\in\Sigma$,
$\Delta^{\ast}_{i}(q,wa)=\Delta_{i}(\Delta^{\ast}_{i}(q,w),a)$.

$q_{\textit{in}}$$q_{s}$$q_{1}$$q_{n}$$q_{1}^{0}$$q_{n}^{0}$$q_{1}^{f}$$q_{n}^{f}$$P_{1}$$P_{n}$…$q_{\textit{fail}}$$!!\tau$$!!\tau$$!!\tau$$!!go$$!!a,a\in\Sigma$$?go$$?go$$?go$$?go$
Figure 4: Protocol $P$ for PSpace-hardness of ConfCover.

We build the protocol $P$ with set of states $Q$, displayed in Figure 4 where
$P_{i}$ for $1\leq i\leq n$ is a protocol mimicking the behaviour of the
automaton $\mathcal{A}_{i}$: $P_{i}=(Q_{i},\Sigma,q_{i}^{0},T_{i})$, with
$T_{i}=\\{(q,?a,q^{\prime})\mid(q,a,q^{\prime})\in\Delta_{i}\\}$. Moreover,
from any state $q\in\bigcup_{1\leq i\leq n}Q_{i}$, there is an outgoing
transition $(q,?\textit{go},q_{\textit{fail}})$. These transitions are
depicted by the outgoing transitions labelled by $?\textit{go}$ from the
orange rectangles.

Note that $P$ is Wait-Only as all states in $P_{i}$ for all $1\leq i\leq n$
are waiting states and the only active states are $q_{\textit{in}}$ and
$q_{s}$. We show that $\bigcap_{1\leq i\leq n}L(\mathcal{A}_{i})\neq\emptyset$
if and only if there is an initial configuration $C\in\mathcal{I}_{P}$ and a
configuration $C^{\prime}\in\mathcal{C}_{P}$ such that
$C\rightarrow^{\ast}C^{\prime}$ and $C_{f}\preceq C^{\prime}$ with
$C_{f}=\Lbag q^{f}_{1},\dots,q^{f}_{n}\Rbag$.

The idea is to synchronize (at least) $n$ processes into simulating the $n$
automata. To this end, we need an additional (leader) process that will
broadcast a message go, which will be received by the $n$ processes, leading
each of them to reach a different automaton initial state. Then, the leader
process will broadcast a word letter by letter. Since the automata are all
complete, these broadcast will be received by all the processes that simulate
the automata, mimicking an execution. If the word belongs to all the automata
languages, then each process simulating the automata ends the simulation on
the unique final state of the automaton. Note that if the leader process
broadcasts the message go a second time, then all the processes simulating the
automata stop their simulation and reach the state $q_{\textit{fail}}$. Formal
proofs can be found in Section 0.C.2.

##  6 Conclusion

We have proved that when extending the model presented in [GSS23] with
broadcasts, StateCover for Wait-Only protocols remains in P, and is even
P-complete. We also explained how to retrieve a P lower bound for the model of
[GSS23] for both problems restricted to Wait-Only protocols. However ConfCover
for Wait-Only protocols is now PSpace-complete. In the future, we wish to
study not only coverability problems but extend the analysis of this model to
liveness properties. We also wish to expand this model with dynamic creations
of messages and processes in order to take a step closer to the modelling of
Java Threads programming, where Threads can dynamically create new objects in
which they can synchronize with notify and notifyAll messages.

## References

  * [AK86] K. R. Apt and D. C. Kozen.  Limits for automatic verification of finite-state concurrent systems.  Inf. Process. Lett., 22(6):307–309, 1986.
  * [ARZ15] B. Aminof, S. Rubin, and F. Zuleger.  On the expressive power of communication primitives in parameterised systems.  In LPAR’15, volume 9450 of Lecture Notes in Computer Science, pages 313–328. Springer, 2015.
  * [BER21] A. R. Balasubramanian, J. Esparza, and M. A. Raskin.  Finding cut-offs in leaderless rendez-vous protocols is easy.  In FOSSACS’21, volume 12650 of LNCS, pages 42–61. Springer, 2021.
  * [DEGM17] A. Durand-Gasselin, J. Esparza, P. Ganty, and R. Majumdar.  Model checking parameterized asynchronous shared-memory systems.  Formal Methods in System Design, 50(2-3):140–167, 2017.
  * [DRB02] G. Delzanno, J. F. Raskin, and L. Van Begin.  Towards the automated verification of multithreaded java programs.  In TACAS’02, volume 2280 of LNCS, pages 173–187. Springer, 2002.
  * [DSTZ12] G. Delzanno, A. Sangnier, R. Traverso, and G. Zavattaro.  On the complexity of parameterized reachability in reconfigurable broadcast networks.  In FSTTCS’12, volume 18 of LIPIcs, pages 289–300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012.
  * [EFM99] J. Esparza, A. Finkel, and R. Mayr.  On the verification of broadcast protocols.  In LICS’99, pages 352–359. IEEE Comp. Soc. Press, July 1999.
  * [EK03] E. Allen Emerson and V. Kahlon.  Model checking guarded protocols.  In (LICS 2003, pages 361–370. IEEE, 2003.
  * [GS92] S. M. German and A. P. Sistla.  Reasoning about systems with many processes.  Journal of the ACM, 39(3):675–735, 1992.
  * [GSS23] L. Guillou, A. Sangnier, and N. Sznajder.  Safety analysis of parameterised networks with non-blocking rendez-vous.  In CONCUR’23, volume 279 of LIPIcs, pages 7:1–7:17. loss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
  * [HS20] F. Horn and A. Sangnier.  Deciding the existence of cut-off in parameterized rendez-vous networks.  In CONCUR’20, volume 171 of LIPIcs, pages 46:1–46:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [Koz77] Dexter Kozen.  Lower bounds for natural proof systems.  In FOCS’77, pages 254–266. IEEE Computer Society, 1977.
  * [Lad75] Richard E. Ladner.  The circuit value problem is log space complete for _P_.  SIGACT News, 7(1):18–20, 1975.
  * [SS13] S. Schmitz and P. Schnoebelen.  The power of well-structured systems.  In CONCUR’13, volume 8052 of Lecture Notes in Computer Science, pages 5–24. Springer, 2013.

##  Appendix 0.A Proofs of Section 3

Proof of Lemma 2.

Formally, we can prove Lemma 2 by induction on $0\leq i\leq k$. For $i=0$, it
comes from the definitions. Now assume that $\widehat{C}_{i}(q)=C_{i}(q)$ for
all $q\in Q\setminus\\{q_{\textit{in}}\\}$, and
$\widehat{C}_{i}(q_{\textit{in}})=C_{i}(q_{\textit{in}})+C^{\prime}_{0}(q_{\textit{in}})$,
and let $M=C^{\prime}_{0}(q_{\textit{in}})$.

  * •

If $t^{\prime}_{i+1}=(p_{1},!!m,p_{2})$, let $C_{i}=\Lbag
p_{1},q^{\prime}_{1},\dots,q^{\prime}_{N^{\prime}-1}\Rbag$ and $C_{i+1}=\Lbag
p_{2},p^{\prime}_{1},\dots,p^{\prime}_{N^{\prime}-1}\Rbag$. For all $1\leq
i\leq N^{\prime}-1$, either $m\notin R(q^{\prime}_{i})$, and
$p^{\prime}_{i}=q^{\prime}_{i}$, or $(q^{\prime}_{i},?m,p^{\prime}_{i})\in T$.
By induction hypothesis, $\widehat{C}_{i}=\Lbag
p_{1},q^{\prime}_{1},\dots,q^{\prime}_{N^{\prime}-1},M\cdot
q_{\textit{in}}\Rbag$. Since $q_{\textit{in}}$ is an active state, we know
that $m\notin R(q_{\textit{in}})$, hence $\widehat{C}_{i+1}=\Lbag
p_{2},p^{\prime}_{1},\dots,p^{\prime}_{N^{\prime}-1},M\cdot
q_{\textit{in}}\Rbag$, and $\widehat{C}_{i+1}(q)=C_{i+1}(q)$ for all $q\in
Q\setminus\\{q_{\textit{in}}\\}$, and
$\widehat{C}_{i+1}(q_{\textit{in}})=C_{i+1}(q_{\textit{in}})+C^{\prime}_{0}(q_{\textit{in}})$.

  * •

If $t^{\prime}_{i+1}=(p_{1},!m,p_{2})$ and there exist $q,q^{\prime}\in Q$
such that $(q,?m,q^{\prime})\in T$ and $C_{i}(q)>0$, then $C_{i}=\Lbag
p_{1},q,q^{\prime}_{1},\dots q^{\prime}_{N^{\prime}-2}\Rbag$ and
$C_{i+1}=\Lbag p_{2},q^{\prime},q^{\prime}_{1},\dots
q^{\prime}_{N^{\prime}-2}\Rbag$. By induction hypothesis,
$\widehat{C}_{i}=\Lbag p_{1},q,q^{\prime}_{1},\dots
q^{\prime}_{N^{\prime}-2},M\cdot q_{\textit{in}}\Rbag$ and hence
$\widehat{C}_{i+1}=\Lbag p_{2},q^{\prime},q^{\prime}_{1},\dots
q^{\prime}_{N^{\prime}-2},M\cdot q_{\textit{in}}\Rbag$.

  * •

If $t^{\prime}_{i+1}=(p_{1},!m,p_{2})$ and for all $q,q^{\prime}\in Q$ such
that $(q,?m,q^{\prime})\in T$, $C_{i}(q)=0$, then for all $q,q^{\prime}\in Q$
such that $(q,?m,q^{\prime})\in T$, $\widehat{C}_{i}(q)=C_{i}(q)=0$. Indeed,
since $q_{\textit{in}}$ is an active state, $q_{\textit{in}}\neq q$. Then
$C_{i+1}=C_{i}-\Lbag p_{1}\Rbag+\Lbag p_{2}\Rbag$ and
$\widehat{C}_{i+1}=\widehat{C}_{i}-\Lbag p_{1}\Rbag+\Lbag p_{2}\Rbag$. Hence,
$\widehat{C}_{i+1}(q)=C_{i+1}(q)$ for all $q\in
Q\setminus\\{q_{\textit{in}}\\}$ and
$\widehat{C}_{i+1}(q_{\textit{in}})=C_{i+1}(q_{\textit{in}})+C^{\prime}_{0}(q_{\textit{in}})$.

$\square$

Proof of Lemma 3. Again, we can prove this property by induction on $0\leq
i\leq k$. For $i=0$, it is obvious since $C_{0}(q)=0$ for all $q\in
Q\setminus\\{q_{\textit{in}}\\}$. Let now $0\leq i<k$ and assume that the
property is true. Let $N_{1}=C_{0}(q_{\textit{in}})$. Then
$\widetilde{C_{i}}\xrightarrow{t_{i+1}}\widetilde{C_{i+1}}$ is a transition
that preserves the property. The proof of it depends on $t_{i+1}$:

  * •

If $t_{i+1}=(p_{1},!!a,p_{2})$, then by induction hypothesis,
$\widetilde{C_{i}}(p_{1})\geq\widetilde{C_{0}}(p_{1})+C_{i}(p_{1})$ if
$p_{1}\neq q_{\textit{in}}$, and
$\widetilde{C_{i}}(p_{1})\geq(M-1).N_{1}+C_{i}(p_{1})$ if
$p_{1}=q_{\textit{in}}$. Moreover, $C_{i}(p_{1})>0$, hence the transition
$t_{i+1}$ can be taken from $\widetilde{C_{i}}$. Let $C_{i}=\Lbag
p_{1},q^{\prime}_{1},\dots,q^{\prime}_{N_{1}-1}\Rbag$, then $C_{i+1}=\Lbag
p_{2},p^{\prime}_{1},\dots,p^{\prime}_{N-1}\Rbag$ such that for all $1\leq
i\leq N$, either $a\notin R(q^{\prime}_{i})$ and
$p^{\prime}_{i}=q^{\prime}_{i}$, or $(q^{\prime}_{i},?a,p^{\prime}_{i})\in T$.
Also, $\widetilde{C_{i}}=\Lbag
p_{1},q^{\prime}_{1},\dots,q^{\prime}_{N_{1}-1},q^{\prime\prime}_{1},\dots,q^{\prime\prime}_{K}\Rbag$
and $\widetilde{C_{i+1}}=\Lbag
p_{2},p^{\prime}_{1},\dots,p^{\prime}_{N_{1}-1},p^{\prime\prime}_{1},\dots,p^{\prime\prime}_{K}\Rbag$,
with, for all $1\leq i\leq K$, either $a\notin R(q^{\prime\prime}_{i})$ and
$p^{\prime\prime}_{i}=q^{\prime\prime}_{i}$, or
$(q^{\prime\prime}_{i},?a,p^{\prime\prime}_{i})\in T$. So it is obvious that
for all $q^{\prime}\in Q$, $\widetilde{C_{i+1}}(q^{\prime})\geq
C_{i+1}(q^{\prime})$. Let now $q^{\prime}\in Q_{A}$. Either
$\widetilde{C_{i+1}}(q^{\prime})=\widetilde{C_{i}}(q^{\prime})+\ell$ for some
$\ell\geq 0$, or
$\widetilde{C_{i+1}}(q^{\prime})=\widetilde{C_{i}}(q^{\prime})-1$ (and
$q^{\prime}=p_{1}$). In the first case,
$C_{i+1}(q^{\prime})=C_{i}(q^{\prime})+\ell^{\prime}$, with
$\ell\geq\ell^{\prime}\geq 0$. Indeed, let $\\{q^{1},\dots,q^{r}\\}$ be the
set of states such that $\widetilde{C_{i}}(q^{j})>0$ and
$(q^{j},?a,q^{\prime})$ for all $1\leq j\leq r$. For all $1\leq j\leq r$,
$C_{i}(q^{j})\leq\widetilde{C_{i}}(q^{j})$ by induction hypothesis, so
$C_{i+1}(q^{\prime})=C_{i}(q^{\prime})+\ell^{\prime}$ and
$\widetilde{C_{i+1}}(q^{\prime})=\widetilde{C_{i}}(q^{\prime})+\ell$ with
$\ell\geq\ell^{\prime}\geq-1$ (observe that if $\ell^{\prime}=-1$, it means
that $q^{\prime}=p_{1}$ and that no process has gone to $p_{1}$ when receiving
$a$). Hence, if $q^{\prime}\neq q_{\textit{in}}$, by induction hypothesis,
$\widetilde{C_{i+1}}(q^{\prime})\geq\widetilde{C_{0}}(q^{\prime})+C_{i}(q^{\prime})+\ell=\widetilde{C_{0}}(q^{\prime})+C_{i+1}(q^{\prime})-\ell^{\prime}+\ell\geq\widetilde{C_{0}}(q^{\prime})+C_{i+1}(q^{\prime})$.
If otherwise $q^{\prime}=q_{\textit{in}}$, by induction hypothesis,
$\widetilde{C_{i+1}}(q_{\textit{in}})=\widetilde{C_{i}}(q_{\textit{in}})+\ell\geq(M-1).N_{1}+C_{i}(q_{\textit{in}})+\ell=(M-1).N_{1}+C_{i+1}(q_{\textit{in}})-\ell^{\prime}+\ell\geq(M-1).N_{1}+C_{i+1}(q_{\textit{in}})$.

In the second case, we have that
$\widetilde{C_{i+1}}(p_{1})=\widetilde{C_{i}}(p_{1})-1$, so no process
receiving message $a$ goes to $p_{1}$. Then $C_{i+1}(p_{1})=C_{i}(p_{1})-1$,
because for all $q\in Q_{W}$ such that $(q,?a,p_{1})\in T$,
$C^{\prime\prime}_{m,i}(q)=0$, and $C^{\prime\prime}_{m,i}(q)\geq C_{i}(q)$,
so no process in $C_{i}$ can receive message $a$ and go to $p_{1}$ neither.
So, if $p_{1}\neq q_{\textit{in}}$, by induction hypothesis,
$\widetilde{C_{i+1}}(p_{1})\geq\widetilde{C_{0}}(p_{1})+C_{i}(p_{1})-1=\widetilde{C_{0}}+C_{i+1}(p_{1})$,
and if $p_{1}=q_{\textit{in}}$,
$\widetilde{C_{i+1}}(q_{\textit{in}})\geq(M-1).N_{1}+C_{i}(q_{\textit{in}})-1=(M-1).N_{1}+C_{i+1}(q_{\textit{in}})$
and we are done.

  * •

Let $t_{i+1}=(p_{1},!a,p_{2})$ and there exist $p,p^{\prime}\in Q$ such that
$(p,?m,p^{\prime})\in T$ and $C_{i}(p)>0$ and $C_{i}(p_{1})>0$. Then,
$C_{i+1}=C_{i}-\Lbag p_{1},p\Rbag+\Lbag p_{2},p^{\prime}\Rbag$. By induction
hypothesis, if $p_{1}\neq q_{\textit{in}}$,
$\widetilde{C_{i}}(p_{1})\geq\widetilde{C_{0}}(p_{1})+C_{i}(p_{1})$, if
$p_{1}=q_{\textit{in}}$,
$\widetilde{C_{i}}(p_{1})\geq(M-1).N_{1}+C_{i}(p_{1})$, and
$\widetilde{C_{i}}(p)\geq C_{i}(p)$ hence
$\widetilde{C_{i}}\xrightarrow{t_{i+1}}\widetilde{C_{i+1}}$. Moreover,
$\widetilde{C_{i+1}}=\widetilde{C_{i}}-\Lbag p_{1},p\Rbag+\Lbag
p_{2},p^{\prime}\Rbag$. Hence, if $p_{1}\neq q_{\textit{in}}$,
$\widetilde{C_{i+1}}(p_{1})=\widetilde{C_{i}}(p_{1})-1\geq\widetilde{C_{0}}(p_{1})+C_{i}(p_{1})-1=\widetilde{C_{0}}(p_{1})+C_{i+1}(p_{1})$,
and if $p_{1}=q_{\textit{in}}$,
$\widetilde{C_{i+1}}(p_{1})=\widetilde{C_{i}}(p_{1})-1\geq(M-1).N_{1}+C_{i}(p_{1})-1=(M-1).N_{1}+C_{i+1}(p_{1})$.
Now, by induction hypothesis, we also have that $\widetilde{C_{i}}(p)\geq
C_{i}(p)$. Hence, $\widetilde{C_{i+1}}(p)=\widetilde{C_{i}}(p)-1\geq
C_{i}(p)-1=C_{i+1}(p)$. Let any other $q\in Q_{A}$. If
$q\notin\\{p_{2},p^{\prime},q_{\textit{in}}\\}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)\geq\widetilde{C_{0}}(q)+C_{i}(q)=\widetilde{C_{0}}(q)+C_{i+1}(q)$.
If $q=q_{\textit{in}}\notin\\{p_{2},p^{\prime}\\}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)\geq(M-1).N_{1}+C_{i}(q)=(M-1).N_{1}+C_{i+1}(q)$.
If $q\in\\{p_{2},p^{\prime}\\}$, then
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq\widetilde{C_{0}}(q)+C_{i}(q)+1=\widetilde{C_{0}}(q)+C_{i+1}(q)$
if $q\neq q_{\textit{in}}$, and
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq(M-1).N_{1}+C_{i}(q)+1=(M-1)+N_{1}+C_{i+1}(q)$
if $q=q_{\textit{in}}$. Let $q\in Q_{W}$ such that $p\neq q$, if
$q\notin\\{p_{2},p^{\prime}\\}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)\geq C_{i}(q)=C_{i+1}(q)$. If
$p\in\\{p_{2},p^{\prime}\\}$, then
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq C_{i}(q)+1=C_{i+1}(q)$.

  * •

If $t_{i+1}=(p_{1},!a,p_{2})$ and for all $p,p^{\prime}\in Q$ such that
$(p,?m,p^{\prime})\in T$, we have that $C^{\prime}_{i}(p)=0$. Then, either
$\widetilde{C_{i}}(p)=0$ for all $p,p^{\prime}\in Q$ such that
$(p,?a,p^{\prime})\in T$, or there exist some $p,p^{\prime}\in Q$ such that
$(p,?m,p^{\prime})\in T$ and $\widetilde{C_{i}}(p)>0$. In the first case,
since $\widetilde{C_{i}}(p_{1})\geq 0$ by induction hypothesis,
$\widetilde{C_{i+1}}=\widetilde{C_{i}}-\Lbag p_{1}\Rbag+\Lbag p_{2}\Rbag$, and
$C_{i+1}=C_{i}-\Lbag p_{1}\Rbag+\Lbag p_{2}\Rbag$. Then it is obvious that
$\widetilde{C_{i+1}}(q)\geq\widetilde{C_{0}}(q)+C_{i+1}(q)$ for all $q\in
Q_{A}\setminus\\{q_{\textit{in}}\\}$, $\widetilde{C_{i+1}}(q)\geq C_{i+1}(q)$
for all $q\in Q_{W}$, and
$\widetilde{C_{i+1}}(q_{\textit{in}})\geq(M-1).N_{1}+C_{i+1}(q_{\textit{in}})$.
In the second case, $\widetilde{C_{i+1}}=\widetilde{C_{i}}-\Lbag
p_{1},p\Rbag+\Lbag p_{2},p^{\prime}\Rbag$. Let $q\in Q_{A}$. If $q=p_{1}$,
then if $q\neq q_{\textit{in}}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)-1\geq\widetilde{C_{0}}(q)+C_{i}(q)-1=\widetilde{C_{0}}(q)+C_{i+1}(q)$,
and if $q=p_{1}=q_{\textit{in}}$, then
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)-1\geq(M-1).N_{1}+C_{i}(q)-1=(M-1).N_{1}+C_{i+1}(q)$.
If $q=p_{2}$, if $q\neq q_{\textit{in}}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq\widetilde{C_{0}}(q)+C_{i}(q)+1=\widetilde{C_{0}}(q)+C_{i+1}(q)$,
and if $q=p_{2}=q_{\textit{in}}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq(M-1).N_{1}+C_{i}(q)+1=(M-1).N_{1}+C_{i+1}(q)$.
If $q=p^{\prime}$, and $q\neq q_{\textit{in}}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq\widetilde{C_{0}}(q)+C_{i}(q)+1>\widetilde{C_{0}}(q)+C_{i+1}(q)$
since $C_{i+1}(p^{\prime})=C_{i}(p^{\prime})+1$. If
$q=p^{\prime}=q_{\textit{in}}$,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq(M-1).N_{1}+C_{i}(q)+1=(M-1).N_{1}+C_{i+1}(q)$.
Otherwise,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)\geq\widetilde{C_{0}}(q)+C_{i}(q)=\widetilde{C_{0}}(q)+C_{i+1}(q)$
if $q\neq q_{\textit{in}}$, and
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)\geq(M-1).N_{1}+C_{i}(q)=(M-1).N_{1}+C_{i+1}(q)$
if $q=q_{\textit{in}}$.

Finally, let $q\in Q_{W}$. If $p=q$, then
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)-1\geq 0$. However,
$C_{i+1}(q)=C_{i}(q)=0$, then $\widetilde{C_{i+1}}(q)\geq C_{i+1}(q)$. If
$q=p_{2}$, then $\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq
C_{i}(q)+1=C_{i+1}(q)$. If $q=p^{\prime}$, then
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)+1\geq
C_{i}(q)+1>C_{i}(q)=C_{i+1}(q)$. Otherwise,
$\widetilde{C_{i+1}}(q)=\widetilde{C_{i}}(q)\geq C_{i}(q)=C_{i+1}(q)$.

$\square$

##  Appendix 0.B Proofs of Section 4.2

We give the formal definitions of the protocol and the formal proofs of
Section 4.2. We start by introducing some notations. We denote an instance of
CVP: $C=(V,o,G,B,b)$ where $V=\\{v_{1},\dots,\linebreak[0]v_{n}\\}$ denotes
the $n$ input variables, $o$ is the output variable,
$G=\\{g_{1},\dots,g_{m}\\}$ the $m$ boolean gates, $B=\\{b_{1},\dots,b_{n}\\}$
the boolean assignment such that for all $1\leq i\leq n$, boolean
$b_{i}\in\\{\top,\bot\\}$ is the assignment of variable $v_{i}$, and $b$ the
boolean output value to test. Let $V^{\prime}=V\cup\\{o_{1},\dots,o_{m}\\}$
where $o_{j}$ is the output variable of gate $j$ for $1\leq j\leq m$. Wlog we
can assume that $o=o_{m}$. For $1\leq j\leq m$, we denote gate $g_{j}$ by
$g_{j}(\diamond,x_{1},x_{2},o_{j})$ with $x_{1},x_{2}\in V^{\prime}$ and
$\diamond\in\\{\vee,\land\\}$ or by $g_{j}(\lnot,x,o_{j})$ with $x\in
V^{\prime}$. As $C$ is acyclic, one can assume that $x_{1},x_{2},x\in
V\cup\\{o_{1},o_{2},\dots,o_{j-1}\\}$.

Let some $x\in V^{\prime}$, we denote $\textsf{bv}(x)$ the boolean value of
$x$ with respect to the input $B$. Note that if $x\in V$, there exists $1\leq
i~\leq n$ such that $x=v_{i}$ and so $\textsf{bv}(x)=b_{i}$.

Let $1\leq j\leq m$, we describe $P_{j}=(Q_{j},\Sigma_{j},T_{j})$ where
$\Sigma_{j}=V^{\prime}\times\\{\top,\bot\\}$ as follows:

  * •

if $g_{j}(\vee,x_{1},x_{2},o_{j})$,
$Q_{j}=\\{q_{0}^{j},q_{\top}^{j},q_{1}^{j},q_{\bot}^{j}\\}$, and
$T_{j}=\\{(q_{0}^{j},?(x_{k},\top),q_{\top}^{j})\mid k=1,2\\}$ $\cup$
$\\{(q_{0}^{j},?(x_{1},\bot)$,$q_{1}^{j})$,
$(q_{1}^{j},?(x_{2},\bot),q_{\bot}^{j})\\}$ $\cup$
$\\{(q_{\top}^{j},!!(o_{j},\top),q_{\top}^{j}),(q_{\bot}^{j},!!(o_{j},\bot),q_{\bot}^{j})\\}$;

  * •

if $g_{j}(\land,x_{1},x_{2},o_{j})$,
$Q_{j}=\\{q_{0}^{j},q_{\top}^{j},q_{1}^{j},q_{\bot}^{j}\\}$, and
$T_{j}=\\{(q_{0}^{j},?(x_{k},\bot),q_{\bot}^{j})\mid k=1,2\\}$ $\cup$
$\\{(q_{0}^{j},?(x_{1},\top)$,$q_{1}^{j})$,
$(q_{1}^{j},?(x_{2},\top),q_{\top}^{j})\\}$ $\cup$
$\\{(q_{\top}^{j},!!(o_{j},\top),q_{\top}^{j}),(q_{\bot}^{j},!!(o_{j},\bot),q_{\bot}^{j})\\}$;

  * •

if $g_{j}(\lnot,x,o_{j})$, $Q_{j}=\\{q_{0}^{j},q_{\top}^{j},q_{\bot}^{j}\\}$,
and
$T_{j}=\\{(q_{0}^{j},?(x,\bot),q_{\top}^{j}),(q_{0}^{j},?(x,\top)$,$q_{\bot}^{j})\\}$
$\cup$
$\\{(q_{\top}^{j},!!(o_{j},\top),q_{\top}^{j}),(q_{\bot}^{j},!!(o_{j},\bot),q_{\bot}^{j})\\}$.

We are now ready to define the protocol associated to $C$,
$P_{C}=(Q,\Sigma,q_{\textit{in}},T)$:

  * •

$Q=\\{q_{\textit{in}}\\}\cup\bigcup_{1\leq j\leq m}Q_{j}$;

  * •

$\Sigma=V^{\prime}\times\\{\top,\bot\\}$;

  * •

$T=\\{(q_{\textit{in}},!!(v_{j},b_{j}),q_{\textit{in}})\mid 1\leq j\leq
n\\}\cup\\{(q_{\textit{in}},!!\tau,q_{0}^{j})\mid 1\leq j\leq
m\\}\bigcup_{1\leq j\leq m}T_{j}$.

Observe that $P$ is Wait-Only: $q_{\textit{in}}$ is an active state, and for
all $1\leq j\leq m$: if $g_{j}$ is a "not" gate, $q_{0}^{j}$ is a waiting
state, and $q_{\bot}^{j},q_{\top}^{j}$ are active states, and if $g_{j}$ is an
"and" gate or an "or" gate, $q_{\bot}^{j},q_{\top}^{j}$ are active states and
$q_{0}^{j},q_{1}^{j}$ are waiting states.

We show that $\textsf{bv}(o)=b$ if and only if there is an initial
configuration $C_{0}\in\mathcal{I}$ and $C_{f}\in\mathcal{C}$ such that
$C_{0}\rightarrow^{\ast}C_{f}$ and $C_{f}(q_{b}^{m})>0$.

###### Lemma 11

If $\textsf{bv}(o)=b$, then there exists $C_{0}\in\mathcal{I}$ and
$C_{f}\in\mathcal{C}$ such that $C_{0}\rightarrow^{\ast}C_{f}$ and
$C_{f}(q_{b}^{m})>0$.

###### Proof

Assume that $\textsf{bv}(o)=b$, and take
$C_{0}=\Lbag(m+1).q_{\textit{in}}\Rbag$. There exists an execution
$C_{0}\rightarrow^{\ast}C_{f}$ with $C_{f}=\Lbag
q_{\textit{in}},q_{y_{1}}^{1},q_{y_{2}}^{2},\dots q_{y_{m}}^{m}\Rbag$ where
$y_{j}=\textsf{bv}(o_{j})$ with the input boolean values $B$ for $1\leq j\leq
m$. By definition, $y_{m}=\textsf{bv}(o)=b$. The execution is:
$C_{0}\rightarrow^{+}C_{1}\rightarrow^{+}\dots\rightarrow^{+}C_{m}$ where
$C_{j}=\Lbag q_{\textit{in}},q_{y_{1}}^{1},\dots
q_{y_{j}}^{j},q_{\textit{in}},\dots,q_{\textit{in}}\Rbag$ for all $0\leq j<m$.
Between $C_{j}$ and $C_{j+1}$, the sequence of transitions is:

  * •

if $g_{j+1}(\vee,x_{1},x_{2},o_{j+1})$ with $\textsf{bv}(x_{k})=\top$ for some
$k\in\\{1,2\\}$, then $\textsf{bv}(o_{j+1})=\top$. Either $x_{k}=v_{i}$ (and
$b_{i}=\top$) for some $1\leq i\leq n$, or $x_{k}=o_{i}$ (and $y_{i}=\top$)
for some $1\leq i\leq j$. In the first case, as $C_{j}(q_{\textit{in}})\geq
2$, then consider the sequence
$C_{j}\xrightarrow{(q_{\textit{in}},!!\tau,q_{0}^{j+1})}C^{\prime}_{j}\xrightarrow{(q_{\textit{in}},!!(v_{i},\top),q_{\textit{in}})}C_{j+1}$.
It holds that $C^{\prime}_{j}=C_{j}-\Lbag q_{\textit{in}}\Rbag+\Lbag
q_{0}^{j+1}\Rbag$ and $C_{j+1}=C^{\prime}_{j}-\Lbag q_{0}^{j+1}\Rbag+\Lbag
q_{\top}^{j+1}\Rbag$. Hence $C_{j+1}=\Lbag q_{\textit{in}},q_{y_{1}}^{1},\dots
q_{y_{j}}^{j},q_{y_{j+1}}^{j+1},\dots,q_{\textit{in}}\Rbag$.

In the second case, $C_{j}(q_{\top}^{i})>0$ as $i\leq j$ and
$\top=\textsf{bv}(o_{i})$, and $C_{j}(q_{\textit{in}})>0$. Consider the
sequence
$C_{j}\xrightarrow{(q_{\textit{in}},!!\tau,q_{0}^{j+1})}C^{\prime}_{j}\xrightarrow{(q_{\top}^{i},!!(o_{i},\top),q_{\top}^{i})}C_{j+1}$.
It holds that $C^{\prime}_{j}=C_{j}-\Lbag q_{\textit{in}}\Rbag+\Lbag
q_{0}^{j+1}\Rbag$ and $C_{j+1}=C^{\prime}_{j}-\Lbag q_{0}^{j+1}\Rbag+\Lbag
q_{\top}^{j+1}\Rbag$. Hence $C_{j+1}=\Lbag q_{\textit{in}},q_{y_{1}}^{1},\dots
q_{y_{j}}^{j},q_{y_{j+1}}^{j+1},\dots,q_{\textit{in}}\Rbag$.

  * •

if $g_{j+1}(\land,x_{1},x_{2},o_{j+1})$ with $\textsf{bv}(x_{k})=\bot$ for
some $k=1,2$, then $\textsf{bv}(o_{j+1})=\bot=y_{j+1}$. The sequence of
transitions is built in an analogous way than the previous case, however this
time the broadcast messages are $\tau$ and $(x_{k},\bot)$ and the reached
state is $q_{\bot}^{j+1}$.

  * •

if $g_{j+1}(\vee,x_{1},x_{2},o_{j+1})$ with
$\textsf{bv}(x_{1})=\textsf{bv}(x_{2})=\bot$, then
$\textsf{bv}(o_{j+1})=\bot$. Either $x_{1}=v_{i}$ (and $b_{i}=\bot$) for some
$1\leq i\leq n$, or $x_{1}=o_{i}$ (and $y_{i}=\bot$) for some $1\leq i\leq j$.
In the first case, as $C_{j}(q_{\textit{in}})\geq 2$, then consider the
sequence
$C_{j}\xrightarrow{(q_{\textit{in}},!!\tau,q_{0}^{j+1})}C_{j,1}\xrightarrow{(q_{\textit{in}},!!(v_{i},\bot),q_{\textit{in}})}C_{j,2}$.
It holds that $C_{j,1}=C_{j}-\Lbag q_{\textit{in}}\Rbag+\Lbag
q_{0}^{j+1}\Rbag$ and $C_{j,2}=C_{j,1}-\Lbag q_{0}^{j+1}\Rbag+\Lbag
q_{1}^{j+1}\Rbag$.

If $x_{1}=o_{i}$ for some $i\leq j$, $C_{j}(q_{\bot}^{i})>0$ as $i\leq j$ and
$\bot=\textsf{bv}(o_{i})$, and $C_{j}(q_{\textit{in}})>0$. Consider the
sequence
$C_{j}\xrightarrow{(q_{\textit{in}},!!\tau,q_{0}^{j+1})}C_{j,1}\xrightarrow{(q_{\bot}^{i},!!(o_{i},\bot),q_{\bot}^{i})}C_{j,2}$.
It holds that $C_{j,1}=C_{j}-\Lbag q_{\textit{in}}\Rbag+\Lbag
q_{0}^{j+1}\Rbag$ and $C_{j,2}=C_{j,1}-\Lbag q_{0}^{j+1}\Rbag+\Lbag
q_{1}^{j+1}\Rbag$.

In both cases, $C_{j,2}=\Lbag q_{\textit{in}},q_{y_{1}}^{1},\dots
q_{y_{j}}^{j},q_{1}^{j+1},\dots,q_{\textit{in}}\Rbag$.

We make the same cases distinctions in order to build the configuration
$C_{j+1}$ such that $C_{j,2}\xrightarrow{(q,!!(x_{2},\bot),q)}C_{j+1}$ where
$q=q_{\textit{in}}$ if $x_{2}\in V$, and otherwise $x_{2}=o_{i}$ for some
$i\leq j$ and $q=q_{\bot}^{i}$.

It holds that $C_{j+1}=C_{j,2}-\Lbag q_{1}^{j+1}\Rbag+\Lbag
q_{\bot}^{j+1}\Rbag$, hence $C_{j+1}=\Lbag q_{\textit{in}},q_{y_{1}}^{1},\dots
q_{y_{j}}^{j},q_{y_{j+1}}^{j+1},\linebreak[0]\dots,q_{\textit{in}}\Rbag$.

  * •

if $g_{j+1}(\land,x_{1},x_{2},o_{j+1})$ with
$\textsf{bv}(x_{1})=\textsf{bv}(x_{2})=\top$, then
$\textsf{bv}(o_{j+1})=\top$. The sequence of transitions is built in an
analogous way than the previous case, however this time the broadcast messages
are $\tau$, $(x_{1},\top)$ and $(x_{2},\top)$ and the reached state is
$q_{\top}^{j+1}$.

  * •

if $g_{j+1}(\lnot,x,o_{j+1})$ with $\textsf{bv}(x)=\top$ (resp. $\bot$), then
$\textsf{bv}(o_{j+1})=\bot$ (resp. $\top$). Either $x=v_{i}$ for some $1\leq
i\leq n$, and as $C_{j}(q_{\textit{in}})\geq 2$, we build the following
sequence:
$C_{j}\xrightarrow{(q_{\textit{in}},!!\tau,q_{0}^{j+1})},C^{\prime}_{j}\xrightarrow{(q_{\textit{in}},(v_{i},b_{i}),q_{\textit{in}})}C_{j+1}$.
It holds that $C^{\prime}_{j}=C_{j}-\Lbag q_{\textit{in}}\Rbag+\Lbag
q_{0}^{j+1}\Rbag$ and $C_{j+1}=C^{\prime}_{j}-\Lbag q_{0}^{j+1}\Rbag+\Lbag
q_{\bar{b}_{i}}^{j+1}\Rbag$ where $\bar{b}_{i}=\bot$ (resp.
$\bar{b}_{i}=\top$).

Otherwise, $x=o_{i}$ for some $i\leq j$, and so $C_{j}(q_{\top}^{i})>0$ (resp.
$C_{j}(q_{\bot}^{i})>0$) and $C_{j}(q_{\textit{in}})>0$. Hence, we can build
the following sequence:
$C_{j}\xrightarrow{(q_{\textit{in}},!!\tau,q_{0}^{j+1})},C^{\prime}_{j}\xrightarrow{(q_{\textit{in}},(o_{i},\textsf{bv}(o_{i})),q_{\textit{in}})}C_{j+1}$.
It holds that $C^{\prime}_{j}=C_{j}-\Lbag q_{\textit{in}}\Rbag+\Lbag
q_{0}^{j+1}\Rbag$ and $C_{j+1}=C^{\prime}_{j}-\Lbag q_{0}^{j+1}\Rbag+\Lbag
q_{\bar{y}_{i}}^{j+1}\Rbag$ where $\bar{y}_{i}=\bot$ (resp.
$\bar{y}_{i}=\top$).

In both cases, $C_{j+1}=\Lbag q_{\textit{in}},q_{y_{1}}^{1},\dots
q_{y_{j}}^{j},q_{y_{j+1}}^{j+1},\dots,q_{\textit{in}}\Rbag$.

Hence, $C_{0}\rightarrow^{+}C_{m}$ where $C_{m}(q_{y_{m}}^{m})>0$, and so if
$b=y_{m}$, $C_{m}(q_{b}^{m})>0$. ∎

###### Lemma 12

If there exists $C_{0}\in\mathcal{I}$ and $C_{f}\in\mathcal{C}$ such that
$C_{0}\rightarrow^{\ast}C_{f}$ and $C_{f}(q_{b}^{m})>0$, then
$\textsf{bv}(o)=b$.

###### Proof

Let $C_{0}\in\mathcal{I}$ and $C_{f}\in\mathcal{C}$ such that
$C_{0}\rightarrow^{\ast}C_{f}$ and $C_{f}(q_{b}^{m})>0$.

First we show that all broadcast messages $(x,b_{x})\in
V^{\prime}\times\\{\top,\bot\\}$ are such that $b_{x}=\textsf{bv}(x)$. We
start by proving it for $x\in V$, and then proceed to prove it for
$x\in\\{o_{1},\dots,o_{m}\\}$ by induction on $m$.

Let $(x,b_{x})$ a broadcast message such that $x\in V$, we note $x=v_{i}$ with
$1\leq i\leq n$. By construction of the protocol $P$, the only broadcast
transition labelled with first element $v_{i}$ is the transition
$(q_{\textit{in}},!!(v_{i},b_{i}),q_{\textit{in}})$ where $b_{i}$ is the input
boolean value for variable $v_{i}$, i.e. $\textsf{bv}(v_{i})=b_{i}$. Hence,
all broadcast messages $(x,b_{x})$ with $x\in V$, are such that
$b_{x}=\textsf{bv}(x)$.

We prove now than for all
$(x,b_{x})\in\\{o_{1},\dots,o_{m}\\}\times\\{\top,\bot\\}$,
$b_{x}=\textsf{bv}(x)$ and we do so by induction on $m$. For $m=1$, we have
that $x=o_{1}$. Note that tuples containing $o_{1}$ can only be broadcast from
$q_{\bot}^{1}$ or $q_{\top}^{1}$. Denote $g_{1}(\diamond,x_{1},x_{2},o_{1})$
or $g_{1}(\lnot,x_{3},o_{1})$ with $\diamond\in\\{\vee,\land\\}$ and
$x_{1},x_{2},x_{3}\in V$ by acyclicity.

  * •

if $\diamond=\vee$, then a process reaching $q_{\top}^{1}$ has necessarily
received $(x_{1},\top)$ or $(x_{2},\top)$, and a process reaching
$q_{\bot}^{1}$ has necessarily received $(x_{1},\bot)$ and $(x_{2},\bot)$. As
we proved, all broadcast messages containing $x_{1}$ (resp. $x_{2}$) are of
the form $(x_{1},\textsf{bv}(x_{1}))$ (resp. $(x_{2},\textsf{bv}(x_{2}))$).
Hence, only one state between $q_{\top}^{1}$ and $q_{\bot}^{1}$ is reachable.
If it is $q_{\top}^{1}$ (resp. $q_{\bot}^{1}$), the only messages containing
$o_{1}$ which can be broadcast are $(o_{1},\top)$ (resp. $(o_{1},\bot)$) and
it holds that
$\top=\textsf{bv}(x_{1})\vee\textsf{bv}(x_{2})=\textsf{bv}(o_{1})$ (resp.
$\bot$) as the process on $q_{\top}^{1}$ (resp. $q_{\bot}^{1}$) received
either $(x_{1},\top)$ or $(x_{2},\top)$ (resp. $(x_{1},\bot)$ and
$(x_{2},\bot)$);

  * •

if $\diamond=\land$, the argument is analogous to the previous case;

  * •

if $\diamond=\lnot$, then a process reaching $q_{\top}^{1}$ has necessarily
received $(x_{3},\bot)$ and a process reaching $q_{\bot}^{1}$ has necessarily
received $(x_{3},\top)$. As we proved, all broadcast messages containing
$x_{3}$ are of the form $(x_{3},\textsf{bv}(x_{3}))$. Hence, only one state
between $q_{\top}^{1}$ and $q_{\bot}^{1}$ is reachable. If it is
$q_{\top}^{1}$ (resp. $q_{\bot}^{1}$), the only messages containing $o_{1}$
which can be broadcast are $(o_{1},\top)$ (resp. $(o_{1},\bot)$) and it holds
that $\top=\lnot\textsf{bv}(x_{3})=\textsf{bv}(o_{1})$ (resp. $\bot$) as the
process on $q_{\top}^{1}$ (resp. $q_{\bot}^{1}$) received $(x_{3},\bot)$
(resp. $(x_{3},\top)$).

Assume the property true for $m$ gates, and let $(o_{m+1},b_{m+1})$ a
broadcast message and note $g_{m+1}(\diamond,x_{1},x_{2},o_{m+1})$ with
$\diamond\in\\{\land,\lor\\}$, or $g_{m+1}(\lnot,x_{3},o_{m+1})$ with
$x_{1},x_{2},x_{3}\in V\cup\\{o_{1},\dots,o_{m}\\}$. By induction hypothesis,
the only broadcast messages containing $x_{1}$, $x_{2}$ or $x_{3}$ are
$(x_{1},\textsf{bv}(x_{1}))$, $(x_{2},\textsf{bv}(x_{2}))$, and
$(x_{3},\textsf{bv}(x_{3}))$. The arguments are then the same than in the case
$m=1$. ∎

Hence, we proved with the two previous lemmas that $\textsf{bv}(o)=b$ if and
only if $q_{b}^{m}$ is coverable and we get the following theorem.

###### Theorem 0.B.1

StateCover for Wait-Only protocols is P-hard.

###### Remark 4

If we transform the Wait-Only protocol presented here into a Wait-Only NB-
Rendez-vous protocol (by transforming all the broadcast transitions into
sending transitions on the same message), the reduction remains sound and
complete. Indeed, in the execution of $P_{C}$ built in Lemma 11, all the
broadcasts are received by only one process. Hence, the same execution is
possible by replacing broadcasts transitions by sending transitions. The proof
of Lemma 12 works exactly the same way if the broadcasts transitions become
sending transitions. Hence, the StateCover and ConfCover problems for Wait-
Only NB-Rendez-vous are P-hard, closing a lower bound open in [GSS23].

##  Appendix 0.C Proofs of Section 5

###  0.C.1 Proofs of Section 5.3

Proof of Lemma 7. We present here the two missing cases in the proof of Lemma
7.

  1. (i)

if $\alpha=!!a$, then by definition of $\rightarrow$, $C=\Lbag
q_{1},\dots,q_{n},q\Rbag$ and $C^{\prime}=\Lbag
q^{\prime}_{1},\dots,q^{\prime}_{n},q^{\prime}\Rbag$ such that for all $1\leq
i\leq n$, either $(q_{i},?a,q^{\prime}_{i})\in T$ or $a\nin R(q_{i})$ and
$q_{i}=q^{\prime}_{i}$. We get the two following disjoint cases:

     * •

$M^{\prime}(q^{\prime})=0$. In this case, $M^{\prime}=\Lbag
q^{\prime}_{i_{1}},q^{\prime}_{i_{2}},\dots q^{\prime}_{i_{K}}\Rbag$ where
$1\leq i_{j}\leq n$ for all $1\leq j\leq K$ and $i_{j}\neq i_{\ell}$ if
$j\neq\ell$. Let $M=\Lbag q_{i_{1}},q_{i_{2}},\dots q_{i_{K}}\Rbag$. Note that
we have $M\preceq C$, hence $C\in\llbracket(M,S)\rrbracket$. Using the
definition of $\rightarrow$, we have as well $M+\Lbag q\Rbag\rightarrow
M^{\prime}+\Lbag q^{\prime}\Rbag$. Furthermore since $C(q)>0$, we have $q\in
S$ by definition of $S$. Applying the definition of
$\Rightarrow_{\textsf{ext}}$ we have
$(M,S)\xRightarrow{t}_{\textsf{ext}}(M^{\prime},S^{\prime})$.

     * •

$M^{\prime}(q^{\prime})>0$. In this case, $M^{\prime}=\Lbag
q^{\prime}_{i_{1}},q^{\prime}_{i_{2}},\dots
q^{\prime}_{i_{K-1}},q^{\prime}\Rbag$ where $1\leq i_{j}\leq n$ for all $1\leq
j<K$ and $i_{j}\neq i_{\ell}$ if $j\neq\ell$. Let $M=\Lbag
q_{i_{1}},q_{i_{2}},\dots q_{i_{K-1}},q\Rbag$. Note that we have $M\preceq C$,
hence $C\in\llbracket(M,S)\rrbracket$. Using the definition of $\rightarrow$,
we have as well $M\rightarrow M^{\prime}$. Applying the definition of
$\Rightarrow_{\textsf{step}}$, we get
$(M,S)\xRightarrow{t}_{\textsf{step}}(M^{\prime},S^{\prime})$.

  2. (ii)

if $\alpha=!a$ and the message is _not_ received (i.e. it is a non blocking
sending), then using the definition of $\rightarrow$, we have
$C^{\prime}=C-\Lbag q\Rbag+\Lbag q^{\prime}\Rbag$ and $a\nin R(p)$ for all
$p\in Q$ such that $(C-\Lbag q\Rbag)(p)>0$. We obtain the two following
disjoint cases:

     * •

$M^{\prime}(q^{\prime})=0$. Since $C^{\prime}(q^{\prime})>0$ and
$M^{\prime}\preceq C^{\prime}$, we deduce that $C^{\prime}=M^{\prime}+\Lbag
q^{\prime}\Rbag+M_{2}$ for some multiset $M_{2}$. By definition of
$C^{\prime}$, we have as well $C=C^{\prime}+\Lbag q\Rbag-\Lbag
q^{\prime}\Rbag$, hence $C=M^{\prime}+\Lbag q\Rbag+M_{2}$. We deduce that
$M^{\prime}\preceq C$ and hence $C\in\llbracket(M^{\prime},S)\rrbracket$.
Furthermore we have $M^{\prime}+\Lbag q\Rbag\rightarrow M^{\prime}+\Lbag
q^{\prime}\Rbag$ as $a\nin R(q)$ for all states $q\in Q$ such that
$M^{\prime}(q)>0$. Consequently,
$(M^{\prime},S)\xRightarrow{t}_{\textsf{ext}}(M^{\prime},S^{\prime})$.

     * •

$M^{\prime}(q^{\prime})>0$. Since $M^{\prime}\preceq C^{\prime}$, we have
$C^{\prime}=M^{\prime}+M_{2}$ for some multiset $M_{2}$. Let
$M=M^{\prime}+\Lbag q\Rbag-\Lbag q^{\prime}\Rbag$. We have hence
$C=C^{\prime}+\Lbag q\Rbag-\Lbag q^{\prime}\Rbag=M^{\prime}+\Lbag q\Rbag-\Lbag
q^{\prime}\Rbag+M_{2}=M+M_{2}$. Hence $M\preceq C$ and
$C\in\llbracket(M,S)\rrbracket$. Furthermore we have that $a\nin R(p)$ for all
$p\in Q$ such that $(M-\Lbag q\Rbag)(p)>0$). We hence deduce that
$M\xrightarrow{t}M^{\prime}$. Applying the definition of
$\Rightarrow_{\textsf{step}}$, we get
$(M,S)\xRightarrow{t}_{\textsf{step}}(M^{\prime},S^{\prime})$.

$\square$

Proof of Lemma 8. Suppose we have
$C_{0}\xrightarrow{t_{1}}C_{1}\xrightarrow{t_{2}}\ldots\xrightarrow{t_{n}}C_{n}$
with $C_{0}=C_{\textit{in}}$ and $C_{n}=C$. We show by induction on $0\leq
i\leq n$ that for all $M_{i}\in\mathcal{C}_{=K}$ such that $M_{i}\preceq
C_{i}$ there exists $S_{i}\subseteq Q$ such that
$C_{i}\in\llbracket(M_{i},S_{i})\rrbracket$ and
$\gamma_{\textit{in}}\Rightarrow^{\ast}(M_{i},S_{i})$.

For $i=0$, we have $C_{\textit{in}}=\Lbag||C||\cdot q_{\textit{in}}\Rbag$ and
$\Lbag K\cdot q_{\textit{in}}\Rbag$ is the unique configuration of size $K$
smaller than $C_{\textit{in}}$. Since $\gamma_{\textit{in}}=(\Lbag K\cdot
q_{\textit{in}}\Rbag,\\{q_{\textit{in}}\\})$, we have
$C_{\textit{in}}\in\llbracket\gamma_{\textit{in}}\rrbracket$.

Assume now that the property holds for $0\leq i<n$. Let
$M_{i+1}\in\mathcal{C}_{=K}$ such that $M_{i+1}\preceq C_{i+1}$. Since
$C_{i}\xrightarrow{t_{i+1}}C_{i+1}$, by applying Lemma 7, there exists
$M_{i}\in\mathcal{C}_{=K}$, $S_{i+1}\subseteq Q$ such that
$(M_{i},S_{i})\Rightarrow(M_{i+1},S_{i+1})$ where $S_{i}=\\{q\in Q\mid
C_{i}(q)>0\\}$, $C_{i}\in\llbracket(M_{i},S_{i})\rrbracket$ and
$C_{i+1}\in\llbracket(M_{i+1},S_{i+1)}\rrbracket$. By induction hypothesis,
there exists $S^{\prime}_{i}\subseteq Q$ such that
$C_{i}\in\llbracket(M_{i},S^{\prime}_{i})\rrbracket$ and
$\gamma_{in}\Rightarrow^{\ast}(M_{i},S^{\prime}_{i})$. But since
$C_{i}\in\llbracket(M_{i},S^{\prime}_{i})\rrbracket$ and $S_{i}=\\{q\in Q\mid
C_{i}(q)>0\\}$, we have $S_{i}\subseteq S^{\prime}_{i}$. Using Lemma 6.2, we
deduce that there exists $S^{\prime}_{i+1}$ such that $S_{i+1}\subseteq
S^{\prime}_{i+1}$ and
$(M_{i},S^{\prime}_{i})\Rightarrow(M_{i+1},S^{\prime}_{i+1})$. Hence
$\gamma_{\textit{in}}\Rightarrow^{\ast}(M_{i+1},S^{\prime}_{i+1})$ and thanks
to Lemma 6.1, $C_{i+1}\in\llbracket(M_{i+1},S^{\prime}_{i+1})\rrbracket$.
$\square$

###  0.C.2 Proofs of Section 5.6

Assume that there exists a word $w=a_{1}\dots a_{k}\in\bigcap_{1\leq i\leq
n}L(\mathcal{A}_{i})$, i.e.,
$q_{i}^{f}=\Delta^{*}(q_{i}^{0},a_{1}\linebreak[0]\dots a_{k})$ for all $1\leq
i\leq n$. Then take $C=\Lbag(n+1).q_{\textit{in}}\Rbag$. There exists an
execution $C\rightarrow^{\ast}C^{\prime}$ with $C^{\prime}=\Lbag
q_{s},q_{1}^{f},\dots,q_{n}^{f}\Rbag\succeq C_{f}$. This execution is
$C\xrightarrow{(q_{\textit{in}},!!\tau,q_{s})}\tilde{C}_{1}\xrightarrow{(q_{\textit{in}},!!\tau,q_{1})}\tilde{C}_{2}\dots\xrightarrow{(q_{\textit{in}},!!\tau,q_{n})}\tilde{C}_{0}\xrightarrow{(q_{s},!!\textit{go},q_{s})}C_{0}\xrightarrow{(q_{s},!!a_{1},q_{s})}C_{1}\xrightarrow{(q_{s},!!a_{2},q_{s})}C_{2}\dots\linebreak[0]\xrightarrow{(q_{s},!!a_{k},q_{s})}C^{\prime}$.

One can check that $C_{0}(q_{i}^{0})=1$ for all $1\leq i\leq n$, and hence, by
definition of $(T_{i})_{1\leq i\leq n}$, $C_{k}(q_{i}^{f})=1$ for all $1\leq
i\leq n$. Hence $C^{\prime}=\Lbag q_{s},q_{1}^{f},\dots,q_{n}^{f}\Rbag\succeq
C_{f}$.

Reciprocally, assume that there exists an initial configuration $C$ and an
execution $C\rightarrow^{\ast}C^{\prime}$ with $C^{\prime}\succeq C_{f}$. We
first make easy observations about the executions of this protocol.

###### Observation 1

Let $C_{1},C_{2}\in\mathcal{C}_{P}$. We write
$C_{1}\xrightarrow{\tau}\\!\\!{}^{*}C_{2}$ if there exists a sequence of $k$
transitions $C_{1}\xrightarrow{t_{1}}\dots\xrightarrow{t_{k}}C_{2}$ such that
$t_{i}\in\\{(q_{\textit{in}},!!\tau,q)\mid
q\in\\{q_{s},q_{1},\dots,q_{n}\\}\\}$ for all $1\leq i\leq k$. Then
$C_{2}(q)\geq C_{1}(q)$ for all $q\in\\{q_{s},q_{1},\dots,q_{n}\\}$,
$C_{2}(q_{\textit{in}})\leq C_{1}(q_{\textit{in}})$, and $C_{2}(q)=C_{1}(q)$
for all other $q\in Q$.

###### Observation 2

Let $C_{1},C_{2}\in\mathcal{C}_{P}$ such that $C_{1}\rightarrow^{\ast}C_{2}$
with no transition $(q_{s},!!\textit{go},q_{s})$. If there is some $1\leq
i\leq n$ with $C_{1}(q)=0$ for all $q\in Q_{i}$, then $C_{2}(q)=0$ for all
$q\in Q_{i}$.

###### Observation 3

Let $C_{1},C_{2}\in\mathcal{C}_{P}$ such that
$C_{1}\xrightarrow{(q_{s},!!\textit{go},q_{s})}C_{2}$. Then,
$C_{2}(q_{s})=C_{1}(q_{s})>0$, and $C_{2}(q)=0$ for all $q\in\bigcup_{1\leq
i\leq n}(Q_{i}\setminus{\\{q^{0}_{i}\\}})$.

We can deduce from these observations that the execution
$C\rightarrow^{\ast}C^{\prime}$ can be decomposed in
$C\rightarrow^{\ast}\hat{C}\xrightarrow{(q_{s},!!\textit{go},q_{s})}C_{0}\rightarrow^{\ast}C^{\prime}$.
Indeed, since $C(q)=0$ for all $q\in\bigcup_{1\leq i\leq n}Q_{i}$, if no
transition $(q_{s},!!\textit{go},q_{s})$ appears in the execution, Observation
2 allows to conclude that $C^{\prime}(q^{f}_{i})=0$ for all $1\leq i\leq n$,
which contradicts the fact that $C^{\prime}\succeq C_{f}$. Assume now that
this transition is the last transition where action go is sent, i.e.,
$C_{0}\rightarrow^{\ast}C^{\prime}$ has no transition
$(q_{s},!!\textit{go},q_{s})$. By Observation 3, $C_{0}(q_{s})>0$ and
$C_{0}(q)=0$ for all $q\in\bigcup_{1\leq i\leq
n}(Q_{i}\setminus\\{q_{i}^{0}\\})$. By Observation 2, we also deduce that
$C_{0}(q_{i}^{0})>0$ for all $1\leq i\leq n$. Otherwise, if there exists
$1\leq j\leq n$ such that $C_{0}(q_{j}^{0})=0$, then $C^{\prime}(q_{j}^{f})=0$
which is a contradiction with $C^{\prime}\succeq C_{f}$.

Now the execution $C^{\prime}_{0}\rightarrow^{\ast}C^{\prime}$ is of the form
$C_{0}\xrightarrow{\tau}\\!\\!{}^{*}C^{\prime}_{0}\xrightarrow{(q_{s},!!a_{1},q_{s})}C_{1}\xrightarrow{\tau}\\!\\!{}^{*}C^{\prime}_{1}\xrightarrow{(q_{s},!!a_{2},q_{s})}C_{2}\dots\xrightarrow{(q_{s},!!a_{k},q_{s})}C_{k}\xrightarrow{\tau}\\!\\!{}^{*}C^{\prime}$.
Using Observation 1, we can obtain a new execution
$C_{0}\xrightarrow{(q_{s},!!a_{1},q_{s})}\tilde{C}_{1}\xrightarrow{(q_{s},!!a_{2},q_{s})}\tilde{C}_{2}\dots\xrightarrow{(q_{s},!!a_{k},q_{s})}\tilde{C}_{k}$
such that for all $1\leq j\leq k$, we let $\tilde{C}_{j}(q_{s})=C_{0}(q_{s})$,
$\tilde{C}_{j}(q_{i})=C_{0}(q_{i})$ for all $1\leq i\leq n$,
$\tilde{C}_{j}(q_{\textit{in}})=C_{0}(q_{\textit{in}})$ and
$\tilde{C}_{j}(q)=C_{j}(q)$ for all other $q$. Moreover,
$\tilde{C}_{k}(q_{i}^{f})=C_{k}(q_{f}^{i})=C^{\prime}(q_{f}^{i})\succeq
C_{f}$.

We can show now that the word $a_{1}\dots a_{k}$ belongs to $\bigcap_{1\leq
i\leq n}L(\mathcal{A}_{i})$. Let $1\leq i\leq n$. It is easy to see that for
all $1\leq j\leq k$, there exists a unique $q_{i}^{j}\in Q_{i}$ such that
$\tilde{C}_{j}(q_{i}^{j})>0$ and $\tilde{C}_{j}(q)=0$ for all $q\in
Q_{i}\setminus\\{q_{i}^{j}\\}$. Moreover, for all $1\leq j\leq k$,
$q_{i}^{j}=\Delta_{i}^{*}(q_{i}^{0},a_{1}\dots a_{j})$. As
$\tilde{C}_{k}(q_{i}^{f})=C^{\prime}(q_{i}^{f})>0$, we get that
$q_{i}^{f}=\Delta_{i}^{*}(q_{i}^{0},a_{1}\dots a_{k})$, and hence $a_{1}\dots
a_{k}\in L(\mathcal{A}_{i})$.