Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks
Abstract
Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We focus here on the synchronization property, asking whether all agents converge to a set of target states after some execution. This problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while it is undecidable for static broadcast networks).
In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents.
1 Introduction
There are numerous application domains for networks formed of an arbitrary number of anonymous agents executing the same code: prominent examples are distributed algorithms, communication protocols, cachecoherence protocols, and biological systems such as populations of cells or individuals, etc. The automated verification of such systems is challenging [3, 8, 12, 15]: its aim is to validate at once all instances of the model, independently of the (parameterized) number of agents. Such a problem can be phrased in terms of infinitestatesystem verification. Exploiting symmetries may lead to efficient algorithms for the verification of relevant properties [7].
Different means of interactions between agents can be considered in such networks, depending on the application domain. Typical examples are shared variables [4, 10, 13], rendezvous [12], and broadcast communications [6, 9]. In this paper, we target ad hoc networks [6], in which the agents can broadcast messages simultaneously to all their neighbours, i.e., to all the agents that are within their radio range. The number of agents and the communication topology are fixed once and for all at the beginning of the execution. Parameterized verification of broadcast networks checks if a specification is met independently of the number of agents and communication topology. It is usually simpler to reason about the dual problem of the existence of an initial configuration (consisting of a network size, an initial state for each agent, and a communication topology) from which some execution violates the given specification.
Several types of specifications have been considered in the literature. We focus here on coverability and synchronization: does there exist an initial configuration from which some agent (resp. all agents at the same time) may reach a particular set of target states. Both problems are undecidable; decidability of coverability can be regained by bounding the length of simple paths in the communication topology [6].
In the case of mobile ad hoc networks (MANETs), agents are mobile, so that the communication links (and thus the neighbourhood of each agent) may evolve over time. To reflect the mobility of agents, Delzanno et al. studied reconfigurable broadcast networks [5, 6]. In such networks, the communication topology can change arbitrarily at any time. Perhaps surprisingly, this modification not only allows for a more faithful modelling of MANETs, but it also leads to decidability of both the coverability and the synchronization problems [6]. A probabilistic extension of reconfigurable broadcast networks has been studied in [1, 2] to model randomized protocols.
A drawback of the semantics of reconfigurable broadcast networks is that they allow arbitrary changes at each reconfiguration. Such arbitrary reconfigurations may not be realistic, especially in settings where communications are frequent enough, and mobility is slow and not chaotic. In this paper, we limit the impact of reconfigurations in several ways, and study how those limitations affect the decidability and complexity of parameterized verification of synchronization.
More specifically, we restrict reconfigurations by limiting the number of changes in the communication graph, either by considering global constraints (on the total number of edges being modified), or by considering local constraints (on the number of updates affecting each individual node). We prove that synchronization is decidable when imposing constant local constraints, as well as when imposing global constraints depending (as a divergent function) on the number of agents. On the other hand, imposing a constant global bound makes synchronization undecidable. We recover decidability by bounding the maximal degree of each node by 1.
2 Broadcast Networks with Constrained Reconfiguration
In this section, we first define reconfigurable broadcast networks; we then introduce several constraints on reconfigurations along executions, and investigate how they compare one to another and with unconstrained reconfigurations.
2.1 Reconfigurable Broadcast Networks
Definition 1
A broadcast protocol is a tuple \(\mathcal {P}=(Q,I,\varSigma ,\varDelta )\) where \(Q\) is a finite set of control states; \(I\in Q\) is the set of initial control states; \(\varSigma \) is a finite alphabet; and \(\varDelta \subseteq (Q\times \{ !!\textit{a},?\!?\textit{a} \mid a\in \varSigma \}\times Q)\) is the transition relation.
Formally, we first define undirected labelled graphs. Given a set \(\mathcal {L}\) of labels, an \(\mathcal {L}\)graph is an undirected graph \(\mathsf {G}= (\mathsf {N},\mathsf {E},\mathsf {L})\) where \(\mathsf {N}\) is a finite set of nodes; \(\mathsf {E}\subseteq \mathcal P_2(\mathsf {N})\)^{1} (notice in particular that such a graph has no selfloops); finally, \(\mathsf {L}:\mathsf {N}\rightarrow \mathcal {L}\) is the labelling function. We let \(\mathcal {G}_\mathcal {L}\) denote the (infinite) set of \(\mathcal {L}\)labelled graphs. Given a graph \(\mathsf {G}\in \mathcal {G}_\mathcal {L}\), we write \(\mathsf {n}\sim \mathsf {n}'\) whenever \(\{\mathsf {n},\mathsf {n}'\} \in \mathsf {E}\) and we let \(\mathsf {Neigh}_{\mathsf {G}}(\mathsf {n}) =\{\mathsf {n}' \mid \mathsf {n}\sim \mathsf {n}'\}\) be the neighbourhood of \(\mathsf {n}\), i.e. the set of nodes adjacent to \(\mathsf {n}\). For a label \(\ell \), we denote by \( \mathsf {G} _{\ell }\) the number of nodes in \(\mathsf {G}\) labelled by \(\ell \). Finally \(\mathsf {L}(\mathsf {G})\) denotes the set of labels appearing in nodes of \(\mathsf {G}\).

(reconfiguration step) \(\mathsf {N}' =\mathsf {N}\) and \(\mathsf {L}' =\mathsf {L}\): a reconfiguration step does not change the set of nodes and their labels, but may change the edges arbitrarily;

