SearcharxivSearch

arXiv subjects

Jan Stückrath

Publications and source records attributed to Jan Stückrath.

2 recordsLinked to original sources

Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

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.

cs.LO

A General Framework for Well-Structured Graph Transformation Systems

Graph transformation systems (GTSs) can be seen as wellstructured transition systems (WSTSs), thus obtaining decidability results for certain classes of GTSs. In earlier work it was shown that wellstructuredness can be obtained using the minor ordering as a well-quasiorder. In this paper we extend this idea to obtain a general framework in which several types of GTSs can be seen as (restricted) WSTSs. We instantiate this framework with the subgraph ordering and the induced subgraph ordering and apply it to analyse a simple access rights management system.

cs.LO