key: cord-0060386-txmup8zs
authors: Balasubramanian, A. R.; Esparza, Javier; Raskin, Mikhail
title: Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_3
sha: 3ac33bd3fb68356113220a4f901310c1b6d17c58
doc_id: 60386
cord_uid: txmup8zs

In rendez-vous protocols an arbitrarily large number of indistinguishable finite-state agents interact in pairs. The cut-off problem asks if there exists a number B such that all initial configurations of the protocol with at least B agents in a given initial state can reach a final configuration with all agents in a given final state. In a recent paper [17], Horn and Sangnier prove that the cut-off problem is equivalent to the Petri net reachability problem for protocols with a leader, and in [Image: see text] for leaderless protocols. Further, for the special class of symmetric protocols they reduce these bounds to [Image: see text] and [Image: see text] , respectively. The problem of lowering these upper bounds or finding matching lower bounds is left open. We show that the cut-off problem is [Image: see text] -complete for leaderless protocols, [Image: see text] -complete for symmetric protocols with a leader, and in [Image: see text] for leaderless symmetric protocols, thereby solving all the problems left open in [17].

Distributed systems are often designed for an unbounded number of participant agents. Therefore, they are not just one system, but an infinite family of systems, one for each number of agents. Parameterized verification addresses the problem of checking that all systems in the family satisfy a given specification.

In many application areas, agents are indistinguishable. This is the case in computational biology, where cells or molecules have no identities; in some security applications, where the agents' identities should stay private; or in applications where the identities can be abstracted away, like certain classes of multithreaded programs [15, 2, 31, 3, 18, 25] . Following [3, 18] , we use the term replicated systems for distributed systems with indistinguishable agents. Replicated systems include population protocols, broadcast protocols, threshold automata, and many other models [15, 2, 11, 7, 16] . They also arise after applying a counter abstraction [28, 3] . In finite-state replicated systems the global state of the system is determined by the function (usually called a configuration) that assigns to each state the number of agents that currently occupy it. This feature makes many verification problems decidable [4, 10] .

Surprisingly, there is no a priori relation between the complexity of a parameterized verification question (i.e., whether a given property holds for all initial configurations, or, equivalently, whether its negation holds for some configuration), and the complexity of its corresponding single-instance question (whether the property holds for a fixed initial configuration). Consider replicated systems where agents interact in pairs [15, 17, 2] . The complexity of single-instance questions is very robust. Indeed, checking most properties, including all properties expressible in LTL and CTL, is PSPACE-complete [9] . On the contrary, the complexity of parameterized questions is very fragile, as exemplified by the following example. While the existence of a reachable configuration that populates a given state with at least one agent is in P, and so well below PSPACE, the existence of a reachable configuration that populates a given state with exactly one agent is as hard as the reachability problem for Petri nets, and so non-elementary [6] . This fragility makes the analysis of parameterized questions very interesting, but also much harder.

Work on parameterized verification has concentrated on whether every initial configuration satisfies a given property (see e.g. [15, 11, 3, 18, 7] ). However, applications often lead to questions of the form "do all initial configurations in a given set satisfy the property?", "do infinitely many initial configurations satisfy the property?", or "do all but finitely many initial configurations satisfy the property?". An example of the first kind is proving correctness of population protocols, where the specification requires that for a given partition I 0 , I 1 of the set of initial configurations, and a partition Q 0 , Q 1 of the set of states, runs starting from I 0 eventually trap all agents within Q 0 , and similarly for I 1 and Q 1 [12] . An example of the third kind is the existence of cut-offs; cut-off properties state the existence of an initial configuration such that for all larger initial configurations some given property holds [8, 4] . A systematic study of the complexity of these questions is still out of reach, but first results are appearing. In particular, Horn and Sangnier have recently studied the complexity of the cut-off problem for parameterized rendez-vous networks [17] . The problem takes as input a network with one single initial state init and one single final state fin, and asks whether there exists a cut-off B such that for every number of agents n ≥ B, the final configuration in which all agents are in state fin is reachable from the initial configuration in which all agents are in state init.

Horn and Sangnier study two versions of the cut-off problem, for leaderless networks and networks with a leader. Intuitively, a leader is a distinguished agent with its own set of states. They show that in the presence of a leader the cut-off problem and the reachability problem for Petri nets problems are inter-reducible, which shows that the cut-off problem is in the Ackermannian complexity class F ω [22] , and non-elementary [6] . For the leaderless case, they show that the problem is in EXPSPACE. Further, they also consider the special case of symmetric networks, for which they obtain better upper bounds: PSPACE for the case of a leader, and NP in the leaderless case. These results are summarized at the top of Table 1 .

