Wait-Only Broadcast Protocols Are Easier to Verify

Guillou, Lucie; Sangnier, Arnaud; Sznajder, Nathalie

doi:10.4230/LIPIcs.MFCS.2025.53

Wait-Only Broadcast Protocols Are Easier to Verify

Lucie Guillou

IRIF, CNRS, Université Paris Cité, France Arnaud Sangnier

DIBRIS, Università di Genova, Italy Nathalie Sznajder

LIP6, CNRS, Sorbonne Université, Paris, France

Abstract

We study networks of processes that all execute the same finite-state protocol and communicate via broadcasts. We are interested in two problems with a parameterized number of processes: the synchronization problem which asks whether there is an execution which puts all processes on a given state; and the repeated coverability problem which asks if there is an infinite execution where a given transition is taken infinitely often. Since both problems are undecidable in the general case, we investigate those problems when the protocol is Wait-Only, i.e., it has no state from which a process can both broadcast and receive messages. We establish that the synchronization problem becomes Ackermann-complete, and the repeated coverability problem is in ExpSpace and PSpace-hard.

Keywords and phrases:

Parameterised verification, Reachability, Broadcast

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Formal languages and automata theory

Related Version:

Long Version: https://arxiv.org/abs/2505.01269 [12]

Funding:

ANR project PaVeDyS (ANR-23-CE48-0005).

DOI:

10.4230/LIPIcs.MFCS.2025.53

Event:

50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Editors:

Paweł Gawrychowski, Filip Mazowiecki, and Michał Skrzypczak

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Distributed systems are at the core of modern computing, and are widely used in critical applications such as sensor networks, or distributed databases. These systems rely on protocols to enable communication, maintain coherence and coordination between the different processes. Because of their distributed nature, such protocols have proved to be error-prone. As a result, the formal verification of distributed systems has become an essential area of research. Formal verification of distributed systems presents unique challenges compared to fthe one of centralized systems. One of the most significant issue is the state explosion problem: the behavior of multiple processes that execute concurrently and exchange information often lead to state spaces that grow exponentially with the number of processes, making the analysis highly challenging. When the systems are parameterized, meaning designed to operate for an arbitrary number of processes, which is often the case in distributed protocols, classical techniques are not useful anymore. The difficulty shifts from state explosion to dealing with an infinite number of system configurations, which leads to undecidability in the general case [1]. Despite these challenges, verification becomes more tractable in certain restricted settings. For instance, in parameterized systems, the behavior of individual processes needs not always to be explicitly represented, which can mitigate state explosion. This has motivated researchers to focus on specific subclasses of systems or communication models where decidability can be achieved without sacrificing too much expressiveness. One such restriction involves protocols where processes are anonymous (i.e., without identities), and communicate via simple synchronous mechanisms, such as rendezvous [9], where two processes exchange a message synchronously. Several variants of this model have been studied, such as communication via a shared register containing some value from a finite set [7], or non-blocking rendezvous [10, 4], where a sender is not prevented from sending a message when no process is ready to receive it. In all these cases, the processes execute the same protocol, which is described by a finite automaton.

A more expressive model is broadcast protocols, introduced by Emerson and Namjoshi [6]. In these protocols, a process can send a broadcast message that is received simultaneously by all other processes (or by all neighboring processes in a network). Several key verification problems arise in this context, including the coverability problem, which asks whether a process can eventually reach a specific (bad) state starting from an initial configuration. Another important property is synchronization, which asks whether all processes can simultaneously reach a given state. Liveness properties, like determining whether infinite executions exist, ensure that certain behaviors occur indefinitely. While broadcast protocols allow more powerful communication than rendezvous protocols, this added expressiveness comes at the cost of increased verification complexity. Indeed, rendezvous communication can be simulated using broadcasts [8]. However, verification becomes significantly harder: while coverability and synchronization can be solved in polynomial time for rendezvous protocols [9], they become respectively Ackermann-complete [8, 20] and undecidable (we show it in this paper) for broadcast protocols. Liveness properties are also undecidable for broadcast protocols [8]. The challenge in verifying broadcast protocols can be understood through their relationship with Vector Addition Systems with States (VASS). Rendezvous-based protocols can be encoded in a VASS, where counters track the number of processes in each state. A rendezvous is simulated by decreasing the counters corresponding to the sender and receiver states and increasing the counters for their post-communication states. While using a VASS for protocols using rendezvous is certainly not the way to go due to the complexity gap between problems on VASS and the existing known polynomial time algorithms to solve verification problems, it is interesting to note that this encoding fails for broadcast protocols because a broadcast message must be received by all processes in a given state, requiring a bulk transfer of a counter value – something not expressible in classical VASS without adding powerful operations such as transfer arcs, which leads to an undecidable reachability problem [21]. However, in some cases, verification of broadcast protocols can become easier, complexity-wise. One example is the setting of Reconfigurable Broadcast Networks, in which communication between processes can be lossy [5]. Liveness properties become decidable in that case [5] and even polynomial time [2].

Another such case is given by a syntactic restriction known as Wait-Only protocols, introduced in [10] in the context of non-blocking rendezvous communication. In Wait-Only protocols, a process cannot both send and receive a message from the same state. From a practical perspective, Wait-Only protocols were proposed to model the non-blocking rendezvous semantics used in Java’s wait/notify/notifyAll synchronization mechanism and C’s wait/signal/broadcast operations with conditional variables, commonly found in multi-threaded programs. In both languages, threads can be awakened by the reception of a message. This naturally leads to distinguishing between action and waiting states: a sleeping thread cannot act on its own and can only be awakened by a signal. This restriction simplifies the possible behaviours of the system, potentially reducing the complexity of the verification. Actually, the coverability problem for Wait-Only broadcast protocols becomes PSpace-complete [11]. Indeed, when processes are in a state where they can receive broadcasts, they cannot send messages, meaning they will move together to the next state, reducing the need for precise counting. Moreover, when a process is in a broadcasting state, it remains there until it decides to send a message, simplifying execution reconstruction and enabling better verification algorithms. By leveraging these properties, we design algorithms for the synchronization problem and liveness properties, obtaining new decidability results for these challenging problems. Proofs omitted due to space contraints can be found in [12].

2 Model and Verification Problems

In this section, we provide the description of a model for networks with broadcast communication together with some associated verification problems we are interested in. First we introduce some useful mathematical notations. We use $\mathbb{N}$ to represent the set of natural numbers, $\mathbb{N}_{>0}$ to represent $\mathbb{N}\setminus\{0\}$ , and for $n,m\in\mathbb{N}$ with $n\leq m$ , we denote by $[n,m]$ the set $\{n,n+1,\dots,m\}$ . For a finite set $E$ and a natural $n>0$ , the set $E^{n}$ represents the $n$ -dimensional vectors with values in $E$ and for $v\in E^{n}$ and $1\leq i\leq n$ , we use $v(i)$ to represent the $i$ -th value of $v$ . Furthermore, for such a vector $v$ , we denote by $||v||$ its dimension $n$ .

Networks of Processes using Broadcast Communication.

In the networks we consider, all the processes execute the same protocol, given by a finite state machine. The actions of this machine can either broadcast a message $a$ to the other processes (denoted by $!! a$ ) or receive a message $a$ (denoted by $? a$ ). For a finite alphabet of messages $\Sigma$ , we use the following notations: $!!\Sigma\overset{\mathrm{def}}{=}\{!!a\mid a\in\Sigma\}$ , $?\Sigma\overset{\mathrm{def}}{=}\{?a\mid a\in\Sigma\}$ and $\mathsf{Op}_{\Sigma}\overset{\mathrm{def}}{=}!!\Sigma\cup?\Sigma$ .

Definition 2.1.

A protocol $P$ is a tuple $(Q,\Sigma,q_{\textit{in}},T)$ where $Q$ is a finite set of states, $\Sigma$ is a finite set of messages, $q_{\textit{in}}\in Q$ is an initial state, and $T\subseteq Q\times\mathsf{Op}_{\Sigma}\times Q$ is a set of transitions.

For all $q\in Q$ , we define $R(q)$ as the set of messages that can be received from state $q$ , given by $\{a\in\Sigma\mid\exists q^{\prime}\in Q,(q,?a,q^{\prime})\in T\}$ . A protocol $P=(Q,\Sigma,q_{\textit{in}},T)$ is Wait-Only whenever for all $q\in Q$ , either $\{q^{\prime}\in Q\mid(q,\alpha,q^{\prime})\in T\text{ with }\alpha\in?\Sigma\}=\emptyset$ , or $\{q^{\prime}\in Q\mid(q,\alpha,q^{\prime})\in T\text{ with }\alpha\in!!\Sigma% \}=\emptyset$ . In a Wait-Only protocol, a state $q\in Q$ such that $\{q^{\prime}\in Q\mid(q,\alpha,q^{\prime})\in T\text{ with }\alpha\in?\Sigma\}\neq\emptyset$ is called a waiting state. A state that is not a waiting state is an action state. We denote by $Q_{W}$ the set of waiting states and by $Q_{A}$ the set of action states (hence $Q_{A}=Q\setminus Q_{W}$ ). Observe that if $q_{\textit{in}}\in Q_{W}$ , then no process is ever able to broadcast messages, for this reason we will always assume that $q_{\textit{in}}\in Q_{A}$ .

For $n\in\mathbb{N}_{>0}$ , an $n$ -process configuration of a protocol $P=(Q,\Sigma,q_{\textit{in}},T)$ is a vector $C\in Q^{n}$ where $C(e)$ represents the state of the $e$ -th process in $C$ for $1\leq e\leq n$ . The configuration is said to be initial whenever $C(e)=q_{\textit{in}}$ for all $1\leq e\leq n$ . The dimension $||C||$ hence characterizes the number of processes in $C$ . For a state $q\in Q$ , we use $C^{-1}(q)$ to represent the set of processes in state $q$ , formally $C^{-1}(q)=\{1\leq e\leq||C||\mid C(e)=q\}$ . For a subset $A\subseteq[1,||C||]$ of processes, we use $C(A)$ to identify the set of states of processes in $A$ , formally $C(A)=\{C(e)\mid e\in A\}$ . We let $\mathcal{C}$ [resp. $\mathcal{I}$ ] be the set of all configurations [resp. initial configurations] of $P$ .

