Checking Graph Programs for Confluence

Abstract

We present a method for statically verifying confluence (functional behaviour) of terminating sets of rules in the graph programming language GP 2, which is undecidable in general. In contrast to other work about attributed graph transformation, we do not impose syntactic restrictions on the rules except for left-linearity. Our checking method relies on constructing the symbolic critical pairs of a rule set using an E-unification algorithm and subsequently checking whether all pairs are strongly joinable with symbolic derivations. The correctness of this method is a consequence of the main technical result of this paper, viz. that a set of left-linear attributed rules is locally confluent if all symbolic critical pairs are strongly joinable, and our previous results on the completeness and finiteness of the set of symbolic critical pairs. We also show that for checking strong joinability, it is not necessary to compute all graphs derivable from a critical pair. Instead, it suffices to focus on the pair’s persistent reducts. In a case study, we use our method to verify the confluence of a graph program that calculates shortest distances.