(communication step) \(\mathsf {N}'=\mathsf {N}\), \(\mathsf {E}'= \mathsf {E}\), and there exists \(\mathsf {n}\in \mathsf {N}\) and \(a\in \varSigma \) such that \((\mathsf {L}(\mathsf {n}),!!\textit{a},\mathsf {L}'(\mathsf {n})) \in \varDelta \), and for every \(\mathsf {n}'\), if \(\mathsf {n}' \in \mathsf {Neigh}_{\mathsf {G}}(\mathsf {n})\), then \((\mathsf {L}(\mathsf {n}'),?\!?\textit{a},\mathsf {L}'(\mathsf {n}')) \in \varDelta \), otherwise \(\mathsf {L}'(\mathsf {n}') = \mathsf {L}(\mathsf {n}')\): a communication step reflects how nodes evolve when one of them broadcasts a message to its neighbours.
An execution of the reconfigurable broadcast network is a sequence \(\rho =(\mathsf {G}_i)_{0\le i\le r}\) of configurations such that for any \(i<r\), there is a step from \(\mathsf {G}_i\) to \(\mathsf {G}_{i+1}\) and \(\rho \) strictly alternates communication and reconfiguration steps (the latter possibly being trivial). An execution is initial if it starts from an initial configuration.
An important ingredient that we heavily use in the sequel is juxtaposition of configurations and shuffling of executions. The juxtaposition of two configurations \(\mathsf {G}= (\mathsf {N},\mathsf {E},\mathsf {L})\) and \(\mathsf {G}' = (\mathsf {N}',\mathsf {E}',\mathsf {L}')\) is the configuration \(\mathsf {G}\oplus \mathsf {G}' = (\mathsf {N}\uplus \mathsf {N}',\mathsf {E}\uplus \mathsf {E}',\mathsf {L}_\oplus )\), in which \(\mathsf {L}_\oplus \) extends both \(\mathsf {L}\) and \(\mathsf {L}'\): \(\mathsf {L}_\oplus (\mathsf {n}) = \mathsf {L}(\mathsf {n})\) if \(\mathsf {n}\in \mathsf {N}\) and \(\mathsf {L}_\oplus (\mathsf {n}) = \mathsf {L}'(\mathsf {n})\) if \(\mathsf {n}\in \mathsf {N}'\). We write \(\mathsf {G}^2\) for the juxtaposition of \(\mathsf {G}\) with itself, and, inductively, \(\mathsf {G}^N\) for the juxtaposition of \(\mathsf {G}^{N1}\) with \(\mathsf {G}\). A shuffle of two executions \(\rho =(\mathsf {G}_i)_{0\le i\le r}\) and \(\rho '=(\mathsf {G}'_j)_{0\le j\le r'}\) is an execution \(\rho _\oplus \) from \(\mathsf {G}_0\oplus \mathsf {G}'_0\) to \(\mathsf {G}_r\oplus \mathsf {G}'_{r'}\) obtained by interleaving \(\rho \) and \(\rho '\). Note that a reconfiguration step in \(\rho _\oplus \) may be composed of reconfigurations from both \(\rho \) and \(\rho '\). We write \(\rho \oplus \rho '\) for the set of shuffle executions obtained from \(\rho \) and \(\rho '\).
Natural decision problems for reconfigurable broadcast networks include checking whether some node may reach a target state, or whether all nodes may synchronize to a set of target states. More precisely, given a broadcast protocol \(\mathcal {P}\) and a subset \(F\subseteq Q\), the coverability problem asks whether there exists an initial execution \(\rho \) that visits a configuration \(\mathsf {G}\) with \(\mathsf {L}(\mathsf {G}) \cap F\not =\emptyset \), and the synchronization problem asks whether there exists an initial execution \(\rho \) that visits a configuration \(\mathsf {G}\) with \(\mathsf {L}(\mathsf {G}) \subseteq F\). For unconstrained reconfigurations, we have:
Theorem 2
([5, 6, 11]). The coverability and synchronization problems are decidable in PTIME for reconfigurable broadcast protocols.
Remark 1
The synchronization problem was proven decidable in [6], and PTIME membership was given in [11, p. 41]. The algorithm consists in computing the set of states of \(\mathcal {P}\) that are both reachable (i.e., coverable) from an initial configuration and coreachable from a target configuration. This can be performed by applying iteratively the algorithm of [5] for computing the set of reachable states (with reversed transitions for computing coreachable states).
Example 1
Consider the broadcast protocol of Fig. 1 with \(I= \{q_0\}\). From each state, unspecified message receptions lead to an (omitted) sink state; this way, each broadcast message triggers a transition in all the neighbouring copies.
For that broadcast protocol, one easily sees that it is possible to synchronize to the set \(\{ q_4,q_6,q_8 \}\). Moreover, three copies are needed and sufficient for that objective, as witnessed by the execution of Fig. 2. The initial configuration has three copies and two edges. If the central node broadcasts \(a\), the other two nodes receive, one proceeding to \(q_5\) and the other to \(q_7\). Then, we assume the communication topology is emptied before the same node broadcasts \(b\), moving to \(q_2\). Finally the node in \(q_5\) connects to the one in \(q_2\) to communicate on \(c\) and then disconnects, followed by a similar communication on \(d\) initiated by the node in \(q_7\).
2.2 Natural Constraints for Reconfiguration
Allowing arbitrary changes in the network topology may look unrealistic. In order to address this issue, we introduce several ways of bounding the number of reconfigurations after each communication step. For this, we consider the following natural pseudometric between graphs, which for simplicity we call distance.
Definition 3
Setting the “distance” to 0 for two graphs that do not agree on the set of nodes or on the labelling function might seem strange at first. This choice is motivated by the definition of constraints on executions (see below) and of the number of reconfigurations along an execution (see Sect. 2.3). Other distances may be of interest in this context; in particular, for a fixed node \(\mathsf {n}\in \mathsf {N}\), we let \(\mathsf {dist}_{\mathsf {n}}(\mathsf {G},\mathsf {G}')\) be the number of edges involving node \(\mathsf {n}\) in the symmetric difference of \(\mathsf {E}\) and \(\mathsf {E}'\) (still assuming \(\mathsf {N}= \mathsf {N}'\) and \(\mathsf {L}= \mathsf {L}'\)).
Constant Number of Reconfigurations per Step. A first natural constraint on reconfiguration consists in bounding the number of changes in a reconfiguration step by a constant number. Recall that along executions, communication and reconfiguration steps strictly alternate.
Definition 4
Let \(k \in \mathbb {N}\). An execution \(\rho = (\mathsf {G}_i)_{0\le i\le r}\) of a reconfigurable broadcast network is kconstrained if for every index \(i<r\), it holds \({\mathsf {dist}(\mathsf {G}_i,\mathsf {G}_{i+1}) \le k}\).
Example 1
(Contd). For the synchronization problem, bounding the number of reconfigurations makes a difference. The sample execution from Fig. 2 is not 1constrained, and actually no 1constrained executions of that broadcast protocol can synchronize to \(\{ q_4,q_5,q_6 \}\). This can be shown by exhibiting and proving an invariant on the reachable configurations (see Lemma 10).
Beyond Constant Number of Reconfigurations per Step. Bounding the number of reconfigurations per step by a constant is somewhat restrictive, especially when this constant does not depend on the size of the network. We introduce other kinds of constraints here, for instance by bounding the number of reconfigurations by k on average along the execution, or by having a bound that depends on the number of nodes executing the protocol.
For a finite execution \(\rho = (\mathsf {G}_i)_{0\le i\le r}\) of a reconfigurable broadcast network, we write \(\mathtt {nb\_comm}(\rho )\) for the number of communication steps along \(\rho \) (notice that \(\lfloor r/2\rfloor \le \mathtt {nb\_comm}(\rho ) \le \lceil r/2\rceil \) since we require strict alternation between reconfiguration and communication steps), and \(\mathtt {nb\_reconf}(\rho )\) for the total number of edge reconfigurations in \(\rho \), that is \(\mathtt {nb\_reconf}(\rho ) = \sum _{i=0}^{r2} \mathsf {dist}(\mathsf {G}_i,\mathsf {G}_{i+1})\).
Definition 5
Let \(k\in \mathbb {N}\). An execution \(\rho \) of a reconfigurable broadcast network is said kbalanced if it starts and ends with a communication step, and satisfies \(\mathtt {nb\_reconf}(\rho ) \le k \cdot (\mathtt {nb\_comm}(\rho )1)\).
This indeed captures our intuition that along a kbalanced execution, reconfigurations on average update less than k links.
Finally, we will also consider two relevant ways to constrain reconfigurations depending on the size of the network: first locally, bounding the number of reconfigurations per node by a constant; second globally, bounding the total number of reconfigurations by a function of the number of nodes.
We first bound reconfigurations locally.
Definition 6
Let \(k \in \mathbb {N}\). An execution \(\rho = (\mathsf {G}_i)_{0\le i\le r}\) of a reconfigurable broadcast network is klocallyconstrained, if, for every node \(\mathsf {n}\) and for every index \(i<r\), \(\mathsf {dist}_{\mathsf {n}}(\mathsf {G}_i,\mathsf {G}_{i+1}) \le k\).
One may also bound the number of reconfigurations globally using bounding functions, that depend on the number of nodes in the network:
Definition 7
Let \(f :\mathbb {N}\rightarrow \mathbb {N}\) be a function. An execution \(\rho = (\mathsf {G}_i)_{0\le i\le r}\) of a reconfigurable broadcast network is fconstrained, if, writing n for the number of nodes in \(\mathsf {G}_0\), it holds \(\mathsf {dist}(\mathsf {G}_i,\mathsf {G}_{i+1}) \le f(n)\) for any \(i<r\).
Notice that if f is the constant function \(n\in \mathbb {N}\mapsto k\) for some \(k\in \mathbb {N}\), fconstrained executions coincide with kconstrained ones, so that our terminology is nonambiguous. Other natural bounding functions are nondecreasing and diverging. This way, the number of possible reconfigurations tends to infinity when the network size grows, i.e. \(\forall n.\ \exists k.\ f(k)\ge n\).
Remark 2
Coverability under constrained reconfigurations is easily observed to be equivalent to coverability with unconstrained reconfigurations: from an unconstrained execution, we can simply juxtapose extra copies of the protocol, which would perform extra communication steps so as to satisfy the constraint. When dealing with synchronization, this technique does not work since the extra copies would also have to synchronize to a target state. As a consequence, we only focus on synchronization in the rest of this paper.
2.3 Classification of Constraints
In this section, we compare our restrictions. We prove that, for the synchronization problem, klocallyconstrained and fconstrained reconfigurations, for diverging functions f, are equivalent to unconstrained reconfigurations. On the other hand, we prove that kconstrained reconfigurations are equivalent to kbalanced reconfigurations, and do not coincide with unconstrained reconfigurations.
Equivalence Between Unconstrained and LocallyConstrained Reconfigurations.
Lemma 8
Let \(\mathcal {P}\) be a broadcast protocol, \(F\subseteq Q\) be a target set, and f be a nondecreasing diverging function. If the reconfigurable broadcast network defined by \(\mathcal {P}\) has an initial execution synchronizing in \(F\), then it has an fconstrained initial execution synchronizing in \(F\).
Proof
We first prove the lemma for the identity function \(\mathsf {Id}\). More precisely, we prove that for an execution \(\rho = (\mathsf {G}_i)_{0\le i\le n}\), of the reconfigurable broadcast network, there exists a \(\mathsf {Id}\)constrained execution \(\rho ' = (\mathsf {G}'_j)_{0\le j\le m}\), whose last transition (if any) is a communication step, and such that for any control state q, \( \mathsf {G}_n _{q} = \mathsf {G}_m' _{q}\). We reason by induction on the length of the execution. The claim is obvious for \({n = 0}\). Suppose the property is true for all naturals less than or equal to some \(n \in \mathbb {N}\), and consider an execution \(\rho =(\mathsf {G}_i)_{0\le i\le n+1}\). The induction hypothesis ensures that there is an fconstrained execution \(\rho '=(\mathsf {G}'_j)_{0\le j\le m}\) with \( \mathsf {G}_n _{q} =  \mathsf {G}_m' _{q}\) for all q. If the last transition from \(\mathsf {G}_n\) to \(\mathsf {G}_{n+1}\) in \(\rho \) is a reconfiguration step, then the execution \(\rho '\) witnesses our claim. Otherwise, the transition from \(\mathsf {G}_n\) to \(\mathsf {G}_{n+1}\) is a communication step, involving a broadcasting node \(\mathsf {n}\) of \(\mathsf {G}_n\) labelled with \(q\), and receiving nodes \(\mathsf {n}_1\) to \(\mathsf {n}_r\) of \(\mathsf {G}_n\), respectively labelled with \(q_1\) to \(q_r\). By hypothesis, \(\mathsf {G}'_m\) also contains a node \(\mathsf {n}'\) labelled with \(q\) and r nodes \(\mathsf {n}'_1\) to \(\mathsf {n}'_r\), labelled with \(q_1\) to \(q_r\). We then add two steps after \(\mathsf {G}'_m\) in \(\rho '\): we first reconfigure the graph so that \(\mathsf {Neigh}_{\mathsf {G}'_{m+1}}(\mathsf {n}')=\{\mathsf {n}'_i \mid 0\le i\le r\}\), which requires changing at most \( \mathsf {G}_0 1\) links, and then perform the same broadcast/receive transitions as between \(\mathsf {G}_n\) and \(\mathsf {G}_{n+1}\).
For the general case of the lemma, suppose f is a nondecreasing diverging function. Further, let \(\rho = (\mathsf {G}_i)_{0\le i\le n}\) be an \(\mathsf {Id}\)constrained execution, and pick k such that \(f(k\cdot  \mathsf {G}_0 ) \ge  \mathsf {G}_0 \). Consider the initial configuration \(\mathsf {G}_0^k\), made of k copies of \(\mathsf {G}_0\), and the execution, denoted \(\rho ^k\), made of k copies of \(\rho \) running independently from each of the k copies of \(\mathsf {G}_0\) in \(\mathsf {G}_0^k\). Each reconfiguration step involves at most \( \mathsf {G}_0 \) links, so that \(\rho ^k\) is fconstrained. \(\square \)
Lemma 9
Let \(\mathcal {P}\) be a broadcast protocol with \(F\subseteq Q\) a target set. If the reconfigurable broadcast network defined by \(\mathcal {P}\) has an initial execution synchronizing in \(F\), then it has a 1locallyconstrained initial execution synchronizing in \(F\).
kConstrained and kBalanced Reconfigurations. We prove here that kconstrained and kbalanced reconfigurations are equivalent w.r.t. synchronization, and that they are strictly stronger than our other restrictions. We begin with the latter:
Lemma 10
There exists a broadcast protocol \(\mathcal {P}\) and a set \(F\subseteq Q\) of target states for which synchronization is possible from some initial configuration when unconstrained reconfigurations are allowed, and impossible, from every initial configuration when only 1constrained reconfigurations are allowed.
A protocol with this property is the one from Example 1, for which we exhibited a 2constrained synchronizing execution. It can be proved that no 1constrained synchronizing executions exist for this protocol, whatever the number of copies. We now prove the main result of this section:
Theorem 11
Let \(\mathcal {P}\) be a broadcast protocol and \(F\subseteq Q\). There exists a kconstrained initial execution synchronizing in \(F\) if, and only if, there exists a kbalanced initial execution synchronizing in \(F\).
Proof
The lefttoright implication is simple: if there is a kconstrained initial execution synchronizing in \(F\), w.l.o.g. we can assume that this execution starts and ends with a communication step; moreover, each reconfiguration step contains at most k edge reconfigurations, so that the witness execution is kbalanced.

