文章基本信息

标题：Towards a Maude Tool for Model Checking Temporal Graph Properties
本地全文：下载
作者：Andrea Vandin ; Alberto Lluch Lafuente
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2011
卷号：41
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：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 mu-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 mu-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.