Giorgio Delzanno

Arnaud Sangnier

Riccardo Traverso

Gianluigi Zavattaro

On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks

We investigate the impact of dynamic topology reconfiguration on the complexity of verification problems for models of protocols with broadcast communication. We first consider reachability of a configuration with a given set of control states and show that parameterized verification is decidable with polynomial time complexity. We then move to richer queries and show how the complexity changes when considering properties with negation or cardinality constraints.

Introduction

Broadcast communication is often used in networks in which individual nodes have no precise information about the underlying connection topology (e.g. ad hoc wireless networks). As shown in [START_REF] Delzanno | On the Power of Cliques in the Parameterized verification of Ad Hoc Networks[END_REF][START_REF] Merro | An observational theory for Mobile Ad Hoc Networks[END_REF][START_REF] Merro | A timed calculus for wireless systems[END_REF][START_REF] Nanz | A Framework for security analysis of mobile wireless networks[END_REF][START_REF] Singh | A process calculus for Mobile Ad Hoc Networks[END_REF][START_REF] Singh | Query-Based model checking of Ad Hoc Network Protocols[END_REF], this type of communication can naturally be specified in models of computation in which a network configuration is represented as a graph and in which individual nodes run an instance of a common protocol. A protocol typically specifies a sequence of control states in which a node can send a message (emitter role), wait for a message (receiver role), or perform an update of its internal state.

Already at this level of abstraction, verification of protocols with broadcast communication turns out to be a very difficult task. A formal account of this problem is given in [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF][START_REF] Delzanno | On the Power of Cliques in the Parameterized verification of Ad Hoc Networks[END_REF], where parameterized control state reachability is proved to be undecidable in an automata-based protocol model in which configurations are arbitrary graphs. The parameterized control state reachability problem consists in verifying the existence of an initial network configuration (with unknown size and topology) that may evolve into a configuration in which at least one node is in a given control state. If such a control state represents a protocol error, then this problem naturally expresses (the complement of) a safety verification task in a setting in which nodes have no information a priori about the size and connection topology of the underlying network.

In presence of non-deterministic reconfigurations of the network topology during an execution, parameterized control state reachability becomes decidable [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF]. Reconfiguration models spontaneous node movement, i.e. each node can dynamically connect (resp. disconnect) to (resp. from) any other node in the network. Furthermore, it also models the dynamic addition (resp. removal) of nodes by means of connection to the network of a previously disconnected idle node (resp. the definitive disconnection of a previously connected node). The decidability proof in [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF] does not give exact complexity bounds of the problem; it simply gives a reduction to Petri net coverability, an ExpSpace-complete problem [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF][START_REF] Rackoff | The Covering and Boundedness Problems for Vector Addition Systems[END_REF]. The precise complexity of parameterized reachability was left as an open problem in [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF].

In this paper we present a comprehensive analysis of the complexity of reachability problems for reconfigurable broadcast networks. We start by generalizing the problem by considering reachability queries defined over assertions that: (i) check the presence or absence of control states in a given configuration generated by some initial configuration, and (ii) cardinality queries that define lower and upper bounds for the number of occurrences of control states in a reachable configuration. In any case the problems require, at least in principle, the exploration of an infinite-state space. Indeed they are formulated for arbitrary initial configurations, and upper bounds to the number of processes per control state are not mandatory in case (ii). We then move to the analysis of the complexity of the considered problems by showing that reachability queries for constraints that only check for the presence of a control state can be checked in polynomial time. When considering both constraints for checking presence and absence of control states the problem turns out to be NP-complete. Finally, we show that the problem becomes PSpace-complete for cardinality queries.

Related Work. As mentioned in the introduction no precise complexity bounds were given for the parameterized control state reachability problem proved decidable in [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF] via a reduction to Petri net marking coverability. In the present paper we attack this problem for different types of reachability queries. The interreducibility of control state reachability in models with dynamic reconfiguration, spontaneous mobility, and node-, message-, or link-failures has been formally studied in [START_REF] Delzanno | Verification of Ad Hoc Networks with Node and Communication Failures[END_REF]. Based on the results in [START_REF] Delzanno | Verification of Ad Hoc Networks with Node and Communication Failures[END_REF], the PTime-algorithm presented in the current paper can be applied not only to reconfigurable networks but also to a variety of protocols models with failures.

Symbolic backward exploration procedures for network protocols specified in graph rewriting have been presented in [START_REF] Joshi | Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems[END_REF] (termination guaranteed for ring topologies) and [START_REF] Saksena | Graph grammar modeling and verification of Ad Hoc Routing Protocols[END_REF] (approximations without termination guarantees). Decidability issues for broadcast communication in unstructured concurrent systems (or, equivalently, in fully connected networks) have been studied, e.g., in [START_REF] Esparza | On the verification of Broadcast Protocols[END_REF], whereas verification of unreliable communicating FIFO systems has been studied, e.g., in [START_REF] Abdulla | Verifying programs with unreliable channels[END_REF].

To our knowledge, exact algorithms (and relative complexity) for parameterized verification has not been studied in previous work on graph-based models of synchronous or asynchronous broadcast communication like [START_REF] Prasad | A Calculus of Broadcasting Systems[END_REF][START_REF] Singh | A process calculus for Mobile Ad Hoc Networks[END_REF][START_REF] Singh | Query-Based model checking of Ad Hoc Network Protocols[END_REF][START_REF] Nanz | A Framework for security analysis of mobile wireless networks[END_REF][START_REF] Ene | A broadcast based calculus for Communicating Systems[END_REF][START_REF] Fehnker | Modelling and verification of the LMAC protocol for wireless sensor networks[END_REF][START_REF] Godskesen | A calculus for Mobile Ad Hoc Networks[END_REF][START_REF] Merro | An observational theory for Mobile Ad Hoc Networks[END_REF][START_REF] Merro | A timed calculus for wireless systems[END_REF][START_REF] Lanese | An operational semantics for a calculus for wireless systems[END_REF][START_REF] Saksena | Graph grammar modeling and verification of Ad Hoc Routing Protocols[END_REF][START_REF] Joshi | Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems[END_REF].

Notes. Sketches of the proofs are included in the body of the paper; detailed proofs are given in appendix.

A Model for Reconfigurable Broadcast Networks 2.1 Syntax and semantics

Our model for reconfigurable broadcast networks is defined in two steps. We first define graphs used to denote network configurations and then define protocols running on each node. The label of a node denotes its current control state. Finally, we give a transition system for describing the interaction of a vicinity during the execution of the same protocol on each node.

Definition 1 A Q-graph is a labeled undirected graph γ = V, E, L , where V is a finite set of nodes, E ⊆ V × V \ { v, v | v ∈ V } is a finite set of edges,
and L is a labeling function from V to a set of labels Q.

We use L(γ) to represent all the labels present in γ (i.e. the image of the function L). The nodes belonging to an edge are called the endpoints of the edge. For an edge u, v in E, we use the notation u ∼ γ v and say that the vertices u and v are adjacent one to another in the graph γ. We omit γ, and simply write u ∼ v, when it is made clear by the context.

Definition 2 A process is a tuple P = Q, Σ, R, Q 0 , where Q is a finite set of control states, Σ is a finite alphabet, R ⊆ Q × ({!!a, ??a | a ∈ Σ}) × Q is the transition relation, and Q 0 ⊆ Q is a set of initial control states.
The label !!a [resp. ??a] represents the capability of broadcasting [resp. receiving] a message a ∈ Σ. For q ∈ Q and a ∈ Σ, we define the set R a (q) = {q ′ ∈ Q | q, ??a, q ′ ∈ R} which contains the states that can be reached from the state q when receiving the message a. We assume that R a (q) is non empty for every a and q, i.e. nodes always react to broadcast messages. Local transitions (denoted by the special label τ ) can be derived by using a special message m τ such that q, ??m τ , q ′ ∈ R implies q ′ = q for every q, q ′ ∈ Q (i.e. receivers do not modify their local states). Given a process P = Q, Σ, R, Q 0 , in the corresponding Reconfigurable Broadcast Network (RBN) a configuration is a Q-graph and an initial configuration is a Q 0 -graph. We use Γ [resp. Γ 0 ] to denote the set of configurations [resp. initial configurations] associated to P. Note that even if Q 0 is finite, there are infinitely many possible initial configurations (the number of Q 0 -graphs). We assume that each node of the graph is a process that runs a common predefined protocol defined by a communicating automaton with a finite set Q of control states. Communication is achieved via selective broadcast, which means that a broadcasted message is received by the nodes which are adjacent to the sender. Non-determinism in reception is modeled by means of graph reconfigurations. We next formalize this intuition.

