{"id":"9425beb4-5c70-4875-9725-bd598fda3b30","arxiv_id":"1908.08635","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A process graph semantics for transition system specifications is proposed, and four sanity requirements are shown to transfer from the classical closed-term semantics.","lead":"This paper gives transition system specifications a new kind of semantics: open terms denote operations on process graphs, not abbreviations for their closed instances. This makes the meaning of operators independent of the surrounding language and repairs a known expressiveness theorem.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Abstract overstates Theorem 2: sanity of P alone does not imply sanity of the process graph semantics; the theorem needs sanity of every extension P+BZ*, and this extra strength is essential.","rationale":"The reader's weakest assumption identifies exactly the gap that matters: Theorem 2 requires the closed-term semantics of every extension P+BZ* to be sane, not merely that of P. The counterexample above shows this is not a pedantic distinction—the abstract's literal implication is false, because a TSS whose own closed-term semantics is trivially compositional up to ↔w can fail compositionality under the process graph semantics once arbitrary process graphs are allowed as valuations. The formal theorem itself is correct as stated, and the proof of Theorem 2 uses the strong antecedent in an essential way when choosing BZ* adequate for the two valuations. The only required change is to the public summary: it must quantify over extensions P+BZ*. Since this is precisely the reader's condition, the conditional verdict stands unchanged. I found no independent flaw in the central construction or in Proposition 5 sufficient to alter the verdict.","tokens_in":20538,"tokens_out":16075,"duration_ms":172332,"concrete_test":"Formalize the counterexample: take P with constant 0 and unary f, with the single rule (x -τ-> y) / f(x) -a-> 0. Check that (i) P's closed-term LTS has no transitions, so its closed-term semantics satisfies (2′)–(5′) up to ↔w; (ii) for BZ*={τ.0, 0}, the closed terms τ.0 and 0 are ↔w-related but f(τ.0) -a-> 0 while f(0) has no a, so Theorem 2's antecedent fails for P+BZ*; (iii) the process graph semantics of P fails requirement (2) up to ↔w for ρ(x)=τ.0 and ν(x)=0. If all three hold, the abstract and introduction must be revised to state the quantified-extension hypothesis.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The transfer claim in the abstract and introduction—that satisfaction of requirements (2)–(5) under the closed-term semantics of a TSS implies their satisfaction under the process graph semantics—is false as stated. Theorem 2 in Section 11 has a strictly stronger antecedent: the closed-term semantics of P + BZ* must satisfy the requirements for every transition-closed set BZ* of process graphs added as constants. This is not a cosmetic strengthening. Let P contain constant 0 and a unary operator f with the single pure rule (x -τ-> y) / f(x) -a-> 0. In P itself no closed term has any transition, so the closed-term semantics satisfies (2′)–(5′) up to weak bisimilarity ↔w. However, for BZ* = {τ.0, 0}, the closed-term semantics of P+BZ* fails (2′): the closed terms τ.0 and 0 are weakly bisimilar, yet f(τ.0) -a-> 0 and f(0) has no a-transition. The same failure transfers to the process graph semantics of P: with ρ(x)=τ.0 and ν(x)=0, we have [x]_P(ρ) ↔w [x]_P(ν) but [f(x)]_P(ρ) not ↔w [f(x)]_P(ν). Thus the condition 'P itself is sane' cannot be substituted for the theorem's 'every extension P+BZ* is sane,' and the abstract's implication is materially too strong.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a process graph semantics for transition system specifications (TSSs), in which every closed term denotes a process graph and every open term denotes an operation on process graphs, in contrast to the classical closed-term semantics that interprets open terms via their closed instantiations. The paper defines the semantics for pure TSSs, proves that for pure TSSs the process graph equivalence is finer than the closed-term equivalence under mild conditions (Theorem 1), and proves a transfer theorem stating that if the closed-term semantics of every extension P + BZ* satisfies sanity requirements (2)-(5) up to the relevant equivalence, then so does the process graph semantics of P (Theorem 2). The paper also discusses congruence properties, compares several equivalences on open terms, and argues that the process graph semantics repairs a failure of preservation of relative expressiveness under conservative extensions. The main theorems are stated with proofs, while Proposition 5 is only sketched and the Section 12 expressiveness result relies on definitions from a previous paper.","tokens_in":20794,"tokens_out":5983,"duration_ms":62025,"significance":"If the central claims are correct, the paper offers a principled alternative to the standard closed-term semantics of SOS, with a concrete example showing that the process graph semantics avoids context-dependent identification of operators. The transfer theorem for sanity requirements is a useful tool that lets existing congruence results for closed-term semantics be reused for the new semantics. The paper is careful about the role of the semantic equivalence relation and about the distinction between manifest and non-manifest induction of a process graph semantics. The detailed proofs of Theorems 1 and 2 are a definite strength, as are the worked examples. However, the advertised implication in the abstract is materially stronger than the actual Theorem 2, and the proof of Proposition 5, which underpins the well-definedness of the semantics for all pure TSSs, is only sketched.","major_comments":[{"comment":"The abstract and the introduction state that satisfaction of requirements (2)-(5) under the closed-term semantics of a TSS implies their satisfaction under the process graph semantics, but Theorem 2 has a strictly stronger hypothesis: the closed-term semantics of every extension P + BZ* must satisfy the requirements for every transition-closed set BZ* of process graphs added as constants, not merely the closed-term semantics of P itself. This strengthening is essential. Let P be the pure TSS with constant 0 and unary f with the single rule (x -τ-> y) / f(x) -a-> 0. In P no closed term has any transition, so the closed-term semantics of P satisfies (2')-(5') up to weak bisimilarity. However, for BZ* = {τ.0, 0}, the closed-term semantics of P + BZ* fails (2'): the closed terms τ.0 and 0 are weakly bisimilar, yet f(τ.0) -a-> 0 while f(0) has no a-transition. The same failure transfers to the process graph semantics of P, using the valuation sending x to τ.0 versus 0. Thus the abstract's implication is false as stated, and the introduction should state the theorem with its actual hypothesis.","section":"Abstract and §1 (cf. §11, Theorem 2)"},{"comment":"Proposition 5, which asserts that every pure TSS manifestly induces a process graph semantics, is the result that makes the semantics well-defined for all pure TSSs and is used in Theorem 1 and in the applications. Its proof is only a sketch, referring to a 'fairly straightforward induction on the size of proofs, with a nested induction on the derivation of rule-boundedness'. Since the well-definedness of the central semantics rests on this proposition, the proof should be given in full, with the induction invariants stated explicitly. As written, a reader cannot verify the nontrivial part of the argument, namely that all terms occurring in a proof of a transition of t[ρ] are of the form t'[ρ] with values already in the minimal set BZ*_0.","section":"§8, Proposition 5"},{"comment":"The expressiveness preservation claim (9) is one of the advertised payoffs of the process graph semantics, but it is not substantiated in this manuscript. The definition of validity of a translation is not given; it is only said that the proof is 'entirely straightforward' once definitions from [14] are supplied. As a result, the claim that the process graph semantics makes (9) hold is not checkable from the paper. Please either include the relevant definitions from [14] and a proof of (9) under the stated mild conditions, or clearly label the discussion as an informal pointer to previous work rather than a theorem proved here.","section":"§12"}],"minor_comments":[{"comment":"In the definition of the lifted equivalence on closed terms, the clause 'whenever (Tr(Σ), A, →, p) ∼ (Tr(Σ), A, →, p)' has a typo: the second p should be q.","section":"§9, Definition 12"},{"comment":"Observation 1 writes 'p, q ∈ Tr(σ)', but σ is not defined at that point and the intended set is Tr(Σ), the closed terms over Σ.","section":"§11, Observation 1"},{"comment":"The notation for recursive terms uses a non-ASCII escape sequence in the display; the rendering should be fixed so that the term /\\X |S\\/ appears consistently in both the definition and the proofs.","section":"§2, Definition 1"},{"comment":"The sentence 'In any adequate choice of BZ* there is a graph in which an a-transition and a b-transition end in a common state' is phrased as a claim about adequacy, but the property needed is transition closure; the wording should be adjusted to avoid confusion.","section":"§8, Example 3"},{"comment":"The concluding paragraph says that requirements (4) and (5) 'surely hold up to any coarser equivalence'; this is true, but the argument is only implicit and could be stated in one sentence for completeness.","section":"§14"}],"recommendation":"major_revision","confidential_remarks":"The paper is a workshop-style contribution and the central transfer theorem is sound with its correct hypothesis, but the abstract and introduction overstate the theorem in a way that a reader could easily rely on. The proof of Proposition 5 should be completed before the paper is accepted in its current form, and the Section 12 claim needs either a proof or an explicit caveat that it depends on definitions from a separate paper. These are fixable issues, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me give you the short version: this is a real contribution, and the main theorems appear to hold, but the abstract overstates what Theorem 2 proves. The stress-test note is correct: the transfer result needs sanity of every extension P + BZ*, not just of P. The counterexample with f(x) -a-> 0 works. So the paper is in good shape formally, but the public summary needs fixing.\n\nWhat's new: van Glabbeek defines a process graph semantics for TSSs by adding process graphs as constants and reading an open term as an operation on graphs. This gives a context-independent meaning to operators, something the closed-term semantics lacks. For pure TSSs, the semantics is well-defined (Proposition 5) and more discriminating than the closed-term semantics (Theorem 1). The hierarchy in Section 13 and the congruence example in Section 10 are nice. The five sanity requirements framework is imported from his earlier work, and Theorem 2 is a useful transfer tool: it lets existing congruence-format results for closed-term semantics be reused. That is worth having.\n\nThe soft spots, in proportion. The big one is the abstract and intro: they say satisfaction under the closed-term semantics of a TSS implies satisfaction under the process graph semantics. Theorem 2 actually requires the closed-term semantics of P + BZ* to satisfy the requirements for every transition-closed set of added process graphs. That is not a cosmetic strengthening. The stress-test example is a clean counterexample to the weaker reading. This should be fixed in the abstract, intro, and concluding remarks; readers who only read those will be misled.\n\nTwo lesser gaps: Proposition 5's proof is a sketch ('straightforward induction') and it is the step that guarantees adequacy for pure TSSs. I believe it, but it deserves a fuller write-up. And Section 12's expressiveness-preservation claim depends on the definition of valid translation from [14], which is not included, so the paper can't fully substantiate the claim that (9) holds under process graph semantics. That is a dependence on prior work, not necessarily a flaw, but it keeps that section at the level of an argument sketch.\n\nBottom line: the central construction and the two main theorems are the kind of thing the SOS community will want to cite. The paper deserves a serious referee and, after the abstract/Theorem 2 mismatch is corrected, publication. It is a workshop paper in length but not in scope.","headline":"A genuinely useful process graph semantics for open terms in TSSs, with a real but fixable mismatch between the abstract's transfer claim and Theorem 2's actual hypothesis.","tokens_in":21318,"tokens_out":2615,"would_cite":true,"duration_ms":25007,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q55","68Q85"],"pacs":[],"model":"deepseek-v4-flash","headline":"A pure TSS gives open terms a context-free meaning as operations on process graphs, not as families of closed instantiations.","keywords":["Transition System Specifications","structural operational semantics","process graphs","closed-term semantics","process graph semantics","compositionality","congruence","recursion"],"falsifier":"To test Theorem 1, look for a pure TSS $P$, an equivalence $\\approx$ on process graphs that identifies each graph with its reachable part, and open terms $t,u$ such that $t \\approx^{pg}_P u$ but some closed substitution $\\sigma$ gives $t[\\sigma] \\not\\approx u[\\sigma]$. To test Theorem 2, find a pure TSS whose extensions $P + \\mathcal{BZ}^*$ all satisfy requirements (2)--(5) under the closed-term semantics, yet the process graph semantics violates one of them, for instance a binary operator that is compositional on closed terms but not on graph-valued arguments.","tokens_in":20284,"feed_emoji":"","tokens_out":5653,"duration_ms":58056,"temperature":0.7,"pith_summary":"This paper argues that the standard closed-term semantics of Transition System Specifications makes the meaning of an operator depend on which other terms happen to be expressible in the language. It proposes an alternative process graph semantics in which open terms denote operations on process graphs directly, evaluated under arbitrary graph-valued valuations. For pure TSSs this semantics always exists, and the equivalence it induces on open terms is at least as discriminating as the closed-term one. The paper also proves a transfer theorem: if the closed-term semantics of every extension of the TSS by graph constants satisfies four of the five sanity requirements, then the process graph semantics satisfies them too. The payoff is that operator meanings remain stable when the language is enriched.","feed_headline":"Process graphs, not closed terms, fix operator meaning","feed_subtitle":"A process graph semantics for pure TSSs keeps operator meaning stable when languages gain new constants.","key_machinery":"The central device is the extension $P + \\mathcal{BZ}^*$: add every graph in a transition-closed set $\\mathcal{BZ}^*$ as a constant, with its transitions as axioms, then define $\\llbracket t \\rrbracket_P(\\rho)$ as the reachable part of the closed term $t[\\rho]$ in $P + \\mathcal{BZ}^*$. A graph set is adequate when enlarging it does not change this value; purity of the TSS guarantees that every supporting transition-closed set is adequate (Proposition 5). A second load-bearing component is the substitution lemma (Proposition 3), which says $\\llbracket t[\\sigma] \\rrbracket(\\rho) \\sim \\llbracket t \\rrbracket(\\llbracket \\sigma \\rrbracket(\\rho))$ under requirements (1)--(4), and this links graph-valued valuations to closed substitutions in the proof of Theorem 1.","core_discovery":"The paper establishes a new interpretation for TSSs. Closed terms are interpreted as the reachable part of the process graph generated by the provable transitions of the TSS; open terms are interpreted by adjoining a transition-closed set of process graphs as constants, evaluating the term under a graph-valued valuation, and taking the reachable part of the resulting closed-term graph. A TSS is pure when every variable in a rule is rule-bound, and pure TSSs induce this semantics unambiguously (Proposition 5). Theorem 1 shows that for pure TSSs, under mild conditions, $t \\approx^{pg}_P u$ implies $t \\approx^{ci}_P u$, so the process graph equivalence is finer; in general the two are incomparable. Theorem 2 shows that requirements (2)--(5), namely compositionality for operators, compositionality for recursion and variables, invariance under $\\alpha$-conversion, and the recursive definition principle, transfer from the closed-term semantics of every extension $P + \\mathcal{BZ}^*$ to the process graph semantics. Requirement (1) does not transfer, but it holds for TSSs whose rules never have a variable as the left-hand side of a conclusion.","pith_inferences":["If the transfer theorem is right, it suggests a modular proof discipline: establish sanity of a language once under closed-term semantics, and obtain a context-independent graph model without additional work; this could simplify future congruence proofs for process algebras with recursion.","The construction via graph-valued constants suggests a general recipe for turning any inductively defined operational semantics into a denotational-style model, with purity as the syntactic condition that makes the model stable under enlargement of the value domain.","A testable extension would be to see whether the process graph semantics can be adapted to timed or probabilistic transitions by choosing appropriate graph-like values, as long as an analogous purity condition holds.","One subtle boundary is requirement (1): it fails for rules that copy transitions through variables, so languages whose rules put variables on the left of conclusions need a separate check; the paper shows the requirement holds when no rule conclusion has a variable as its source."],"forward_implications":["For pure TSSs, changing the ambient language by adding operators, constants, or rules cannot silently change the meaning of existing open terms, because meanings are read off from arbitrary process graphs rather than from the closed terms of the current signature.","Semantic equivalences lifted to open terms via the process graph semantics are finer than via the closed-term semantics (Theorem 1), so accidental identifications like $f(x) \\sim id(x)$ in Example 1 disappear once $\\tau$-transitions become possible.","The expressiveness preorder is preserved under conservative extensions under the process graph semantics, whereas it fails under the closed-term semantics (Section 12).","Sanity requirements (2)--(5) do not need to be re-proved from scratch for the new semantics: existing closed-term congruence and recursion results for formats such as ntyft/ntyxt transfer automatically (Theorem 2).","The recursive definition principle and invariance under $\\alpha$-conversion hold for the process graph semantics of pure TSSs in the ntyft/ntyxt format with recursion, since they already hold for the closed-term semantics."],"supporting_citations":[{"why":"Defines Transition System Specifications and the tyft/tyxt format; supplies the notion of purity that Proposition 5 generalises.","marker":"[16]"},{"why":"Proposes the five sanity requirements used in Section 3 and transferred in Theorem 2.","marker":"[10]"},{"why":"Introduces process graphs and their use as a semantic domain for process algebras.","marker":"[3]"},{"why":"Provides strong bisimulation and the CCS-style process calculi used in the examples and in lifting equivalences.","marker":"[21]"},{"why":"Gives congruence and recursion formats under the closed-term semantics, which Theorem 2 transfers to the process graph semantics.","marker":"[13]"},{"why":"Supplies the theory of encodings and expressiveness used in Section 12 to show failure under closed-term semantics and success under process graph semantics.","marker":"[14]"},{"why":"Provides the analysis of open-term bisimilarity that yields the hierarchy $\\leftrightarrow^{fh} \\subseteq \\leftrightarrow^{hp} \\subseteq \\leftrightarrow^{pg} \\subseteq \\leftrightarrow^{ci}$.","marker":"[23]"}],"fun_headline_variants":["A context-free semantics for transition system specifications","Pure TSSs get finer process graph equivalence","Why operator meaning should come from process graphs","Four TSS sanity conditions transfer to graph semantics"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The transfer theorem assumes the closed-term semantics is sane not merely for the original TSS, but for every extension that adds arbitrary process graphs as new constants; it is this stronger assumption that lets open terms be evaluated under arbitrary graph-valued valuations.","fun_headline_variants_meta":{"raw":{"variants":["A context-free semantics for transition system specifications","Pure TSSs get finer process graph equivalence","Why operator meaning should come from process graphs","Four TSS sanity conditions transfer to graph semantics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000295,"raw_usage":{"total_tokens":1749,"prompt_tokens":1014,"completion_tokens":735,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":630,"completion_tokens_details":{"reasoning_tokens":678}},"tokens_in":630,"tokens_out":735,"duration_ms":7639,"temperature":1.0,"reasoning_tokens":678,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:34:09.680913+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"To test Theorem 1, look for a pure TSS $P$, an equivalence $\\approx$ on process graphs that identifies each graph with its reachable part, and open terms $t,u$ such that $t \\approx^{pg}_P u$ but some closed substitution $\\sigma$ gives $t[\\sigma] \\not\\approx u[\\sigma]$. To test Theorem 2, find a pure TSS whose extensions $P + \\mathcal{BZ}^*$ all satisfy requirements (2)--(5) under the closed-term semantics, yet the process graph semantics violates one of them, for instance a binary operator that is compositional on closed terms but not on graph-valued arguments.","supporting_citations":[{"cited_title":"Bergstra & J.W","cited_arxiv_id":null,"evidence_quote":"Introduces process graphs and their use as a semantic domain for process algebras."},{"cited_title":"Milner (1990): Operational and algebraic semantics of concurrent process es","cited_arxiv_id":null,"evidence_quote":"Provides strong bisimulation and the CCS-style process calculi used in the examples and in lifting equivalences."},{"cited_title":"Rensink (2000): Bisimilarity of Open T erms","cited_arxiv_id":null,"evidence_quote":"Provides the analysis of open-term bisimilarity that yields the hierarchy $\\leftrightarrow^{fh} \\subseteq \\leftrightarrow^{hp} \\subseteq \\leftrightarrow^{pg} \\subseteq \\leftrightarrow^{ci}$."}],"review_version":1}