Showing 1–2 of 2 results for author: Stückrath, J

Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

Authors: Giorgio Delzanno, Jan Stückrath

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… ▽ More 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. △ Less

Submitted 18 July, 2014; v1 submitted 16 July, 2014; originally announced July 2014.

Comments: Extended version of a submittion accepted at RP'14 Workshop

A General Framework for Well-Structured Graph Transformation Systems

Authors: Barbara König, Jan Stückrath

Abstract: 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) WS… ▽ More 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. △ Less

Submitted 18 June, 2014; originally announced June 2014.

Comments: Extended version (including proofs) of a paper accepted at CONCUR 2014