Given a process P = Q, Σ, R, Q 0 , a reconfigurable broadcast network is defined by the transition system RBN (P) = Γ, →, Γ 0 where the transition relation →⊆ Γ × Γ is such that: for γ, γ ′ ∈ Γ with γ = V, E, L , we have γ → γ ′ iff γ ′ = V, E ′ , L ′ and one of the following conditions holds:

Broadcast E ′ = E and ∃v ∈ V s.t. L(v), !!a, L ′ (v) ∈ R and L ′ (u) ∈ R a (L(u))
for every u ∼ v, and L(w) = L ′ (w) for any other node w.

Graph reconfiguration

E ′ ⊆ V × V \ { v, v | v ∈ V } and L = L ′ .
We use → * to denote the reflexive and transitive closure of →. RBN is an adequate formalism to abstractly represent broadcast communication with features like spontaneous mobility, node-, message-and link-failures.

Parameterized Reachability Problems

Given a process P = Q, Σ, R, Q 0 , a cardinality constraint ϕ over P is a formula which defines lower and upper bounds for the number of occurrences of each control state in a configuration. The formulae are defined by the following grammar, where a ∈ N, q ∈ Q, and b ∈ (N \ {0}) ∪ {+∞}:

ϕ ::= a ≤ #q < b | ϕ ∧ ϕ | ϕ ∨ ϕ | ¬ϕ
We denote by CC the class of cardinality constraints, by CC[≥ 1] the class in which negation is forbidden and atomic proposition have only the form #q ≥ 1 (there exists at least one occurrence of q), and finally by CC[≥ 1, = 0] the class of cardinality constraints as in CC[≥ 1] but where atoms can also be of the form #q = 0. Given a configuration γ = V, E, L of P and q ∈ Q, we denote by #γ(q) the number of vertices in γ labeled by q, that is #γ

(q) = |{v ∈ V | L(v) = q}|. The satisfaction relation |= for atomic formulas is defined as follows γ |= a ≤ #q < b iff a ≤ #γ(q) < b.
It is defined in the natural way for compound formulas.

We are now ready to state the cardinality reachability problem (CRP):

Input: A process P with RBN (P) = Γ, →, Γ 0 and a cardinality constraint ϕ.

Output: Yes, if ∃γ 0 ∈ Γ 0 and γ 1 ∈ Γ s.t. γ 0 → * γ 1 and γ 1 |= ϕ; no, otherwise.

If the answer to this problem is yes, we will write P |= ♦ϕ. Note that when dealing with the complexity of this problem we will suppose that the size of the input is the size of the process defined by the product of the number of states times the number of edges added to the size of the formula in which the integer values are encoded in unary.

We use the term parameterized to remark that the initial configuration is not fixed a priori. In fact, the only constraint that we put on the initial configuration is that the nodes have labels taken from Q 0 without any information on their number or connection links.

As a special case we can define the control state reachability problems studied in [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF] as the CRP for the simple constraint #q ≥ 1 (i.e. is there a reachable configuration in which the state q is exposed?). Similarly, we can define the target reachability problem studied in [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF] as an instance of CRP in which control states that must not occur in a target configuration are constrained by formulas like #q = 0.

According to our semantics, the number of nodes stays constant in each execution starting from the same initial configuration. As a consequence, when fixing the initial configuration γ 0 , we obtain finitely many possible reachable configurations. Thus, checking if there exists γ 1 reachable from a given γ 0 s.t. γ 1 |= ϕ for a constraint ϕ is a decidable problem. On the other hand, checking the parameterized version of the reachability problem is in general much more difficult. E.g. consider constraints of the form #q ≥ 1: CRP is undecidable for a semantics without non-deterministic graph reconfigurations [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF]. In [START_REF] Delzanno | Parameterized verification of Ad Hoc Networks[END_REF] it is also proved that CRP for the same class of constraints is decidable. However, the proposed decidability proof is based on a reduction to the problem of coverability in Petri nets which is known to be ExpSpace-complete [START_REF] Rackoff | The Covering and Boundedness Problems for Vector Addition Systems[END_REF][START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF]. Since no lowerbound was provided, the precise complexity of CRP with simple constraints was left as an open problem that we close in this paper by showing that it is PTimecomplete.

CRP restricted to constraints in CC[≥ 1]

In this section, we study CRP restricted to CC[≥ 1]. These constraints characterize configurations in which a given set of control states is present but they cannot express neither the absence of states nor the number of their occurrences. We first give a lower bound for this problem.

Proposition 1 CRP restricted to CC[≥ 1] is PTime-hard.
Sketch of proof. The idea for the proof is based on a LogSpace-reduction from the Circuit Value Problem (CVP), which is know to be PTime-complete [START_REF] Ladner | The circuit value problem is logspace complete for P[END_REF]. The protocol P built from the CVP instance has an initial state for each of the input variables which broadcasts its truth assignment, and another one for each gate of the input circuit. In the sub-protocol associated to individual gates, a process waits for messages representing inputs and then broadcasts messages representing outputs in such a way that CVP is satisfied iff P |= ♦#ok ≥ 1, where ok is a state reached only when the last gate produces the expected output.

We now show that CRP restricted to CC[≥ 1] is in PTime. We first observe that, in order to decide if control state q can be reached, we can focus our attention on initial configurations in which the topology is fully connected (i.e. graphs in which all pairs of nodes are connected). Indeed, graph reconfigurations can be applied to non-deterministically transform a topology into any other one.

Another key observation is that if the control state q is reached once from the initial configuration γ 0 , then it can be reached an arbitrary number of times by considering larger and larger initial configurations γ ′ 0 . More specifically, the initial configuration γ ′ 0 is obtained by replicating several times the initial graph γ 0 . The replicated parts are then connected in all possible ways (to obtain a fully connected topology). We can then use dynamic reconfiguration in order to mimic parallel executions of the original system and reach a configuration with several repeated occurrences of state q.

For what concerns constraints in CC[≥ 1] this property of CRP avoids the need of counting the occurrences of states. We just have to remember which states can be generated by repeatedly applying process rules. As a consequence, in order to define a decision procedure for checking control state reachability we can take the following assumptions: (i) forget about the topology underlying the initial configuration; (ii) forget about the number of occurrences of control states in a configuration; (iii) consider a single symbolic path in which at each step we apply all possible rules whose preconditions can be satisfied in the current set and then collect the resulting set of computed states.

We now formalize the previous observations. Let P = Q, Σ, R, Q 0 be a process with RBN (P) = Γ, →, Γ 0 and let Reach(P) be the set of reachable Algorithm 1: Computing the set of control states reachable in a RBN

Input : P = Q, Σ, R, Q 0 a p
S := Q 0 oldS := ∅ while S = oldS do oldS := S f o r a l l q 1 , !!a, q 2 ∈ R such t h a t q 1 ∈ oldS do S := S ∪ {q 2 } ∪ {q ′ ∈ Q | q, ??a, q ′ ∈ R ∧ q ∈ oldS } end f o r end while control states equals to {q ∈ Q | ∃γ ∈ Γ 0 .∃γ ′ ∈ Γ. s.t. γ → * γ ′ and q ∈ L(γ ′ )}.
We will now prove that Algorithm 1 computes Reach(P). Let S be the result of the Algorithm 1 (note that this algorithm necessarily terminates because the while-loop is performed at most |Q| times). We have then the following lemma.

Lemma 1 The two following properties hold:

(i) There exist two configurations γ 0 ∈ Γ 0 and γ ∈ Γ such that γ 0 → * γ and L(γ) = S.

(ii) S = Reach(P).

Proof: We first prove (i). We denote by S 0 , S 1 , . . . , S n the content of S after each iteration of the loop of the Algorithm 1. We recall that an undirected

graph γ = V, E, L is complete if v, v ′ ∈ E for all v, v ′ ∈ V .
We will now consider the following statement: for all j ∈ {0, . . . , n}, for all k ∈ N, there exists a complete graph γ j,k = V, E, L in Γ verifying the two following points:

1. L(γ j,k ) = S j and for each q ∈ S j , the set {v ∈ V | L(v) = q} has more than k elements (i.e. for each element q of S j there are more than k nodes in γ j,k labeled with q), 2. there exits γ 0 ∈ Γ 0 such that γ 0 → * γ j,k .

To prove this statement we reason by induction on j. First, for j = 0, the property is true, because for each k ∈ N, the graph γ 0,k corresponds to the complete graphs where each of the initial control states appears at least k times. We now assume that the property is true for all naturals smaller than j (with j < n) and we will show it is true for j + 1. We define C a as the set

{ q 1 , !!a, q 2 , q, ??a, q ′ ∈ R × R | q 1 , q ∈ S j } and M its cardinality. Let k ∈ N and let N = k + 2 * k * M .
We consider the graph γ j,N where each control state present in S j appears at least N times (such a graph exists by the induction hypothesis). From γ j,N , we build the graph γ j+1,k obtained by repeating k times the following operations:

