Parameterized Verification of Coverability in Well-Structured Broadcast Networks

TL;DR

This paper develops a theoretical framework for verifying coverability in broadcast networks where processes are well-structured transition systems, providing algorithms and decidability results for dynamic and static topologies.

Contribution

It introduces well-structured broadcast networks and proves coverability decidability for both reconfigurable and static topologies.

Findings

Decidability of coverability in reconfigurable well-structured broadcast networks.

Decidability of coverability in static communication topologies.

Algorithm for coverability in networks with link reconfiguration.

Abstract

Parameterized verification of coverability in broadcast networks with finite state processes has been studied for different types of models and topologies. In this paper, we attempt to develop a theory of broadcast networks in which the processes can be well-structured transition systems. The resulting formalism is called well-structured broadcast networks. We give an algorithm to decide coverability of well-structured broadcast networks when reconfiguration of links between nodes is allowed. Further, for various types of communication topologies, we also prove the decidability of coverability in the static case as well. We do this by showing that for these types of static communication topologies, the broadcast network itself is a well-structured transition system, hence proving the decidability of coverability in the broadcast network.