Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems (Full Version)

TL;DR

This work addresses proving (non-)reachability of bad states in potentially infinite state spaces arising from graph transformation and reactive systems described by nested conditions. It combines abstract interpretation to obtain a finite abstraction with a counter-example guided abstraction refinement loop to iteratively refine a finite predicate set until conclusive results or time limits are reached. The framework is formulated in a general category-theoretic setting, with states as arrows, transitions as conditional rules, and abstractions driven by a finite set of nested conditions; a prototype for graphs (DPO-like rules on $\mathbf{Graph}_{fin}$) is implemented and evaluated on small cases. The results highlight the practicality of CEGAR in this setting, while also identifying challenges—especially entailment in nested conditions—that limit scalability and motivate further refinement and tooling improvements.

Abstract

This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.

Figures (2)

• Figure 1: A schematic depiction of the CEGAR loop
• Figure 2: Composition of cospans $f$ and $g$ is done via pushouts

Theorems & Definitions (3)

• definition thmcounterdefinition: Condition
• definition thmcounterdefinition: Satisfaction
• definition thmcounterdefinition: Reactive system rules