• for each pair q 1 , !!a, q 2 , q, ??a, q ′ ∈ C a , select a node labeled by q 1 and one labeled by q and update their label respectively to q 2 and q ′ (this simulates a broadcast from the node labeled by q 1 received by the node labeled q in the configuration in which all the other nodes have been disconnected thanks to the reconfiguration and reconnected after). Note that the two selected nodes can communicate because the graph is complete.

By applying these rules it is then clear that γ j,N → * γ j+1,k and also that γ j+1,k verifies the property 1 of the statement. Since by induction hypothesis, we have that there exists γ 0 ∈ Γ 0 such that γ 0 → * γ j,N , we also deduce that γ 0 → * γ j+1,k , hence the property 2 of the statement also holds. From this we deduce that (i) is true.

To prove (ii), from (i) we have that S ⊆ Reach(P) and we now prove that Reach(P) ⊆ S. Let q ∈ Reach(P). We show that q ∈ S by induction on the minimal length of an execution path γ 0 → * γ such that γ 0 ∈ Γ 0 and q ∈ L(γ). If the length is 0 then q ∈ Q 0 hence also q ∈ S. Otherwise, let γ ′ → γ be the last transition of the execution. We have that there exists q 1 ∈ L(γ ′ ) such that q 1 , !!a, q ∈ R [or q 1 , q 2 ∈ L(γ ′ ) such that q 1 , !!a, q 3 , q 2 , ??a, q ∈ R]. By induction hypothesis we have that q 1 ∈ S [or q 1 , q 2 ∈ S]. By construction, we can conclude that also q ∈ S. Since constraints in CC[≥ 1] check only the presence of states and do not contain negation, given a configuration γ and a constraint ϕ in CC[≥ 1] such that γ |= ϕ, we also have that γ ′ |= ϕ for every γ ′ such that L(γ) ⊆ L(γ ′ ). Moreover, given a process P, by definition of Reach(P) we have that L(γ) ⊆ Reach(P) for every reachable configuration γ, and by Lemma 1 there exists a reachable configuration γ f such that L(γ f ) = Reach(P). Hence, to check P |= ♦ϕ it is sufficient to verify whether γ f |= ϕ for such a configuration γ f . This can be done algorithmically as follows: once the set Reach(P) is computed, check if the boolean formula obtained from ϕ by replacing each atomic constraint of the form #q ≥ 1 by true if q ∈ Reach(P) and by false otherwise is valid. This allows us to state the following theorem.

Theorem 1 CRP restricted to CC[≥ 1] is PTime-complete.
Proof: The lower bound is given by Proposition 1. To obtain the upper bound, it suffices to remark that the Algorithm 1 is in PTime since it requires at most |Q| iterations each one requiring at most |R| 2 look-ups (of active broadcast/receive transitions) for computing new states to be included, and also that evaluating the validity of a boolean formula can be done in polynomial time.

CRP restricted to constraints in CC[≥ 1, = 0]

