An Operational Semantics of Graph Transformation Systems Using Symmetric Nets

Italy); Lorenzo Capra (Dipartimento di Informatica Universit\`a degli Studi di Milano; Milan

REVIEW 2 major objections 5 minor 14 references

An Operational Semantics of Graph Transformation Systems Using Symmetric Nets

T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Graph transformation systems acquire an operational semantics in Symmetric Nets: each rewriting rule becomes a net transition sharing two places that encode the graph, and six structural conditions guarantee every firing rewrites one…

desk verdict A novel and practical GTS-to-Symmetric-Nets encoding undercut by a false well-definedness theorem: Property 1 fails on a concrete counterexample, so the paper needs a corrected condition and proper proof before it can be accepted. read the letter →

arxiv 1909.01750 v1 pith:WL7CGEKR submitted 2019-09-04 cs.FL

Lorenzo Capra (Dipartimento di Informatica Università degli Studi di Milano , Milan , Italy) This is my paper · ORCID

classification cs.FL MSC 68Q8568Q42

keywords graphtransformationsystemssymmetricnetscolouredPetrioperationalsemanticsrewritingsymbolicreachabilitystructuralanalysisrulewell-definedness

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper tries to establish that a graph transformation system can be executed and analysed as a Symmetric Net, a coloured Petri net with an explicit symmetry-aware syntax. The central move is to encode a directed graph as the combined marking of two places, Node and Edge, and to encode each rewriting rule as a transition connected to those places. The claim is that if a transition satisfies six purely structural conditions, then every firing on a graph-encoding marking produces another graph-encoding marking, so the net's reachability graph is an operational interleaving semantics for the graph transformation system. If this holds, existing net-based state-space and structural analysis techniques apply to graph rewriting, including automatic symbolic checks that rules are well defined.

What carries the argument

The load-bearing object is the encoding of a graph as the shared marking of two places, Node (colour domain N) and Edge (colour domain N×N), together with the six structural conditions on a transition's arc functions. Conditions 1 and 2 enforce simplicity, meaning that checks and generated edges never require multiplicities above one; condition 3 prevents node duplication; conditions 4 through 6 prevent dangling edges by requiring newly referenced nodes to be inserted and by using inhibitor arcs to ensure that withdrawn nodes have no incident edges except those removed contextually. Property 1 is the result that these conditions are sufficient. A second piece of machinery is the symbolic structural calculus on arc functions, whose terms include transpose, composition, difference, and support, from which the symbolic relations SC, SCC, and SME are defined and used to analyse potential conflicts among rule instances.

What would settle it

Build a graph transformation system containing Rule 1d, which creates a new node, and fix a colour class N of size k. Starting from a one-node graph, fire the rule repeatedly; after k-1 firings the encoded graph has k distinct nodes, and the next firing would need a new colour not present in N, so no valid binding exists and the net's reachability graph stops. The original graph transformation system, if nodes are unbounded, continues, directly contradicting the claim that the encoding models all possible evolutions.

Watch

Extended reading notes

Core claim

The paper's central claim is that graph rewriting can be formalized inside Symmetric Nets without leaving the net formalism. A graph is a set of node tokens and edge tokens; a rule is a transition whose input, output, and inhibitor arcs match a subgraph, delete it, and insert the rewritten subgraph. Property 1 states that any transition satisfying the six conditions listed in Section 3.3 is well defined: the firing of any valid instance in a graph-encoding marking always yields a graph-encoding marking. Consequently, the reachability graph of the net is exactly the state-transition system of the graph transformation system, and, when the initial marking is symbolic, the symbolic reachability graph is a quotient that folds isomorphic graph states. The paper also shows that the same structural calculus used to prove well-definedness can compute conflict and concurrency relations among rules, so rule validation becomes a symbolic calculation.

Load-bearing premise

The load-bearing premise is that the single finite colour class N always has enough distinct colours to name every node that can appear during the graph system's evolution; if some run creates more nodes than |N|, the symmetric net cannot represent that run.

Editorial extensions

If this is right

Every graph transformation system whose rules satisfy conditions 1 through 6 can be analysed with the full state-space machinery of symmetric nets, because the reachability graph is the operational interleaving semantics of the system.
With a symbolic initial marking, the symbolic reachability graph folds isomorphic graphs into one state while preserving liveness and safety properties, which can drastically reduce the number of states for highly symmetric graphs.
Rule well-definedness becomes a symbolic, automatable check: the six conditions are expressed as equivalences of arc-function terms, so a tool can verify them without enumerating net unfoldings.
The structural relations SC, SCC, and SME give necessary conditions for conflict, causal connection, and mutual exclusion, so a designer can detect which rules are potentially concurrent and which instances are mutually exclusive.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial extension: if Property 1 is accepted, the same two-place encoding should extend to multigraphs and hypergraphs by relaxing the simplicity conditions and making the inhibitor-arc checks multiplicity-aware; the paper only sketches this as ongoing work, so this is an extrapolation.
Editorial extension: the symbolic reachability graph's reduction depends on the automorphism group of the graph being rewritten; on graphs with few symmetries the canonicalization cost, which the paper notes is comparable to graph isomorphism, may outweigh the state-space saving.
Editorial extension: the six conditions are sufficient but not obviously necessary; a testable question is whether every rewriting rule that preserves graph-encoding markings can be re-expressed to satisfy them, or whether some safe rules are excluded.
Editorial extension: if the conjectured bridge to double-pushout rewriting is built, then the SN structural calculus would provide an algebraic way to compute pushout conflicts symbolically; until then, the relationship between SN rules and pushout derivations remains open.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

You should know two things about Capra's arXiv:1909.01750. The idea is genuinely useful: encode graph transformation systems as Symmetric Nets in the reverse direction (GTS into SN, instead of the usual PN-as-GTS), opening up GreatSPN and the SNExpression structural calculus for graph rewriting. The encoding is simple and the worked examples are reproducible. The second thing is that the paper's central well-definedness result, Property 1, is false as stated. The one-sentence "proof" is not just thin; the claim fails on a concrete counterexample.

The problem is in conditions 4–6. They prevent dangling edges that would come from pre-existing edges incident to a deleted node, but they do not prevent a rule from adding an output edge incident to a node that the same rule deletes. Consider a transition with I[Node]=n1+n2, O[Node]=n3, I[Edge]=, O[Edge]=, H[Node]=n3, and H[Edge] the set of all edges incident to n1 or n2 except . Conditions 1–6 all hold. In a graph-encoding marking containing only n1, n2, and , the transition is enabled. Firing removes n1, n2, and , then adds n3 and , leaving n1 present in Edge but absent from Node. That is not a graph-encoding. So Property 1 fails.

What is worth saving: the direction is new, the symbolic concurrency check via SC/SME relations is a sensible use of the author's earlier calculus, and the informal encoding idea is sound. But the formal core is load-bearing and broken. The fix is not deep—require that any node incident to an output edge and deleted by the rule be re-added in O[Node], e.g. by adding a condition like nodes(O[Edge]) ∩ W-[Node] ⊆ O[Node], or by modifying condition 4 to subtract W-[Node] rather than I[Node]. Until such a condition is added and Property 1 is proved properly, the paper is not acceptable.

There is also the acknowledged finite-color-class limitation: the encoding covers only bounded node creation. That is a scope restriction, not a fatal flaw, and the author states it. The open relationship to DPO is explicitly left for future work, which is honest.

Who should read this: anyone working on bridging graph rewriting with Petri net tools, and reviewers of a revised version. The counterexample above should appear in the revision. I'd send the paper back for major revision rather than desk reject; the idea deserves referee time.

Referee Report

2 major / 5 minor

Summary. This paper proposes an operational semantics for graph transformation systems based on Symmetric Nets. A directed graph is encoded as the marking of two places Node and Edge over a finite color class N; each graph rewriting rule is encoded as a transition connected to those places, with input, output, and inhibitor arc functions. Six structural conditions are given as sufficient for a rule to be well-defined, and Property 1 claims that any rule satisfying them preserves graph-encoding markings. The paper then illustrates the encoding on several rules, shows how the symbolic reachability graph folds isomorphic graphs, and uses the SN structural calculus to compute conflict and causal relations on a small GTS. The paper concludes with directions for multigraphs and for comparing the approach with algebraic graph transformation.

Significance. If the main property held, the encoding would be a useful bridge between GTS and a well-supported Petri net formalism, giving symbolic reachability and structural analysis for free. The paper is clearly written and the examples are concrete; the encoding idea is simple, and the use of existing SN tools (GreatSPN, SNExpression) is a practical strength. However, the central correctness property is false as stated, and the finite color-class assumption restricts the class of GTS that can be represented. The manuscript needs a corrected well-definedness condition and an actual proof before the central claim can be accepted.

major comments (2)

[Section 3.3, Property 1] The claim of Property 1 is false. Consider a transition R with variables n1,n2,n3 and arc functions I[Node,R]=n1, O[Node,R]=n2, I[Edge,R]=<n1,n3>, O[Edge,R]=<n1,n2>, H[Node,R]=n2, and H[Edge,R] the set of all edges incident to n1 except <n1,n3> (for instance the support of <All,n1>+<n1,All>-<n1,n3>). Conditions 1-6 are satisfied: NA=(n1+n2)-(n1+n3)-n1 = n2 is contained in O[Node,R]; W+[Edge,R]=<n1,n2> is contained in <All,NA>; condition 6 holds by the definition of H[Edge,R]; the other conditions are immediate. Starting from the graph-encoding marking m with m(Node)=nd1+nd3 and m(Edge)=<nd1,nd3>, the instance (n1,n2,n3)=(nd1,nd2,nd3) is enabled; firing removes nd1 and <nd1,nd3> and adds nd2 and <nd1,nd2>, producing m(Node)=nd3 and m(Edge)=<nd1,nd2>, in which nd1 occurs in Edge but not in Node. The gap is that condition 4 only requires output-edge nodes absent from all input arcs to be added to Node; it does not prevent an output edge from being incident to a node that is withdrawn from Node but also occurs in the input edge. A necessary additional condition is that every node in the support of W+[Edge,R] either belongs to O[Node,R] or is not withdrawn, i.e., (<n1+n2> composed with O[Edge,R]) intersect W-[Node,R] is a subset of O[Node,R]. The proof of Property 1 must be expanded to a real proof of this corrected condition.
[Section 3.1] The encoding assumes a finite basic color class N with 'enough elements to cover all possible evolutions of a graph.' Since Symmetric Nets have finite color classes, the proposed semantics only applies to GTS whose reachable graphs never require more than |N| nodes. Rules 1d and 1f, which create new nodes, are therefore representable only up to that bound. The paper should explicitly restrict the scope of the claimed operational semantics to node-bounded GTS and discuss the consequences for the examples and for the practical claims in the abstract and conclusions.

minor comments (5)

[Section 2.2.4] 'AS an example' should read 'As an example'.
[Section 3.3] The phrase 'conditions 1-6)' has an inconsistent parenthesis; it should be 'conditions 1-6'.
[Section 3.4] The notation 'mG0(Node) =<nd1 + nd2 + nd3 + nd4>' is ambiguous; a multiset should be written as a formal sum without angle brackets, and the surrounding text should use consistent notation for multisets.
[Section 4] The sentence 'all the calculus were done with SNExpression tool' is ungrammatical; it should state that all computations were performed with the SNExpression tool and should identify the version used for reproducibility.
[Section 3.3] The assertion that all rules in Figure 1 are well-defined is not verified in the text; since the conditions are central, the paper should either provide the symbolic expressions that satisfy each condition or make the verification scripts available in the repository.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the graph encoding and well-definedness conditions are defined directly in the paper, and the cited self-authored structural calculus is used as tool support rather than as the basis of the central claim.

full rationale

The central derivation is the encoding of a graph as a marking of places Node and Edge, the translation of graph rewriting rules into SN transitions, and the claim (Property 1) that transitions satisfying conditions 1–6 preserve graph-encoding markings. These notions are introduced directly in Sections 3.1–3.3 and do not presuppose the target result. The conditions are local structural criteria on arc functions, and Property 1 is a preservation claim about those criteria; even if the proof sketch is terse ('The proof is just a direct consequence of the explanation above'), that is a proof-strength issue, not circularity. The paper does cite prior work by the same author, especially [3], [4], and [5], for the SN structural calculus and the SNExpression tool. Those citations are used to automate the checking of the conditions and to compute structural relations; they are not used to define the encoding or to justify Property 1. Thus the self-citations are present but not load-bearing for the claimed operational semantics. The paper is not self-contained in the sense of giving a fully formal proof of Property 1, and the skeptical counterexample suggests the sufficient conditions may be too weak, but that would be a correctness defect, not a circular reduction of the result to its inputs.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No numerical parameters are fitted; the paper introduces no new entities. The construction relies on standard Symmetric Net semantics, on a finite color class assumption, and on prior structural calculus results. Dynamic subclasses and symbolic markings are existing SN notions from the cited literature.

assumptions (4)

domain assumption Symmetric Net theory and symbolic reachability graph semantics are correct and applicable.
Section 2 introduces SN concepts from [6] and [7]; the paper does not re-derive them.
domain assumption The basic color class N is finite and contains enough elements for all graph evolutions considered.
Stated in Section 3.1. This bounds the set of reachable graphs and is not guaranteed for arbitrary GTS with unbounded node creation.
domain assumption Graph encodings are restricted to set-valued markings with multiplicities at most one and no dangling edges.
Section 3.1 defines graph-encoding markings this way; all further arguments assume the invariant holds before each firing.
domain assumption The structural calculus of [3] and [4] is sound and the SNExpression tool computes the stated symbolic relations.
Section 4 uses the calculus to compute SC and SME relations; no independent verification is given in this paper.

how reviews work

0 comments

Cite this review

Pith. "Pith review of An Operational Semantics of Graph Transformation Systems Using Symmetric Nets." pith.science (2026). https://pith.science/paper/WL7CGEKR

@misc{pith2026190901750,
  author       = {Pith},
  title        = {Pith review of: An Operational Semantics of Graph Transformation Systems Using Symmetric Nets},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WL7CGEKR}},
  note         = {Machine review of arXiv:1909.01750}
}

read the original 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.

Figures

Figures reproduced from arXiv: 1909.01750 by the authors.

**Figure 2.** a simple GTS composed of Rules 1,3 that when applied to an instance c 0 of t 0 gives the set of instances of t that are in such a relation with (t 0 , c 0 ). Symbolic relations build on a couple of auxiliary ones, involving a pair place/transition, both with arity cd(p) → 2 cd(t) : Rb[t, p] = W−[p,t] t (Removed by), given a color c of p provides the set of instances of t that withdraw c from p; Ab[t, p] = W+[p,t] t … view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

14 extracted references · 10 canonical work pages

[1]

Baarir, M

S. Baarir, M. Beccuti, D. Cerotti, M. De Pierro, S. Donatelli & G. Franceschinis (2009): The GreatSPN Tool: Recent Enhancements. SIGMETRICS Perform. Eval. Rev. 36(4), pp. 4–9, doi:10.1145/1530873.1530876

work page arXiv 2009
[2]

Baldan, A

P. Baldan, A. Corradini, F. Gadducci & U. Montanari (2010): From Petri Nets to Graph Transformation Systems. ECEASST 26, doi:10.14279/tuj.eceasst.26.368

work page doi:10.14279/tuj.eceasst.26.368 2010
[3]

Capra, M

L. Capra, M. De Pierro & G. Franceschinis (2015): Computing structural properties of symmetric nets , pp. 125–140. 9259, Springer International Publishing, doi:10.1007/978-3-319-22264-6 9

work page doi:10.1007/978-3-319-22264-6 2015
[4]

Capra, M

L. Capra, M. De Pierro & G. Franceschinis (2005): A High Level Language for Structural Relations in Well-Formed Nets. In: Proc. of the 26th Int. Conf. A TPN 2005 , LNCS 3536, Springer, pp. 168–187, doi:10.1007/11494744 11

doi:10.1007/11494744 2005
[5]

Capra, M

L. Capra, M. De Pierro & G. Franceschinis (2013): A Tool for Symbolic Manipulation of Arc Functions in Symmetric Net Models . In: Proceedings of the 7th International Conference on Per- formance Evaluation Methodologies and Tools , ValueTools ’13, ICST, Torino, Italy, pp. 320–323, doi:10.4108/icst.valuetools.2013.254407

work page arXiv 2013
[6]

Chiola, C

G. Chiola, C. Dutheillet, G. Franceschinis & S. Haddad (1993): Stochastic well-formed colored nets and symmetric modeling applications . IEEE Transactions on Computers 42(11), pp. 1343–1360, doi:10.1109/12.247838

work page doi:10.1109/12.247838 1993
[7]

Chiola, C

G. Chiola, C. Dutheillet, G. Franceschinis & S. Haddad (1997): A symbolic reachability graph for coloured petri nets. Theoretical Computer Science 176(1), pp. 39 – 65, doi:10.1016/S0304-3975(96)00010-2

work page doi:10.1016/s0304-3975(96)00010-2 1997
[8]

A Corradini (2006): Concurrent graph and term graph rewriting . pp. 438–464, doi:10.1007/3-540-61604- 7 69

work page doi:10.1007/3-540-61604- 2006

Show all 14 references

[9]

Dutheillet & S

C. Dutheillet & S. Haddad (1993): Conﬂict Sets in Colored Petri Nets. In: proc. of Petri Nets and Performance Models, pp. 76–85, doi:10.1109/PNPM.1993.393433

1993
[10]

Ehrig & J

H. Ehrig & J. Padberg (2003): Graph Grammars and Petri Net Transformations . pp. 496–536, doi:10.1007/978-3-540-27755-2 14

2003 doi
[11]

Jensen (1997): Coloured Petri Nets

K. Jensen (1997): Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. V olume 1, Basic Concepts. Monographs in Theoretical Computer Science, Springer-Verlag, 2nd corrected printing 1997. ISBN: 3-540-60943-1., doi:10.1007/978-3-662-03241-1

1997 doi
[12]

Jensen & G

K. Jensen & G. Rozenberg, editors (1991): High-level Petri Nets: Theory and Application. Springer-Verlag, London, UK, doi:10.1007/978-3-642-84524-6

1991 doi
[13]

Kreowski (1980): A Comparison Between Petri-Nets and Graph Grammars

H.J. Kreowski (1980): A Comparison Between Petri-Nets and Graph Grammars. 100, pp. 306–317, doi:10.1007/3-540-10291-4 22

1980 doi
[14]

Reisig (1985): Petri Nets: An Introduction

W. Reisig (1985): Petri Nets: An Introduction . Springer-Verlag New York, Inc., New York, NY , USA, doi:10.1007/978-3-642-69968-9

1985 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Baarir, M

S. Baarir, M. Beccuti, D. Cerotti, M. De Pierro, S. Donatelli & G. Franceschinis (2009): The GreatSPN Tool: Recent Enhancements. SIGMETRICS Perform. Eval. Rev. 36(4), pp. 4–9, doi:10.1145/1530873.1530876

work page arXiv 2009

[2] [2]

Baldan, A

P. Baldan, A. Corradini, F. Gadducci & U. Montanari (2010): From Petri Nets to Graph Transformation Systems. ECEASST 26, doi:10.14279/tuj.eceasst.26.368

work page doi:10.14279/tuj.eceasst.26.368 2010

[3] [3]

Capra, M

L. Capra, M. De Pierro & G. Franceschinis (2015): Computing structural properties of symmetric nets , pp. 125–140. 9259, Springer International Publishing, doi:10.1007/978-3-319-22264-6 9

work page doi:10.1007/978-3-319-22264-6 2015

[4] [4]

Capra, M

L. Capra, M. De Pierro & G. Franceschinis (2005): A High Level Language for Structural Relations in Well-Formed Nets. In: Proc. of the 26th Int. Conf. A TPN 2005 , LNCS 3536, Springer, pp. 168–187, doi:10.1007/11494744 11

doi:10.1007/11494744 2005

[5] [5]

Capra, M

L. Capra, M. De Pierro & G. Franceschinis (2013): A Tool for Symbolic Manipulation of Arc Functions in Symmetric Net Models . In: Proceedings of the 7th International Conference on Per- formance Evaluation Methodologies and Tools , ValueTools ’13, ICST, Torino, Italy, pp. 320–323, doi:10.4108/icst.valuetools.2013.254407

work page arXiv 2013

[6] [6]

Chiola, C

G. Chiola, C. Dutheillet, G. Franceschinis & S. Haddad (1993): Stochastic well-formed colored nets and symmetric modeling applications . IEEE Transactions on Computers 42(11), pp. 1343–1360, doi:10.1109/12.247838

work page doi:10.1109/12.247838 1993

[7] [7]

Chiola, C

G. Chiola, C. Dutheillet, G. Franceschinis & S. Haddad (1997): A symbolic reachability graph for coloured petri nets. Theoretical Computer Science 176(1), pp. 39 – 65, doi:10.1016/S0304-3975(96)00010-2

work page doi:10.1016/s0304-3975(96)00010-2 1997

[8] [8]

A Corradini (2006): Concurrent graph and term graph rewriting . pp. 438–464, doi:10.1007/3-540-61604- 7 69

work page doi:10.1007/3-540-61604- 2006