Graph Grammars: A Comparison between Verification Methods

Graph grammars are a formal specification language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. Graph grammars can be analysed through model-checking and theorem proving. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. The main aim of this paper is to present the main existing approaches for the analysis of graph grammars considering each one of these techniques, describing a brief comparative between them.