\(p_0=0\);

\(p_{2i+1} = p_{2i}+k\) for \(i\le (n1)/2\) (this corresponds to a communication step);

\(p_{2i+2} = p_{2i+1}  \mathsf {dist}(\mathsf {G}_{2i+1},\mathsf {G}_{2i+2})\) for \(i\le (n1)/21\) (reconfiguration step).
That \(\rho \) is kbalanced translates as \(p_{n1} \ge 0\): the sequence \((p_i)_{0\le i\le n}\) stores the value of \(k\cdot \mathtt {nb\_comm}(\rho _{\le i})  \mathtt {nb\_reconf}(\rho _{\le i})\) for each prefix \(\rho _{\le i}\) of \(\rho \); being kbalanced means that \(p_{n}\ge k\), and since the last step is a communication step, this in turn means \(p_{n1}\ge 0\). On the other hand, in order to be kconstrained, it is necessary (but not sufficient) to have \(p_i\ge 0\) for all \(0\le i\le n\).
We build a kconstrained execution by shuffling several copies of \(\rho \). We actually begin with the case where \(k=1\), and then extend the proof to any k. We first compute how many copies we need. For this, we split \(\rho \) into several phases, based on the potential \((p_i)_{0\le i\le n}\) defined above. A phase is a maximal segment of \(\rho _{\le n1}\) (the prefix of \(\rho \) obtained by dropping the last (communication) step) along which the sign of the potential is constant (or zero): graphs \(\mathsf {G}_i\) and \(\mathsf {G}_j\) are in the same phase if, and only if, for all \(i\le l\le l'\le j\), it holds \(p_l\cdot p_{l'}\ge 0\). We decompose \(\rho \) as the concatenation of phases \((\rho _j)_{0\le j\le m}\); since \(\rho \) is kbalanced, m is even, and \(\rho _0\), \(\rho _m\), and all evennumbered phases are nonnegative phases (i.e., the potential is nonnegative along those executions), while all oddnumbered executions are nonpositive phases. Also, all phases end with potential zero, except possibly for \(\rho _m\). See Fig. 3 for an example of a decomposition into phases.
Lemma 12
For any phase \(\rho _i = \mathsf {G}_{b_i} \cdots \mathsf {G}_{e_i}\) of a 1balanced execution \(\rho = \mathsf {G}_0 \cdots \mathsf {G}_n\), there exists \(\kappa _i \le (e_ib_i)/2\) such that for any \(N \in \mathbb {N}\), there exists a 1constrained execution from \(\mathsf {G}_0^{{\kappa _i}} \oplus \mathsf {G}_{b_i}^N\) to \(\mathsf {G}_1^{{\kappa _i}} \oplus \mathsf {G}_{e_i}^N\).
Proof
We handle nonnegative and nonpositive phases separately. In a nonnegative phase, we name repeated reconfiguration step any reconfiguration step that immediately follows another (possibly from the previous phase) reconfiguration step (so that if there are four consecutive reconfiguration steps, the last three are said repeated); similarly, we name repeated communication step any communication step that is immediately followed (possibly in the next phase) by another communication step (hence the first three of fours consecutive communication steps are repeated).
We first claim that any nonnegative phase contains at least as many repeated communication steps as it contains repeated reconfiguration steps. Indeed, any nonrepeated communication step in a nonnegative phase is necessarily followed by a nonrepeated reconfiguration step, and conversely, and nonnegative phases have at least as many communication steps as they have reconfiguration steps.
As a consequence, we can number all repeated reconfiguration steps from 1 (earliest) to \(\kappa _i\) (latest), for some \(\kappa _i\), and similarly for repeated communication steps. Clearly enough, in a nonnegative phase, for any \(1\le j\le \kappa _i\), the repeated communication step numbered j occurs before the repeated reconfiguration step carrying the same number.

