Formal Verification of Graph Grammars using Mathematical Induction

Graph grammars are a formal description technique suitable for the specification of distributed and reactive systems. Model-checking of graph grammars is currently supported by various approaches. However, in many situations the use of this technique can be very time and space consuming, hindering the verification of properties of many systems. 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.