Graph Transformation Systems (GTS) and Petri Nets (PN) are two central, theoretically sound, formal models for concurrent or distributed systems. A lot of papers have focused on the relationship between GTS and PN. It is generally accepted that PN are instances of GTS due to the lack of ability to adapt or reconfigure their structure. In this paper, which extends a recent one, we reverse this perspective by presenting a formal definition of GTS in terms of Symmetric Nets (SN). SN are a standard High-Level PN formalism featuring a compact syntax which highlights behavioral symmetries of systems. The major strength lies in the possibility of using well-established tools to edit/efficiently analyze (SN-based) graph transformation models. We follow a structural approach, based on a newly implemented symbolic calculus, to validate Graph Transformation Rules (GTR) and formally verify GTS properties. In the second part of the paper, we supply a semantic characterization of the SN-based graph transformation model, by carrying out a thorough comparison with the classical, algebraic double-pushout (DPO) approach. We constructively and formally show how to translate any DPO rule to a corresponding, elementary or composite, SN rule. We treat both injective and non-injective DPO rules/rule matches. The comparison shows that the SN approach is, in some sense, a generalization of the DPO.

A structural approach to graph transformation based on symmetric Petri nets / L. Capra. - In: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING. - ISSN 2352-2208. - 120(2021 Apr), pp. 100639.1-100639.27. [10.1016/j.jlamp.2021.100639]

A structural approach to graph transformation based on symmetric Petri nets

L. Capra
2021

Abstract

Graph Transformation Systems (GTS) and Petri Nets (PN) are two central, theoretically sound, formal models for concurrent or distributed systems. A lot of papers have focused on the relationship between GTS and PN. It is generally accepted that PN are instances of GTS due to the lack of ability to adapt or reconfigure their structure. In this paper, which extends a recent one, we reverse this perspective by presenting a formal definition of GTS in terms of Symmetric Nets (SN). SN are a standard High-Level PN formalism featuring a compact syntax which highlights behavioral symmetries of systems. The major strength lies in the possibility of using well-established tools to edit/efficiently analyze (SN-based) graph transformation models. We follow a structural approach, based on a newly implemented symbolic calculus, to validate Graph Transformation Rules (GTR) and formally verify GTS properties. In the second part of the paper, we supply a semantic characterization of the SN-based graph transformation model, by carrying out a thorough comparison with the classical, algebraic double-pushout (DPO) approach. We constructively and formally show how to translate any DPO rule to a corresponding, elementary or composite, SN rule. We treat both injective and non-injective DPO rules/rule matches. The comparison shows that the SN approach is, in some sense, a generalization of the DPO.
Double pushout; Graph transformation systems; Operational semantics; Structural analysis; Symmetric nets
Settore INF/01 - Informatica
apr-2021
Article (author)
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 5.15 MB
Formato Adobe PDF
5.15 MB Adobe PDF Visualizza/Apri
1-s2.0-S235222082100002X-main.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 1.94 MB
Formato Adobe PDF
1.94 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/847492
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact