Towards a Maude Tool for Model Checking Temporal Graph Properties

Alberto Lluch Lafuente, Andrea Vandin

Research output: Contribution to journalConference articleResearchpeer-review

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 languageEnglish
JournalElectronic Communications of the EASST
Volume41
Number of pages14
ISSN1863-2122
Publication statusPublished - 2011
Externally publishedYes
Event10th International Workshop on Graph Transformation and Visual Modeling Techniques - Saarbrucken, Germany
Duration: 2 Apr 20113 Apr 2011
Conference number: 10

Conference

Conference10th International Workshop on Graph Transformation and Visual Modeling Techniques
Number10
CountryGermany
CitySaarbrucken
Period02/04/201103/04/2011

Fingerprint Dive into the research topics of 'Towards a Maude Tool for Model Checking Temporal Graph Properties'. Together they form a unique fingerprint.

Cite this