In [17] the question of improving the upper bounds or finding matching lower bounds is left open. In this paper we close it with a surprising answer: All elementary upper bounds of [17] can be dramatically improved. In particular, our main result shows that the EXPSPACE bound for the leaderless case can be brought down to P. Further, the PSPACE and NP bounds of the symmetric case can be lowered to NP and NC, respectively, as shown at the bottom of Table 1 .

We also obtain matching lower bounds. Finally, we provide almost tight upper bounds for the size of the cut-off B; more precisely, we show that if B exists, then B ∈ 2 n O(1) for a protocol of size n.

Our results follow from two lemmas, called the Scaling and Insertion Lemmas, that connect the continuous semantics for Petri nets to their standard semantics. In the continuous semantics of Petri nets transition firings can be scaled by a positive rational factor; for example, a transition can fire with factor 1/3, taking "1/3 of a token" from its input places. The continuous semantics is a relaxation of the standard one, and its associated reachability problem is much simpler (polynomial instead of non-elementary [14, 6, 5] ). The Scaling Lemma 1 states that given two markings M, M of a Petri net, if M is reachable from M in the continuous semantics, then nM is reachable from nM in the standard semantics for some n ∈ 2 m O(1) , where m is the total size of the net and the markings. The Insertion Lemma states that, given four markings M, M , L, L , if M is reachable from M in the continuous semantics and the marking equation L = L + Ax has a solution x ∈ Z T (observe that x can have negative components), then nM +L is reachable from nM + L in the standard semantics for some n ∈ 2 m O(1) . We think that these lemmas can be of independent interest.

The paper is organized as follows. Section 2 contains preliminaries; in particular, it defines the cut-off problem for rendez-vous networks and reduces it to the cut-off problem for Petri nets. Section 3 gives a polynomial time algorithm for the leaderless cut-off problem for acyclic Petri nets. Section 4 introduces the Scaling and Insertion Lemmas, and Section 5 presents the novel polynomial time algorithm for the cut-off problem. Sections 6 and 7 present the results for symmetric networks, for the cases with and without leaders, respectively.

Due to lack of space, full proofs of some of the lemmas can be found in the appendix.

Multisets Let E be a finite set. For a semi-ring S, a vector from E to S is a function v : E → S. The set of all vectors from E to S will be denoted by S E . In this paper, the semi-rings we will be concerned with are the natural numbers N, the integers Z and the non-negative rationals Q ≥0 (under the usual addition and multiplication operators). The support of a vector v is the set v := {e : v(e) = 0} and its size is the number v = e∈ v abs(v(e)) where abs(x) denotes the absolute value of x. Vectors from E to N are also called discrete multisets (or just multisets) and vectors from E to Q ≥0 are called continuous multisets.

Given a multiset M and a number α we let α · M be the multiset given by Rendez-vous protocols and the cut-off problem. Let Σ be a fixed finite set which we will call the communication alphabet and we let RV (Σ) = {!a, ?a : a ∈ Σ}. The symbol !a denotes that the message a is sent and ?a denotes that the message a is received. Definition 1. A rendez-vous protocol P is a tuple (Q, Σ, init, fin, R) where Q is a finite set of states, Σ is the communication alphabet, init , fin ∈ Q are the initial and final states respectively and R ⊆ Q × RV (Σ) × Q is the set of rules.

The size |P| of a protocol is defined as the number of bits needed to encode P in {0, 1} * using some standard encoding. A configuration C of P is a multiset of states, where C(q) should be interpreted as the number of agents in state q. We use C(P) to denote the set of all configurations of P. An initial (final) configuration C is a configuration such that C(q) = 0 if q = init (resp. C(q) = 0 if q = fin). We use C n init (C n fin ) to denote the initial (resp. final) configuration such that C n init (init) = n (resp. C n fin (fin) = n). The operational semantics of a rendez-vous protocol P is given by means of a transition system between the configurations of P. We say that there is a transition between C and C , denoted by C ⇒ C iff there exists a ∈ Σ, p, q, p , q ∈ Q such that (p, !a, p ), (q, ?a, q ) ∈ R, C ≥ p, q and C = C − p, q + p , q . As usual, * = ⇒ denotes the reflexive and transitive closure of ⇒. The cut-off problem for rendez-vous protocols, as defined in [17] , is:

