Abstract

By tradition, researchers working on model checking tools continuously try to make their tools faster and allow them to handle larger models. GROOVE is a model checking tool which uses the mathematical formalism of graphs and graph transformations to specify models and system behavior. Graph transformation systems allow complex models to be visualized and are a natural way of modeling object oriented systems.

Graph transformation systems only allow their rules to be matched existentially, which poses a serious limitation. Complex constructions with so-called helper edges are often created to perform a task more than once. This causes the model to be more complicated than it should be, for both the user and the tool.

This thesis defines an extension of the use of the single pushout approach which allows nesting of alternated quantifiers to an arbitrary depth. This means entire subgraphs may now be matched without first knowing exactly how many nodes it will contain. The formalism has also been implemented in the GROOVE graph transformation tool and shows drastic decreases of required statespace and computing time for several well-known models.

Additional Resources

1. The paper