{"id":"30a07da7-1935-42d1-beb0-d17ccd47a227","arxiv_id":"2501.15325","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Skip-free unified-star axioms are complete for bisimilarity on any supported, malleable equational theory, generalizing Grabmayer-Fokkink and yielding new probabilistic completeness theorems.","lead":"For process algebras whose branching is governed by an equational theory, the paper proves a general completeness theorem: a uniform axiom system captures bisimilarity whenever the theory admits support and is malleable. This unifies known completeness results and yields new ones for probabilistic process algebras.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Entry/body rules in Prop 5.7 label non-existent transitions when the star term s does not depend on u, so Proposition 5.7 is unsound for the syntax as defined.","rationale":"The reader identified Theorem 2.13 as the weakest assumption, but that is an imported published result whose use is direct. A more immediate and internal problem is in the paper's own derivation of (Expressivity). Proposition 5.7 defines an entry/body labelling of (Exp,γ) by rules (10), which are copied from the binary-star case. For the general star e(s)1e2 these rules are not sound: when s(u,v)=v, the expression e(s)1e2 is semantically just e2, so it need not have the self-loop or loop-entry transitions that the rules assert. The example a(v)b in SL is a concrete witness: Fig. 3 gives γ(a(v)b)=γ(b)={(b,✓)}, with no self-loop, but rule (10) derives an entry self-loop. Consequently the constructed relation is not an entry/body labelling at all, and Proposition 5.7 fails as written. Because Theorem 5.15 relies on Proposition 5.7 to show that every generated subsystem is in the class C, this is a load-bearing gap in the proof of the central claim. The theorem may still be true, and the gap may be repairable by adding an occurrence condition on u in s to rules (10), but the paper currently does not state or prove such a repair. Therefore the appropriate verdict is CONDITIONAL: the completeness proof is incomplete until Proposition 5.7 is corrected or the syntax is restricted. This is an internal correctness issue rather than a concern about external consensus, so it overrides the external-theorem concern as the primary objection.","tokens_in":37860,"tokens_out":39076,"duration_ms":360617,"concrete_test":"Instantiate T=SL with e1=a, e2=b, s(u,v)=v. Compute γ(a(v)b) using Fig. 3: since s=v, γ(a(v)b)=γ(b)={(b,✓)}. Verify that (a(v)b, a(v)b) is not in the transition relation, while rule (10) derives a(v)b →e a(v)b. If this holds, the labelling in Proposition 5.7 is not a partition of →δ, confirming the gap. A further check is to repair the rule by adding the condition that u occurs in s (or supp(sρ) contains its first variable) and re-run Proposition 5.7 for all s; if the repair is not stated, the completeness proof is incomplete.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The completeness theorem depends on Proposition 5.7 for (Expressivity), i.e., that (Exp,γ) is well-layered with respect to the entry/body labelling defined by rules (10). But rules (10) are not valid for arbitrary S-terms s(u,v): the first two rules assert that e(s)1e2 has a loop-entry transition whenever e1 can reach success, regardless of whether s actually uses u. According to Fig. 3, γ(e(s)1e2) = sρ(γ(e1(e(s)1e2)), γ(e2)); if s(u,v)=v, this is just γ(e2). For T=SL, e1=a, e2=b, s=v, we have γ(a(v)b) = {(b,✓)}, so there is no transition a(v)b → a(v)b. Rule (10) nonetheless derives a(v)b →e a(v)b. Thus the relation →e is not a partition of the actual transition relation, and the construction in Proposition 5.7 is not an entry/body labelling. Example 4.3 explicitly allows s=v, so this is not an excluded case. Since Proposition 5.7 is the only source of (Expressivity) for the class of well-layered M-systems, the proof of Theorem 5.15 is incomplete for the syntax as presented.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a unifying framework for axiomatizing bisimilarity in process algebras with branching parametrized by an equational theory T. It introduces skip-free unified-star expressions Exp over an arbitrary equational theory, defines a syntactic M-system (Exp, γ), and proposes an inference system T∗ (Figure 4). The main theorem (Theorem 5.15) states that for every supported, malleable equational theory T, bisimilarity of expressions coincides with provable equivalence in T∗. The proof adapts the Grabmayer--Fokkink completeness argument: it establishes expressivity (the syntactic system is well-layered), closure under homomorphic images (via the imported Theorem 2.13), and solvability (unique canonical solutions to well-layered M-systems). The framework is claimed to recover completeness for the semilattice theory SL∗ and guarded algebra GA∗, and to yield new completeness theorems for convex algebra CA∗ and guarded convex algebra GC∗.","tokens_in":38097,"tokens_out":16355,"duration_ms":159606,"significance":"If the main theorem is correct, this is a valuable and genuinely abstract contribution: it isolates two structural conditions (support and malleability) under which a uniform completeness proof works, recovers two known results, and produces new completeness theorems for probabilistic and guarded-probabilistic process algebras. The paper is also careful to give nontrivial nonexamples, such as convex semilattices, and to state the reliance on the external closure theorem of Grabmayer and Fokkink. The proof is mostly in the appendix and follows the expected architecture, but the validity of Proposition 5.7 is essential and, as detailed below, needs repair before the main theorem is established.","major_comments":[{"comment":"The entry/body rules in (10) do not respect the actual transition structure for star terms whose term s does not depend on the loop variable u. For T = SL, take e1 = a, e2 = b and s(u,v) = v. Then by Fig. 3, γ(a(v)b) = vρ(γ(a(a(v)b)), γ(b)) = γ(b) = {(b, ✓)}, so there is no transition a(v)b → a(v)b. Rule (10) nevertheless derives a(v)b →e a(v)b via the first or second premise, since a → ✓. Because Definition 2.11 requires →e to be a partition of the actual transition relation →δ, this is not an entry/body labelling of (Exp, γ). Example 4.3 explicitly allows s = v, so the issue is not an excluded case. Since Proposition 5.7 is the only source of (Expressivity) for the class of well-layered M-systems, the proof of Theorem 5.15 is incomplete for the syntax as defined. The rules need to be restricted to star terms that actually use u (or the syntax of Exp needs to be changed accordingly), and the proof of Lemma C.2 must be reworked under that restriction.","section":"Section 5, Proposition 5.7"},{"comment":"The well-layeredness conditions as written are inconsistent with self-loop entry transitions, which the rules generate for genuinely looping terms such as a(u)b with T = SL and s(u,v) = u. The actual chart has a(u)b →a a(u)b, and rule (10) labels this self-loop as →e. Property 2 then requires a(u)b →b+ a(u)b, contradicting property 1. The proof of Proposition 5.7 in the appendix avoids the contradiction by proving property 2 only for transitions with e′ ≠ e. If the intended definition of well-layered is meant to exclude the case x = y in property 2, that exclusion must be stated explicitly; otherwise the definition and the rules are in direct conflict.","section":"Definition 2.11 and rules (2)/(10)"}],"minor_comments":[{"comment":"In Example 4.3, the line 'γ(a ∗ b) = ...' should presumably read 'γ((a + b) ∗ c) = ...', since the surrounding text is discussing (a + b) ∗ c.","section":"Section 2, Example 4.3"},{"comment":"Please clarify whether property 2 of well-layeredness applies to self-loop entry transitions; the proof in the appendix silently uses it only for transitions with distinct source and target.","section":"Section 2, Definition 2.11"},{"comment":"The statement of Lemma C.2 uses the notation f1(e(s)1 e2) with f1 ranging over expressions, but in the case e1 → ✓ the apparent form would require f1 to be the success marker, which is not an expression. This case needs to be separated out or stated more carefully.","section":"Appendix C, Lemma C.2"},{"comment":"The statement of the main theorem should explicitly note that it depends on the imported closure result Theorem 2.13 (Grabmayer--Fokkink), which is not reproved in this paper.","section":"Section 5, Theorem 5.15"}],"recommendation":"major_revision","confidential_remarks":"The paper is a strong and valuable abstraction, and I would not reject it: the main architectural idea is sound and the counterexample raised by the stress-test is a local but load-bearing defect in the entry/body labelling. The fix appears to be within the scope of the framework—restrict the star syntax or the rules to terms that actually depend on the loop variable u, and repair Definition 2.11 and Lemma C.2 accordingly. The dependence on the external Theorem 2.13 should be prominently stated, as it is a genuine black-box premise of the completeness theorem. I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the abstract framework is genuinely appealing, and if the main theorem were solid it would be a nice unification. But there is a real gap in the proof of Proposition 5.7 that breaks Theorem 5.15 for the syntax as defined.\n\nThe new material: support and malleability are clean conditions, and showing that SL, GA, CA, and GC all fit is useful. Recovering the Grabmayer–Fokkink result and adding probabilistic regular expressions and generalized ProbGKAT is a genuine contribution, assuming the result holds. The appendix is detailed and the proof strategy is transparent.\n\nThe problem: the entry/body rules (10) in Appendix C are not sound with respect to the actual transition relation. The first rule says from e1 → ✓ deduce e(s)1 e2 →e e(s)1 e2, regardless of whether s actually uses u. But if s(u,v)=v, then γ(e(s)1 e2) = γ(e2), so there is no such transition. Concretely, with T=SL, e1=a, e2=b, s=v, we have γ(a(v)b) = {(b,✓)} and no self-loop. Yet rule (10) derives a(v)b →e a(v)b. Example 4.3 explicitly allows s=v, so this isn't a corner case. A self-loop entry transition violates well-layeredness (property 2 requires y →b+ x, impossible), so (Exp,γ) is not well-layered via this labelling, Proposition 5.7 fails, and (Expressivity) collapses. Since the completeness theorem depends on this, Theorem 5.15 is unproven for the full syntax.\n\nCould this be patched? Maybe by requiring u to occur in s, or by adjusting the rules to only fire when the transition exists. But the paper imposes no such restriction, and the examples depend on s=v. So as submitted, the main result doesn't go through.\n\nThe imported Theorem 2.13 is also heavy, but that's a known external result; the real issue is internal. This is a paper that could be fixed, but it needs a substantive revision. It deserves a serious referee, but not acceptance in its current form.","headline":"A promising unification with a real gap: the entry/body rules in Proposition 5.7 are unsound for star terms that don't use the loop variable, so Theorem 5.15 is unproven as stated.","tokens_in":38644,"tokens_out":5788,"would_cite":false,"duration_ms":50064,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q85","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that for any equational theory with a support and a malleability property, bisimilarity of skip-free star expressions is completely axiomatized by a fixed set of rules, unifying four known or new process-algebra…","keywords":["completeness theorem","bisimilarity","process algebra","equational theory","skip-free star expressions","coalgebra","guarded Kleene algebra with tests","probabilistic regular expressions"],"falsifier":"Find a supported, malleable equational theory T and two skip-free unified-star expressions that are bisimilar in (Exp, γ) yet not provably equal in T*; the easiest place to look is the convex-semilattice theory CS, where malleability fails, or a weighted-transition (semimodule) theory where the canonical solution might not be unique. Alternatively, exhibit a well-layered chart whose homomorphic image is not well-layered, which would refute the imported closure theorem.","tokens_in":37626,"feed_emoji":"⚖️","tokens_out":7288,"duration_ms":62757,"temperature":0.7,"pith_summary":"This paper proves a single completeness theorem for a whole family of process algebras at once. Fix an equational theory T that describes how processes branch — nondeterministically, probabilistically, or under tests; if T has a support (each term has a well-defined set of essential variables) and is malleable (any term can be split along a partition of its variables into s(t1, t2)), then one fixed set of axioms completely axiomatizes bisimilarity for skip-free star expressions over T. The theorem recovers the known completeness results for 1-free regular expressions and skip-free guarded Kleene algebra with tests, and it yields new completeness theorems for probabilistic regular expressions and for guarded convex algebra. The payoff is that five axiom schemes replace a collection of bespoke, hard-won completeness arguments.","feed_headline":"General completeness theorem unifies four process-algebra proofs","feed_subtitle":"Same five axioms completely axiomatize bisimilarity for any supported, malleable branching theory","key_machinery":"The carrying object is an M-system, a coalgebra for the functor M(Act × (✓ + (−))) where M is the free-algebra construction of the branching theory T; the syntactic M-system (Exp, γ) gives every skip-free unified-star expression a transition structure. A support is a natural transformation supp : M ⇒ P that assigns each term its set of essential variables, and malleability says that any term can be rewritten, along any partition of its variables, as s(t1, t2) with t1 and t2 on the two parts. These two conditions allow the well-layered chart technology — entry/body labellings, loop-around reachability, and the canonical solution formula of Definition 5.13 — to be lifted from ordinary charts to arbitrary M-systems.","core_discovery":"The central claim is Theorem 5.15: for every supported, malleable equational theory T, if two skip-free unified-star expressions are bisimilar in the syntactic M-system (Exp, γ), then the equational theory T* proves them equal. The axioms of T* state that provable T-equivalence is respected (T), that sequential composition is associative (A) and right-distributive (D), that the s-star unfolds as a recursion equation (U), and that this recursion equation has a unique solution (RSP). The proof follows the strategy of the earlier 1-free completeness argument: every expression generates a finite, well-layered subsystem; well-layered systems are closed under homomorphic images (by an imported theorem); and every well-layered M-system has a unique solution, computed by a canonical formula. Therefore two bisimilar expressions share a common bisimulation quotient, whose unique solution witnesses their provable equality.","pith_inferences":["The two conditions are plausibly close to necessary, not just sufficient: without support there is no underlying chart to layer, and without malleability the unique-solution formula cannot be built; a characterization of all supported, malleable theories would delimit exactly which branching effects admit such finite axiomatizations.","The semimodule instantiation generalizes to any semiring-valued transition system, suggesting a template for proving completeness of weighted process algebras beyond the three concrete examples.","A concrete stress test is the convex semilattice theory CS: if a counterexample to completeness of CS* exists, it would confirm that the malleability boundary is real, and it might be found by looking at bisimilar pairs whose common quotient needs a non-malleable mixture of convex and semilattice structure."],"forward_implications":["Bisimilarity and provable equivalence coincide for every supported, malleable theory T, so bisimilarity is automatically a congruence for the skip-free expressions of that theory.","The completeness of CA* gives a finitary axiomatization for bisimilarity of 1-free probabilistic regular expressions, and the completeness of GC* does the same for a skip-free variant of probabilistic guarded Kleene algebra with tests.","The two existing completeness results, for SL* and GA*, are not merely analogous but instantiations of one theorem, which explains why their proofs share the same structure.","The framework reduces the open problem of full GKAT completeness to bringing the 'skip' constant into the supported-malleable world, likely by adding a right-annihilation axiom for 0."],"supporting_citations":[{"why":"Supplies the original completeness theorem for 1-free regular expressions (SL*) whose proof strategy this paper abstracts.","marker":"[6]"},{"why":"Provides the well-layered chart machinery, including Theorem 2.13 (closure under homomorphic images) and the canonical solution formula that the proof lifts to M-systems.","marker":"[27]"},{"why":"Establishes the completeness result for skip-free GKAT (GA*) that is recovered as an instantiation.","marker":"[9]"},{"why":"Gives the probabilistic regular expressions whose skip-free fragment yields the new CA* completeness theorem.","marker":"[22]"},{"why":"Introduces probabilistic GKAT (ProbGKAT), whose skip-free variant is captured by the new GC* instantiation.","marker":"[21]"},{"why":"Observes that 1-free star expressions and skip-free GKAT are process algebras parametrised by equational theories, the starting point of this framework.","marker":"[28]"},{"why":"Proves completeness of Milner's full proof system for regular expressions modulo bisimilarity, the long-standing goal this abstract framework ultimately targets.","marker":"[5]"}],"fun_headline_variants":["General completeness theorem unifies skip-free star algebras","Axiomatizing bisimilarity for skip-free star algebras","New completeness theorem for skip-free process algebras","Unified proof: skip-free star algebras have complete axioms","General completeness for skip-free star algebras"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof imports, without reproving, the theorem that well-layered charts are closed under homomorphic images; if that theorem fails, the completeness argument collapses at Theorem 5.9.","fun_headline_variants_meta":{"raw":{"variants":["General completeness theorem unifies skip-free star algebras","Axiomatizing bisimilarity for skip-free star algebras","New completeness theorem for skip-free process algebras","Unified proof: skip-free star algebras have complete axioms","General completeness for skip-free star algebras"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000721,"raw_usage":{"total_tokens":3150,"prompt_tokens":775,"completion_tokens":2375,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":391,"completion_tokens_details":{"reasoning_tokens":2302}},"tokens_in":391,"tokens_out":2375,"duration_ms":14244,"temperature":1.0,"reasoning_tokens":2302,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T14:24:15.927224+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a supported, malleable equational theory T and two skip-free unified-star expressions that are bisimilar in (Exp, γ) yet not provably equal in T*; the easiest place to look is the convex-semilattice theory CS, where malleability fails, or a weighted-transition (semimodule) theory where the canonical solution might not be unique. Alternatively, exhibit a well-layered chart whose homomorphic image is not well-layered, which would refute the imported closure theorem.","supporting_citations":[{"cited_title":"In: ESOP","cited_arxiv_id":null,"evidence_quote":"Establishes the completeness result for skip-free GKAT (GA*) that is recovered as an instantiation."}],"review_version":1}