Given: A rendez-vous protocol P Decide: Is there B ∈ N such that C n init * = ⇒ C n fin for every n ≥ B ? If such a B exists then we say that P admits a cut-off and that B is a cut-off for P.

Petri nets. Rendez-vous protocols can be seen as a special class of Petri nets.

A Petri net is a tuple N = (P, T, Pre, Post) where P is a finite set of places, T is a finite set of transitions, Pre and Post are matrices whose rows and columns are indexed by P and T respectively and whose entries belong to N. The incidence matrix A of N is defined to be the P × T matrix given by A = Post − Pre. Further by the weight of N , we mean the largest absolute value appearing in the matrices Pre and Post.

The size |N | of N is defined as the number of bits needed to encode N in {0, 1} * using some suitable encoding. For a transition t ∈ T we let

t] > 0}. We extend this notation to set of transitions in the obvious way. Given a Petri net N , we can associate with it a graph where the vertices are P ∪ T and the edges are

A Petri net N is called acyclic if its associated graph is acyclic. A marking of a Petri net is a multiset M ∈ N P , which intuitively denotes the number of tokens that are present in every place of the net. For t ∈ T and markings M and M , we say that M is reached from M by firing t, denoted A firing sequence is any sequence of transitions σ = t 1 , t 2 , . . . , t k ∈ T * . The support of σ, denoted by σ , is the set of all transitions which appear in σ. We let σσ denote the concatenation of two sequences σ, σ .

Given a firing sequence 

where − → σ ∈ N T is the the Parikh image of σ, defined as the vector whose com-

for transition t is equal to the number of times t appears in σ. From rendez-vous protocols to Petri nets. Let P = (Q, Σ, init, fin, R) be a rendez-vous protocol. Create a Petri net N P = (P, T, Pre, Post) as follows.

The set of places is Q. For each letter a ∈ Σ and for each pair of rules r = (q, !a, s), r = (q , ?a, s ) ∈ R, add a transition t r,r to N P and set

It is clear that any configuration of a protocol P is also a marking of N P , and vice versa. Further, the following proposition is obvious. Proposition 1. For any two configurations C and C we have that C * = ⇒ C over the protocol P iff C * − → C over the Petri net N P .

Consequently, the cut-off problem for Petri nets, defined by

generalizes the problem for rendez-vous protocols.

We show that the cut-off problem for acyclic Petri nets can be solved in polynomial time. The reason for considering this special case first is that it illustrates one of the main ideas of the general case in a very pure form.

Let us fix a Petri net system (N , M, M ) for the rest of this section, where N = (P, T, P re, P ost) is acyclic and A is its incidence matrix. It is well-known that in acyclic Petri nets the reachability relation is characterized by the marking equation (see e.g. [24] ): This proposition shows that the reachability problem for acyclic Petri nets reduces to the feasibilty problem (i.e., existence of solutions) of systems of linear diophantine equations over the nonnegative integers. So the reachability problem for acyclic Petri nets is in NP, and in fact both the reachability and the feasibility problems are NP-complete [13] .

There are two ways to relax the conditions on the solution so as to make the feasibility problem polynomial. Feasibility over the nonnegative rationals and feasibility over all integers are both in P. The first is due to the polynomiality of linear programming. For the second, feasibility can be decided in polynomial time after computing the Smith or Hermite normal forms (see e.g. [29] ), which can themselves be computed in polynomial time [19] . We show that the cut-off problem can be reduced to these two relaxed problems.

Horn and Sangnier proved in [17] a very useful charaterization of the rendezvous protocols with a cut-off: A rendez-vous protocol P admits a cut-off iff there exists n ∈ N such that C n init * = ⇒ C n fin and C n+1 init * = ⇒ C n+1 fin . The proof immediately generalizes to the case of Petri nets:

then n 2 is a cut-off for the system.

Using this lemma, we characterize those acyclic Petri net systems which admit a cut-off. Intuitively, the existence of the rational solution x ∈ Q T ≥0 guarantees nM * − → nM for infinitely many n, and the existence of the integer solution y ∈ Z T guarantees that for one of those n we have (n + 1)M * − → (n + 1)M as well. 