the first copy starting in \(\mathsf {G}_{b_i}\) follows the execution \(\rho _i\) until reaching the repeated reconfiguration step number 1. That reconfiguration step cannot be performed immediately as it follows another reconfiguration step. Notice that during this stage, this copy has taken at least one repeated communication step, numbered 1;

the second copy then follows \(\rho _i\) until reaching its first repeated communication step (which must occur before the first repeated reconfiguration step). It takes this communication step, then allowing the first copy to perform its first repeated reconfiguration step;

this simulation continues, each time having the \(l+1\)st copy of the system taking its jth repeated communication step in order to allow the lth copy to perform its jth repeated reconfiguration step. Nonrepeated steps can always be performed individually by each single copy. Also, the first copy may always take repeated communication steps not having a corresponding reconfiguration step, as in the first stage of this part.
Notice that the number of copies involved in this process is arbitrary. The process lasts as long as some copies may advance within phase \(\rho _i\). Hence, when the process stops, all copies of the original system either have reached the end of \(\rho _i\), or are stopped before a repeated reconfiguration step. For the copies in the latter situation, we use the copies starting from \(\mathsf {G}_0\). It remains to prove that having \(\kappa _i\) such copies is enough to make all processes reach the end of \(\rho _i\).
For this, we first assume that the potential associated with \(\rho _i\) ends with value zero. This must be the case of all phases except the last one, which we handle after the general case. We first notice that in the execution we are currently building, any repeated communication step performed by any (but the very first) copy that started from \(\mathsf {G}_{b_i}\) is always followed by a repeated reconfiguration step. Similarly, nonrepeated communication steps of any copy is followed by a nonrepeated broadcast step of the same copy. As a consequence, the potential associated with the global execution we are currently building never exceeds the total number of repeated communication steps of performed by the first copy; hence it is bounded by \(\kappa _i\), whatever the number N of copies involved. As a consequence, at most \(\kappa _i\) communication steps are sufficient in order to advance all copies that started from \(\mathsf {G}_{b_i}\) to the end of \(\rho _i\).
Finally, the case of the last phase \(\rho _m\) (possibly ending with positive potential) is easily handled, since it has more communication steps than reconfiguration steps.
The proof for nonpositive phases is similar.
Pick a 1balanced execution \(\rho = \mathsf {G}_0 \cdots \mathsf {G}_n\), and decompose it into phases \(\rho _1 \cdots \rho _m\). For each phase \(\rho _i\), we write \(\kappa _i\) for the total number of repeated reconfiguration steps, and we let \(\kappa =\sum _{1\le i\le m} \kappa _i\) for the total number of repeated reconfiguration steps along \(\rho \). Notice that \(\kappa \le n/2\).
Lemma 13
For every 1balanced execution \(\rho = \mathsf {G}_0 \cdots \mathsf {G}_n\), and for every \(N \in \mathbb {N}\), there exists a 1constrained execution from \(\mathsf {G}_1^N \oplus \mathsf {G}_{e_m}^{\kappa N}\) to \(\mathsf {G}_n^{N+\kappa N}\).
Combining the above two lemmas, we obtain the following proposition, which refines the statement of the Theorem 11:
Proposition 14
For every 1balanced execution \(\rho = \mathsf {G}_0 \cdots \mathsf {G}_n\) and every \(N \ge \kappa ^2+\kappa \), there exists a 1constrained execution from \(\mathsf {G}_0^N\) to \(\mathsf {G}_n^N\).
We finally extend this result to \(k>1\). In this case, splitting \(\rho \) into phases is not as convenient as when \(k=1\): indeed, a nonpositive phase might not end with potential zero (because communication steps make the potential jump by k units). Lemma 12 would not hold in this case.
We circumvent this problem by first shuffling k copies of \(\rho \) in such a way that reconfigurations can be gathered into groups of size exactly k. This way, we can indeed split the resulting execution into nonnegative and nonpositive phases, always considering reconfigurations of size exactly k; we can then apply the techniques above in order to build a synchronizing kconstrained execution. This completes our proof. \(\square \)
3 Parameterized Synchronization Under Reconfiguration Constraints
3.1 Undecidability for kConstrained Reconfiguration
Although synchronization is decidable in PTIME [6, 11] for reconfigurable broadcast networks, the problem becomes undecidable when reconfigurations are kconstrained.
Theorem 15
The synchronization problem is undecidable for reconfigurable broadcast networks under kconstrained reconfigurations.
Proof

