Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

TL;DR

This paper presents a novel approach for parameterized verification of graph transformation systems with neighborhood-based guards, enabling analysis of complex distributed protocols on arbitrary network structures.

Contribution

It introduces a new class of graph rewrite rules with neighborhood conditions and provides a symbolic verification procedure with proven correctness.

Findings

Successfully verified the Distributed Dining Philosophers protocol on arbitrary networks.

Developed a symbolic procedure working on minimal representations of upward closed sets.

Proved correctness using categorical and well-structured transition system frameworks.

Abstract

We introduce a new class of graph transformation systems in which rewrite rules can be guarded by universally quantified conditions on the neighbourhood of nodes. These conditions are defined via special graph patterns which may be transformed by the rule as well. For the new class for graph rewrite rules, we provide a symbolic procedure working on minimal representations of upward closed sets of configurations. We prove correctness and effectiveness of the procedure by a categorical presentation of rewrite rules as well as the involved order, and using results for well-structured transition systems. We apply the resulting procedure to the analysis of the Distributed Dining Philosophers protocol on an arbitrary network structure.