We derive a polynomial time algorithm for the cut-off problem from the characterization of Theorem 1. The first step is the following lemma. A very similar lemma is proved in [14] , but since the proof is short we give it for the sake of completeness:

Lemma 2. If the marking equation is feasible over Q ≥0 , then it has a solution with maximum support. Moreover, such a solution can be found in polynomial time.

Proof. If y, z ∈ Q T ≥0 are solutions of the marking equation, then we have M = M + A((y + z)/2) and y ∪ z ⊆ (y + z)/2 . Hence if the marking equation if feasible over Q ≥0 , then it has a solution with maximum support.

To find such a solution in polynomial time we proceed as follows. For every transition t we solve the linear program M = M + Av, v ≥ 0, v(t) > 0. (Recall that solving linear programs over the rationals can be done in polynomial time). Let {t 1 , . . . , t n } be the set of transitions whose associated linear programs are feasible over Q T ≥0 , and let {u 1 , . . . , u n } be solutions to these programs. Then 1/n · n i=1 u i is a solution of the marking equation with maximum support.

We now have all the ingredients to give a polynomial time algorithm.

Theorem 2. The cut-off problem for acyclic net systems can be solved in polynomial time.

Proof. First, we check that the marking equation has a solution over the nonnegative rationals. If such a solution does not exist, by Theorem 1 the given net system does not admit a cut-off.

Suppose such a solution exists. By Lemma 2 we can find a non-negative rational solution x with maximum support in polynomial time. Let U contain all the transitions t such that x t = 0. We now check in polynomial time if the marking equation has a solution y over Z T such that y t = 0 for every t ∈ U . By Theorem 1 such a solution exists iff the net system admits a cut-off.

The rendez-vous protocol given in Figure 2 , which was stated in [17] , is an example of a protocol where the smallest cut-off is exponential in the size of the protocol. In the next sections, we will actually prove that if a net system N (acyclic or not) admits a cut-off, then there is one with a polynomial number of bits in |N |. To this end, we prove two intermediate lemmas to help us come up with a characterization for cut-off admissible net systems in the general case. We believe that these two lemmas could be of independent interest in their own right. Further, the proofs of both lemmas are provided so that it will enable us later on to derive a bound on the cut-off for net systems.

The Scaling Lemma shows that, given a Petri net system (N , M, M ), whether nM * − → nM holds for some n ≥ 1 can be decided in polynomial time; moreover, if nM * − → nM holds for some n, then it holds for some n with at most (|N |(log M + log M )) O(1) bits. The name of the lemma is due to the fact that the firing sequence leading from nM to nM is obtained by scaling up a continuous firing sequence from M to M ; the existence of such a continuous sequence can be decided in polynomial time [14] .

In the rest of the section we first recall continuous Petri nets and the charaterization of [14] , and then present the Scaling Lemma 2 .

Reachability in continuous Petri nets. Petri nets can be given a continuous semantics (see e.g. [1, 30, 14] ), in which markings are continuous multisets; we call them continuous markings. A continuous marking M enables a transition t with factor λ ∈ Q ≥0 if M (p) ≥ λ · P re[p, t] for every place p; we also say that M enables λt. If M enables λt, then λt can fire or occur, leading to a new marking M given by M (p) = M (p) + λ · A[p, t] for every p ∈ P . We denote this by 

In the acyclic case, the existence of a cut-off is characterized by the existence of solutions to the marking equation Q T ≥0 and Z T . Intuitively, in the general case we replace the existence of solutions over Q T ≥0 by the conditions of the Scaling Lemma, and the existence of solutions over Z T by the Insertion Lemma:

Lemma 5 (Insertion Lemma). Let M, M , L, L be markings of N satisfying M σ − → M for some σ ∈ T * and L = L + Ay for some y ∈ Z T such that y ⊆ σ . Then µM + L * − → µM + L for µ = y ( − → σ nw + nw + 1) , where w is the weight of N , and n is the number of places in • σ .

The idea of the proof is a follows: In a first stage, we asynchronously execute multiple "copies" of the firing sequence σ from multiple "copies" of the marking M , until we reach a marking at which all places of • σ contain a sufficiently large number of tokens. At this point we temporarily interrupt the executions of the copies of σ to insert a firing sequence with Parikh mapping y − → σ + y.

