Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability

Lucie Guillou, Corto Mascle, Nicolas Waldburger

TL;DR

This model lies at the frontier of decidability as other classical problems on this model are undecidable; this is in particular true for the target problem where all processes must synchronize on a given state.

Abstract

We consider the parameterized verification of arbitrarily large networks of agents which communicate by broadcasting and receiving messages. In our model, the broadcast topology is reconfigurable so that a sent message can be received by any set of agents. In addition, agents have local registers which are initially distinct and may therefore be thought of as identifiers. When an agent broadcasts a message, it appends to the message the value stored in one of its registers. Upon reception, an agent can store the received value or test this value for equality with one of its own registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We establish that this problem is decidable; however, it is as hard as coverability in lossy channel systems, which is non-primitive recursive. This model lies at the frontier of decidability as other classical problems on this model are undecidable; this is in particular true for the target problem where all processes must synchronize on a given state. By contrast, we show that the coverability problem is NP-complete when each agent has only one register.

Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability

TL;DR

This model lies at the frontier of decidability as other classical problems on this model are undecidable; this is in particular true for the target problem where all processes must synchronize on a given state.

Abstract

We consider the parameterized verification of arbitrarily large networks of agents which communicate by broadcasting and receiving messages. In our model, the broadcast topology is reconfigurable so that a sent message can be received by any set of agents. In addition, agents have local registers which are initially distinct and may therefore be thought of as identifiers. When an agent broadcasts a message, it appends to the message the value stored in one of its registers. Upon reception, an agent can store the received value or test this value for equality with one of its own registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We establish that this problem is decidable; however, it is as hard as coverability in lossy channel systems, which is non-primitive recursive. This model lies at the frontier of decidability as other classical problems on this model are undecidable; this is in particular true for the target problem where all processes must synchronize on a given state. By contrast, we show that the coverability problem is NP-complete when each agent has only one register.
Paper Structure (34 sections, 41 theorems, 5 equations, 12 figures)

This paper contains 34 sections, 41 theorems, 5 equations, 12 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Definitions of the Model
  4. Classical Definitions
  5. A Complexity Lower Bound for COVER Using LCS
  6. Coverability Decidability for Signature Protocols
  7. Local runs
  8. Unfolding Trees
  9. Bounding the Size of a Coverability Witness
  10. Coverability Decidability in the General Case
  11. Generalizing Unfolding Trees
  12. Bounding the Size of the Unfolding Tree.
  13. Undecidability of the "target problem"
  14. Cover in 1-BNRA
  15. Conclusion
  16. ...and 19 more sections

Key Result

theorem 1

Let $\Sigma$ a finite alphabet and $g : \mathbb{N} \to \mathbb{N}$ a primitive recursive function. There exists a function $f \in \mathscr{F}_{\omega^{|\Sigma| - 1}}$ such that, for all $n \in \mathbb{N}$, every "bad" sequence $w_1, w_2, \ldots$ such that $|w_i| \leq g^{(i)}(n)$ for all $i$ has at m

Figures (12)

  • Figure 1: Example of a "protocol".
  • Figure 2: Example of a "signature protocol".
  • Figure 3: Example of an "unfolding tree@@sg" derived from $\rho$. Grids correspond to "local runs", a column of a grid is a "local configuration". Transition $\delta_{ij}$ is the transition between state $q_i$ and state $q_j$, for example $\delta_{01} = (q_0, \textbf{rec}(\textsf{rdy}, 2, \downarrow), q_1)$. If $\delta$ is a reception of $m\in \mathcal{M}$, $\mathsf{ext}(\delta,v)$ corresponds to receiving message $(m,v)$; if $\delta$ is a broadcast of $m \in \mathcal{M}$, $\mathsf{int}(\delta)$ corresponds to broadcasting $(m,\mathsf{id})$ where $\mathsf{id}$ is the value in the first register of the agent. Initial values of "reception-only" registers are irrevelant and written as $\mlq \_ \mrq$. Colors correspond to message types.
  • Figure 4: Illustration of the proof of \ref{['lem:towerbound_signature']}.
  • Figure 5: Example of an "unfolding tree". $\delta_{ri}$ (resp. $\delta_{bi}$) denotes the reception (resp. broadcast) transition of message $m_i$ in the protocol described in \ref{['fig:ex1']}. Values that are never broadcast are omitted and written as $\mlq \_ \mrq$.
  • ...and 7 more figures

Theorems & Definitions (86)

  • definition 1
  • definition 2: Semantics
  • remark 1
  • remark 2
  • definition 3
  • remark 3
  • definition 4: Signature protocols
  • theorem 1: ""Length function theorem"" SchmitzS2011upperHigman
  • proposition 1
  • proof : Proof sketch
  • ...and 76 more