Abstract
We present our prototypical tool for the verification of graph transformation systems. The major novelty of our tool is that it provides a model checker for temporal graph properties based on counterpart semantics for quantified µ-calculi. Our tool can be considered as an instantiation of our approach to counterpart semantics which allows for a neat handling of creation, deletion and merging in systems with dynamic structure. Our implementation is based on the object-based machinery of Maude, which provides the basics to deal with attributed graphs. Graph transformation systems are specified with term rewrite rules. The model checker evaluates logical formulae of second-order modal µ-calculus in the automatically generated Counterpart Model (a sort of unfolded graph transition system) of the graph transformation system under study. The result of evaluating a formula is a set of assignments for each state, associating node variables to actual nodes.
| Original language | English |
|---|---|
| Journal | Electronic Communications of the EASST |
| Volume | 41 |
| Number of pages | 14 |
| ISSN | 1863-2122 |
| Publication status | Published - 2011 |
| Externally published | Yes |
| Event | 10th International Workshop on Graph Transformation and Visual Modeling Techniques - Saarbrucken, Germany Duration: 2 Apr 2011 → 3 Apr 2011 Conference number: 10 |
Conference
| Conference | 10th International Workshop on Graph Transformation and Visual Modeling Techniques |
|---|---|
| Number | 10 |
| Country/Territory | Germany |
| City | Saarbrucken |
| Period | 02/04/2011 → 03/04/2011 |