The net effect of this sequence is to transfer some copies of M to M , leaving the other copies untouched, and exactly one copy of L to L . In the third stage, we resume the interrupted executions of the copies of σ, which completes the transfer of the remaining copies of M to M . Since each of the markings in {M ip } p∈ • σ can be obtained from M by firing a (suitable) prefix of σ, it is easy to see that from the marking µM + L = λ y M + L + (λ x λ y nw + λ y nw )M we can reach the marking First := λ y M + L + p∈ • σ (λ x λ y w + λ y w )M ip . This completes our first stage. Second stage -Insert: Since y ⊆ σ , if y(t) = 0 then x(t) = 0. Since x(t) ≥ 0 for every transition, it now follows that (λ y x + y)(t) ≥ 0 for every transition t and (λ y x + y)(t) > 0 precisely for those transitions in σ .

Let ξ be any firing sequence such that − → ξ = λ y x + y. Notice that for every place p ∈ • σ , First(p) ≥ λ x λ y w +λ y w ≥ (λ y x+y) ·w . By an easy induction on ξ , it follows that that First ξ − → Second for some marking Second. By the marking equation, it follows that Second = λ y M + L + p∈ • σ (λ x λ y w + λ y w )M ip . This completes our second stage.

Third stage: Notice that for each place p ∈ • σ , by construction of M ip , there is a firing sequence which takes the marking M ip to the marking M . It then follows that there is a firing sequence which takes the marking Second to the marking λ y M + L + p∈ • σ (λ x λ y w + λ y w )M = µM + L . This completes our third stage and also completes the desired firing sequence from µM + L to µM + L .

Let (N , M, M ) be a net system with N = (P, T, P re, P ost), such that A is its incidence matrix. As in Section 3, we first characterize the Petri net systems that admit a cut-off, and then provide a polynomial time algorithm.

We generalize the characterization of Theorem 1 for acyclic Petri net systems to general systems. Let τ = t 1 t 2 · · · t k . Construct the rational firing sequence σ := t 1 /n t 2 /n · · · t k /n. From the fact that nM It is well known that if a system of linear equations over the integers is feasible, then there is a solution which can be described using a number of bits which is polynomial in the size of the input (see e.g. [20] ). Hence, we can assume that y can be described using s O(1) bits.

By Lemma 4 there exists n (which can be described using s O(1) bits) and a firing sequence τ with τ = σ such that nM τ − → nM . Hence knM * − → knM is also possible for any k ∈ N. By Lemma 5, there exists µ (which can once again be described using s O(1) bits) such that µnM + M * − → µnM + M is possible. By Lemma 1 the system (N , M, M ) admits a cut-off with a polynomial number of bits in s.

Notice that we have actually proved that if a net system admits a cut-off then it admits a cut-off with a polynomial number of bits in its size. Since the cut-off problem for a rendez-vous protocol P can be reduced to a cut-off problem for the Petri net system (N P , init , fin ), it follows that, Corollary 1. If the system (N , M, M ) admits a cut-off then it admits a cutoff with a polynomial number of bits in |N |(log M + log M ). Hence, if a rendez-vous protocol P admits a cut-off then it admits a cut-off with a polynomial number of bits in |P|.

We use the characterization given in the previous section to provide a polynomial time algorithm for the cut-off problem. The following lemma, which was proved in [14] and whose proof is given in the appendix, enables us to find a firing sequence between two markings with maximum support. Lemma 6. [14] Among all the rational firing sequences σ such that M σ −→ Q M , there is one with maximum support. Moreover, the support of such a firing sequence can be found in polynomial time.

We now have all the ingredients to prove the existence of a polynomial time algorithm.

Theorem 5. The cut-off problem for net systems can be solved in polynomial time.

Proof. First, we check that there is a rational firing sequence σ with M This immediately proves that the cut-off problem for rendez-vous protocols is also in polynomial time. By an easy logspace reduction from the Circuit Value Problem [21] , we prove that Lemma 7. The cut-off problem for rendez-vous protocols is P-hard.

Clearly, this also proves that the cut-off problem for Petri nets is P-hard.

In [17] Horn and Sangnier introduce symmetric rendez-vous protocols, where sending and receiving a message at each state has the same effect, and show that the cut-off problem is in NP. We improve on their result and shown that it is in NC.

