{"id":"18b80745-450f-439b-a70e-fd44165dc5e5","arxiv_id":"1909.01750","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A graph transformation system is given an operational semantics in Symmetric Nets, with structural conditions that keep the encoding well-defined.","lead":"This paper formalizes graph transformation systems as Symmetric Nets, a class of colored Petri nets, where graph states are markings and rewriting rules are transition firings. It shows how existing Petri net tools and a structural calculus can be used to analyze graph rewriting rules.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Property 1 is false: a transition satisfying conditions 1–6 can delete a node and add an edge incident to it, producing a dangling edge and a non-graph-encoding marking.","rationale":"The reader identified the finite color class limitation as the weakest assumption, but the more fundamental issue is that the main theorem, Property 1, admits a concrete counterexample. Conditions 1–6 as written do not prevent a transition from deleting a node and simultaneously adding an edge incident to that deleted node. The example above is a fully legitimate SN transition under the paper's syntax, satisfies all six structural conditions, and fires from a graph-encoding marking to a marking with a dangling edge. Therefore the central claim that the SN firing rule is a faithful graph rewriting operation is not merely unproved; it is false in the stated generality. The finite-N issue is real and explicitly acknowledged, but it is a scope limitation; the counterexample is a correctness flaw in the core formal claim. A repaired version could add the missing preservation condition and then prove a corrected Property 1, so the approach is not hopeless, but the current manuscript cannot be accepted as-is. This moves the verdict from CONDITIONAL to REJECT.","tokens_in":11532,"tokens_out":13887,"duration_ms":129108,"concrete_test":"Implement the transition described above in GreatSPN/SNExpression syntax: I[Node]=n1+n2, O[Node]=n3, I[Edge]=<n1,n2>, O[Edge]=<n1,n3>, H[Node]=n3, H[Edge]=((<All-n1,n1>+<n1,All>) composed with (n1+n2)) - <n1,n2>. Use SNExpression to symbolically verify that conditions 1–6 all hold. Then fire the instance (R, n1=nd1, n2=nd2, n3=nd3) from the graph-encoding marking m(Node)=nd1+nd2, m(Edge)=<nd1,nd2>. If the tool reports the six conditions true and the resulting marking contains nd1 in Edge but not in Node, the counterexample is confirmed and Property 1 is refuted.","verdict_should_be":"REJECT","load_bearing_attack":"The central formal claim is Property 1 in Section 3.3: any transition whose arc functions satisfy conditions 1–6 preserves graph-encoding markings. This is not merely under-proved; it is false. Conditions 4–6 are meant to prevent dangling edges, but condition 4 only forces output of nodes that occur in new edges and do not occur in input edges or input nodes. It does not require that a node deleted by the rule be absent from output edges. Consider a transition R on N={nd1,nd2,nd3} with I[Node,R]=n1+n2, O[Node,R]=n3, I[Edge,R]=<n1,n2>, O[Edge,R]=<n1,n3>, H[Node,R]=n3, and H[Edge,R]=((<All-n1,n1>+<n1,All>) composed with (n1+n2)) - <n1,n2>. Check the six conditions: NA = (<n1+n3> - <n1+n2>) - (n1+n2) = <n3> ⊆ O[Node,R]; W+[Node,R]=n3 ≤ H[Node,R]; W+[Edge,R]=<n1,n3> is covered by <All,n3> in condition 5; condition 6 holds with equality. From m(Node)=nd1+nd2 and m(Edge)=<nd1,nd2>, R is enabled; firing removes nd1, nd2 and <nd1,nd2>, then adds nd3 and <nd1,nd3>. The resulting marking has nd1 in Edge but not in Node, so it is not a graph-encoding. Hence Property 1 fails as stated. The repair is to require that every node appearing in output edges either is in O[Node,R] or is preserved (not in W-[Node,R]); equivalently, condition 4 should subtract W-[Node,R] rather than I[Node,R], and an additional check should forbid output edges incident to deleted, non-preserved nodes.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":11878,"tokens_out":16148,"duration_ms":152705,"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":[{"comment":"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":"Section 3.3, Property 1"},{"comment":"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.","section":"Section 3.1"}],"minor_comments":[{"comment":"'AS an example' should read 'As an example'.","section":"Section 2.2.4"},{"comment":"The phrase 'conditions 1-6)' has an inconsistent parenthesis; it should be 'conditions 1-6'.","section":"Section 3.3"},{"comment":"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":"Section 3.4"},{"comment":"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":"Section 4"},{"comment":"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.","section":"Section 3.3"}],"recommendation":"major_revision","confidential_remarks":"The core theorem needs repair, but the flaw is local and the proposed encoding is still promising. I recommend major revision rather than rejection. The finite color-class limitation should be clearly scoped in the revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nThe 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]=<n1,n2>, O[Edge]=<n1,n3>, H[Node]=n3, and H[Edge] the set of all edges incident to n1 or n2 except <n1,n2>. Conditions 1–6 all hold. In a graph-encoding marking containing only n1, n2, and <n1,n2>, the transition is enabled. Firing removes n1, n2, and <n1,n2>, then adds n3 and <n1,n3>, leaving n1 present in Edge but absent from Node. That is not a graph-encoding. So Property 1 fails.\n\nWhat 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.\n\nThere 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.\n\nWho 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.","headline":"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.","tokens_in":12446,"tokens_out":11359,"would_cite":false,"duration_ms":95015,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q85","68Q42"],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["graph transformation systems","symmetric nets","coloured Petri nets","operational semantics","graph rewriting","symbolic reachability graph","structural analysis","rule well-definedness"],"falsifier":"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.","tokens_in":11298,"feed_emoji":"🕸️","tokens_out":6395,"duration_ms":61284,"temperature":0.7,"pith_summary":"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.","feed_headline":"One encoding turns graph rewriting rules into symmetric net transitions","feed_subtitle":"Each graph rule becomes a net transition; reachable states give the semantics, and structural checks validate the rules.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines Symmetric Nets (formerly well-formed nets), the formalism on which the entire encoding is built.","marker":"[6]"},{"why":"Introduces symbolic reachability graphs, used here to fold isomorphic graph-encoding markings into a compact state space.","marker":"[7]"},{"why":"Provides the symbolic calculus for structural properties of symmetric nets that the paper uses to verify the six well-definedness conditions.","marker":"[3]"},{"why":"Defines the high-level language for structural relations in well-formed nets, on which the SC, SCC, and SME relations are based.","marker":"[4]"},{"why":"Shows Petri net classes as instances of graph transformation systems, the perspective that this paper reverses.","marker":"[13]"},{"why":"Supplies the tool used to build the ordinary and symbolic reachability graphs presented in the paper's examples.","marker":"[1]"}],"fun_headline_variants":["Symmetric nets turn graph rules into firing transitions","Graph rewriting semantics encoded in symmetric nets","Symbolic validation of rules via symmetric net firing","Reachability of symmetric nets equals graph rewriting","One encoding makes graph rules become net transitions"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Symmetric nets turn graph rules into firing transitions","Graph rewriting semantics encoded in symmetric nets","Symbolic validation of rules via symmetric net firing","Reachability of symmetric nets equals graph rewriting","One encoding makes graph rules become net transitions"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000582,"raw_usage":{"total_tokens":2684,"prompt_tokens":833,"completion_tokens":1851,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":449,"completion_tokens_details":{"reasoning_tokens":1783}},"tokens_in":449,"tokens_out":1851,"duration_ms":13300,"temperature":1.0,"reasoning_tokens":1783,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T05:08:05.958894+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Chiola, C","cited_arxiv_id":null,"evidence_quote":"Defines Symmetric Nets (formerly well-formed nets), the formalism on which the entire encoding is built."},{"cited_title":"Chiola, C","cited_arxiv_id":null,"evidence_quote":"Introduces symbolic reachability graphs, used here to fold isomorphic graph-encoding markings into a compact state space."},{"cited_title":"Capra, M","cited_arxiv_id":null,"evidence_quote":"Provides the symbolic calculus for structural properties of symmetric nets that the paper uses to verify the six well-definedness conditions."},{"cited_title":"Kreowski (1980): A Comparison Between Petri-Nets and Graph Grammars","cited_arxiv_id":null,"evidence_quote":"Shows Petri net classes as instances of graph transformation systems, the perspective that this paper reverses."},{"cited_title":"Baarir, M","cited_arxiv_id":null,"evidence_quote":"Supplies the tool used to build the ordinary and symbolic reachability graphs presented in the paper's examples."}],"review_version":1}