We now define the broadcast network semantics associated to a protocol $P=(Q,\Sigma,q_{\textit{in}},T)$ . For configurations $C,C^{\prime}\in\mathcal{C}$ , transition $t=(q,!!a,q^{\prime})\in T$ and $e\in[1,||C||]$ , we write $C\xrightarrow{e,t}C^{\prime}$ whenever $||C||=||C^{\prime}||$ , $C(e)=q$ , $C^{\prime}(e)=q^{\prime}$ and, for all $e^{\prime}\in[1,||C||]\setminus\{e\}$ , either a reception occurs, i.e., $(C(e^{\prime}),?a,C^{\prime}(e^{\prime}))\in T$ , or the process cannot receive $a$ , in which case ( $a\not\in R(C(e^{\prime}))$ and $C(e^{\prime})=C^{\prime}(e^{\prime})$ ). Intuitively, the $e$ -th process of $C$ broadcasts a message $a$ , which is received by all processes able to receive it, while the other processes remain in their current state. We note $C\rightarrow C^{\prime}$ if there exists $e\in[1,||C||]$ and $t\in T$ such that $C\xrightarrow{e,t}C^{\prime}$ and use $\rightarrow^{\ast}$ [resp. $\rightarrow^{+}$ ] for the reflexive and transitive [resp. transitive] closure of $\rightarrow$ . A finite [resp. infinite] execution is a finite [resp. infinite] sequence of configurations $\rho=C_{0}\ldots C_{\ell}$ [resp. $\rho=C_{0}\ldots$ ] such that $C_{0}\in\mathcal{I}$ and $C_{i-1}\rightarrow C_{i}$ for all $0<i\leq\ell$ [resp. for all $i>0$ ]. Its length $|\rho|$ is equal to $\ell+1$ [resp. $\omega$ ]. We write $\Lambda$ [resp. $\Lambda_{\omega}$ ] for the set of finite [resp. infinite] executions. For an execution $\rho=C_{0}C_{1}\ldots\in\Lambda\cup\Lambda_{\omega}$ and $0\leq i<|\rho|$ , we use $\rho_{i}$ to denote $C_{i}$ , the $i$ -th configuration. We use $\textbf{\#proc}(\rho)$ to represent $||C_{0}||$ , the number of processes in the execution. For $0\leq i<j<|\rho|$ , we define $\rho_{i,j}\overset{\mathrm{def}}{=}\rho_{i}\ldots\rho_{j}$ . We also let $\rho_{\geq i}\overset{\mathrm{def}}{=}\rho_{i}\rho_{i+1}\ldots$ and $\rho_{\leq i}\overset{\mathrm{def}}{=}\rho_{0}\ldots\rho_{i}$ . For $e\in[1,\textbf{\#proc}(\rho)]$ , we denote by $\rho(e)$ the sequence of states $\rho_{0}(e)\rho_{1}(e)\ldots$ .

Figure 1: Example of a Wait-Only protocol

P

.

Example 2.2.

Figure 1 illustrates an example of a Wait-Only protocol. The waiting states are $q_{1},{q}_{2},{q}_{5},{q}_{6}$ , and $q_{7}$ , with $R({q}_{5})=\{b,c\}$ . Here is one of its execution with $3$ processes:

\begin{array}[]{l}(q_{\textit{in}},q_{\textit{in}},q_{\textit{in}})% \xrightarrow{1,(q_{\textit{in}},!!d,q_{1})}(q_{1},q_{\textit{in}},q_{\textit{% in}})\xrightarrow{2,(q_{\textit{in}},!!d,q_{1})}(q_{1},q_{1},q_{\textit{in}})% \xrightarrow{3,(q_{\textit{in}},!!a,q_{\textit{in}})}({q}_{5},{q}_{2},q_{% \textit{in}})\\ \xrightarrow{3,(q_{\textit{in}},!!c,q_{\textit{in}})}({q}_{3},{q}_{2},q_{% \textit{in}})\xrightarrow{3,(q_{\textit{in}},!!b,q_{7})}({q}_{3},{q}_{3},q_{7}% ).\end{array}

Verification Problems.

We investigate two verification problems over broadcast networks: the synchronization problem (Synchro) and the repeated coverability problem (RepCover). Synchro asks, given a protocol $P=(Q,\Sigma,q_{\textit{in}},T)$ and a state $q_{f}\in Q$ , whether there exist $C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ , and $C^{\prime}(e)=q_{f}$ for all $e\in[1,||C^{\prime}||]$ . RepCover asks, given a protocol $P=(Q,\Sigma,q_{\textit{in}},T)$ and a transition $t=(q,!!a,q^{\prime})\in T$ , whether there exist $\rho\in\Lambda_{\omega}$ and $e\in[1,\textbf{\#proc}(\rho)]$ , such that for all $i\in\mathbb{N}$ , there exists $j>i$ verifying $\rho_{j}\xrightarrow{e,t}\rho_{j+1}$ .

Theorem 2.3.

Synchro and RepCover are undecidable.

We give the proof of the undecidability of Synchro in [12], while the undecidability of RepCover was established in [8, Theorem 5.1]. In the remainder of the paper, we show that by restricting to Wait-Only protocols, one can regain decidability.

$\blacktriangleright$ Remark 2.4.

Throughout the remainder of this paper, we will consider protocols without self-loop broadcast transitions of the form $(q,!!a,q)$ . Such transitions can be transformed into two transitions $(q,!!a,p_{q})$ , $(p_{q},!!\$,q)$ where $p_{q}$ is a new state added to the set of states and $\$$ is a new message added to the alphabet. This transformation of the protocol is equivalent to the original one with respect to Synchro and RepCover.

Vector Addition System with States.

In the following, we will extensively rely on the model of Vector Addition Systems with States (VASS) which we introduce below. A VASS is a tuple $\mathcal{V}=(\textsf{Loc},\ell_{0},\mathsf{X},\Delta)$ where Loc is a finite set of locations, $\ell_{0}\in\textsf{Loc}$ is the initial location, $\mathsf{X}$ is a finite set of natural variables, called counters, and $\Delta\subseteq\textsf{Loc}\times\mathbb{Z}^{\mathsf{X}}\times\textsf{Loc}$ is a finite set of transitions. A configuration of $\mathcal{V}$ is a pair $(\ell,v)$ in $\textsf{Loc}\times\mathbb{N}^{\mathsf{X}}$ where $v$ provides a value for each counter. The initial configuration is $(\ell_{0},\mathbf{0})$ where $\mathbf{0}(\mathsf{x})=0$ for all $\mathsf{x}\in\mathsf{X}$ . Given two configurations $(\ell,v)$ , $(\ell^{\prime},v^{\prime})$ and a transition $(\ell,\delta,\ell^{\prime})\in\Delta$ , we write $(\ell,v)\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{\delta}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(\ell^{\prime},v^{% \prime})$ whenever $v^{\prime}(\mathsf{x})=v(\mathsf{x})+\delta(\mathsf{x})$ for all counters $\mathsf{x}\in\mathsf{X}$ . We simply use $(\ell,v)\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle% \sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(\ell^{\prime},v^{\prime})$ when there exists $(\ell,\delta,\ell^{\prime})\in\Delta$ such that $(\ell,v)\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{\delta}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(\ell^{\prime},v^{% \prime})$ . We denote $\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}$ for the transitive and reflexive closure of $\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}$ . An (infinite) execution (or run) of the VASS is a (infinite) sequence of configurations $(\ell_{0},v_{0}),(\ell_{1},v_{1}),\dots,(\ell_{n},v_{n})$ , starting with the initial configuration and such that $(\ell_{i},v_{i})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(\ell_{i+1},v_{i+1})$ for all $0\leq i<n$ .

Reach, the well-known reachability problem for VASS, is defined as follows: given a VASS $\mathcal{V}=(\textsf{Loc},\ell_{0},\mathsf{X},\Delta)$ and a location $\ell_{f}\in\textsf{Loc}$ , is there an execution from $(\ell_{0},\mathbf{0})$ to $(\ell_{f},\mathbf{0})$ ?

Theorem 2.5 (Membership [18], Hardness [3, 17]).

Reach is Ackermann-complete.

3 Solving Synchro for Wait-Only Protocols

To solve Synchro we show in this section that we can build a VASS that simulates the behavior of a broadcast network running a Wait-Only protocol. An intuitive way to proceed, inspired by the counting abstraction proposed for protocols communicating by pairwise rendez-vous communication [9], consists in having one counter per state of the protocol, that stores the number of processes that populate that state. Initially, the counter associated with the initial state can be incremented as much as one wants: this will determine the number of processes of the execution simulated in the VASS. Then, the simulation of broadcast messages $(q,!!a,q^{\prime})$ amounts to decrementing the counter associated to $q$ and increment the counter associated to $q^{\prime}$ . However, simulating receptions of the message (e.g. a transition $(p,?a,p^{\prime})$ ), requires to empty the counter associated to $p$ and transfer its value to the counter associated to $q^{\prime}$ . This transfer operation is not something that can be done in VASS unless the model is extended with special transfer transitions, leading to an undecidable reachability problem [21]. To circumvent this problem, we rely on two properties of Wait-Only protocols: (1) processes that occur to be in the same waiting state follow the same path of reception in the protocol, and end in the same action state (we show how to take care of potential non-determinism in the next section) and (2) processes in an action state cannot be influenced by the behaviour of other processes as they cannot receive any message. Thanks to property (1), instead of precisely tracking the number of processes in each waiting state, we only count the processes in a “waiting region” – a connected component of waiting states populated by processes that will all reach the same action state simultaneously. The waiting region allows us also to monitor when the processes go out from a waiting region to an action state. We will explain later how we use property (2) to handle the transfer of values of counters within the VASS semantics, and thus simulating processes leaving a waiting region.

For the rest of this section, we fix $P=(Q,\Sigma,q_{\textit{in}},T)$ a Wait-Only protocol (with $Q_{W}$ [resp. $Q_{A}$ ] the set of waiting states [resp. action states]) for which we assume w.l.o.g. the existence of an uncoverable state $q_{u}\in Q$ verifying $q\neq q_{u}$ and $q^{\prime}\neq q_{u}$ for all $(q,\alpha,q^{\prime})\in T$ and $q_{u}\neq q_{\textit{in}}$ . Furthermore, we consider a final waiting state $q_{f}\in Q_{W}$ . To ease the reading, we assume in this section that the final state $q_{f}$ is a waiting state, but our construction could be adapted to the case where $q_{f}$ is an action state. Moreover, we show in the next section that Synchro in this latter case is easier to solve.

3.1 Preliminary properties

We present here properties satisfied by Wait-Only protocols, which we will rely on for our construction. We first show with Lemma 3.1 that if, during an execution, two processes fulfill two conditions: ( $i$ ) they are on the same waiting state $q_{w}$ , and ( $i i$ ) the next action state they reach (not necessarily at the same time) is the same (namely $q_{a}$ ), then one can build an execution where they both follow the same path between $q_{w}$ and $q_{a}$ . This is trivial for deterministic protocols (where for all $q\in Q$ and $\alpha\in\mathsf{Op}_{\Sigma}$ , there is at most one transition of the form $(q,\alpha,q^{\prime})\in T$ ) and is also true for non-deterministic protocols.

For an execution $\rho\in\Lambda\cup\Lambda_{\omega}$ of $P$ , an index $0\leq j<|\rho|$ , a waiting state $q\in Q_{W}$ and a process number $e\in[1,\textbf{\#proc}(\rho)]$ such that $\rho_{j}(e)=q$ , we define $\textbf{na-index}(\rho,j,e)=\min\{k\mid j\leq k\leq|\rho|\textrm{ and }\rho_{k% }(e)\in Q_{A}\}$ , i.e. the first moment after $\rho_{j}$ where the process $e$ reaches an action state (if such moment does not exist, it is set to $|\rho|$ ). We note $\textbf{na-state}(\rho,j,e)\overset{\textrm{def}}{=}\rho_{\textbf{na-index}(% \rho,j,e)}(e)$ the next action state for process $e$ from $\rho_{j}$ if $\textbf{na-index}(\rho,j,e)\neq|\rho|$ and otherwise we take the convention that $\textbf{na-state}(\rho,j,e)$ is equal to $q_{u}$ , the uncoverable state of the protocol $P$ . Finally, we let $\textbf{na}(\rho,j,e)=(\textbf{na-state}(\rho,j,e),\textbf{na-index}(\rho,j,e))$ .

Lemma 3.1.

Let $\rho\in\Lambda\cup\Lambda_{\omega}$ be an execution of $P$ . If there exist $e_{1},e_{2}\in[1,\textbf{\#proc}(\rho)]$ and $0\leq j<|\rho|$ such that (i) $\rho_{j}(e_{1})=\rho_{j}(e_{2})\in Q_{W}$ , (ii) $\textbf{na}(\rho,j,e_{1})=(q,j_{1})$ , and (iii) $\textbf{na}(\rho,j,e_{2})=(q,j_{2})$ with $j_{1}\leq j_{2}<|\rho|$ , then there exists an execution $\rho^{\prime}$ of the form $\rho_{\leq j}\rho^{\prime}_{j+1}\ldots\rho^{\prime}_{j_{2}}\rho_{\geq j_{2}+1}$ such that $\rho^{\prime}_{k}(e_{1})=\rho^{\prime}_{k}(e_{2})=\rho_{k}(e_{1})$ for all $j+1\leq k\leq j_{1}$ , and $\rho^{\prime}_{k}(e_{1})=\rho_{k}(e_{1})$ and $\rho^{\prime}_{k}(e_{2})=q$ for all $j_{1}<k\leq j_{2}$ . In particular $\textbf{na}(\rho^{\prime},j,e_{1})=\textbf{na}(\rho^{\prime},j,e_{2})=(q,j_{1})$ .

Example 3.2.

Consider the protocol $P$ in Figure 1 and the execution $\rho$ of Example 2.2. We have $\rho_{2}(1)=\rho_{2}(2)=q_{1}$ and $\textbf{na}(\rho,2,1)=(q_{3},4)$ and $\textbf{na}(\rho,2,2)=(q_{3},5)$ . Applying Lemma 3.1, we build: $\rho^{\prime}=(q_{\textit{in}},q_{\textit{in}},q_{\textit{in}})\rightarrow(q_{% 1},q_{\textit{in}},q_{\textit{in}})\rightarrow(q_{1},q_{1},q_{\textit{in}})% \rightarrow(q_{5},q_{5},q_{\textit{in}})\rightarrow(q_{3},q_{3},q_{\textit{in}% })\rightarrow(q_{3},q_{3},q_{7})$ where process $1$ and process $2$ follow the same path between $q_{1}$ and $q_{3}$ . However, consider the following events from $(q_{1},q_{1},q_{\textit{in}})$ : $(q_{1},q_{1},q_{\textit{in}})\rightarrow(q_{2},q_{5},q_{\textit{in}})% \rightarrow(q_{3},q_{6},q_{7})\rightarrow(q_{4},q_{4},q_{4})$ , here we cannot apply the lemma as from $q_{1}$ , processes $1$ and $2$ reach two different next action states ( $q_{3}$ and $q_{4}$ ).

The above lemma enables us to focus on a specific subset of executions for Synchro, which we refer to as well-formed. In these executions, at any moment, two processes in the same waiting state and with the same next action state, follow the same path of receptions. Formally, an execution $\rho$ of a protocol $P$ is well-formed iff for all $0\leq i<|\rho|$ , for all $e_{1},e_{2}\in[1,\textbf{\#proc}(\rho)]$ such that $\rho_{i}(e_{1})=\rho_{i}(e_{2})\in Q_{W}$ and $\textbf{na-state}(\rho,i,e_{1})=\textbf{na-state}(\rho,i,e_{2})=q$ , it holds that $\rho_{k}(e_{1})=\rho_{k}(e_{2})$ for all $i\leq k\leq\textbf{na-index}(\rho,i,e_{1})$ . From Lemma 3.1, we immediately get:

Corollary 3.3.

There exists an execution $\rho=C_{0}\ldots C_{n}$ such that $C_{n}(e)=q_{f}$ for all $e\in[1,\textbf{\#proc}(\rho)]$ iff there exists a well-formed execution from $C_{0}$ to $C_{n}$ .

We finally provide a result which will allow us to bound the size of the VASS that we will build from the given Wait-Only protocol. Given an execution $\rho\in\Lambda\cup\Lambda_{\omega}$ of $P$ , an index $0\leq j<|\rho|$ and an action state $q_{a}\in Q_{A}$ , we define $\textbf{na-index-set}(\rho,j,q_{a})$ as the set of indices where processes in a waiting state at $\rho_{j}$ will reach $q_{a}$ , if it is their next action state: $\textbf{na-index-set}(\rho,j,q_{a})\overset{\textrm{def}}{=}\{i\mid\textrm{ % there exists\nobreakspace}e\in[1,\textbf{\#proc}(\rho)]\text{ s.t. }\rho_{j}(e% )\in Q_{W}\text{ and }\textbf{na}(\rho,j,e)=(q_{a},i)\}$ .

Lemma 3.4.

For all well-formed executions $\rho$ , for all $0\leq j<|\rho|$ , and for all $q_{a}\in Q_{A}$ , we have $|\textbf{na-index-set}(\rho,j,q_{a})|\leq|Q_{W}|$ .

Proof.

If we have $|\textbf{na-index-set}(\rho,j,q_{a})|>|Q_{W}|$ , by pigeon hole principle there exist $e_{1},e_{2}\in[1,\textbf{\#proc}(\rho)]$ such that $\rho_{j}(e_{1})=\rho_{j}(e_{2})\in Q_{W}$ and such that $\textbf{na}(\rho,j,e_{1})=(q_{a},i_{1})$ and $\textbf{na}(\rho,j,e_{2})=(q_{a},i_{2})$ with $i_{1}<i_{2}$ . Consequently $\rho_{i_{1}}(e_{1})=q_{a}\in Q_{A}$ and $\rho_{i_{1}}(e_{2})\in Q_{W}$ hence $\rho_{i_{1}}(e_{1})\neq\rho_{i_{1}}(e_{2})$ , which contradicts the definition of well-formedness. $\hfill\blacktriangleleft$

3.2 Building the VASS that Simulates a Broadcast Network

Summaries.

We present here the formal tool we use to represent processes in waiting states. We begin by introducing some notations. A print pr is a set of waiting states. Given a non empty subset of states $A=\{q_{1},\dots,q_{n}\}\subseteq Q$ , we define a configuration $\overset{\bullet}{A}\in Q^{n}$ such that $\overset{\bullet}{A}(e)=q_{e}$ for all $e\in[1,n]$ . When $A=\{q\}$ , we write $\overset{\bullet}{q}\in Q^{1}$ instead of $\overset{\bullet}{\{q\}}$ . Conversely, given a configuration $C$ , we define $\textbf{set}(C)=\{q\in Q\mid C^{-1}(q)\neq\emptyset\}$ . For two configurations $C\in Q^{n}$ and $C^{\prime}\in Q^{m}$ , we let $C\oplus C^{\prime}$ be the configuration $C^{\prime\prime}\in Q^{n+m}$ defined by: $C^{\prime\prime}(e)=C(e)$ if $1\leq e\leq n$ and $C^{\prime\prime}(e)=C^{\prime}(e-n)$ if $n+1\leq e\leq m+n$ . A summary $S$ is a tuple $(\textsf{pr},q_{a},k)$ such that $\textsf{pr}\subseteq Q_{W}$ is a print, $q_{a}\in Q_{A}$ is an exit state, and $k\in[1,|Q_{W}|+1]$ is an identifier. The label of $S$ is $\textbf{lab}(S)=(q_{a},k)$ and we denote its print by $\mathbf{print}(S)$ . Finally, we define a special summary Done.

In our construction, each process in a waiting state is associated with a summary while processes in action states are handled by the counters of the VASS. Intuitively, a summary $(\textsf{pr},q_{a},k)$ represents a set of processes lying in the set $\textsf{pr}\subseteq Q_{W}$ that will reach the same next action state $q_{a}$ simultaneously (this restriction is justified by Lemma 3.1). Since the set of waiting states pr evolve during the simulation, each summary must be uniquely identified. To achieve this, we use an integer $k\in[1,|Q_{W}|+1]$ . Hence each summary is identified with the pair $(q_{a},k)$ . We do not need more than $|Q_{W}|+1$ different identifiers, because when a process enters a new summary (i.e it arrives in a waiting state $q_{w}$ from an action state), aiming for next action state $q_{a}$ , it either joins an existing summary with exit state $q_{a}$ , or create a new one. In the latter case, well-formed executions ensure that no existing summary $S=(\textsf{pr},q_{a},k)$ with exit state $q_{a}$ is such that $q_{w}\in\textsf{pr}$ . Otherwise two processes would be in the same state $q_{w}$ , aiming for the same action state, but at different moments, contradicting Lemma 3.1. Note that we need $|Q_{W}|+1$ different identifers, and not $|Q_{W}|$ for technical reasons. Finally, the special summary Done is used to indicate when the processes described by a summary reach the exit action state.

We now describe how summaries evolve with the sequence of transitions. Let $S=(\textsf{pr},q_{a},k)$ and $S^{\prime}=(\textsf{pr}^{\prime},q_{a},k)$ be two summaries (with the same exit state and identifier) and $t=(q,!!b,q^{\prime})\in T$ such that there exists a configuration $C^{\prime}$ verifying $\overset{\bullet}{{q}}\oplus\overset{\bullet}{\textsf{pr}}\xrightarrow{1,t}% \overset{\bullet}{{q^{\prime}}}\oplus C^{\prime}$ . We then write $S\xRightarrow{t}S^{\prime}$ whenever $\textbf{set}(C^{\prime})=\textsf{pr}^{\prime}\subseteq Q_{W}$ . This represents the evolution of a summary upon reception of message $b$ , when the processes all stay in waiting states, and no new process joins the “waiting region” of the given summary. We write $S\xRightarrow{t,+q^{\prime}}S^{\prime}$ whenever $q^{\prime}\in Q_{W}$ and $\textbf{set}(C^{\prime})\cup\{q^{\prime}\}=\textsf{pr}^{\prime}\subseteq Q_{W}$ . In that latter case, the process responsible for the transition $t$ joins the “waiting region” represented by $S$ . This typically occurs when the process’s next action state is $q_{a}$ , and it reaches $q_{a}$ simultaneously with the processes described by $S$ . Finally, we use $S\xRightarrow{t}\texttt{Done}$ whenever $\textbf{set}(C^{\prime})=\{q_{a}\}$ . This represents the evolution (and disappearance) of $S$ when all the processes reach $q_{a}$ (they all reach it simultaneously).

Example 3.5.

Returning to the protocol $P$ of Figure 1, consider the summary $S_{0}=(\{q_{1}\},{q}_{3},1)$ . Observe that $S_{0}\xRightarrow{(q_{\textit{in}},!!a,q_{\textit{in}})}(\{{q}_{2}\},{q}_{3},1)$ and $S_{0}\xRightarrow{(q_{\textit{in}},!!a,q_{\textit{in}})}(\{{q}_{5}\},{q}_{3},1)$ . However, by definition, we do not have $S_{0}\xRightarrow{(q_{\textit{in}},!!a,q_{\textit{in}})}(\{{q}_{5},{q}_{2}\},{% q}_{3},1)$ . Indeed, processes summarized in $S_{0}$ are forced to all go either on ${q}_{2}$ or on ${q}_{5}$ upon receiving $a$ : thanks to Corollary 3.3, we consider only well-formed executions, where all processes summarized in $S_{0}$ choose the same next state. Additionnaly, we have $(\{{q}_{2}\},{q}_{3},1)\xRightarrow{(q_{\textit{in}},!!b,q_{7})}\texttt{Done}$ and $(\{q_{1}\},{q}_{4},1)\xRightarrow{(q_{\textit{in}},!!a,q_{\textit{in}})}(\{{q}% _{5}\},{q}_{4},1)\xRightarrow{(q_{\textit{in}},!!b,q_{7}),+q_{7}}(\{{q}_{6},q_% {7}\},{q}_{4},1)\xRightarrow{(q_{\textit{in}},!!d,q_{1})}\texttt{Done}$ . However, note that we do not have $(\{{q}_{2}\},{q}_{4},1)\xRightarrow{(q_{\textit{in}},!!b,q_{7})}\texttt{Done}$ , since the action state ${q}_{3}$ reached from ${q}_{2}$ upon receiving $b$ is not the exit state ${q}_{4}$ .

Definition of the VASS.

We now explain how we use the summaries in the VASS simulating the executions in the network. First we say that a set $\SS$ of summaries is coherent if for all distinct pairs $(\textsf{pr}_{1},q_{1},k_{1}),(\textsf{pr}_{2},{q}_{5},k_{2})\in\SS$ such that $q_{1}={q}_{5}$ , we have $k_{1}\neq k_{2}$ and $\textsf{pr}_{1}\cap\textsf{pr}_{2}=\emptyset$ . We denote by CoSets the set of coherent sets of summaries. For a set of summaries $\SS$ we let $\textbf{lab}(\SS)=\{\textbf{lab}(S)\mid S\in\SS\}$ . Observe that, when $\SS$ is coherent, for a label $(q,k)\in\textbf{lab}(\SS)$ , there is a unique $S\in\SS$ such that $\textbf{lab}(S)=(q,k)$ .

We define the VASS $\mathcal{V}_{P}$ simulating the protocol $P$ as follows: $\mathcal{V}_{P}=(\textsf{Loc},s_{0},\mathsf{X},\Delta)$ , where $\textsf{Loc}=\textsf{CoSets}\cup\{s_{0}\}\cup\{s_{f}\}$ , the set of counters is $\mathsf{X}=\{\mathsf{x}_{q}\mid q\in Q_{A}\}\cup\{\mathsf{x}_{{(q,k)}}\mid q% \in Q_{A},k\in[1,|Q_{W}|+1]\}$ , and the set of transitions $\Delta=\Delta_{0}\cup(\bigcup_{t\in T}\Delta_{t})\cup\Delta_{e}$ , is defined as follows:

$\blacksquare$
$\Delta_{0}$ contains exactly the following transitions:
- –
  
  $(s_{0},\delta_{0},s_{0})$ where $\delta_{0}(\mathsf{x}_{q_{\textit{in}}})=1$ and $\delta_{0}(\mathsf{x})=0$ for all other counters;
- –
  
  $(s_{0},\textbf{0},\emptyset)$ where 0 is the null vector (note that the empty set is coherent);
- –
  
  $(\{S_{f}\},\textbf{0},s_{f})\in\Delta$ where $S_{f}=(\{q_{f}\},q_{u},1)$ ;
- –
  
  $(s_{f},\delta_{f},s_{f})\in\Delta$ where $\delta_{f}(\mathsf{x}_{(q_{u},1)})=-1$ and $\delta_{f}(\mathsf{x})=0$ for all other counters.
$\blacksquare$
For $t=(q,!!a,q^{\prime})\in T$ , we have $(\SS,\delta,\SS^{\prime})\in\Delta_{t}$ iff one of the following conditions holds:
1. a.
  
  $q^{\prime}\in Q_{A}$ and $\SS=\{S_{1},\dots,S_{k}\}$ . Then, for all $1\leq i\leq k$ , there exists $S^{\prime}_{i}$ such that $S_{i}\xRightarrow{t}S^{\prime}_{i}$ and $\SS^{\prime}=\{S^{\prime}_{i}\mid 1\leq i\leq k\}\setminus\{\texttt{Done}\}$ . Moreover, $\delta(\mathsf{x}_{q})=-1$ , $\delta(\mathsf{x}_{q^{\prime}})=1$ and $\delta(\mathsf{x})=0$ for all $\mathsf{x}\in\mathsf{X}\setminus\{\mathsf{x}_{q},\mathsf{x}_{q^{\prime}}\}$ . Here we simply update the sets of states populated by processes in waiting states after the transition $t$ . Some summaries may have disappeared from $\SS$ if the processes represented by this summary have reached their exit action state when receiving $a$ . For now, we only modify the counters associated to the states $q$ and $q^{\prime}$ . Note that this is well-defined, since we assume in Remark 2.4 that there is no self-loop of the form $(q,!!a,q)$ .
2. b.
  
  $q^{\prime}\in Q_{W}$ , $\SS=\{S_{1},\dots,S_{k}\}$ , and there exists $1\leq i\leq k$ and $S^{\prime}_{i}$ such that $S_{i}\xRightarrow{t,+q^{\prime}}S^{\prime}_{i}$ . For all $j\neq i$ , there exists $S^{\prime}_{j}$ such that $S_{j}\xRightarrow{t}S^{\prime}_{j}$ . Then $\SS^{\prime}=\{S^{\prime}_{j}\mid 1\leq j\leq k\}\setminus\{\texttt{Done}\}$ . Moreover, $\delta(\mathsf{x}_{q})=-1$ , $\delta(\mathsf{x}_{\textbf{lab}(S_{i})})=1$ and $\delta(\mathsf{x})=0$ for all $\mathsf{x}\in\mathsf{X}\setminus\{\mathsf{x}_{q},\mathsf{x}_{{\textbf{lab}(S_{% i})}}\}$ . In that case, the process having performed the transition joins an existing summary $S_{i}$ . We have then modified accordingly the counters associated to $q$ and to the appropriate summary.
3. c.
  
  $q^{\prime}\in Q_{W}$ and $\SS=\{S_{1},\dots,S_{k}\}$ . For all $1\leq j\leq k$ , there exists $S^{\prime}_{j}$ such that $S_{j}\xRightarrow{t}S^{\prime}_{j}$ . Then $\SS^{\prime}=(\{S^{\prime}_{1},\dots,S^{\prime}_{k}\}\setminus\{\texttt{Done}% \})\cup\{(\{q^{\prime}\},q_{a},k)\}$ for some $q_{a}\in Q_{A}$ and $k\in[1,|Q_{W}|+1]$ such that $(q_{a},k)\not\in\textbf{lab}(\SS)$ . Moreover, $\delta(\mathsf{x}_{q})=-1$ , $\delta(\mathsf{x}_{(q_{a},k)})=1$ , and $\delta(\mathsf{x})=0$ for all $\mathsf{x}\in\mathsf{X}\setminus\{\mathsf{x}_{q},\mathsf{x}_{(q_{a},k)}\}$ . This case happens when the process having sent the message $a$ reaches a waiting state, and its expected next action pair (index and state) does not correspond to any existing summary. In that case, it joins a new summary, the counter associated to the state $q$ is decremented and the counter of this new summary is incremented.
$\blacksquare$

Finally, $\Delta_{e}$ allows to empty the counters associated to summaries that have disappeared from the set of locations. It is defined as the set of transitions $(\SS,\delta,\SS^{\prime})$ such that: $\SS=\SS^{\prime}$ and there exists $(q,k)\not\in\textbf{lab}(\SS)$ with $\delta(\mathsf{x}_{q})=+1$ and $\delta(\mathsf{x}_{(q,k)})=-1$ and for all other counters, $\delta(\mathsf{x})=0$ .

Transitions from $\Delta_{e}$ allow the transfer of counter values from summaries that have disappeared to the counter of their exit action state. This transfer is not immediate, as it is done through iterative decrements and increments of counters. In particular, it is possible for the execution of the VASS to continue without the counter of a disappeared summary being fully transfered. The processes represented by the counter of a disappeared summary behave in the same way as processes in the exit action state that do not take any action. These counters can be emptied later, but always from a location from where no summary with the same label exists. This ensures that there is no ambiguity between processes in a waiting region and those on an action state that have not yet been transferred to the appropriate counter.

Figure 2: The structure of the VASS

\mathcal{V}

.

Figure 3: One successor of location

\{(\{{q}_{2}\},{q}_{3},1),(\{q_{1}\},{q}_{3},2),(\{q_{1},{q}_{5}\},{q}_{4},1)\}

(left location) after the broadcast transition

(q_{\textit{in}},!!b,q_{7})

.

Figure 4: Three successors of location

\{(\{{q}_{2}\},{q}_{3},1)\}

(top left location) after the broadcast transition

(q_{\textit{in}},!!d,q_{1})

.

Example 3.6.

Figures 4, 4, and 4 illustrate the VASS $\mathcal{V}_{P}$ built for the protocol $P$ from Figure 1. Figure 4 shows its overall structure: any run reaching $(s_{f},\mathbf{0})$ starts by incrementing the counter of the initial state and ends by decrementing the counter of the summary $({q_{f}},q_{u},1)$ . Here, $q_{u}$ is an artificial, unreachable state used to ensure that the counted processes must end in $q_{f}$ (since they cannot be in $q_{u}$ ). Figure 4 illustrates how message receptions and summary creations are handled. The top-left location contains a single summary $(\{q_{2}\},q_{3},1)$ , representing configurations where all processes on $Q_{W}$ are in $q_{2}$ , all progressing to $q_{3}$ . After the broadcast $(q_{\textit{in}},!!d,q_{1})$ , three behaviors may follow. In the first case (right), the sender creates a new summary $(\{q_{1}\},q_{4},1)$ (pink). In the second (diagonal), it creates another new summary $(\{q_{1}\},q_{3},2)$ (orange), indicating a different arrival time at $q_{3}$ . In the third (below), it joins an existing summary, and $q_{1}$ is added to the print. Well-formed executions restrict the number of summaries with the same exit state, as there are at most $|Q_{W}|$ distinct moments where processes can reach a given action state (Lemma 3.4). Figure 4 illustrates summary deletion. The transition $(q_{\textit{in}},!!b,q_{7})$ causes the sender to join the pink summary (bottom one), incrementing its counter. Processes in the green summary ( $\{{q}_{2}\},{q}_{3},1$ ) receive the message via $({q}_{2},?b,{q}_{3})$ , reaching their exit state ${q}_{3}$ . This summary is deleted in the next location. From there, value of $\mathsf{x}_{({q}_{3},1)}$ is transferred to the counter $\mathsf{x}_{{q}_{3}}$ with the loop transition. If it is not taken enough times, $\mathsf{x}_{({q}_{3},1)}$ may remain non-zero. This does not affect correctness: $\mathsf{x}_{({q}_{3},1)}$ will be decremented eventually from a state in which there is no summary labeled with $({q}_{3},1)$ . Not decrementing soon enough only delay the moment the corresponding processes will move from the action state ${q}_{3}$ .

$\blacktriangleright$ Remark 3.7.

In the sequel of this paper, the size of $\mathcal{V}_{P}$ will be of interest to us. Hence, observe that $|\textsf{Loc}|=|\textsf{CoSets}|+3\leq 2^{|Q_{A}|\times(|Q_{W}|+1)\times 2^{|Q% _{W}|}}+3$ (as one summary is composed of a state in $Q_{A}$ , one label in $[1,|Q_{W}|+1]$ and one set of waiting states), and $|\mathsf{X}|=|Q_{A}|+|Q_{A}|\times(|Q_{W}|+1)$ .

Soundness of the construction.

We show now that if there exists a run in the VASS $\mathcal{V}_{P}$ from $(s_{0},\mathbf{0})$ to $(s_{f},\mathbf{0})$ , then in the network built from $P$ , there exist $C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ and $C^{\prime}(e)=q_{f}$ for all $e\in[1,||C^{\prime}||]$ .

We say that a configuration $(\ell,v)$ of $\mathcal{V}_{P}$ is an S-configuration if $\ell=\SS$ for some $\SS\in\textsf{CoSets}$ . The implementation of an S-configuration $\lambda=(\SS,v)$ is the set of network configurations $\llbracket\lambda\rrbracket\subseteq\mathcal{C}$ defined as follows: $C\in\llbracket\lambda\rrbracket$ if and only if there exists a function $f:[1,||C||]\rightarrow\mathsf{X}$ such that $|f^{-1}(\mathsf{x})|=v(\mathsf{x})$ for all $\mathsf{x}\in\mathsf{X}$ , and

CondImpl1

for all $\mathsf{x}_{q}\in\mathsf{X}$ with $q\in Q_{A}$ , we have $C(e)=q$ for all $e\in f^{-1}(\mathsf{x}_{q})$ ,;
CondImpl2

for all $\mathsf{x}_{(q,k)}\in\mathsf{X}$ , if there exists $(\textsf{pr},q,k)\in\SS$ for some $\textsf{pr}\subseteq Q_{W}$ , then $C(e)\in\textsf{pr}\cup\{q\}$ for all $e\in f^{-1}(\mathsf{x}_{{q,k}})$ ;
CondImpl3

for all $\mathsf{x}_{(q,k)}\in\mathsf{X}$ , if $(q,k)\notin\textbf{lab}(\SS)$ , then $C(e)=q$ for all $e\in f^{-1}(\mathsf{x}_{{q,k}})$ .

In an implementation of $\lambda$ , the processes populate states according to the values of the counters. All processes associated with a counter $\mathsf{x}_{q}$ of an action state will populate this exact state (CondImpl1). However, processes associated with a counter $\mathsf{x}_{(q,k)}$ of a summary do not necessarily populate waiting states. This occurs when the label $(q,k)$ does not appear in $\SS$ while the associated counter remains strictly positive. Such a situation arises when a summary has been previously deleted, but its counter has not been emptied. Since all associated processes have already reached the exit action state, the processes associated to the corresponding counter have to populate this active state (CondImpl3). If the summary with label $(q,k)$ is active (i.e. its label appears in $\SS$ ), the processes associated with $\mathsf{x}_{(q,k)}$ will be in the corresponding waiting region, or in the exit action state (CondImpl2). This may seem contradictory, as all processes are supposed to reach their exit state simultaneously. However, the processes already on the exit action state are “old” processes, that remained after a previous deletion of this summary (cf. CondImpl3). These processes will be allowed to send messages only when they are identified with the counter of the active state, meaning when the corresponding transition in $\Delta_{e}$ will be taken. The next lemma allows to build an execution of the protocol $P$ from an execution of the VASS $\mathcal{V}_{P}$ .

Lemma 3.8.

Let $\lambda,\lambda^{\prime}$ be two S-configurations of $\mathcal{V}_{P}$ and $C\in\llbracket\lambda\rrbracket$ . If $\lambda\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{\delta}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}\lambda^{\prime}$ in $\mathcal{V}_{P}$ then there exists $C^{\prime}\in\llbracket\lambda^{\prime}\rrbracket$ such that $C\rightarrow^{\ast}C^{\prime}$ for $P$ .

Sketch of Proof..

Assume $\lambda=(\SS,v)$ and $\lambda^{\prime}=(\SS^{\prime},v^{\prime})$ . Then either $(\SS,\delta,\SS^{\prime})\in\Delta_{e}$ or $(\SS,\delta,\SS^{\prime})\in\Delta_{t}$ for some $t\in T$ . In the first case, we show that if $C\in\llbracket\lambda\rrbracket$ , then $C\in\llbracket\lambda^{\prime}\rrbracket$ . Otherwise, let $t=(q,!!a,q^{\prime})$ , there is a process $e$ such that $C(e)=q$ . The transition $\delta$ in the VASS makes all the summaries and counters evolve according to the reception of the message $a$ . According to the different cases a, b or c, one can build a configuration $C^{\prime}\in\llbracket\lambda^{\prime}\rrbracket$ such that $C\rightarrow C^{\prime}$ . $\hfill\blacktriangleleft$

Lemma 3.9.

If $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},\mathbf{% 0})$ in $\mathcal{V}_{P}$ , then there exist $C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ and $C^{\prime}(e)=q_{f}$ for all $e\in[1,||C^{\prime}||]$ .

Proof.

From the definition of $\mathcal{V}_{P}$ , any run from $(s_{0},\mathbf{0})$ to $(s_{f},\mathbf{0})$ is of the form $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\emptyset,v_{% init})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle% \sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\{S_{f}\},v_{f})\mathbin{% \stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{% 0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},\mathbf{0})$ where $v_{init}(\mathsf{x}_{q_{\textit{in}}})=n$ for some $n\in\mathbb{N}$ and $v_{init}(\mathsf{x})=0$ for all $\mathsf{x}\in\mathsf{X}\setminus\{\mathsf{x}_{q_{\textit{in}}}\}$ , whereas $v_{f}(\mathsf{x}_{(q_{u},1)})=v_{init}(\mathsf{x}_{q_{\textit{in}}})=n$ and $v_{f}(\mathsf{x})=0$ for all $\mathsf{x}\in\mathsf{X}\setminus\{\mathsf{x}_{(q_{u},1)}\}$ . Define $C$ as the initial configuration in $\mathcal{I}$ with $n$ processes (i.e. $||C||=n$ ). Trivially, $C\in\llbracket(\emptyset,v_{init})\rrbracket$ and with Lemma 3.8 and a simple induction, we get that there exists $C^{\prime}\in\llbracket(\{S_{f}\},v_{f})\rrbracket$ such that $C\rightarrow^{\ast}C^{\prime}$ . Observe that by definition of $v_{f}$ , and since $C^{\prime}\in\llbracket(\{S_{f}\},v_{f})\rrbracket$ , there exists $f:[1,n]\rightarrow\mathsf{X}$ such that $f^{-1}(\mathsf{x}_{(q_{u},1)})=[1,n]$ . Using CondImpl2, we have $C^{\prime}(e)\in\{q_{f},q_{u}\}$ for all $e\in[1,n]$ with $n=||C^{\prime}||$ . Since $q_{u}$ is unreachable by construction, we deduce that $C^{\prime}(e)=q_{f}$ for all $e\in[1,||C^{\prime}||]$ . $\hfill\blacktriangleleft$

Completeness of the construction.

Let us first introduce some new definitions. Given a well-formed execution $\rho\in\Lambda\cup\Lambda_{\omega}$ , two indices $0\leq i<j<|\rho|$ and an action state $q_{a}\in Q_{A}$ , we define $E^{\rho,i}_{q_{a},j}$ , the set of processes in waiting states in $\rho_{i}$ , and whose next action state is $q_{a}$ , reached at $\rho_{j}$ . Formally, $E^{\rho,i}_{q_{a},j}=\big{\{}e\in[1,\textbf{\#proc}(\rho)]\mid\rho_{i}(e)\in Q% _{W}\textrm{ and }\textbf{na}(\rho,i,e)=(q_{a},j)\big{\}}$ . Furthermore, an S-configuration $\lambda=(\SS,v)$ is a representative of the configuration $\rho_{i}$ in $\rho$ iff the following conditions are respected:

CondRepr1

for all $q\in Q_{A}$ , $v(\mathsf{x}_{q})=|\rho_{i}^{-1}(q)|$ , and

for all $q_{a}\in Q_{A}$ , there is an injective function $r_{q_{a}}:\textbf{na-index-set}(\rho,i,q_{a})\rightarrow[1,|Q_{W}|+1]$ s.t.:

CondRepr2

$\SS=\{(\rho_{i}(E^{\rho,i}_{q_{a},j}),q_{a},r_{q_{a}}(j))\mid q_{a}\in Q_{A},j% \in\textbf{na-index-set}(\rho,i,q_{a})\}$
CondRepr3

for all $q_{a}\in Q_{A}$ , we have $v(\mathsf{x}_{(q_{a},r_{q_{a}}(j))})=|E^{\rho,i}_{q_{a},j}|$ for all
$j\in\textbf{na-index-set}(\rho,i,q_{a})$ and $v(\mathsf{x}_{(q_{a},k)})=0$ for all $k\notin r_{q_{a}}(\textbf{na-index-set}(\rho,i,q_{a}))$ .

In a representative of the configuration $\rho_{i}$ , the counters faithfully count the number of processes on active states (CondRepr1), and on waiting regions. The set $E_{q_{a},j}^{\rho,i}$ gathers exactly the set of processes that populate a same waiting region in a representative of $\rho_{i}$ in $\rho$ : they all reach the same next action state $q_{a}$ at the same instant $j$ . The set $\textbf{na-index-set}(\rho,i,q_{a})$ being bounded by $|Q_{W}|$ (cf. Lemma 3.4), we can associate with each of these indices a unique identifier, given by the injective function $r_{q_{a}}$ . We use a spare identifier for technical reasons, to handle more easily situations when $|Q_{W}|$ summaries exist in the location of the VASS, and a new summary is created while one of the previous summaries is deleted at the next step. Then, CondRepr2 and CondRepr3 require that the counters corresponding to the summaries and the summaries themselves reflect faithfully the situation in the configuration $\rho_{i}$ with respect to $\rho$ . Observe that such a representative is tightly linked to the simulated execution, since we need to know the future behavior of the different processes to determine the different summaries. Finally, if we let $\mathbf{repr}(\rho,i)$ be the set of all $S$ -configurations that are representatives of $\rho_{i}$ in $\rho$ , we establish the following result before proving the main lemma of this subsection (Lemma 3.11).

Lemma 3.10.

Let $\rho$ be a well-formed execution, and $0\leq i<|\rho|$ . For all $\lambda_{i}\in\mathbf{repr}(\rho,i)$ , there exists $\lambda_{i+1}\in\mathbf{repr}(\rho,i+1)$ such that $\lambda_{i}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}\lambda_{i+1}$ in $\mathcal{V}_{P}$ .

Sketch of Proof..

From an S-configuration $\lambda_{i}=(\SS_{i},v_{i})$ in $\mathbf{repr}(\rho,i)$ , we can compute the effect on $\SS_{i}$ of the transition $t=(q,!!a,q^{\prime})$ taken in $\rho$ to go from $\rho_{i}$ to $\rho_{i+1}$ , and find a matching transition $(\SS_{i},\delta,\SS_{i+1})\in\Delta_{t}$ (according to whether $q^{\prime}$ is a waiting state or not, and in the latter case, whether it joins an existing summary or a new one, depending of the execution $\rho$ ). We then obtain a new configuration $\lambda^{\prime}=(\SS_{i+1},v^{\prime})$ such that $\lambda_{i}\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{\delta}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}\lambda^{\prime}$ . Note that $\lambda^{\prime}$ is not necessarily in $\mathbf{repr}(\rho,i+1)$ : if some summaries have been deleted between $\lambda_{i}$ and $\lambda^{\prime}$ , the transition $(\SS_{i},\delta,\SS_{i+1})$ in $\mathcal{V}_{P}$ has not updated the corresponding counters. Hence we need to apply transitions from $\Delta_{e}$ to empty counters corresponding to deleted summaries and accordingly increase corresponding counters on matching action states to obtain $\lambda_{i+1}=(\SS_{i+1},v_{i+1})$ in $\mathbf{repr}(\rho,i+1)$ . $\hfill\blacktriangleleft$

Lemma 3.11.

If there exist $C\in\mathcal{I}$ , and $C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ in $P$ and $C^{\prime}(e)=q_{f}$ for all $e\in[1,||C^{\prime}||]$ , then $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},\mathbf{% 0})$ in $\mathcal{V}_{P}$ .

Proof.

Thanks to Corollary 3.3, we know there exists a well-formed execution $\rho$ from $C$ to $C^{\prime}$ . Let $K=||C||$ and $n=|\rho|-1$ . First, consider the sequence $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{0},v_{0})% \mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(\emptyset,v_{0})$ where $v_{0}(\mathsf{x}_{q_{\textit{in}}})=K$ and for all other counters $\mathsf{x}$ , $v_{0}(\mathsf{x})=0$ . Observe that, since $q_{\textit{in}}\in Q_{A}$ , $(\emptyset,v_{0})\in\mathbf{repr}(\rho,0)$ . By applying inductively Lemma 3.10, we get that $(\emptyset,v_{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\SS_{1},v_{1})% \mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}\cdots\mathbin{\stackrel{{% \scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{% 0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\SS_{n},v_{n})$ with $(\SS_{n},v_{n})\in\mathbf{repr}(\rho,n)$ . By definition, every time that $\textbf{na-state}(\rho,i,e)=q_{u}$ for some process $e$ , then $\textbf{na-index}(\rho,i,e)=n+1$ , hence there will always be at most one summary with exit state $q_{u}$ . So in the execution we build, every time that some summary $(\textsf{pr},q_{u},k)\in\SS_{i}$ , we chose $k=1$ . We then have $v_{n}(\mathsf{x}_{q_{u},1})=K$ and $v_{n}(\mathsf{x})=0$ for all other $\mathsf{x}\in\mathsf{X}\setminus\{\mathsf{x}_{q_{u},1}\}$ . Hence, by construction of $\mathcal{V}_{P}$ , we have $(\SS_{n},v_{n})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s_{f},v_{n})\mathbin{% \stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{% 0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},\mathbf{0})$ . $\hfill\blacktriangleleft$

Using Lemma 3.10 and Lemma 3.11 and the fact that the reachability problem for VASS is decidable (see Theorem 2.5) we get the main theorem of this section.

Theorem 3.12.

Synchro restricted to Wait-Only protocols is decidable.

3.3 Lower Bound for Synchro in Wait-Only Protocols

Figure 5: Protocol

P

associated to a VASS

\mathcal{V}

. The dashed edge

(\ell_{f},?\textsf{start},\textsf{err})

will only be considered in Section 4.2.

In this subsection we reduce the reachability problem for VASS to Synchro. We fix a VASS $\mathcal{V}=(\textsf{Loc},\ell_{0},\mathsf{X},\Delta)$ and a final location $\ell_{f}\in\textsf{Loc}$ . W.l.o.g., we suppose that any transition in $\Delta$ either increments or decrements of 1 exactly one counter. Hence, for a transition $(\ell,\delta,\ell^{\prime})\in\textsf{Loc}$ , we might describe $\delta$ by giving only $\delta(\mathsf{x})$ for the only $\mathsf{x}\in\mathsf{X}$ such that $\delta(\mathsf{x})\neq 0$ .

We explain how to build a protocol $P_{\mathcal{V}}$ that simulates $\mathcal{V}$ : it is depicted in Figure 5 in which we don’t consider the dashed edge. The states zero and $\{\textsf{unit}_{\mathsf{x}}\mid\mathsf{x}\in\mathsf{X}\}$ represent the evolution of the different counters of the VASS while the blue box $P^{\prime}_{\mathcal{V}}$ describes the evolution of $\mathcal{V}$ with respect to its locations. Formally, $P^{\prime}_{\mathcal{V}}$ consists of a set of states $Q_{\mathcal{V}}=\textsf{Loc}\cup\{\frownie\}$ and a set of transitions $T_{\mathcal{V}}=\{(\ell,?\textsf{inc}_{\mathsf{x}},\ell^{\prime})\mid(\ell,% \delta,\ell^{\prime})\in\Delta\textrm{ and }\delta(\mathsf{x})=1\}\cup\{(\ell,% ?\textsf{dec}_{\mathsf{x}},\ell^{\prime})\mid(\ell,\delta,\ell^{\prime})\in% \Delta\textrm{ and }\delta(\mathsf{x})=-1\}\cup\{(\ell,?m,\frownie)\mid m\in\{% \textsf{inc}_{\mathsf{x}},\textsf{dec}_{\mathsf{x}}\mid\mathsf{x}\in\mathsf{X}\}\}$ . Some transitions of $T_{\mathcal{V}}$ are depicted in Figure 6.

Figure 6: Part of

P^{\prime}_{\mathcal{V}}

that simulates respectively the transition

(\ell,\delta,\ell^{\prime})\in\Delta

with

\delta(\mathsf{x})=1

at the left, and

(\ell^{\prime\prime},\delta,\ell^{\prime\prime\prime})\in\Delta

with

\delta(\mathsf{x})=-1

at the right.

We then obtain the following theorem.

Theorem 3.13.

Synchro with Wait-Only protocols is Ackermann-complete.

Sketch of Proof..

The upper bound follows from Theorem 3.12 and Theorem 2.5. For the lower bound, we give the ideas that prove that the reduction described above is correct. In particular, there exist $C_{0}\in\mathcal{I}$ and $C_{f}\in\mathcal{C}$ such that $C_{0}\rightarrow^{\ast}C_{f}$ in $P_{\mathcal{V}}$ and $C_{f}(e)=q_{f}$ for all $e\in[1,||C_{f}||]$ if and only if $(\ell_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\ell_{f},% \mathbf{0})$ in $\mathcal{V}$ .

Assume that $(\ell_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\ell_{f},% \mathbf{0})$ in $\mathcal{V}$ , and let $K\in\mathbb{N}$ be the maximum value of $\sum_{\mathsf{x}\in\mathsf{X}}v(\mathsf{x})$ reached during the run. We choose $C_{0}$ such that $||C_{0}||=K+1$ . The execution proceeds as follows: all processes except one (the leader) broadcast a dummy message $\$$ . The leader then broadcasts start and reaches $\ell_{0}$ , while the others move to zero. These simulate the counter values, and the leader simulates the VASS by moving through the states of $P^{\prime}_{\mathcal{V}}$ . The value of counter $\mathsf{x}$ is represented by the number of processes in $\textsf{unit}_{\mathsf{x}}$ . To simulate an increment of $\mathsf{x}$ from $(\ell_{i},v_{i})$ to $(\ell_{i+1},v_{i+1})$ , a process in zero sends $\textsf{inc}_{\mathsf{x}}$ , which the leader receives to transition to $\ell_{i+1}$ . If the current configuration correctly represents $(\ell_{i},v_{i})$ , the new one faithfully represents $(\ell_{i+1},v_{i+1})$ . At the end of the simulation, the leader reaches $\ell_{f}$ , and the other processes remain in zero. They then broadcast end, and the leader (now in $\ell^{\prime}_{f}$ ) broadcasts verif, gathering all processes in $q_{f}$ .

To prove the other direction, we must show that the processes cannot cheat in simulating the VASS. First, note that reaching $q_{f}$ requires exactly one broadcast of verif, a second would send the original sender to err. This ensures that only one process (the leader) simulates the VASS by moving through $P_{\mathcal{V}}$ . Second, counter updates must follow the VASS transitions: any unauthorized update would cause the leader to receive an unexpected message and transition to the losing state $\frownie$ . Finally, when the leader reaches $\ell_{f}$ , all other processes must be in zero. If not, problems occur during the final steps: one process (the helper) broadcasts end, which sends the leader to $\ell^{\prime}_{f}$ . Then, all remaining processes must reach z-end before the unique verif broadcast. If a process in $\textsf{unit}_{\mathsf{x}}$ moves to z-end, it must broadcast $\textsf{dec}_{\mathsf{x}}$ , which is received by other processes in z-end, sending them, including the helper, to $\textsf{err}^{\prime}$ . As a result, the helper misses verif and cannot reach $q_{f}$ , preventing a successful execution. Thus, the simulation must end with the leader in $\ell_{f}$ and all others in zero. $\hfill\blacktriangleleft$

4 Synchro is ExpSpace-complete when the Target State is an Action State

Upper bound.

We show that Synchro when $q_{f}\in Q_{A}$ can be reduced to the mutual reachability problem on VASS, defined as follows: given a VASS $\mathcal{V}=(\textsf{Loc},\ell_{0},\mathsf{X},\Delta)$ and a location $\ell_{f}$ , do there exist a run from $(\ell_{0},\mathbf{0})$ to $(\ell_{f},\mathbf{0})$ and one from $(\ell_{f},\mathbf{0})$ to $(\ell_{0},\mathbf{0})$ . This problem is shown to be in ExpSpace [16]. More precisely, Leroux establishes the ExpSpace-membership and provides a bound on the lengths of the runs, for the mutual reachability problem in VAS (Vector Addition Systems). However, by applying the VASS-to-VAS transformation presented in [14], we get the following result.

Theorem 4.1 ([16] Corollary 10.6, Transformation of [14]).

Given a VASS $\mathcal{V}=(\textsf{Loc},\ell_{0},\mathsf{X},\Delta)$ , if there are two runs $(\ell_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\ell_{f},% \mathbf{0})$ and $(\ell_{f},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\ell_{0},% \mathbf{0})$ , then there are two runs $(\ell_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\ell_{f},% \mathbf{0})$ and $(\ell_{f},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\ell_{0},% \mathbf{0})$ whose lengths are bounded by $17(|\mathsf{X}|+3)^{2}x^{15(|\mathsf{X}|+3)^{|\mathsf{X}|+5}}$ where $x=(1+2(|\textsf{Loc}|+1)^{2})^{2}$ .

Given a Wait-Only protocol $P=(Q,\Sigma,q_{\textit{in}},T)$ and a target state $q_{f}\in Q_{A}$ , we explain how to transform it into a VASS where mutual reachability is equivalent to Synchro. We build the VASS $\mathcal{V}_{P}=(\textsf{Loc},\mathsf{X},s_{0},\Delta)$ as described in Section 3.2, with some modifications. The first two modifications simply encode the fact that the target state is not a waiting sate anymore, while the third one ensures the mutual reachability.

$\blacksquare$

We add a state $s^{\prime}_{f}$ and the transition $(\{S_{f}\},\mathbf{0},s_{f})$ is replaced by two transitions: $(\emptyset,\delta,s^{\prime}_{f})$ and $(s^{\prime}_{f},\delta^{\prime},s_{f})$ . Here, $\delta(\mathsf{x}_{q_{f}})=-1$ , $\delta^{\prime}(\mathsf{x}_{q_{f}})=1$ , and for all other counters $\mathsf{x}$ , $\delta(\mathsf{x})=\delta^{\prime}(\mathsf{x})=0$ . It prevents the reachability of $(s_{f},\mathbf{0})$ to be trivial with the run $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(\emptyset,\mathbf{0})% \mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s_{f},\mathbf{0})$ .
$\blacksquare$

The transition $(s_{f},\delta_{f},s_{f})$ is replaced by $(s_{f},\delta^{\prime}_{f},s_{f})$ , where $\delta^{\prime}_{f}(\mathsf{x}_{q_{f}})=-1$ and $\delta^{\prime}_{f}(\mathsf{x})=0$ for all other counters $\mathsf{x}$ .
$\blacksquare$

We add a transition $(s_{f},\mathbf{0},s_{0})$ to allow the resetting of $\mathcal{V}_{P}$ to $s_{0}$ after reaching $s_{f}$ .

Lemma 4.2.

There exists $C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ and, for all $e\in[1,||C^{\prime}||]$ , $C^{\prime}(e)=q_{f}$ if and only if there are two runs $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},\mathbf{% 0})$ and $(s_{f},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{0},\mathbf{% 0})$ in $\mathcal{V}_{P}$ .

Sketch of Proof..

Assume that there exist $C\in\mathcal{I}$ and $C^{\prime}\in\mathcal{C}$ such that $C\rightarrow^{\ast}C^{\prime}$ and, for all $e\in[1,||C^{\prime}||]$ , $C^{\prime}(e)=q_{f}$ . Since the main body of $\mathcal{V}_{P}$ is the same as in Section 3.2 we can, like in Lemma 3.11, build a run of $\mathcal{V}_{P}$ from $(s_{0},\mathbf{0})$ to $(s_{f},\mathbf{0})$ . By construction of $\mathcal{V}_{P}$ , $(s_{f},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s_{0},\mathbf{0})$ .Assume now that $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},\mathbf{% 0})$ (and $(s_{f},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s_{0},\mathbf{0})$ ). Observe that it might be the case that the run looks like $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},v_{1})% \mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s_{0},v_{1})\mathbin{\stackrel{{% \scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{% 0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},v_{2})\dots(s_{0},v_{k})\mathbin{% \stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\rule{% 0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},\mathbf{0})$ . By construction of the VASS, we know that there is an execution $(s_{0},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\emptyset,v^{% \prime}_{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\emptyset,v^{% \prime\prime}_{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s^{\prime}_{f},v^{% \prime\prime\prime}_{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}% {{{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle% \sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s_{f},v^{\prime% \prime}_{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},v_{1})$ . Here $v^{\prime}_{0}$ is the valuation obtained after having increased the counter $\mathsf{x}_{q_{\textit{in}}}$ , $v^{\prime\prime}_{0}$ is the valuation obtained just before going to $s^{\prime}_{f}$ , and $v_{1}$ is obtained after having decremented counter $\mathsf{x}_{q_{f}}$ . Adapting the proof of Lemma 3.9 to this case, we deduce the existence of an execution of the protocol from an initial configuration $C_{0}$ to a configuration $C^{\prime}_{0}$ such that $|{C^{\prime}_{0}}^{-1}(q)|=0$ for all $q\in Q_{W}$ , and $|{C^{\prime}_{0}}^{-1}(q)|=v^{\prime\prime}_{0}(\mathsf{x}_{q})+\sum_{i=1,% \dots,{|Q_{W}|+1}}v^{\prime\prime}_{0}(\mathsf{x}_{(q,i)})$ for all $q\in Q_{A}$ . From the portion of run of the VASS $(s_{0},v_{1})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\emptyset,v^{% \prime}_{1})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(\emptyset,v^{% \prime\prime}_{1})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s^{\prime}_{f},v^{% \prime\prime\prime}_{1})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}% {{{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle% \sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(s_{f},v^{\prime% \prime}_{1})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{% \scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}^{\ast}(s_{f},v_{2})$ , we similarly get another sequence of configurations of the protocol from a configuration $C_{1}$ (not necessarily initial because $v_{1}$ might not be equal to 0 for some counters other than $\mathsf{x}_{q_{\textit{in}}}$ ) to a configuration $C^{\prime}_{1}$ such that $C_{1}\rightarrow^{\ast}C^{\prime}_{1}$ and $|{C^{\prime}_{1}}^{-1}(q)|=0$ for all $q\in Q_{W}$ . Observe however that these two sequences can be merged into a single one, of size $v^{\prime}_{0}(\mathsf{x}_{q_{\textit{in}}})+(v^{\prime}_{1}(\mathsf{x}_{q_{% \textit{in}}})-v_{1}(\mathsf{x}_{q_{\textit{in}}}))$ (the second part corresponds to processes added in $q_{\textit{in}}$ with transition $(s_{0},\delta_{\textit{in}},s_{0})$ , and $\delta_{in}(\mathsf{x}_{q_{\textit{in}}})=1$ ). The execution then first behaves like the execution from $C_{0}$ to $C^{\prime}_{0}$ , potentially leaving some processes in the initial state (in particular processes from $v^{\prime}_{1}(\mathsf{x}_{q_{\textit{in}}})-v_{1}(\mathsf{x}_{q_{\textit{in}}})$ ). Once this first part is over, all the processes are either in the initial state, or in an action state (because ${C^{\prime}_{0}}^{-1}(q)=0$ for all $q\in Q_{W}$ ). Then, one can simulate the second sequence, (processes already in $q_{f}$ from the first execution won’t be affected because they are in an action state, so they won’t receive any message. This would not be true if $q_{f}\in Q_{W}$ ). Since the execution of $\mathcal{V}_{P}$ eventually reaches $(s_{f},\mathbf{0})$ , it means that it reaches $(s_{f},v_{k+1})$ where $v_{k+1}(\mathsf{x})=0$ for all $\mathsf{x}\neq\mathsf{x}_{q_{f}}$ . Then, by iterating the construction described above, one obtains an execution of $P$ from an initial configuration to a configuration $C_{f}$ such that $C_{f}(e)=q_{f}$ for all $e\in[1,||C_{f}||]$ . $\hfill\blacktriangleleft$

As runs of doubly exponential length can be guessed in exponential space in the size of the VASS and $\textsc{ExpSpace}=\textsc{NExpspace}$ , we get the following theorem using Remarks 3.7 and 4.1. Observe that even if the number of locations is doubly exponential in the size of the protocol, the bound of Theorem 4.1 is polynomial in $|\textsf{Loc}|$ and doubly exponential in $|\mathsf{X}|$ , hence lengths of the runs to guess remain doubly exponential in the size of the protocol.

Theorem 4.3.

Synchro for Wait-Only protocols is in ExpSpace when $q_{f}\in Q_{A}$ .

Lower bound.

ExpSpace-hardness follows from a reduction of the coverability problem in VASS, which is ExpSpace-hard [19], and stated as follows: given a VASS $\mathcal{V}=(\textsf{Loc},\ell_{0},\mathsf{X},\Delta)$ of dimension $d\in\mathbb{N}$ , and a location $\ell_{f}\in\textsf{Loc}$ , decide whether there is an execution from $(\ell_{0},\mathbf{0})$ to $(\ell_{f},v)$ for some $v\in\mathbb{N}^{d}$ .

The reduction uses the protocol depicted in Figure 5, this time including the dashed edge but excluding the thick edges: $q_{f}$ is now an action state. Then $\ell_{f}$ is coverable iff there exists an execution $C_{0}\rightarrow^{\ast}C_{f}$ in which all processes reach $q_{f}$ . The execution of the VASS can be simulated in the protocol like in Section 3.3. The processes that may still remain in the states $\textsf{unit}_{\mathsf{x}}$ can reach z-end even when $\ell^{\prime}_{f}$ is populated (recall that all the thick edges have been removed). Once this is done, all processes can gather in $q_{f}$ . Conversely, if there exists an execution in which all processes reach $q_{f}$ , it means that $\ell_{f}$ is coverable. Let $e_{0}$ be the first process to broadcast start, then an execution of the VASS covering $\ell_{f}$ can be built based on the sequence of states visited by $e_{0}$ between $\ell_{0}$ and $\ell_{f}$ . This relies on three keys observations: (1) The process $e_{0}$ must visit $\ell_{f}$ , otherwise it cannot reach $q_{f}$ . (2) When $e_{0}$ is between $\ell_{0}$ and $\ell_{f}$ , $e_{0}$ is the only process in this region. If another process attempts to join by broadcasting start, $e_{0}$ will receive the message and go to err, preventing it from reaching $q_{f}$ . (3) When $e_{0}$ reaches $\ell_{0}$ for the first time, no other process is in the states $\{\textsf{unit}_{\mathsf{x}}\mid\mathsf{x}\in\mathsf{X}\}$ , since start is sent for the first time at this point. Hence, with Theorem 4.3, it establishes the following result.

Theorem 4.4.

Synchro for Wait-Only protocols is ExpSpace-complete when $q_{f}\in Q_{A}$ .

5 Solving the Repeated Coverability problem for Wait-Only Protocols

Upper Bound.

We show that RepCover on Wait-Only protocols is in ExpSpace, via the repeated coverability problem in VASS: given a VASS $\mathcal{V}=(\textsf{Loc},\ell_{\textit{init}},\mathsf{X},\Delta)$ and a location $\ell_{f}\in\textsf{Loc}$ , is there an infinite execution $(\ell_{init},\mathbf{0})\mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}% {{{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle% \sim\mkern-3.9mu}{\scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}(\ell_{1},v_{1})% \mathbin{\stackrel{{\scriptstyle\scriptscriptstyle{}}}{{{\scriptstyle\sim% \mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{\scriptstyle\sim\mkern-3.9mu}{% \scriptstyle\rule{0.3014pt}{0.0pt}\rhd}}}}\dots$ such that, for all $i\in\mathbb{N}$ , there exists $j>i$ such that $\ell_{j}=\ell_{f}$ ? We rely on the following theorem.

Theorem 5.1 (Theorem 3.1 of [13]).

For a VASS $\mathcal{V}=(\textsf{Loc},\ell_{\textit{init}},\mathsf{X},\Delta)$ , the repeated coverability problem is solvable in $O(\log(l)+\log(|\textsf{Loc}|))2^{c|\mathsf{X}|\log(|\mathsf{X}|)}$ nondeterministic space for some constant $c$ independent of $\mathcal{V}$ , and where the absolute values of components of vectors in $\Delta$ are smaller than $l$ .

Let $P=(Q,\Sigma,q_{\textit{in}},T)$ be a Wait-Only protocol and $t_{f}=(q,!!a,q^{\prime})$ the transition that has to occur infinitely often. We build a VASS $\mathcal{V}_{P}$ based on the construction presented in Section 3.2. This time, we add a new set of states $\textsf{CoSets}_{\smiley}=\{(\SS,\smiley)\mid\SS\in\textsf{CoSets}\}$ . and the set of transitions $\{(\SS,\delta,(\SS^{\prime},\smiley))\mid(\SS,\delta,\SS^{\prime})\in\Delta_{t% _{f}}\}\cup\{(\SS,\smiley),\mathbf{0},\SS)\mid\SS\in\textsf{CoSets}\}$ . Hence, when a process takes the transition $t_{f}$ , it is highlighted in $\mathcal{V}_{P}$ by going in a location tagged with $\smiley$ , before continuing the execution. Taking the protocol of Figure 1, with $t_{f}=(q_{\textit{in}},!!d,q_{1})$ , the previous transition from the location of the VASS $\{(\{q_{3}\},q_{4},1)\}$ to the location $\{(\{q_{3}\},q_{4},1),(\{q_{1}\},q_{6},1)\}$ (see Figure 4) is now transformed into two transitions in the VASS we build here: one from $(\{(\{q_{3}\},q_{4},1)\})$ to the location $(\{(\{q_{3}\},q_{4},1),(\{q_{1}\},q_{6},1)\},\smiley)$ and one from $(\{(\{q_{3}\},q_{4},1),(\{q_{1}\},q_{6},1)\},\smiley)$ to $\{(\{q_{3}\},q_{4},1),(\{q_{1}\},q_{6},1)\}$ . There is an execution of $P$ with a process that takes $t_{f}$ infinitely often iff there is an execution of $\mathcal{V}_{P}$ where one state in $\textsf{CoSets}_{\smiley}$ is visited infinitely often. The procedure to decide RepCover is then: guess a location $\ell_{f}$ in $\textsf{CoSets}_{\smiley}$ and solve the repeated coverability problem for $\mathcal{V}_{P}$ and $\ell_{f}$ . From Remarks 3.7 and 5.1, this can be done in $O(\log(2)+(|Q|+1)^{2}\times 2^{|Q|}+2)2^{c(|Q|+1)^{3}\log((|Q|+1)^{3})}$ nondeterministic space. The overall procedure is then in $\textsc{NExpSpace}=\textsc{ExpSpace}$ . Hence, the following theorem.

Theorem 5.2.

RepCover is in ExpSpace.

$\blacktriangleright$ Remark 5.3.

One could define RepCover with a reception transition that has to occur infinitely often. The VASS we described hereabove can be adapted by enlarging each location with the current state of the witness process. This can also be done in ExpSpace.

Lower bound.

Figure 7: The part of

P

with transition

t_{f}=(q_{n+2},!!\smiley,q_{1})

. We write

?\Sigma

for

?m,\forall m\in\Sigma

.

Figure 8: The part of

P

simulating automaton

i

.

We reduce the intersection non-emptiness problem for deterministic finite automata, which is known to be PSpace-complete [15], to RepCover. Let $\mathcal{A}_{1},\dots,\mathcal{A}_{n}$ be deterministic, complete finite automata, with $\mathcal{A}_{i}=(A,Q_{i},q_{i}^{0},{q_{i}^{f}},\Delta_{i})$ for $1\leq i\leq n$ . The reduction assumes a single accepting state per automaton, which does not affect complexity. We denote by $A^{\ast}$ the set of words over the alphabet $A$ , and extend each transition function $\Delta_{i}$ to $A^{\ast}$ by defining: $\Delta_{i}^{\ast}(q,\varepsilon)=q$ , and $\Delta_{i}^{\ast}(q,wa)=\Delta_{i}(\Delta_{i}^{\ast}(q,w),a)$ for all $w\in A^{\ast}$ and $a\in A$ .

We define a protocol $P=(Q,\Sigma,q_{\textit{in}},T)$ composed of several components. For each automaton $\mathcal{A}_{i}$ , $P$ includes a component $P_{i}=(Q^{i},T^{i})$ (see Figure 8), where $Q^{i}=Q_{i}$ and $T^{i}=\{(q_{1}^{i},?a,q_{2}^{i})\mid(q_{1}^{i},a,q_{2}^{i})\in\Delta_{i}\}$ . The main control component (see Figure 8) includes the transition $t_{f}=(q_{n+2},!!\smiley,q_{1})$ , which must occur infinitely often. A process taking $t_{f}$ infinitely often also receives infinitely many sequences of messages $\$\cdot\text{end}_{1}\cdot\text{end}_{2}\dots\text{end}_{n}$ , where each $\text{end}_{i}$ is broadcast by the component simulating $\mathcal{A}_{i}$ . In addition to transitions in Figures 8 and 8, $T$ also includes: $\{(q_{\textit{in}},!!a,q_{\textit{in}})\mid a\in A\}\cup\{(q_{\textit{in}},!!% \$,q_{\textit{in}})\}$ . One can show that there exists a word $w=a_{1}\dots a_{n}$ in the intersection of the $n$ automata iff there is an execution in which $t_{f}$ is taken infinitely often.

Theorem 5.4.

RepCover is PSpace-hard.

References

[1] K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307–309, 1986. doi:10.1016/0020-0190(86)90071-2.
[2] Peter Chini, Roland Meyer, and Prakash Saivasan. Liveness in broadcast networks. Computing, 104(10):2203–2223, 2022. doi:10.1007/S00607-021-00986-Y.
[3] Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229–1240. IEEE, 2021. doi:10.1109/FOCS52979.2021.00120.
[4] Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. Towards the automated verification of multithreaded java programs. In TACAS 2002, volume 2280 of LNCS, pages 173–187. Springer, 2002. doi:10.1007/3-540-46002-0_13.
[5] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 313–327, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. doi:10.1007/978-3-642-15375-4_22.
[6] E.A. Emerson and K.S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 70–80, 1998. doi:10.1109/LICS.1998.705644.
[7] J. Esparza, P. Ganty, and R. Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV’13, volume 8044 of LNCS, pages 124–140. Springer-Verlag, 2013. doi:10.1007/978-3-642-39799-8_8.
[8] Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 352–359. IEEE Computer Society, 1999. doi:10.1109/LICS.1999.782630.
[9] S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675–735, 1992. doi:10.1145/146637.146681.
[10] Lucie Guillou, Arnaud Sangnier, and Nathalie 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. doi:10.4230/LIPICS.CONCUR.2023.7.
[11] Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Safety verification of wait-only non-blocking broadcast protocols. In Application and Theory of Petri Nets and Concurrency - 45th International Conference, PETRI NETS 2024, volume 14628 of Lecture Notes in Computer Science, pages 291–311. Springer, 2024. doi:10.1007/978-3-031-61433-0_14.
[12] Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Wait-only broadcast protocols are easier to verify, 2025. arXiv:2506.22144.
[13] Peter Habermehl. On the complexity of the linear-time mu -calculus for petri-nets. In Pierre Azéma and Gianfranco Balbo, editors, Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN ’97, Toulouse, France, June 23-27, 1997, Proceedings, volume 1248 of Lecture Notes in Computer Science, pages 102–116. Springer, 1997. doi:10.1007/3-540-63139-9_32.
[14] John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135–159, 1979. doi:10.1016/0304-3975(79)90041-0.
[15] Dexter Kozen. Lower bounds for natural proof systems. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 254–266. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.16.
[16] Jérôme Leroux. Vector addition system reversible reachability problem. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 327–341. Springer, 2011. doi:10.1007/978-3-642-23217-6_22.
[17] Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241–1252. IEEE, 2021. doi:10.1109/FOCS52979.2021.00121.
[18] Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1–13. IEEE, 2019. doi:10.1109/LICS.2019.8785796.
[19] R.J. Lipton. The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science). Department of Computer Science, Yale University, 1976. URL: https://books.google.fr/books?id=7iSbGwAACAAJ.
[20] 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. doi:10.1007/978-3-642-40184-8_2.
[21] Rüdiger Valk. Self-modifying nets, a natural extension of petri nets. In ICALP’78, volume 62 of LNCS, pages 464–476. Springer, 1978. doi:10.1007/3-540-08860-1_35.

[bib.bib1] [1] K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307–309, 1986. doi:10.1016/0020-0190(86)90071-2.

[bib.bib2] [2] Peter Chini, Roland Meyer, and Prakash Saivasan. Liveness in broadcast networks. Computing, 104(10):2203–2223, 2022. doi:10.1007/S00607-021-00986-Y.

[bib.bib3] [3] Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229–1240. IEEE, 2021. doi:10.1109/FOCS52979.2021.00120.

[bib.bib4] [4] Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. Towards the automated verification of multithreaded java programs. In TACAS 2002, volume 2280 of LNCS, pages 173–187. Springer, 2002. doi:10.1007/3-540-46002-0_13.

[bib.bib5] [5] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 313–327, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. doi:10.1007/978-3-642-15375-4_22.

[bib.bib6] [6] E.A. Emerson and K.S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 70–80, 1998. doi:10.1109/LICS.1998.705644.

[bib.bib7] [7] J. Esparza, P. Ganty, and R. Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV’13, volume 8044 of LNCS, pages 124–140. Springer-Verlag, 2013. doi:10.1007/978-3-642-39799-8_8.

[bib.bib8] [8] Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 352–359. IEEE Computer Society, 1999. doi:10.1109/LICS.1999.782630.

[bib.bib9] [9] S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675–735, 1992. doi:10.1145/146637.146681.

[bib.bib10] [10] Lucie Guillou, Arnaud Sangnier, and Nathalie 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. doi:10.4230/LIPICS.CONCUR.2023.7.

[bib.bib11] [11] Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Safety verification of wait-only non-blocking broadcast protocols. In Application and Theory of Petri Nets and Concurrency - 45th International Conference, PETRI NETS 2024, volume 14628 of Lecture Notes in Computer Science, pages 291–311. Springer, 2024. doi:10.1007/978-3-031-61433-0_14.

[bib.bib12] [12] Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Wait-only broadcast protocols are easier to verify, 2025. arXiv:2506.22144.

[bib.bib13] [13] Peter Habermehl. On the complexity of the linear-time mu -calculus for petri-nets. In Pierre Azéma and Gianfranco Balbo, editors, Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN ’97, Toulouse, France, June 23-27, 1997, Proceedings, volume 1248 of Lecture Notes in Computer Science, pages 102–116. Springer, 1997. doi:10.1007/3-540-63139-9_32.

[bib.bib14] [14] John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135–159, 1979. doi:10.1016/0304-3975(79)90041-0.

[bib.bib15] [15] Dexter Kozen. Lower bounds for natural proof systems. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 254–266. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.16.

[bib.bib16] [16] Jérôme Leroux. Vector addition system reversible reachability problem. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 327–341. Springer, 2011. doi:10.1007/978-3-642-23217-6_22.

[bib.bib17] [17] Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241–1252. IEEE, 2021. doi:10.1109/FOCS52979.2021.00121.

[bib.bib18] [18] Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1–13. IEEE, 2019. doi:10.1109/LICS.2019.8785796.

[bib.bib19] [19] R.J. Lipton. The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science). Department of Computer Science, Yale University, 1976. URL: https://books.google.fr/books?id=7iSbGwAACAAJ.

[bib.bib20] [20] 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. doi:10.1007/978-3-642-40184-8_2.

[bib.bib21] [21] Rüdiger Valk. Self-modifying nets, a natural extension of petri nets. In ICALP’78, volume 62 of LNCS, pages 464–476. Springer, 1978. doi:10.1007/3-540-08860-1_35.

Wait-Only Broadcast Protocols Are Easier to Verify

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Model and Verification Problems

Networks of Processes using Broadcast Communication.

Definition 2.1.

Example 2.2.

Verification Problems.

Theorem 2.3.

▶ Remark 2.4.

Vector Addition System with States.

Theorem 2.5 (Membership [18], Hardness [3, 17]).

3 Solving Synchro for Wait-Only Protocols

3.1 Preliminary properties

Lemma 3.1.

Example 3.2.

Corollary 3.3.

Lemma 3.4.

Proof.

3.2 Building the VASS that Simulates a Broadcast Network

Summaries.

Example 3.5.

Definition of the VASS.

Example 3.6.

▶ Remark 3.7.

Soundness of the construction.

Lemma 3.8.

Sketch of Proof..

Lemma 3.9.

Proof.

Completeness of the construction.

Lemma 3.10.

Sketch of Proof..

Lemma 3.11.

Proof.

Theorem 3.12.

3.3 Lower Bound for Synchro in Wait-Only Protocols

Theorem 3.13.

Sketch of Proof..

4 Synchro is ExpSpace-complete when the Target State is an Action State

Upper bound.

Theorem 4.1 ([16] Corollary 10.6, Transformation of [14]).

Lemma 4.2.

Sketch of Proof..

Theorem 4.3.

Lower bound.

Theorem 4.4.

5 Solving the Repeated Coverability problem for Wait-Only Protocols

Upper Bound.

Theorem 5.1 (Theorem 3.1 of [13]).

Theorem 5.2.

▶ Remark 5.3.

Lower bound.

Theorem 5.4.

References

$\blacktriangleright$ Remark 2.4.

$\blacktriangleright$ Remark 3.7.

$\blacktriangleright$ Remark 5.3.