Recall that NC is the set of problems in P that can be solved in polylogarithmic parallel time, i.e., problems which can be solved by a uniform family of circuits with polylogarithmic depth and polynomial number of gates. Two wellknown problems which lie in NC are graph reachability and feasibility of linear equations over the finite field F 2 of size 2 [27, 23] . We proceed to formally define symmetric protocols and state our results. Definition 3. A rendez-vous protocol P = (Q, Σ, init, fin, R) is symmetric, iff its set of rules is symmetric under swapping !a and ?a for each a ∈ Σ, i.e., for each a ∈ Σ, we have (q, !a, q ) ∈ R iff (q, ?a, q ) ∈ R.

Horn and Sangnier show that, because of their symmetric nature, there is a very easy characterization for cut-off admitting symmetric protocols. fin . From a symmetric protocol P, we can derive a graph G(P) where the vertices are the states and there is an edge between q and q iff there exists a ∈ Σ such that (q, a, q ) ∈ R. The following proposition is immediate from the definition of symmetric protocols: Proposition 4. Let P be a symmetric protocol. There exists an even number e such that C e init * − → C e fin iff there is a path from init to fin in the graph G(P). Proof. The left to right implication is obvious. For the other side, suppose there is a path init, q 1 , q 2 , . . . , q m−1 , fin in the graph G(P). Then notice that 2·init → 2 · q 1 → 2 · q 2 · · · → 2 · q m−1 → 2 · q f is a valid run of the protocol.

Since graph reachability is in NC , this takes care of the "even" case from Proposition 3. Hence, we only need to take care of the "odd" case from Proposition 3.

Fix a symmetric protocol P for the rest of the section. As a first step, for each state q ∈ Q, we compute if there is a path from init to q and if there is a path from q to fin in the graph G(P). Since graph reachability is in NC this computation can be carried out in NC by parallely running graph reachability for each q ∈ Q. If such paths exist for a state q then we call q a good state, and otherwise a bad state. The following proposition easily follows from the symmetric nature of P: Proposition 5. If q ∈ Q is a good state, then 2 · init * − → 2 · q and 2 · q * − → 2 · fin .

Similar to the general case of rendez-vous protocols, given a symmetric protocol P we can construct a Petri net N P whose places are the states of P and which faithfully represents the reachability relation of configurations of P. Observe that this construction can be carried out in parallel over all the states in Q and over all pairs of rules in R. Let N = (P, T, P re, P ost) be the Petri net that we construct out of the symmetric protocol P and let A be its incidence matrix. We now write the marking equation for N as follows: We introduce a variable v[t] for each transition t ∈ T and we construct an equation system Eq enforcing the following three conditions:

-v[t] = 0 for every t ∈ T such that • t ∪ t • contains a bad state. By definition of a bad state, such transitions will never be fired on any run from an initial to a final configuration and so our requirement is safe.

= 0 for each q / ∈ {init, fin}. Notice that the net-effect of any run from an initial to a final configuration on any state not in {init, fin} is 0 and hence this condition is valid as well.

It is clear that the construction of Eq can be carried out in parallel over each q ∈ Q and each t ∈ T . Finally, we solve Eq over arithmetic modulo 2, i.e., we solve Eq over the field F 2 which as mentioned before can be done in NC. We have: Proof. (Sketch.) The left to right implication is true because of taking modulo 2 on both sides of the marking equation. For the other side, we use an idea similar to Lemma 5. Let x be a solution to Eq over F 2 . Using Proposition 5 we first populate all the good states of Q with enough processes such that all the good states except init have an even number of processes. Then, we fire exactly once, all the transitions t such that x[t] = 1. Since x satisfies Eq, we can now argue that in the resulting configuration, the number of processes at each bad state is 0 and the number of processes in each good state except fin is even. Hence, we can once again use Proposition 5 to conclude that we can move all the processes which are not at fin to the final state fin. 

In this section, we extend symmetric rendez-vous protocols by adding a special process called leader. We state the cut-off problem for such protocols and prove that it is NP-complete.

A symmetric leader protocol is a pair of symmetric protocols P = (P L , P F ) where P L = (Q L , Σ, init L , fin L , R L ) is the leader protocol and P F = (Q F , Σ, init F , fin F , R F ) is the follower protocol where Q L ∩ Q F = ∅.

