An Operational Semantics of Graph Transformation Systems Using Symmetric Nets

TL;DR

This paper presents an operational semantics for graph transformation systems using Symmetric Nets, bridging GTS and Petri nets to enhance analysis and validation of concurrent models.

Contribution

It introduces a novel approach to formalize GTS semantics with Symmetric Nets, enabling symbolic validation of graph rewriting rules.

Findings

Operational semantics for GTS via Symmetric Nets

Validation of graph rewriting rules using structural calculus

Enhanced analysis techniques for concurrent systems

Abstract

Graph transformation systems (GTS) have been successfully proposed as a general, theoretically sound model for concurrency. Petri nets (PN), on the other side, are a central and intuitive formalism for concurrent or distributed systems, well supported by a number of analysis techniques/tools. Some PN classes have been shown to be instances of GTS. In this paper, we change perspective presenting an operational semantics of GTS in terms of Symmetric Nets, a well-known class of Coloured Petri nets featuring a structured syntax that outlines model symmetries. Some practical exploitations of the proposed operational semantics are discussed. In particular, a recently developed structural calculus for SN is used to validate graph rewriting rules in a symbolic way.