Christoffer Lind Andersen (1), Radu Iosif (1), and Arnaud Sangnier (2)
(1) Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France
(2) DIBRIS, Università di Genova, Italy
We consider families of networks represented as graphs with processes modelled by automata who can communicate by synchronous broadcast where one node can send out a message which is received by all its neighbours. Our research of network topologies provides a model for distributed systems under 2 different semantics, reliable and unreliable, such that we can study verification of systems, in particular we study the following safety problem known as control state reachability: is there a network in the given family, such that some process can reach an error location?
To answer this verification question we use graphs defined by vertex replacement graph grammars to represent network topologies where each node can be expanded to either a clique or cloud (anti-clique) of an unbounded size. A graph grammar defined by vertex replacement is a set of variables and recursive rules where the derivation of a term leads to a concrete graph using a signature known as the vertex replacement algebra. Graph grammars have a strong connection with monadic second order logic (MSO) where most importantly we know it is decidable if a graph in the language of a grammar satisfies an MSO formula (known as the filtering theorem).
Our main result is a decidability procedure where we provide a labelling of the graph where the nodes a labelled by its reachable states exactly and prove this labelling is consistent with reachability in the network. This labelling is possible because of two properties called the local successor property and the composition property for emitters which are two criteria that the labelling respects. We characterize this labelling as an MSO formula and again prove it is consistent with the reachable states labelling which leads to our general decidability result; if the network semantics satisfies the two criteria, then the safety problem is decidable. For our specific results we show that in general the safety problem is undecidable for reliable communication where there is no loss of messages and everyone who can receive a message has to. Decidability is regained once we consider unreliable communication where we allow receivers to ignore messages. Another way decidability can be regained is restricting the automata by ensuring different processes cannot send and receive messages from the same control state (also known as the wait-only syntactic restriction).