A configuration of a symmetric leader protocol P is a multiset over Q L ∪ Q F such that q∈Q L C(q) = 1. This corresponds to the intuition that exactly one process can execute the leader protocol. For each n ∈ N, let C n init (resp. C n fin ) denote the initial (resp. final) configuration of P given by C n init (init L ) = 1 (resp. C n fin (fin L ) = 1) and C n init (init F ) = n (resp. C n fin (fin F ) = n). We say that C = ⇒ C if there exists (p, !a, p ), (q, ?a, q ) ∈ R L ∪ R F , C ≥ p, q and C = C − p, q + p , q . Since we allow at most one process to execute the leader protocol, given a configuration C, we can let lead(C) denote the unique state q ∈ Q L such that C(q) > 0.

Definition 5. The cut-off problem for symmetric leader protocols is the following.

Input: A symmetric leader protocol P = (P L , P F ). Output: Is there B ∈ N such that for all n ≥ B, C n init * = ⇒ C n fin . We know the following fact regarding symmetric leader protocols. Let P = (P L , P F ) be a symmetric leader protocol with P L = (Q L , Σ, init L , fin L , R L ) and P F = (Q F , Σ, init F , fin F , R F ). Similar to the previous section, from P F we can construct a graph G(P F ) where the vertices are given by the states Q F and the edges are given by the rules in R F . In G(P F ), we can clearly remove all vertices which are not reachable from the state init F and which do not have a path to fin F . In the sequel, we will assume that such vertices do not exist in G(P F ).

Similar to the general case, we will construct a Petri net N P from the given symmetric leader protocol P. However, the construction is made slightly complicated due to the presence of a leader.

From P = (P L , P F ), we construct a Petri net N = (P, T, P re, P ost) as follows: Let P be Q L ∪ Q F . For each a ∈ Σ and r = (q, !a, s), r = (q , ?a, s ) ∈ R L ∪R F such that at most one of r and r belongs to R L , we will have a transition t r,r ∈ T in N such that -P re[p, t] = 0 for every p / ∈ {q, q }, P ost[p, t] = 0 for every p / ∈ {s, s } -If q = q then P re[q, t] = −2, otherwise P re[q, t] = P re[q , t] = −1 -If s = s then P ost[s, t] = 2, otherwise P ost[s, t] = P ost[s , t] = 1.

Transitions t r,r in which exactly one of r, r is in R L will be called leader transitions and transitions in which both of r, r are in R F will be called followeronly transitions. Notice that if t is a leader transition, then there is a unique place p ∈ • t ∩ Q L and a unique place p ∈ t • ∩ Q L . These places will be denoted by t.from and t.to respectively.

As usual, we let A denote the incidence matrix of the constructed net N . The following proposition is obvious from the construction of the net N Proposition 7. For two configurations C and C , we have that C * = ⇒ C in the protocol P iff C * − → C in the net N .

Because P is symmetric we have the following fact, which is easy to verify.

For any vector x ∈ N T , we define lead(x) to be the set of all leader transitions such that x[t] > 0. The graph of the vector x, denoted by G(x) is defined as follows: The set of vertices is the set {t.from : t ∈ lead(x)} ∪ {t.to : t ∈ lead(x)}. The set of edges is the set {(t.from, t.to) : t ∈ lead(x)}. Further, for any two vectors x, y ∈ N T and a transition t ∈ T , we say that

Definition 6. Let C be a configuration and let x ∈ N T . We say that the pair (C, x) is compatible if C + Ax ≥ 0 and every vertex in G(x) is reachable from lead(C).

The following lemma states that as long as there are enough followers in every state, it is possible for the leader to come up with a firing sequence from a compatible pair. Lemma 9. Suppose (C, x) is a compatible pair such that C(q) ≥ 2 x for every q ∈ Q F . Then there is a configuration D and a firing sequence ξ such that C ξ − → D and − → ξ = x.

Proof. (Sketch.) We prove by induction on x . If x[t] > 0 for some follower-only transition, then it is easy to verify that if we let C be such that C t − → C and x be x[t--], then (C , x ) is compatible and C(q) ≥ 2 x for every q ∈ Q F . Suppose x[t] > 0 for some leader transition. Let p = lead(C). If p belongs to some cycle S = p, r 1 , p 1 , r 2 , p 2 , . . . , p k , r k+1 , p in the graph G(x), then we let C r1 − → C and x = x[t--]. It is easy to verify that C + Ax ≥ 0, C (q) ≥ 2 x for every q ∈ Q F and lead(C ) = p 1 . Any path P in G(x) from p to some vertex s either goes through p 1 or we can use the cycle S to traverse from p 1 to p first and then use P to reach s. This gives a path from p 1 to every vertex s in G(x ).

