For several years I have maintained an interest in graph transformation, which combines the strengths of graphs and rules into a single, abstract computational model. In this setting, the state of a computation is represented as a graph, and the computational steps are applications of graph rewrite rules (akin to applications of rules in Chomsky string grammars, but lifted to the richer domain of graphs).
Consider for example the figure to the right, which contains a set of rules, a program constructed over them, and an example execution on the empty graph Ø. Even without giving the formal semantics, it may already be clear – simply from the graphical nature of the rules – that executing the program on the empty graph will construct a tree. Such an execution will apply the rule init exactly once, which dutifully (and unconditionally) creates a fresh node. Then, as demanded by the iteration construct !, the rule grow is repeatedly and nondeterministically applied until some (unspecified) termination condition is satisfied. Each application of this rule requires a node in the graph to be matched (the number establishes which node on the right-hand side is the same one), before gluing onto it an outgoing edge and fresh node. Observe that no matter how many times (if any) the rule grow is applied, the property – or rather, invariant – of being a tree is maintained.
But how do we prove that this invariant is maintained? Or more generally, how do we verify that a program based on graph transformation is correct with respect to a given specification? One might wonder at this point whether this question is even worth answering – but to see that it is, we must look somewhat beyond our tree-generating program, which on its own, fails to convey the power and flexibility of graph transformation. Correctness counts in many of its more practical applications throughout computer science and software engineering: from the semantics and implementation of functional programming languages, to the specification and analysis of pointer structures, object-oriented systems, and model transformations.
Research in verifying graph transformations broadly belongs to one of two camps: model checking or proofs. Although the former is supported by some excellent tools (GROOVE being amongst my favourites), it is also important to explore the latter, which involves the use of logic, semantics, and proof calculi to unequivocally show that programs satisfy their specifications. The seminal work here is due to Karl-Heinz Pennemann, who paved the way to automatic correctness proofs with respect to a logic of first-order graph properties; the theory of which my thesis extended to attribute-manipulating rules.
Unfortunately, the restriction to first-order properties is quite a limiting factor in the context of graphs. In particular, it excludes the possibility of verifying so-called “non-local” properties, of which there are many familiar and important ones: the existence of arbitrary-length paths, the absence of cycles, connectedness, and bipartiteness; to name just a few. Without paths or cycles, what can we prove of interest about our tree-generating program? And in a more practical setting, it is easy to conjure scenarios in which we will suffer. How might we prove the absence of deadlock, for example, in a model of some distributed algorithm, when we cannot reason about the absence of cycles?
Detlef Plump and I set out to address this limitation in our recent paper, Verifying Monadic Second-Order Properties of Graph Programs. First, we extended Pennemann’s logic for graphs to one equivalently expressive to monadic second-order (MSO) logic – a logic very well studied in the context of graph structure (most famously by Bruno Courcelle and his colleagues). The extension allows one to quantify over sets of nodes or edges, and assert that particular nodes or edges belong to particular sets. While a conceptually simple extension, it is rather a powerful one, allowing for a large class of important non-local properties to be expressed – including all of those listed above. Then, and most importantly, we showed that the logic can be integrated into proof systems by defining, and proving correct, an effective weakest precondition construction relative to arbitrary rules and postconditions.
The paper is primarily a theoretical contribution, demonstrating (for the curious!) that this weakest precondition construction can be extended to an MSO-based graph logic. Unfortunately, all but the most trivial formulae of this logic are difficult for users to write and interpret, and the constructed preconditions are not particularly concise. A more practical approach for verification – that the paper also begins to explore – might be to work with a set of more “direct” predicates for particular non-local properties of interest, rather than full MSO. The paper, for example, explores a predicate for expressing the existence of an arbitrary-length path between two given nodes; an important non-local property, but non-trivial to specify in MSO logic. We were particularly pleased to discover that we could define the weakest precondition construction for such predicates entirely in terms of such predicates, i.e. without the need to introduce any set quantifiers.
We published and presented the work at ICGT 2014 (as part of STAF 2014) in York, UK, and would be glad to receive your comments and criticisms. The postprint and slides are available below, and the printed version can be downloaded from SpringerLink.