control states encode the control state of the 2counter machine;

counter states are used to model counter values: for each counter \(c_j\in \{c_1,c_2\}\), we have a state \(\textsf {zero}\smash {_{j}} \) and a state \(\textsf {one}\smash {_{j}} \). The value of counter \(c_j\) in the simulation will be encoded as the number of edges in the communication topology between the control node and counter nodes in state \(\textsf {one}\smash {_{j}} \); moreover, we will require that control nodes have no communication links with counter nodes in state \(\textsf {zero}\smash {_{j}} \). Incrementations and decrementations can then be performed by creating a link with a node in \(\textsf {zero}\smash {_{j}} \) and sending this node to \(\textsf {one}\smash {_{j}} \), or sending a \(\textsf {one}\smash {_{j}} \)node to \(\textsf {zero}\smash {_{j}} \) and removing the link.

we cannot avoid having several control nodes; instead, given a synchronizing execution of the broadcast protocol, we will select one control node and show that it encodes a correct execution of the 2counter machine;

in order to reach a synchronizing configuration, the selected control node will have to perform at least as many reconfiguration steps as broadcast steps. Because we consider 1constrained runs, it will perform exactly the same number of reconfiguration steps as broadcast steps, so that no useless/unexpected reconfigurations may take place during the simulation;

