Verification of graph grammars using a logical approach

Graph grammars may be used as specification technique for different kinds of systems, specially in situations in which states are complex structures that can be adequately modeled as graphs (possibly with an attribute data part) and in which the behavior involves a large amount of parallelism and can be described as reactions to stimuli that can be observed in the state of the system. The verification of properties of such systems is a difficult task due to many aspects: the systems in many situations involve an infinite number of states; states themselves are complex and large; there are a number of different computation possibilities due to the fact that rule applications may occur in parallel. There are already some approaches to verification of graph grammars based on model checking, but in these cases only finite state systems can be analyzed. Other approaches propose over- and/or under-approximations of the state space, but in this case it is not possible to check arbitrary properties. This work proposes a relational and logical approach to graph grammars that allows formal verification of systems using mathematical induction. We use relational structures to define graph grammars and first-order logic to model graph transformations. This approach allows proving properties of systems with infinite state spaces. In this paper we first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed graphs, that are graphs in which values are associated to vertices. Attributed graph grammars are very interesting from a practical point of view, since it is possible to use variables and terms when specifying the behavior expressed by rules. These values (or terms) come from algebras specified as abstract data types. The use of attributed graphs gives the specifier a language that is more suitable for specification, merging the advantages of the graphical representation with the standard representation of classical data types. We show that attributes can be smoothly integrated in our representation of graph grammars, giving rise to a framework to reason about attributed graph grammars.