If p does not belong to any cycle in G(x), then using the fact that C +Ax ≥ 0, we can show that there is exactly one out-going edge t from p in G(x). We then let C t − → C and x = x[t--]. Since any path in G(x) from p has to necessarily use this edge t, it follows that in G(x ) there is a path from t.to = lead(C ) to every vertex.

Lemma 10. Let par ∈ {0, 1}. There exists k ∈ N such that C k init * − → C k fin and k ≡ par (mod 2) iff there exists n ∈ N, x ∈ N T such that n ≡ par (mod 2), (C n init , x) is compatible and C n fin = C n init + Ax.

Proof. (Sketch.) The left to right implication is easy and follows from the marking equation along with induction on the number of leader transitions in the run. For the other side, we use an idea similar to Lemma 5. Let (C n init , x) be the given compatible pair. We first use Proposition 8 to populate all the states of Q F with enough processes such that all the states of Q F except init F have an even number of processes. Then we use Lemma 9 to construct a firing sequence ξ which can be fired from C n init and such that − → ξ = x. By means of the marking equation, we then argue that in the resulting configuration, the leader is in the final state, n followers are in the state fin F and every other follower state has an even number of followers. Once again, using Proposition 8 we can now move all the processes which are not at fin F to the final state fin F . Lemma 11. Given a symmetric leader protocol, checking whether a cut-off exists can be done in NP.

Proof. By Proposition 6 it suffices to find an even number e and an odd number o such that C e init * − → C e fin and C o init * − → C o fin . Suppose we want to check that there exists 2k ∈ N such that C 2k init * − → C 2k fin . We first non-deterministically guess a set of leader transitions S = {t 1 , . . . , t k } and check that for each t ∈ S, we can reach t.from and t.to from init L using only the transitions in S.

Once we have guessed all this, we write a polynomially sized integer linear program as follows: We let v denote |T | variables, one for each transition in T and we let n be another variable, with all these variables ranging over N. We then enforce the following conditions: C 2n fin = C 2n init + Av and v[t] = 0 ⇐⇒ t / ∈ S and solve the resulting linear program, which we can do in non-deterministic polynomial time [26] . If there exists a solution, then we accept. Otherwise, we reject.

By Lemma 10 and by the definition of compatibility, it follows that at least one of our guesses gets accepted iff there exists 2k ∈ N such that C 2k init * − → C 2k fin . Similarly we can check if exists 2l + 1 ∈ N such that C 2l+1 init * − → C 2l+1 fin . By a reduction from 3-SAT, we prove that Lemma 12. The cut-off problem for symmetric leader protocols is NP-hard.

Continuous and hybrid Petri nets

Computation in networks of passively mobile finite-state sensors

Symbolic counter abstraction for concurrent software

Decidability of Parameterized Verification

The abc of Petri net reachability relaxations

The reachability problem for Petri nets is not elementary

On the complexity of parameterized reachability in reconfigurable broadcast networks

Schloss Dagstuhl -Leibniz-Zentrum für Informatik

Model checking large-scale and parameterized resource allocation systems

Decidability and complexity of Petri net problems -an introduction

Parameterized verification of crowds of anonymous processes

On the verification of broadcast protocols

Verification of population protocols

Decidability issues for Petri nets -a survey

Complexity analysis of continuous Petri nets

Reasoning about systems with many processes

Tutorial on parameterized model checking of fault-tolerant distributed algorithms

Deciding the existence of cut-off in parameterized rendezvous networks

Dynamic cutoff detection in parameterized concurrent programs

Polynomial algorithms for computing the Smith and Hermite normal forms of an integer matrix

On the computational complexity of integer programming problems

The circuit value problem is Log Space complete for

Reachability in vector addition systems is primitiverecursive in fixed dimension

A fast parallel algorithm to compute the rank of a matrix over an arbitrary field

Petri nets: Properties, analysis and applications

Distributed information processing in biological and computational systems

On the complexity of integer programming

Liveness with (0, 1, infty)-counter abstraction

Algorithmic algebraic number theory, Encyclopedia of mathematics and its applications

Continuous Petri nets: Expressive power and decidability issues

Computation with finite stochastic chemical reaction networks

), 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 chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use