Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

DOI10.1007/978-3-319-11439-2_6MaRDI QIDQ3447696zbMATH OpenOpenAlexFDO

Authors Giorgio Delzanno, Jan Stückrath

Publication date 28 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.4394

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• Verification of graph transformation systems with context-free specifications
• Verifying a behavioural logic for graph transformation systems
• Towards the Verification of Attributed Graph Transformation Systems
• Unfolding Graph Transformation Systems: Theory and Applications to Verification
• Verifying graph transformation systems with description logics
• Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems
• A framework for the verification of infinite-state graph transformation systems
• Modeling and verifying graph transformations in proof assistants
• Application of Graph Transformation in Verification of Dynamic Systems

Cited in

(6)

• Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems
• Logic-based verification of the distributed dining philosophers protocol
• Verification of graph transformation systems with context-free specifications
• Declarative parameterized verification of distributed protocols via the Cubicle model checker
• scientific article; zbMATH DE number 7453189 (Why is no real title available?)
• Well-structured graph transformation systems

This page was built for publication: Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3447696)