control nodes will periodically run special broadcasts that would send any connected nodes (except nodes in state \(\textsf {one}\smash {_{j}} \)) to a sink state, thus preventing synchronization. This way, we ensure that particular control node is clean. Initially, we require that control nodes have no connections at all.
We now present the detailed construction, depicted at Figs. 4, 5, 6 and 7. Each state of the protocol is actually able to synchronize with all the messages. Some transitions are not represented on the figures, to preserve readability: all nodes with no outgoing transitions (i.e., state \(L_\textsf {halt}\) corresponding to the halting state, as well as states \(\textsf {zero}\smash {_{j}} '\) and \(\textsf {done}\smash {_{i}} \)) actually carry a selfloop synchronizing on all messages; all other omitted transitions lead to a sink state, which is not part of the target set.
Let us explain the intended behaviour of the incrementation module of Fig. 5: when entering the module, our control node \(\mathsf {n}\) in state L is linked to \(c_1\) counter nodes in state \(\textsf {one}\smash {_{1}} \) and to \(c_2\) counter nodes in state \(\textsf {one}\smash {_{2}} \); it has no other links. Moreover, all auxiliary nodes are either in state \(\textsf {free}\smash {_{i}} \) or in state \(\textsf {done}\smash {_{i}} \). Running through the incrementation module from L will use one counter node \(\mathsf {m}\) in state \(\textsf {zero}\smash {_{j}} \) (which is used to effectively encode the increase of counter \(c_j\)) and four auxiliary nodes \(a_1\) (initially in state \(\textsf {free}\smash {_{1}} \)), \(a_2\) (in state \(\textsf {free}\smash {_{2}} \)), and \(a_3\) and \(a'_3\) (in state \(\textsf {free}\smash {_{3}} \)).

a link is created between the control node \(\mathsf {n}\) and the first auxiliary node \(a_1\), followed by a message exchange \(!!\textit{iinit}\);

a link is created between \(\mathsf {n}\) and \(\mathsf {m}\), and node \(a_1\) broadcasts Open image in new window ;

a link is created between \(\mathsf {n}\) and \(a_2\), and \(\mathsf {n}\) broadcasts \(!!\textit{iask}_j\), which is received by both \(a_2\) and \(\mathsf {m}\);

a link is created between \(\mathsf {n}\) and \(a_3\); node \(\mathsf {m}\) sends its acknowledgement \(!!\textit{iack}_j\) to \(\mathsf {n}\);

a link is created between \(\mathsf {n}\) and \(a'_3\); node \(\mathsf {n}\) sends \(!!\textit{iok}_j\), received by \(\mathsf {m}\), \(a_2\), \(a_3\) and \(a'_3\);

the link between \(\mathsf {n}\) and \(a_1\) is removed, and \(a_2\) sends Open image in new window ;

the link between \(\mathsf {n}\) and \(a_2\) is removed, and \(a_3\) sends Open image in new window ;

the link between \(\mathsf {n}\) and \(a_3\) is removed, and \(a'_3\) sends Open image in new window ;

finally, the link between \(\mathsf {n}\) and \(a'_3\) is removed, and \(\mathsf {n}\) sends \(!!\textit{iexit}\).
After this sequence of steps, node \(\mathsf {n}\) has an extra link to a counter node in state \(\textsf {one}\smash {_{j}} \), which indeed corresponds to incrementing counter \(c_j\). Moreover, no nodes have been left in an intermediary state. A similar analysis can be done for the second module, which implements the zerotest and decrementation. This way, we can prove that if the twocounter machine has a halting computation, then there is an initial configuration of our broadcast protocol from which there is an execution synchronizing in the set F formed of the halting control state and states \(\textsf {one}\smash {_{j}} \), \(\textsf {zero}\smash {_{j}} '\) and \(\textsf {done}\smash {_{i}} \).
It now remains to prove the other direction. More precisely, we prove that from a 1constrained synchronizing execution of the protocol, we can extract a synchronizing execution in some normal form, from which we derive a halting execution of the twocounter machine.
Fix a 1constrained synchronizing execution of the broadcast network. First notice that when a control node \(\mathsf {n}\) reaches some state L (the first node of an incrementation or decrementation module), it may only be linked to counter nodes in state \(\textsf {one}\smash {_{j}} \): this is because states L can only be reached by sending \(!!\textit{iexit}\), \(!!\textit{dexit}\), \(!!\textit{texit}\), or \(!!\textit{start}\). The former two cases may only synchronize with counter nodes in state \(\textsf {one}\smash {_{j}} \); in the other two cases, node \(\mathsf {n}\) may be linked to no other node. Hence, for a control node \(\mathsf {n}\) to traverse an incrementation module, it must get links to four auxiliary nodes (in order to receive the four \(\textit{fr}\) messages), those four links must be removed (to avoid reaching the sink state), and an extra link has to be created in order to receive message iack \(_j\). In total, traversing an incrementation module takes nine communication steps and at least nine reconfiguration steps. Similarly, traversing a decrementation module via any of the two branches takes at least as many reconfiguration steps as communication steps. In the end, taking into account the initial \(!!\textit{start}\) communication step, if a control node \(\mathsf {n}\) is involved in \(B_\mathsf {n}\) communication steps, it must be involved in at least \(B_\mathsf {n}1\) reconfiguration steps.
Assume that every control node \(\mathsf {n}\) is involved in at least \(B_\mathsf {n}\) reconfiguration steps: then we would have at least as many reconfiguration steps as communication steps, which in a 1constrained execution is impossible. Hence there must be a control node \(\mathsf {n}_0\) performing \(B_{\mathsf {n}_0}\) communication steps and exactly \(B_{\mathsf {n}_0}1\) reconfiguration steps. As a consequence, when traversing an incrementation module, node \(\mathsf {n}_0\) indeed gets connected to exactly one new counter node, which indeed must be in state \(\textsf {one}\smash {_{j}} \) when \(\mathsf {n}_0\) reaches the first state of the next module. Similarly, traversing a decrementation/zerotest module indeed performs the expected changes. It follows that the sequence of steps involving node \(\mathsf {n}_0\) encodes a halting execution of the twocounter machines. \(\square \)
The 1constrained executions in the proof of Theorem 15 have the additional property that all graphs describing configurations are 2boundedpath configurations. For \(K \in \mathbb {N}\) a configuration \(\mathsf {G}\) is a Kboundedpath configuration if the length of all simple paths in \(\mathsf {G}\) is bounded by K. Note that a constant bound on the length of simple paths implies that the diameter (i.e. the length of the longest shortest path between any pair of vertices) is itself bounded. The synchronization problem was proved to be undecidable for broadcast networks without reconfiguration when restricting to Kboundedpath configurations [6]. In comparison, for reconfigurable broadcast networks under kconstrained reconfigurations, the undecidability result stated in Theorem 15 can be strengthened into:
Corollary 16
The synchronization problem is undecidable for reconfigurable broadcast networks under kconstrained reconfigurations when restricted either to boundedpath configurations, or to boundeddiameter configurations.
3.2 Decidability Results
fConstrained and kLocallyConstrained Reconfigurations. From the equivalence (w.r.t. synchronization) of klocallyconstrained, fconstrained and unconstrained executions (Lemmas 8 and 9), and thanks to Theorem 2, we immediately get:
Corollary 17
Let \(k \in \mathbb {N}\) and \(f:\mathbb {N}\rightarrow \mathbb {N}\) be a nondecreasing diverging function. The synchronization problem for reconfigurable broadcast networks under klocallyconstrained (resp. fconstrained) reconfigurations is decidable in PTIME.
Bounded Degree Topology. We now return to kconstrained reconfigurations, and explore restrictions that allow one to recover decidability of the synchronization problem. We further restrict kconstrained reconfigurations by requiring that the degree of nodes remains bounded, by 1; in other terms, communications correspond to rendezvous between the broadcasting node and its single neighbour.
Theorem 18
The synchronization problem is decidable for reconfigurable broadcast networks under kconstrained reconfiguration when restricted to 1boundeddegree topologies.
Sketch of Proof. The proof consists in transforming the synchronization problem above into a reachability problem for some Petri net. The Petri net has two kinds of places (plus a few auxiliary places): one place for each state of the protocol, representing isolated nodes (i.e., nodes having no neighbours), and one place for each pair of states of the protocol, representing pairs of connected nodes. Since we restrict to degree1 topologies, any node of the network is in one of those two configurations. Places representing isolated nodes are simply called isolated places in the sequel, while places corresponding to pairs of connects nodes are called connected places.
An initialization phase stores tokens in the places described above, so as to represent the initial configuration. In a second phase, the Petri net simulates an execution of the reconfigurable broadcast network: communication steps and (kconstrained) reconfiguration steps are easily encoded as transitions of this Petri net: communication steps correspond to moving tokens from one place to the place obtained by updating the states as prescribed by the transitions of the broadcast protocol. Atomic reconfigurations may create or remove links, either consuming two tokens in isolated places and adding a token in the corresponding connected place, or the other way around. We use k auxiliary places in order to count the number of atomic reconfigurations, in order to enforce the kconstraint.
Finally, the Petri net may enter a terminal phase, where it checks synchronization by absorbing all tokens that lie in (isolated or connected) places corresponding to target states. In the end, the simulated execution has been synchronizing if, and only if, no tokens remain in any of the main states.
4 Conclusion
Restricting reconfigurations in reconfigurable broadcast networks is natural to better reflect mobility when communications are frequent enough and the movement of nodes is not chaotic. In this paper, we studied how constraints on the number of reconfigurations (at each step and for each node, at each step and globally, or along an execution) change the semantics of networks, in particular with respect to the synchronization problem, and affect its decidability. Our main results are the equivalence of kconstrained and kbalanced semantics, the undecidability of synchronization under kconstrained reconfigurations, and its decidability when restricting to 1boundeddegree topologies.
As future work, we propose to investigate, beyond the coverability and synchronization problems, richer objectives such as cardinality reachability problems as in [5]. Moreover, for semantics with constrained reconfigurations that are equivalent to the unconstrained one as far as the coverability and synchronization problems are concerned, it would be worth studying the impact of the reconfiguration restrictions (e.g. klocallyconstrained or fconstrained) on the minimum number of nodes for which a synchronizing execution exists, and on the minimum number of steps to synchronize.
Footnotes
 1.
For a finite set S and \(1\le k\le  S \), we let \(\mathcal P_k(S)=\{ T\subseteq S\mid  T =k\}\).
References
 1.Bertrand, N., Fournier, P., Sangnier, A.: Playing with probabilities in reconfigurable broadcast networks. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 134–148. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642548307_9CrossRefGoogle Scholar
 2.Bertrand, N., Fournier, P., Sangnier, A.: Distributed local strategies in broadcast networks. In: CONCUR 2015, LIPIcs, vol. 42, pp. 44–57. LZI (2015). http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.44
 3.Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of parameterized verification. In: Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2015)CrossRefGoogle Scholar
 4.Bouyer, P., Markey, N., Randour, M., Sangnier, A., Stan, D.: Reachability in networks of register protocols under stochastic schedulers. In: ICALP 2016, LIPIcs, vol. 55, pp. 106:1–106:14. LZI (2016). http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.106
 5.Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS 2012, LIPIcs, vol. 18, pp. 289–300. LZI (2012). http://dx.doi.org/LIPIcs.FSTTCS.2012.289
 6.Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642153754_22CrossRefGoogle Scholar
 7.Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods Syst. Des. 9(1–2), 105–131 (1996). https://doi.org/10.1007/FBF00625970CrossRefGoogle Scholar
 8.Esparza, J.: Keeping a crowd safe: on the complexity of parameterized verification (invited talk). In: STACS 2014, LIPIcs, vol. 25, pp. 1–10. LZI (2014). http://dx.doi.org/10.4230/LIPIcs.STACS.2014.1
 9.Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352–359. IEEE Computer Society Press (1999). http://dx.doi.org/10.1109/LICS.1999.782630
 10.Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous sharedmemory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124–140. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642397998_8CrossRefGoogle Scholar
 11.Fournier, P.: Parameterized verification of networks of many identical processes. Thèse de doctorat, Université Rennes 1, France (2015)Google Scholar
 12.German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992). https://doi.org/10.1145/146637.146681MathSciNetCrossRefzbMATHGoogle Scholar
 13.Hague, M.: Parameterised pushdown systems with nonatomic writes. In: FSTTCS 2011, LIPIcs, vol. 13, pp. 457–468. LZI (2011). http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2011.457
 14.Minsky, M.: Computation: Finite and Infinite Machines. Prentice Hall, Englewood Cliffs (1967)zbMATHGoogle Scholar
 15.Suzuki, I.: Proving properties of a ring of finitestate machines. Inf. Process. Lett. 28(4), 213–214 (1988). https://doi.org/10.1016/00200190(88)902116MathSciNetCrossRefzbMATHGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.