2014/07/16 by Giorgio Delzanno, Delzanno, Giorgio, Jan Stückrath +1
Computer Science · #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Semantic Web and Ontologies #cs.LO
paper · pdf · doi:10.48550/arxiv.1407.4394
Extended version of a submittion accepted at RP'14 Workshop
arxiv created 2014/07/18 · arxiv updated 2014/07/21
We introduce a new class of graph transformation systems in which rewrite rules can be guarded by universally quantified conditions on the neighbourhood of nodes. These conditions are defined via special graph patterns which may be transformed by the rule as well. For the new class for graph rewrite rules, we provide a symbolic procedure working on minimal representations of upward closed sets of configurations. We prove correctness and effectiveness of the procedure by a categorical presentation of rewrite rules as well as the involved order, and using results for well-structured transition systems. We apply the resulting procedure to the analysis of the Distributed Dining Philosophers protocol on an arbitrary network structure.