University of Twente Student Theses
Nested quantification in graph transformation rules
Kuperus, J.H. (2007) Nested quantification in graph transformation rules.
![[img]](http://essay.utwente.nl/style/images/fileicons/application_pdf.png) |
PDF
569kB |
| 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. |
| Item Type: | Essay (Master) |
| Clients: | Formal Methods & Tools |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/581 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page