Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy

TL;DR

The paper studies the cut-off problem for parameterized rendez-vous networks, showing that continuous Petri-net techniques yield sharp elementary bounds across variants. The core contribution is a pair of Scaling and Insertion lemmas that link continuous reachability to discrete runs, enabling polynomial-time solutions for leaderless and certain symmetric cases, along with NC and NP characterizations in other settings. It tightens the complexity landscape established by Horn and Sangnier (CONCUR 2020), proving, among others, that leaderless cut-off lies in P, leaderless symmetric in NC, and symmetric-with-a-leader in NP, with matching lower bounds. It also introduces the bounded-loss cut-off variant and resolves its complexity (P-complete for leaderless, NL-complete for leaderless symmetric). The results rely on a robust Petri-net framework and its continuous semantics, suggesting broader applicability of these methods to parameterized verification problems.

Abstract

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 (Horn and Sangnier, CONCUR 2020), Horn and Sangnier proved that the cut-off problem is decidable (and at least as hard as the Petri net reachability problem) for protocols with a leader, and in EXPSPACE for leaderless protocols. Further, for the special class of symmetric protocols they reduce these bounds to PSPACE and NP, respectively. The problem of lowering these upper bounds or finding matching lower bounds was left open. We show that the cut-off problem is P-complete for leaderless protocols and in NC for leaderless symmetric protocols. Further, we also consider a variant of the cut-off problem suggested in (Horn and Sangnier, CONCUR 2020), which we call the bounded-loss cut-off problem and prove that this problem is P-complete for leaderless protocols and NL-complete for leaderless symmetric protocols. Finally, by reusing some of the techniques applied for the analysis of leaderless protocols, we show that the cut-off problem for symmetric protocols with a leader is NP-complete, thereby improving upon all the elementary upper bounds of (Horn and Sangnier, CONCUR 2020).

Figures (10)

• Figure 1: An example of a rendez-vous protocol
• Figure 2: Petri net corresponding to the protocol from Figure \ref{['fig:expo']}
• Figure 3: A net with cut-off 2.
• Figure 4: A modification of the protocol from Figure \ref{['fig:expo']}
• Figure 5: Petri net corresponding to the protocol from Figure \ref{['fig:expo-1']}

Theorems & Definitions (87)

• Definition 2.1
• Example 2.2
• Definition 2.3
• Proposition 2.4
• proof
• Proposition 2.5
• Example 2.6
• Theorem 2.7
• Corollary 2.8
• Proposition 3.1: Murata89