We consider now decidability and complexity of CRP for constraints in CC[≥ 1, = 0]. This kind of queries can be used to specify that a given control state is not present in a configuration (using atomic constraints of the form #q = 0).

Proposition 2 CRP for constraints in CC[≥ 1, = 0] is NP-hard.
Sketch of proof. The proof is based on a reduction of the boolean satisfiability problem (SAT), which is known to be NP-complete. The encoding of the SAT instance for a boolean formula Φ with variables in V is based on a protocol with only local transitions from a single initial state into states that encode truth assignments in {v, v | v ∈ V }. A CC[≥ 1, = 0] query is then built in order to guarantee that there are no contradicting assignments to variables. The query also ensures that the selected assignments satisfy the formula Φ, where positive literals v are replaced by #v ≥ 1 and negative literals ¬v are replaced by #v = 0.

We will now give an algorithm in NP to solve CRP for constraints in CC[≥ 1, = 0]. As for Algorithm 1, this new algorithm works on sets of control states. The algorithm works in two main phases. In a first phase it generates an increasing sequence of sets of control states that can be reached in the considered process definition. At each step the algorithm adds the control states obtained from the application of the process rules to the current set of labels. Unlike the Algorithm 1, this new algorithm does not merge different branches, i.e. application of distinct rules may lead to different sequences of sets of control states. In a second phase the algorithm only removes control states applying again process rules in order to reach a set of control states that satisfies the given constraint.

Algorithm 2: Solving CRP for constraints in CC[≥ 1, = 0]

Input : P = Q, Σ, R, Q 0 a p r o c e s s and ϕ a c o n s t r a i n t o v e r P i n CC[≥ 1, = 0] Output : Does P |= ♦ϕ ? guess S 0 , . . . , Sm, T 1 , . . . , Tn ⊆ Q with m, n ≤ |Q| i f S 0 ⊆ Q 0 then return f a l s e f o r a l l i ∈ {0, . . . , m -1} do i f S i+1 ∈ postAdd(P, S i ) then return f a l s e end f o r T 0 = Sm f o r a l l i ∈ {0, . . . , n -1} do i f T i+1 ∈ postDel(P, T i )
then return f a l s e end f o r I f Tn s a t i s f i e s ϕ then return true e l s e return f a l s e For a process P = Q, Σ, R, Q 0 and a set S ⊆ Q, we define the operator postAdd(P, S) ⊆ 2 Q as follows: S ′ ∈ postAdd(P, S) if and only if the two following conditions are satisfied: (i) S ⊆ S ′ and (ii) for all q ′ ∈ S ′ \ S, there exists a rule q, !!a, q ′ ∈ R such that q ∈ S (q ′ is produced by a broadcast) or there exist rules p, !!a, p ′ and q, ??a, q ′ ∈ R such that q, p ∈ S and p ′ ∈ S ′ (q ′ is produced by a reception). In other words, all the states in S ′ ∈ postAdd(P, S) are either in S or states obtained from the application of broadcast/reception rules to labels in S. Similarly, we define the operator postDel(P, S) ⊆ 2 Q as follows: S ′ ∈ postDel(P, S) if and only if S ′ ⊆ S and one of the following conditions hold: either S \ S ′ = ∅ or [S \ S ′ = {q} and there exists a rule q, !!a, q ′ ∈ R such that q ′ ∈ S ′ ] or [S \ S ′ = {q} and there exist two rules p, !!a, p ′ , q, ??a, q ′ ∈ R such that p, p ′ , q ′ ∈ S ′ (q is consumed by a broadcast)] or [S \ S ′ = {p, q} and there exist two rules p, !!a, p ′ , q, ??a, q ′ ∈ R such that p ′ , q ′ ∈ S ′ (p and q are consumed by a broadcast)]. Finally, we say that a set S ⊆ Q satisfies an atom #q = 0 if q ∈ S and it satisfies an atom #q ≥ 1 if q ∈ S; satisfiability for composite boolean formulae of CC[≥ 1, = 0] is then defined in the natural way. We have then the following Lemma.

Lemma 2 There is an execution of Algorithm 2 which answers YES on input P and ϕ iff P |= ♦ϕ.

It is then clear that each check performed by the Algorithm 2 (i.e. S 0 ⊆ Q 0 and S i+1 ∈ postAdd(P, S i ) and T i+1 ∈ postAdd(P, T i ) and T n satisfies ϕ) can be performed in polynomial time in the size of the process P and of the formula ϕ and since m and n are smaller than the number of control states in P, we deduce the following theorem (the lower bound being given by Proposition 2). Theorem 2 CRP for constraints in CC[≥ 1, = 0] is NP-complete.

Complexity of CRP in Full CC

In this section we will show that CRP for the entire class of cardinality constraints CC is PSpace-complete. First we prove the lower bound.

Proposition 3 CRP is PSpace-hard.

Proof: We use a reduction from reachability in 1-safe Petri nets. A Petri net N is a tuple N = P, T, m 0 , where P is a finite set of places, T is a finite set of transitions t, such that • t and t • are multisets of places (pre-and postconditions of t), and m 0 is a multiset of places that indicates how many tokens are located in each place in the initial net marking. Given a marking m, the firing of a transition t such that • t ⊆ m leads to a new marking m ′ obtained as

m ′ = m \ • t ∪ t • .
A Petri net P is 1-safe if in every reachable marking every place has at most one token. Reachability of a specific marking m 1 from the initial marking m 0 is decidable for Petri nets, and PSpace-complete for 1-safe nets [START_REF] Cheng | Complexity Results for 1-Safe Nets[END_REF]. Given a 1-safe net N = P, T, m 0 and a marking m 1 , we encode the reachability problem as a CRP problem for the process P and cardinality constraint ϕ defined next. For each place p ∈ P , we introduce control states p 1 and p 0 to denote the presence or absence of the token in p, respectively. Furthermore, we introduce a special control state ok. The control state is used to control the net simulation. Transitions of the controller are depicted in the upper part of Fig. 1. The first rule of the controller selects the current transition to simulate. The simulation of the transition t with • t = {p 1 , . . . , p n } and t • = {q 1 , . . . , q m } is defined via two sequences of messages (we denote • t and t • as sets instead of multisets because we are considering a 1-safe net and it is hence not possible that a transition consumes or produces more than one token for each place). The first one is used to remove the token from p 1 , . . . , p n , whereas the second one is used to put the token in q 1 , . . . , q m . To guarantee that every involved place reacts to the protocol -i.e. messages are not lost-the controller waits for an acknowledgement from each of them. Transitions of places are depicted in the lower part of Fig. 1. It is not restrictive to assume that there is only one token in the initial marking m 0 (otherwise we add an auxiliary initial place and a transition that generates m 0 by consuming the initial token). Let p 0 be such a place. We define the initial states Q 0 of the process P as {p 0 1 , ok} ∪ {p 0 | p ∈ P \ {p 0 }}, in order to initially admit control states representing the controller, the presence of the initial token, and the absence of tokens in other places. The reduction does not work if there are several copies of controller nodes and/or place representations (i.e. p 1 , p 0 , . . .) interacting during a simulation (interferences between distinct nodes representing controllers/places may lead to incorrect results). However we can ensure that the reduction is accurate by checking the number of occurrences of states exposed in the final configuration: it is sufficient to check that only one controller and only one node per place in the net are present. Besides making this check, the cardinality constraint ϕ should also verify that the represented net marking coincides with m 1 . Namely, we define ϕ as follows:

ϕ = p∈ m1,t∈T #p 1 = 1 ∧ #p 0 = 0 ∧ #aux a t,p = 0 ∧ #aux b t,p = 0 ∧ q ∈ m1,t∈T #q 1 = 0 ∧ #q 0 = 1 ∧ #aux a t,q = 0 ∧ #aux b t,q = 0 ∧ #ok = 1∧ t∈T (#ok t = 0) ∧ t∈T,q∈P #a t,q = 0 ∧ #b t,q = 0 ∧ #a ack t,q = 0 ∧ #b ack t,q = 0
Since the number of nodes stays constant during an execution, the post-condition specified by ϕ is propagated back to the initial configuration. Therefore, if the protocol satisfies CRP for ϕ, then in the initial configuration there must be one single controller node with state ok, and for each place p one single node with either state p 1 or state p 0 . Under this assumption, it is easy to check that a run of the protocol corresponds precisely to a firing sequence in the 1-safe net. Thus an execution run satisfies ϕ if and only if the corresponding firing sequence reaches the marking m 1 . We now show that there exists an algorithm to solve CRP in PSpace. The main idea is to use a symbolic representation of configurations in which the behavior of a network is observed exactly for a fixed number of nodes only. For all the other nodes, we only maintain the control state they are labeled with and not their precise number.

Without loss of generality, we consider for simplicity only processes with Q 0 = {q 0 }, as multiple initial states can be encoded through local transitions from q 0 . Given a process P = Q, Σ, R, {q 0 } and a cardinality constraint ϕ over P we denote by val(ϕ) ∈ N the largest natural constant that appears in ϕ. We then denote by psize(ϕ) the natural |Q| * val(ϕ). Intuitively psize(ϕ) is the number of witness nodes we keep track of: we reserve val(ϕ) processes to each control state that may appear in ϕ.

A symbolic configuration for P and ϕ is then a pair θ = v, S where v ∈ Q psize(ϕ) is a vector of psize(ϕ) elements of Q and S ⊆ Q. For q ∈ Q, we then write #v(q) to indicate the number of occurrences of q in the vector v. Note that by definition 0 ≤ #v(q) ≤ psize(ϕ) for every q ∈ Q and that q∈Q #v(q) = psize(ϕ). This allows us to describe the set of configurations [[θ]] ⊆ Γ characterized by a symbolic configuration θ = v, S as follows: we have γ ∈ [[θ]] if and only #γ(q) > #v(q) for every q ∈ S and #γ(q) = #v(q) for every q ∈ Q \ S. Hence a symbolic configuration θ = v, S represents all the configurations such that the number of occurrences of a control state q is greater than the number of occurrences of q in v if q ∈ S, or equal when q / ∈ S.

We will say that a symbolic configuration θ satisfies the cardinality constraint ϕ, written θ |= ϕ, iff γ |= ϕ for all γ ∈ [[θ]]. We use Θ to represent the set of symbolic configurations. We make the following non restrictive assumptions: there is no constraint on the unique initial state q 0 in the cardinality constraints, the only outgoing transitions from the state q 0 are local transitions (labelled with τ ), in the symbolic configurations v, S we always have q 0 ∈ S, and the initial configuration θ 0 is (q 0 , . . . , q 0 ), {q 0 } . The most important assumption is the first one about the absence of constraints on q 0 : it is needed to guarantee the correctness of our symbolic procedure. For instance, consider a process P = {q 0 }, Σ, R, {q 0 } and a cardinality constraint ϕ of the form 1 ≤ #q 0 < 2. We have then psize(ϕ) = 2 and the symbolic configurations are of the form (q 0 , q 0 ), S . It is then obvious that all the symbolic configurations do not satisfy ϕ while the initial concrete configuration with only one node does. The above assumptions are not restrictive because given a process P = Q, Σ, R, {q 0 } and a cardinality constraint ϕ, we can define a new process

P ′ = Q ′ , Σ, R ′ , {q init } where Q ′ = Q ∪ {q init } and R ′ = R ∪ { q init ,
τ, q 0 }, i.e. q init is a new initial state from which the process is enabled to go to q 0 thanks to a local transition. As there is no constraint in ϕ about q init it is immediate to prove the following Lemma:

Lemma 3 P |= ♦ϕ if and only if P ′ |= ♦ϕ.
We now define a relation on the symbolic configurations to represent the effect that process rules have on symbolic configurations. Let P = Q, Σ, R, {q 0 } be a process, ϕ a cardinality constraint and θ the associated set of symbolic configurations. For each rule r ∈ R of form q, !!a, q ′ , we define the symbolic transition relation r ⊆ Θ × Θ as follows, we have v, S r v ′ , S ′ if and only if at least one of the two following conditions holds:

1. (broadcast from a state in v) there exists i ∈ {1, . . . , psize(ϕ)} such that v[i] = q and v ′ [i] = q ′ (i.e. the sending process switches state according to r) and:

• for all j ∈ {1, . . . , psize(ϕ)} \ {i} we have either v[j] = v ′ [j] or there exists q r , ??a, q ′ r ∈ R such that v[j] = q r and v ′ [j] = q ′ r (i.e. other processes in the pool may or may not react to the broadcast);

• for each q s ∈ Q \ {q 0 }: -if q s ∈ S ′ \ S then there exists q ′ s ∈ S and q ′ s , ??a, q s ∈ R, -if q s ∈ S \ S ′ then there exists q ′ s ∈ S ′ and q s , ??a, q ′ s ∈ R.

2.

(broadcast from a state in S) we have q ∈ S and q ′ ∈ S ′ (note that we could have that q ∈ S ′ or q / ∈ S ′ ), and the following conditions hold:

• for all j ∈ {1, . . . , psize(ϕ)} we have either v[j] = v ′ [j] or there exists q r , ??a, q ′ r ∈ R such that v[j] = q r ∧ v ′ [j] = q ′ r ; • for each q s ∈ Q \ {q, q ′ }, we have:

if q s ∈ S ′ \ S then there exists q ′ s , ??a, q s ∈ R with q ′ s ∈ S, -if q s ∈ S \ S ′ then there exists q s , ??a, q ′ s ∈ R with q ′ s ∈ S ′ .

We denote by ⊆ Θ × Θ the relation such that θ θ ′ if and only if there exists a rule r ∈ R such that θ r θ ′ , and * represents its reflexive and transitive closure. The intuition behind this construction is that we do not perform any abstraction on the states present in the vector v but only on the states present in S, this because the states present in v are used as witnesses to satisfy the cardinality constraint ϕ.

As an example, for psize(ϕ) = 5, let (q 1 , q 2 , q 0 , q 0 , q 0 ), {q 0 , q 1 , q 2 } be a symbolic configuration, and q 1 , !!a, q ′ 1 and q 2 , ??a, q ′ 2 be two transition rules. With a broadcast from a process in the vector we may reach, among others, (q ′ 1 , q 2 , q 0 , q 0 , q 0 ), {q 0 , q 1 , q 2 } , (q ′ 1 , q ′ 2 , q 0 , q 0 , q 0 ), {q 0 , q 1 , q 2 , q ′ 2 } , or (q ′ 1 , q ′ 2 , q 0 , q 0 , q 0 ), {q 0 , q 1 , q ′ 2 } , whereas a broadcast from a process in the set may lead to (q 1 , q 2 , q 0 , q 0 , q 0 ), {q 0 , q 1 , q 2 , q ′ 1 } , (q 1 , q 2 , q 0 , q 0 , q 0 ), {q 0 , q 1 , q ′ 1 , q ′ 2 } , (q 1 , q ′ 2 , q 0 , q 0 , q 0 ), {q 0 , q 1 , q 2 , q ′ 1 , q ′ 2 } , or (q 1 , q ′ 2 , q 0 , q 0 , q 0 ), {q 0 , q ′ 1 , q ′ 2 } . We will now prove that the symbolic configurations are well-suited to solve CRP. First, we show that if a symbolic configuration which satisfies ϕ is reachable from the initial symbolic configuration, then there is a concrete configuration reachable from an initial configuration in γ 0 which also satisfies ϕ. This ensures a sound reasoning on symbolic configurations. Sketch of proof. For a symbolic θ = v, S in Θ and N ∈ N, we denote by

[[θ]] N = {γ ∈ [[θ]] | ∀q ∈ S.#γ(q) > (N + #v(q))}, i.e.

the set of configurations which belong to [[θ]

] in which for each q ∈ S, there are at least N vertices (in addition to those already in the vector v). Note that with this definition

[[θ]] 0 = [[θ]].
We then can prove the following property: given θ ∈ Θ such that θ 0 * θ, there exists N ∈ N such that for all γ ∈ [[θ]] N , there exists an initial configuration γ 0 ∈ Γ 0 such that γ 0 → * γ. To show that this property is true, we reason by induction on the length of the execution choosing the N adequately at each step of the induction. Then if there exists θ ∈ Θ such that θ 0 * θ and θ |= ϕ, then there exists γ 0 ∈ θ 0 and γ ∈ [[θ]] such that γ 0 → * γ, and by the definition of |= for symbolic configuration we deduce also that γ |= ϕ. Hence P |= ♦ϕ.

We will now show that a reasoning on symbolic configurations leads to completeness, in other words that if there is a reachable configuration that satisfies the cardinality constraint ϕ, then there is a reachable symbolic configuration that satisfies ϕ.

Lemma 5 If P |= ♦ϕ, then there exists θ ∈ Θ such that θ 0 * θ and θ |= ϕ.

Sketch of proof.

In order to prove this Lemma, we need to introduce some auxiliary notations. Given a configuration γ ∈ Γ, we define ↑ q0 γ as the set

{γ ′ ∈ Γ | ∀q ∈ Q \ {q 0 }. #γ ′ (q) = #γ(q)}.
The above definition is needed because we could reach a configuration γ which does not have enough processes to be represented by a symbolic configuration, but we can complete it by adding new vertices labelled by the initial state q 0 in order to solve the problem. We can then prove the following property by induction on the length of the concrete execution: for γ 0 ∈ Γ 0 and γ ∈ Γ such that γ 0 → * γ, for all θ ∈ Θ verifying

↑ q0 γ ∩ [[θ]] = ∅, we have θ 0 * θ.
Basically, this property stipulates that given a reachable configuration γ, each symbolic configuration θ whose semantics [[θ]] contains γ (modulo processes in state q 0 ) is also reachable. The next step consists in proving that if γ ∈ Γ is a configuration satisfying γ |= ϕ then there exists θ ∈ Θ such that ↑ q0 γ ∩ [[θ]] = ∅ and θ |= ϕ. This can be proved providing an algorithm that builds θ = v, S such that, for each q ∈ Q, either the processes in state q can be exactly represented within v only when #γ(q) ≤ val(ϕ), or #v(q) = val(ϕ) and q ∈ S when #γ(q) > val(ϕ) (i.e. v is not large enough, recall that, apart for the states q 0 used to fill the "holes" in v, we reserve only up to val(ϕ) processes per state in v). Consider, e.g., a process with states Q = {q 0 , q 1 , q 2 }, the formula ϕ = 0 ≤ #q 1 < 3 ∧ 1 ≤ #q 2 < +∞ and the configuration with five processes γ = q 1 , q 2 , q 2 , q 2 , q 2 such that γ |= ϕ. The symbolic configuration θ obtained is then (q 1 , q 2 , q 2 , q 2 , q 0 , q 0 , q 0 , q 0 , q 0 ), {q 0 , q 2 } .

Since P |= ♦ϕ, there exists an initial configuration γ 0 ∈ Γ 0 and a configuration γ ∈ Γ such that γ 0 → * γ and γ |= ϕ. By the second property we know there exists θ ∈ Θ such that ↑ q0 γ ∩ [[θ]] = ∅ and θ |= ϕ, and the first property allows us to say that θ 0 * θ.

We will now explain why CRP is in PSpace. The main idea is that we can reason on the graph of symbolic configurations. Note that by definition, since Θ = Q psize(ϕ) × 2 Q , the total number of symbolic configurations is |Θ| = |Q| psize(ϕ) * 2 |Q| . Furthermore, checking whether a symbolic configuration satisfies a cardinality constraint can be done in PTime and checking whether two symbolic configurations belong to the symbolic transition relation can also be done in PTime. The PSpace algorithm (which is in reality an NPSpace algorithm) at each step guesses a new symbolic configuration, checks whether it is reachable from the previous guessed one and verifies whether it satisfies ϕ. When it encounters a symbolic configuration that satisfies ϕ, it returns that P |= ♦ϕ. Note that this algorithm needs only to store the number of configurations it has seen until now, and when this number reaches |Q| psize(ϕ) * 2 |Q| , it means that the algorithm have seen all the symbolic configurations. Hence to store this number and the current and next symbolic configurations, the algorithm needs polynomial space (a number smaller than |Q| psize(ϕ) * 2 |Q| can be stored into a counter which requires at most psize(ϕ) * log (|Q|) + |Q| log (2) space). Finally, lemmas 4 and 5 ensure us that such an algorithm is sound and complete and from Proposition 3 we have also a lower bound for CRP. Hence we deduce the main result of this paper.

Theorem 3 CRP is PSpace-complete.

A Proofs

A.1 Proof of Proposition 1

The proof is based on a LogSpace-reduction from the Circuit Value Problem (CVP) which is know to be PTime-complete [START_REF] Ladner | The circuit value problem is logspace complete for P[END_REF]. CVP is defined as follows: given an acyclic Boolean circuit with k input variables, m boolean gates (of type and, or, not), a single output variable and a truth assignment for the input variables, is the value of the output equal to a given boolean value?

Assume an instance of CVP C with input/output/intermediate value names taken from a finite set V N . We denote by v 1 , . . . , v k ∈ V N the inputs and by v ∈ V N the output. Furthermore, each gate g is represented by its signature

g(⊙, i 1 , i 2 , o) with i 1 , i 2 , o ∈ V N and ⊙ ∈ {∨, ∧} or by g(¬, i, o) with i, o ∈ V N .
Finally, let b 1 , . . . , b k ∈ {true, f alse} be a truth assignment for the inputs and b ∈ {true, f alse} the value for the output to be tested.

The process P C associated to C has two types of initial states: q 0 (init nodes), and g (gate nodes) for each gate g of C. A node in state q 0 broadcasts (an arbitrary number of) messages that model the initial assignments to input variables. Since the assignment is fixed, broadcasting these messages several times (or receiving them from different initial nodes) does not harm the correctness of the encoding. When receiving an evaluation for their inputs (from an initial node or another gate node), a gate node evaluates the corresponding boolean function and then repeatedly broadcasts the value of the corresponding output. Since C is acyclic, once computed, the output value remains always the same (i.e. recomputing it does not harm). Finally, reception of a value v for output z sends a q 0 node into state ok. Reachability of an output value v reduces then to CRP for the process P C with ok the control state to be reached.

Formally, the process rules are defined as follows. For i ∈ {1, . . . , k}, we have rules q 0 , !!(v i = b i ), q 0 and q 0 , ??(v = b), ok . They model the assignment of value v i to input x i and reception of output value v.

For gate g(⊙, i 1 , i 2 , o) and for each assignment

α = b ′ 1 , b ′ 2 (with b ′ 1 , b ′ 2 ∈ {true, f alse}) of values to i 1 , i 2 (
a constant number for each gate), we associate the following subprotocol:

g g α 1 g α 2 g α f ??(i 1 = b ′ 1 ) ??(i 2 = b ′ 2 ) ??(i 2 = b ′ 2 ) ??(i 1 = b ′ 1 ) !!(o = b ′ 1 ⊙ b ′ 2 )
(Self-loops associated to receptions for which there are no explicit rules are omitted). We use a similar encoding for a not gate. Consider now the resulting process P C = Q, Σ, R, {q 0 }∪{g | g is a gate in C} with corresponding transition system RBN = Γ, →, Γ 0 . There exists γ ∈ Γ 0 and γ ′ in Γ s.

A.2 Proof of Proposition 2

The proof is based on a reduction of the boolean satisfiability problem (SAT) which is known to be NP-complete. Let Φ be a boolean formula in conjunctive normal form over the set of variables V = {v 1 , . . . , v k }. We define a process P with initial state q 0 and the following set of rules

R = { q 0 , τ, v | v ∈ V } ∪ { q 0 , τ, v | v ∈ V }.
From Φ, we build a constraint ϕ ∧ ψ where ϕ is the formula obtained from Φ by replacing each positive literal v by #v ≥ 1 and each negative literal ¬v by #v ≥ 1 and

ψ = k i=1 (#v i ≥ 1 ∧ #v i = 0) ∨ (#v i = 0 ∧ #v i ≥ 1)
. The former constraint is the natural encoding of the input propositional formula whereas the latter assigns a consistent interpretation to the control state labels v i and v i as assignments to the propositional variable v i . The constraint ϕ ∧ ψ is a formula in CC.

A node in the initial state q 0 makes a guess for the boolean valuation of a variable v by moving to state v [resp. to v] if the associated chosen value is true [resp. false]. The formula ψ ensures that no contradictory valuation is generated by stating that for each variable v in V only one type of control state v or v is chosen. Assume that the formula Φ is satisfiable and let {b 1 , . . . , b k } ∈ {true, false} k be an interpretation over the variables {v 1 , . . . , v k } that satisfies it. From an initial configuration γ 0 with k nodes, it is possible to reach a configuration γ such that γ |= ψ and for all 1

≤ i ≤ k if b i = true then γ ′ |= #v i ≥ 1 else γ ′ |= #v i = 0. γ |= ϕ ∧ ψ
clearly holds here. Vice versa, if there exists a computation that reaches a configuration that satisfies ϕ ∧ ψ, then we have m ≥ k nodes whose labels correspond to a consistent interpretation of the variables in V and which satisfies Φ.

A.3 Proof of Lemma 2

Let P = Q, Σ, R, Q 0 a process with RBN (P) = Γ, →, Γ 0 and ϕ a constraint over P in CC. First we assume that the Algorithm 2 answers YES on input P and ϕ. This means that there exists S 0 , . . . , S m , T 0 , T 1 , . . . , T n such that 1 ≤ m, n ≤ |Q| and S 0 ⊆ Q 0 , and for all i ∈ {0, . . . , m -1}, S i+1 ∈ postAdd(P, S i ) and T 0 = S m and for all i ∈ {0, . . . , n -1}, T i+1 ∈ postDel(P, T i ). We will now prove that there exists two configurations γ 0 ∈ Γ 0 and γ ∈ Γ such that γ 0 → * γ and L(γ) = T n . First, as reasoning the same way we did in the proof of Lemma 1, we can deduce that for any k ∈ N \ {0}, there exists γ 0 ∈ Γ 0 and a complete graph γ k = V, E, L in Γ such that L(γ k ) = S m and for every q ∈ S m the set {v ∈ V | L(v) = q} has more than k elements. Now we are going to prove that for any j ∈ {0, . . . , n}, for all k ∈ N \ {0}, there is a complete graph γ j,k such that:

1. L(γ j,k ) = T j and for each q ∈ S j , the set {v ∈ V | L(v) = q} has more than k elements (i.e. for each element q of S j there are more than k nodes in γ j,k labelled with q), 2. there exits γ 0 ∈ Γ 0 such that γ 0 → * γ j,k .

To prove this statement we reason by induction on j. For j = 0, since the statement holds for S m , it holds also for T 0 = S m . We now assume that the property is true for all naturals smaller than j (with j < n) and we will show it is true for j + 1. We consider now the set T j \ T j+1 (assuming it is not empty, otherwise the property trivially holds). By property of the operator postDel, we have T j+1 ⊆ T j . Now let k ∈ N, the graph γ j+1,k is obtained from γ j,k+1 as follows:

• if T j+1 \T j = {q} and there exists a rule q, !!a, q ′ ∈ R such that q ′ ∈ T j+1 ], then this rule is applied to all the nodes labelled by q; first each node is isolated with the reconfiguration rule, then the broadcast rule is performed and then the complete graph is rebuilt. Note that the application of this rule consecutively will only increase the number of nodes labelled by q ′ which were already present in γ j,N ;

• if T j+1 \ T j = {q} and there exist two rules p, !!a, p ′ , q, ??a, q ′ ∈ R such that p, p ′ , q ′ ∈ T j+1 (q is consumed by a broadcast), then all the nodes labelled by q are isolated together with a node labelled by p so that all these nodes are connected, then p broadcast a sending all the other nodes in q ′ and finally the complete graph is rebuilt; as a consequence there is no more nodes labelled by q, the number of nodes labelled by q ′ and p ′ have increased and the number of nodes labelled by p has decreased of one unit;

• if T j+1 \T j = {p, q} and there exist two rules p, !!a, p ′ , q, ??a, q ′ ∈ R such that p ′ , q ′ ∈ T j+1 (p and q are consumed by a broadcast), then as for the second case, we first eliminate all the nodes labelled by q by isolating them together with one node labelled by p, and then all the nodes labelled by p can be eliminated the same way it is done in the first case we considered.

By applying these rules it is then clear that γ j,k+1 → * γ j+1,k and also that γ j+1,k verifies the property 1 of the statement. Since by induction hypothesis, we have that there exists γ 0 ∈ Γ 0 such that γ 0 → * γ j,k+1 , we also deduce that γ 0 → * γ j+1,k , hence the property 2 of the statement also holds. Hence if the Algorithm 2 returns YES on input P and ϕ, we deduce that there exist a reachable configuration γ ∈ Γ such that L(γ) = T n and since T n satisfies ϕ, we also have that γ |= ϕ, hence P |= ♦ϕ. We now assume that there exists two configurations γ 0 ∈ Γ 0 and γ ∈ Γ such that γ 0 → + γ (the case γ 0 = γ can be easily verified) and γ |= ϕ. Hence there exists γ 1 , . . . , γ k ∈ Γ such that γ 0 → + γ 1 . . . → + γ k with γ k = γ and for all i ∈ {1, . . . , k}, exactly one broadcast rule has been applied between γ i and γ i+1 . From this execution we build a sequence of set of control states (S ′ i ) 0≤i≤k such that S ′ 0 = L(γ 0 ) and for all 0

≤ i ≤ k -1, S ′ i+1 = S ′ i ∪ L(γ i )
. By definition of the broadcast rule and of the operator postAdd, we deduce that S ′ i+1 ∈ postAdd(P, S ′ i ). From this sequence, we can furthermore extract a subsequence (S i ) 0≤i≤m such that for all 0 ≤ i ≤ m -1, S i+1 ∈ postAdd(P, S i ) and S i+1 = S i and for all 0 ≤ j ≤ k, there exists 0 ≤ i ≤ m such that S ′ j = S i . Since we have S i ⊂ S i+1 for all 0 ≤ i ≤ m -1, we deduce that necessarily m ≤ |Q|. Now we build another sequence of control states (T ′ i ) 0≤i≤k such that T ′ 0 = S m and for all 0

≤ i ≤ k -1, T ′ i+1 = T ′ i \ E i where for all 0 ≤ i ≤ k -1, E i = {q ∈ L(γ i ) | ∃j > i s.t. q ∈ L(γ j )}.
In other words, to build T ′ i+1 from T ′ i we delete the control states q that are present in γ i and will never be present in any γ j for j > i. We recall that by construction for all 1 ≤ i ≤ k, we have L(γ i ) ⊆ T ′ 0 and hence by construction of the sequence (T ′ i ) 0≤i≤k we have necessarily L(γ) = T ′ k . By definition of the broadcast rule and of the operator postDel, we also deduce that T ′ i+1 ∈ postDel(P, T ′ i ). From this sequence, we can furthermore extract a subsequence (T i ) 0≤i≤n such that for all 0 ≤ i ≤ n -1, T i+1 ∈ postDel(P, T i ) and T i+1 = T i and for all 0 ≤ j ≤ k, there exists 0 ≤ i ≤ n such that T ′ j = T i . Since we have T i+1 ⊂ T i for all 0 ≤ i ≤ n -1, we deduce that necessarily n ≤ |Q| and also we have T (n) = L(γ). Since γ |= ϕ, we deduce that T n satisfies ϕ and consequently we have proved that there is an execution of Algorithm 2 which answers YES on input P and ϕ.

A.4 Proof of Lemma 3

Assume P |= ♦ϕ, then there are a configuration γ 0 and a configuration γ of P such that γ 0 → * γ and γ |= ϕ. In P ′ we can take the initial configuration γ ′ 0 with the same number of nodes as in γ 0 , assume that all the node begin to fire the transition q init , τ, q 0 (hence all the nodes will be labeled by q 0 ) and then perform the same execution as in P, hence P ′ |= ♦ϕ. Now assume that P ′ |= ♦ϕ, hence there are an initial configuration γ ′ 0 and a configuration γ ′ of P ′ such that γ ′ 0 → * γ ′ and γ ′ |= ϕ. It is possible to simulate in P almost the same execution (without the use of the rule q init , τ, q 0 ) by taking as initial configuration in P the configurations which have as cardinality the number of γ ′ which are not labelled by q init and thus obtaining an execution which leads to a configuration which satisfies φ.

A.5 Proof of Lemma 4

For a symbolic θ = v, S in Θ and N ∈ N, we denote by [[θ]] N = {γ ∈ [[θ]] | ∀q ∈ S.#γ(q) > (N + #v(q))}, i.e. the set of configurations which belong to [[θ]] in which for each q ∈ S, there are at least N vertices (in addition to those already in the vector v). Note that with this definition [[θ]] 0 = [[θ]]. We then have the following lemma.

Lemma 6 For all θ ∈ Θ such that θ 0 * θ, there exists N ∈ N such that for all γ ∈ [[θ]] N , there exists an initial configuration γ 0 ∈ Γ 0 such that γ 0 → * γ.

Proof: Let θ ∈ Θ such that θ 0 * θ. Then there exists θ 1 , . . . , θ m in Θ such that θ 0 θ 1 . . . θ m and θ m = θ. We will prove the statement of the Lemma by induction on the length of this symbolic execution. The base case, when m = 0, is obvious since we have [[θ 0 ]] ⊆ Γ 0 , it is then sufficient to take N = 0. Now let m > 0 and assume the property is true for all i ∈ {0, . . . , m-1}, we will prove it holds for θ m . First, by hypothesis of induction, we have that there exists N m-1 such that for all γ ∈ [[θ m-1 ]] Nm-1 , there exists an initial configuration γ 0 ∈ Γ 0 such that γ 0 → * γ. Since θ m-1 θ m , there exists a rule r ∈ R of the form q 1 , !!a, q 2 such that θ m-1 r θ m . We now proceed by a case analysis on the application of the rule r to obtain the symbolic configuration θ m = v ′ , S ′ from θ m-1 = v, S .

First, assume the sending process is in the vector v. There exists i ∈ {1, . . . , psize(ϕ)} such that v[i] = q 1 and v ′ [i] = q 2 . Let N m = (N m-1 + 1) * (|S \ S ′ | + 1) (where |S \ S ′ | denotes the cardinality of the set S \ S ′ ). Note that N m > N m-1 . We will prove that for all γ ′ ∈ [[θ m ]] Nm there exists γ ∈ [[θ m-1 ]] Nm-1 such that γ → + γ ′ . From γ ′ , we will build a configuration γ in [[θ m-1 ]] Nm-1 such that γ → + γ ′ . First, we need to divide the set of control states Q in different subsets. For each q ′ ∈ S ′ \ S, we know there exists q, ??a, q ′ ∈ R with q ∈ S; note that there might exist more than one such transition, but among them we choose one and we denote by origin(q ′ ) the corresponding state q. Similarly for each q ∈ S \ S ′ , we know there exists q, ??a, q ′ ∈ R with q ′ ∈ S ′ ; note that there might exist more than one such transition, but among them we choose one and we denote by destination(q) the corresponding state q ′ . For q ∈ S, we then define the set From(q) = {q ′ ∈ S ′ \ S | q = origin (q ′ )}. Intuitively this set characterizes the control states which are newly appearing in S ′ and their presence is due to the reception of a from a vertex in state q. Similarly for q ′ ∈ S ′ we define To(q ′ ) = {q ′′ ∈ S \ S ′ | q ′ = destination (q ′′ )}, which intuitively characterizes the control state that disappears from S and their associated vertex changes their state to q ′ . The configuration γ should then verify the following requirements, for each q ∈ Q:

1. If q ∈ S ∩ S ′ , then: #γ(q) = #v(q)+#γ ′ (q)-#v ′ (q)+ q ′ ∈From(q)

[(#γ ′ (q ′ )-#v ′ (q ′ ))-|To(q ′ )| * (N m-1 +1)] 2. If q ∈ S \ S ′ , then: #γ(q) = #v(q)+(N m-1 +1)+ q ′ ∈From(q)

[(#γ ′ (q ′ )-#v ′ (q ′ ))-|To(q ′ )| * (N m-1 +1)]

If q /

∈ S, then #γ(q) = #v(q)

Note that the number of labels of vertices labelled by a given control state q ∈ Q is the only relevant information that need to be considered because then thanks to the reconfiguration rule of the RBN, we can obtain any labeled graphs (i.e. the topology can be changed in any wished direction).

Let us now check that the requirements for γ ensure that γ ∈ [[θ m-1 ]] Nm-1 , that is that we have for each q ∈ Q, if q / ∈ S, then #γ(q) = #v(q) (this is guaranteed by the requirement 3. on γ) and if q ∈ S, then #γ(q) > (N m-1 + #v(q)). We will now prove this last point. Let q ∈ S. First we will show that q ′ ∈From(q) [(#γ ′ (q ′ ) -#v ′ (q ′ )) -|To(q ′ )| * (N m-1 + 1)] ≥ 0. Let q ′ ∈ From(q), since q ′ ∈ S ′ , we have that #γ ′ (q ′ ) -#v ′ (q ′ ) > N m , hence by definition of N m we deduce that #γ ′ (q ′ ) -#v ′ (q ′ ) > (N m-1 + 1) * (|S \ S ′ | + 1), consequently [(#γ ′ (q ′ )-#v ′ (q ′ ))-|To(q ′ )| * (N m-1 +1)] > (N m-1 +1) * (|S \S ′ |+1-|To(q ′ )|). But since To(q ′ ) ⊆ (S \ S ′ ), this allows us to deduce that [(#γ ′ (q ′ ) -#v ′ (q ′ )) -|To(q ′ )| * (N m-1 + 1)] > 0. We can now prove that for all q ∈ S, we have #γ(q) > (N m-1 + #v(q)). If q ∈ S \ S ′ , thanks to requirement 2. and the previous consideration, it is obvious that #γ(q) > (N m-1 + #v(q)). If q ∈ S ∩ S ′ , then thanks to requirement 1. and to the previous consideration, we have that #γ(q) > #v(q) + #γ ′ (q) -#v ′ (q), but since q ∈ S ′ , we have that #γ ′ (q) -#v ′ (q) > N m > N m-1 , hence #γ(q) > #v(q) > N m-1 . This allows us to deduce that the configuration γ ∈ [[θ m-1 ]] Nm-1 .

It remains now to check that γ → + γ ′ . The main idea is that first we begin to use the non-deterministic reconfiguration to obtain a graph as we want in order to make the nodes react correctly to the broadcast. We will now explain why requirements 1. to 3. ensure that γ → + γ ′ . We will focus our attention on the vertices labelled with control states in S. Assume there is a control state q of |Θ|, which simplifies in psize(ϕ) * log (|Q|) + |Q| log (2), i.e. polynomial in the size of Q and ϕ. Algorithm 3 uses two variables to encode the symbolic configurations θ and θ ′ , and one counter i that increments up to |Θ|; because of the previous considerations, the local variables are encoded in polynomial space. Thanks to Lemma 9 we can conclude that the algorithm works in NPSpace = PSpace, and therefore, because of Proposition 3, CRP is PSpace-complete.

  r o c e s s Output : S ⊆ Q th e s e t o f r e a c h a b l e c o n t r o l s t a t e s i n RBN (P)

Lemma 4

 4 If there exists θ ∈ Θ such that θ 0 * θ and θ |= ϕ, then P |= ♦ϕ.

  t. γ → * γ ′ and γ ′ |= #ok ≥ 1 iff b is the value for v in C with input values b 1 , . . . , b k .

  Figure 1: Simulation of a transition t with • t = {p 1 , . . . , p n } and t • = {q 1 , . . . , q m }.

	τ		ok t	!!a t,p1	a t,p1	??a ack t,p1	a ack t,p1		a ack t,pn-1	!!a t,pn	a t,pn
	ok										??a ack t,pn
	??b ack t,qm	b t,qm	!!b t,qm	b ack t,qm-1		b ack t,q1	??b ack t,q1	b t,q1	!!b t,q1	a ack t,pn
	p 1	??a t,p	aux a t,p	!!a ack t,p	p 0	p 0	??b t,p	aux b t,p	!!b ack t,p	p 1

in S but not in S ′ (i.e. we analyze requirement 2.) For this control state we put at least #v(q) + (N m-1 + 1), one assumption we made is that the (N m-1 + 1) will change their label to destination (q), consequently thanks to this we are sure that there are at least |To(destination(q))| * (N m-1 + 1) vertices labelled by destination(q) in γ ′ . Then however it might be the case that in γ, we need more nodes labelled by q because these nodes will change their label into some node q ′ that do not belong to S but to S ′ . This is the case for the nodes q ′ such that q = origin(q ′ ), and the quantity of nodes labelled by q we need to add is precisely for each such label q ′ : [(#γ ′ (q ′ ) -#v ′ (q ′ )) -|To(q ′ )| * (N m-1 + 1)], i.e. the number of nodes labelled by q ′ in γ ′ to which is subtracted the number of nodes in γ labelled by a state in S \ S ′ that change their state to q ′ (this quantity being |To(q ′ )| * (N m-1 + 1) as we have already mentioned). For the control state q ∈ S ∩ S ′ , the reasoning is similar. Hence what we have shown is that we choose the requirements 1. and 2. to ensure that γ → + γ ′ . Finally since γ ∈ [[θ m-1 ]] Nm-1 , by induction hypothesis, we have that there exists γ 0 ∈ Γ 0 such that γ 0 → * γ and consequently we also deduce that γ 0 → * γ ′ .

The case where the broadcast is performed by a node whose control state is taken from S can be treated in a similar way.

We can now prove Lemma 4. Assume there exists θ ∈ Θ such that θ 0 * θ and θ |= ϕ. From Lemma 6, we know that there exists γ 0 ∈ θ 0 and γ ∈ [[θ]] such that γ 0 → * γ, and by the definition of |= for symbolic configuration we deduce also that γ |= ϕ. Consequently we have P |= ♦ϕ.

A.6 Proof of Lemma 5

Given a configuration γ ∈ θ, we define ↑ q0 γ as the set {γ ′ ∈ Γ | ∀q ∈ Q \ {q 0 }. #γ ′ (q) = #γ(q)}. The following lemma then holds.

Lemma 7 Let γ 0 ∈ Γ 0 and γ ∈ Γ such that γ 0 → * γ. Then for all θ ∈ Θ such that ↑ q0 γ ∩ [[θ]] = ∅, we have θ 0 * θ.

Proof: Let γ 0 ∈ Γ 0 and γ ∈ Γ such that γ 0 → * γ. Then there exists γ 1 , . . . , γ m in Γ such that γ 0 → γ 1 → . . . → γ m and γ m = γ. We will prove the statement of the Lemma by induction on the length of this symbolic execution. The base case, when m = 0, is obvious since if ↑ q0 γ 0 ∩ [[θ]] = ∅ implies that θ = θ 0 (in fact, we know that the only control state present in γ 0 is q 0 ). Now let m > 0 and assume the property is true for all i ∈ {0. . . . , m -1}, we will prove it holds for γ m . Let

either a reconfiguration rule or broadcast rule is applied to go from γ m-1 to γ m . Assume a reconfiguration rule is applied, then only the edges change between γ m-1 and γ m , hence we have

and by induction hypothesis we deduce that θ 0 * θ. We now suppose that there exists a rule r = q, !!a,

First we need to introduce some notations. Since we have

(on the domain of the elements of v different than q 0 the function node is hence injective). Note that since γ m-1 → r γ m , we have by definition of the transition relation in RBN, V = V ′ and E = E ′ . We build the vector v m-1 ∈ Q psize(ϕ) , as follows, for each i ∈ {1, . . . , psize(ϕ)}:

After we build the set S m-1 ⊆ Q as follows:

q)}. By construction and using the definitions of → and , we deduce easily the two following properties:

θ m . Hence using the hypothesis of induction, we have also θ 0 * θ m-1 which allows us to deduce that θ 0 * θ m . Basically, Lemma 7 says that given a reachable configuration γ, each symbolic configuration θ whose semantics [[θ]] contains γ (modulo processes in state q 0 ) is also reachable. We next formalize that such a θ actually exists whenever γ satisfies ϕ.

Proof: Given a process P = Q, Σ, R, {q 0 } , a formula ϕ, and a configuration γ ∈ Γ such that γ |= ϕ, we build a symbolic configuration θ = (v, S) ∈ Θ where S = {q 0 } ∪ {q ∈ Q | q = q 0 , #γ(q) > val(ϕ)}, v has size psize(ϕ), #v(q 0 ) ≥ 0, and for all q ∈ Q \ {q 0 }, #v(q) = val(ϕ) if q ∈ S, or #v(q) = #γ(q) otherwise. It is straightforward, by construction, that psize(ϕ) = |Q| * val(ϕ) is big enough to let the vector v contain all the generated processes, because each q ∈ Q \ {q 0 } will occur at most val(ϕ) times, and q 0 will fill in the rest. Furthermore, for each γ ′ ∈ [[θ]], #γ ′ (q 0 ) > 0 and for every q ∈ Q \ {q 0 }, either q / ∈ S and #γ ′ (q) = #γ(q), or q ∈ S and #γ(q) > #v(q), meaning that ↑ q0 γ ∩ [[θ]] = ∅. We will now proceed by induction on the structure of the formula to show that γ |= ϕ if and only if θ |= ϕ.

a ≤ #γ ′ (q) < b. By construction, #γ ′ (q) is either equal to #γ(q) when b = +∞, or it is greater or equal than #γ(q) otherwise, meaning that a ≤ #γ(q) < b.

Disjunction The proof is almost identical to the one for conjunction.

Negation By definition, γ |= ¬ϕ 1 iff γ |= ϕ 1 . We conclude that γ |= ϕ 1 iff θ |= ϕ 1 by application of the inductive hypothesis.

We can now prove Lemma 5. Since P |= ♦ϕ, there exist an initial configuration γ 0 ∈ Γ 0 and a configuration γ ∈ Γ such that γ 0 → * γ and γ |= ϕ. By Lemma 8 we know there exists θ ∈ Θ such that ↑ q0 γ ∩ [[θ]] = ∅ and θ |= ϕ and thanks to Lemma 7 we have that θ 0 * θ.

A.7 Proof of Theorem 3

In order to solve CRP we provide Algorithm 3.

Algorithm 3: Solving CRP

Before to analyze the correctness and complexity of this Algorithm, we need the following Lemma.

Lemma 9 (i) For any θ ∈ Θ and any formula ϕ, θ |= ϕ can be decided in PTime. (ii) For all θ, θ ′ ∈ Θ, θ θ ′ is decidable in PTime.

Proof: We first prove part (i) of the Lemma. Let ψ = a ≤ #q < b be an atom of ϕ, and let θ = (v, S) ∈ Θ. Then, θ |= ψ if b = +∞, q / ∈ S, and a ≤ #v(q) < b or if b = +∞ and #v(q) ≥ a. All of these tests can be done in PTime in the size of ϕ. After assigning a truth value to each atom, the truth of the whole formula can be computed in PTime, as an instance of the Circuit Value Problem.

Let us now proceed to prove part (ii). The proof will follow the definition of ⊆ Θ × Θ. Let θ = (v, S) and θ ′ = (v ′ , S ′ ) be two symbolic configurations, and let q, !!a, q ′ ∈ R be a broadcast rule. First, let us consider the case of a broadcast from the vector v.

For all i ∈ {1, . . . , psize(ϕ)}, there are three possibilities: v[i] is the only sending process such that v[i] = q and v ′ [i] = q ′ (constant time); there exists a rule q r , ??a, q ′ r ∈ R such that v[i] = q r and v ′

time). Checking the conditions on all the elements in vector v takes overall no more than |R| * psize(ϕ) steps. For each q s ∈ Q, we have two conditions to check on the sets S and S ′ : if q s ∈ S ′ \ S, then there is a q ′ s ∈ S such that q ′ s , ??a, q s ∈ R; if q s ∈ S \ S ′ , then there is a q ′ s ∈ S such that q s , ??a, q ′ s ∈ R. Both membership of states and existence of rules can be computed in linear time in the size of the process, thus checking the conditions for S and S ′ is in PTime too. The case of a broadcast from the set S can be handled in a similar way. The Lemma follows from observing that all we need to do, is to repeat the PTime check for all broadcast rules r ∈ R.

We know, thanks to lemmas 4 and 5, that we are able to reach a symbolic configuration which satisfies a given cardinality constraint ϕ if and only if P |= ♦ϕ. Being Θ = Q psize(ϕ) × 2 Q , the total number of symbolic states is |Θ| = |Q| psize(ϕ) * 2 |Q| , namely all possible configurations of the vector multiplied by the number of subsets of Q. The space needed to encode θ ∈ Θ is the logarithm