{"id":"f2519165-7373-46c0-93ff-347c1dffe33b","arxiv_id":"1909.00286","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"This paper defines a synchron-based concurrency relation for CCS, ABC, and CCSS, making the justness criterion formally available and proving it agrees with previous coinductive definitions.","lead":"Justness is a completeness criterion for which runs of a distributed system count as complete, sitting between progress and fairness. This paper defines a precise concurrency relation for CCS and its broadcast and signal extensions, and proves it yields a feasible justness notion that matches earlier definitions.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Closure property (2) rests on Lemma 6's informal 'delete dynamic nodes' argument; a counterexample there would invalidate the LTSC construction, so Proposition 6 deserves a direct exhaustive check.","rationale":"The reader and I identify the same fragile premise: the derivation-tree shape is assumed to fully determine transition interference. I locate that premise concretely in Lemma 6 and its use in Proposition 6, which underpins Corollary 3. The concern is not that Lemma 6 is false; it is that the proof is informal at exactly the point where residual existence is derived from synchron shapes. Since the central claim is a formal theorem, a direct computational verification of Proposition 6 is the cheapest way to test it. The agreement theorems with [16] and [7] give consistency among the paper's own definitions but do not externally validate this closure step, and Theorem 1 assumes (2) rather than establishing it. No counterexample surfaced during review, so the reader's ACCEPT verdict stands; the proposed check would either raise confidence further or expose a refutation.","tokens_in":37263,"tokens_out":20593,"duration_ms":235695,"concrete_test":"Implement Definitions 8–14 for finite CCS, ABC and CCSS terms (e.g., action set {a,b,c}, process depth ≤5), and exhaustively verify Proposition 6: for every pair t,v of derivations with source(t)=source(v) and t ⌣• v, compute Σ={ς@v | ς∈nς(t)} and check that Σ is target(v)-consistent by finding a derivation t′ with source target(v), nς(t′)=Σ, 𝓁(t′)=𝓁(t) and t ; t′. Also test closure (2) on one- and two-step paths. Include Examples 4–6 as known passing cases. A single violation refutes Corollary 3; exhaustive success up to the bound materially supports the central construction.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Corollary 3 (closure property (2)) is the load-bearing step: without it Definitions 5–6 do not yield a well-defined justness notion and Theorem 1 cannot be applied. The proof of Corollary 3 goes through Proposition 6, whose key step is Lemma 6. Lemma 6 takes a P-consistent synchron set Σ from a derivation t and a matching set Σ′⊆ς(Q) with each ς;ς′, and asserts that deleting the 'marked' dynamic nodes (+L, +R, A:, ˆr) from t yields a derivation with source Q and necessary synchrons Σ′. The consistency of that marking is asserted in prose rather than proved, and the case of altered broadcast partners is handled by a sketch. This is the precise place where the derivation-tree representation is assumed to be a complete record of interference: if some Q produces an inconsistent marking, or if altered broadcast partners change the label or necessary-synchron structure, then property (2) fails and the synchron relation does not define an LTSC. Theorems 2–4, Proposition 13 and the agreement with [16] and [7] compare versions of the same construction and cannot detect such a failure; they presuppose (4)–(7). Footnote 5 shows this machinery has already contained a subtle type error, so the informal deletion argument is the most load-bearing unverified step. I found no concrete counterexample, but the lemma is exactly the kind of claim that an exhaustive finite check can settle.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper makes the completeness criterion of justness — intermediate between progress and fairness — available for the transition systems of CCS and its extensions with broadcast communication (ABC) and signals (CCSS). The earlier concurrency-relation-based definition of justness from [18] is turned into a concrete construction: the paper represents transitions as derivation trees, decomposes them into 'synchrons' (paths from root to leaf), and defines a concurrency relation ⌣• from synchron structure (Section 6, Definitions 10–12). The main results are: closure property (2) holds (Corollary 3), so the construction is an LTSC; B-justness is feasible (Theorem 1 with Section 10); dynamic and static component-based concurrency relations give the same justness (Theorem 2); and the concurrency-based justness coincides with the coinductive definitions of [16] and [7] (Theorems 3 and 4, Propositions 13–15). Section 13 lifts the results to abstract paths, recovering the original justness notions of [16, 7, 3].","tokens_in":37590,"tokens_out":22151,"duration_ms":204106,"significance":"If the construction is sound, this is a substantive contribution: it replaces the coinductive, operator-by-operator definitions of justness for ABC and CCSS with a uniform, syntax-directed concurrency relation, proves feasibility, and shows agreement with the earlier formalisations. The paper's strengths include the detailed theorem chain from closure property (2) to feasibility and equivalence; the honest v2 correction in footnote 5, which records and fixes a real type error in Propositions 11 and 12; the informative comparison of dynamic versus static components and of the dynamically sequential fragment (Sections 7–8); and the fact that the agreement theorems relate to independently defined prior notions rather than being circular. The principal limitation is that the adequacy of the synchron model of interference is an axiom: the equivalence results compare two versions of the same construction and presuppose closure property (2), so they cannot by themselves validate the claim that derivation-tree shape captures all interference.","major_comments":[{"comment":"The proof of Lemma 6 is a sketch at the most load-bearing step of the paper: closure property (2), which turns the construction into an LTSC and makes Theorem 1 applicable, depends on Proposition 6, whose key step is Lemma 6. The assertion that the marking of deleted dynamic nodes is consistent is stated in prose rather than derived, and the treatment of altered broadcast partners consists of a single sentence. In view of footnote 5, which reports that an earlier version of exactly this synchron machinery contained a subtle type error, I ask for a complete proof of Lemma 6: an inductive definition of the deletion operation on derivation trees, a proof that all necessary synchrons of the same derivation agree on which dynamic nodes are deleted, and a full case analysis for receptive and discarding partners in broadcast communications. Since this is decidable on finite processes, an exhaustive check of closure property (2) on a bounded signature would also settle the correctness risk; I found no concrete counterexample.","section":"§6 (Lemma 6; Proposition 6; Corollary 3)"},{"comment":"Two auxiliary steps of Proposition 6 are asserted without proof. First, Definition 14 chooses the active synchron of u that is 'closest' to ς without proving uniqueness; uniqueness does hold, because two distinct active synchrons of one derivation diverge at a first argument, so a single synchron ς can match at most one of them, but the argument should be spelled out. Second, Observation 1 ('if ς∈ς(P) and ς ⌣•d u with source(u)=P, then ς@u∈ς(target(u))') is the exact step that transfers a synchron into the target state's synchron set, and it is stated without proof; it needs a short structural induction on u, including the broadcast case in which the receiver side of u may change. Both points are load-bearing for Proposition 6 and hence for Corollary 3.","section":"§6 (Definition 14; Observation 1)"},{"comment":"The central modelling axiom of the paper is that interference between transitions is captured exactly by the relative syntax of their derivation trees: concurrency is defined by where synchrons sit under parallel operators (Definitions 10 and 12), and the static and dynamic components of Section 7 inherit this shape. The equivalence theorems (Theorems 2–4, Proposition 13) compare versions of the same construction and presuppose closure property (2), so they cannot detect a failure of this premise. If two transitions interfere semantically without sharing a static operator position in their derivation trees, the criterion will classify some non-runs as complete or some runs as incomplete. I found no concrete counterexample; nevertheless, because this is the fragile premise of the whole development, I would welcome a test against an independent semantic model, for example an exhaustive finite-state validation of closure property (2) on a bounded signature, or a comparison with the Petri net or event structure semantics cited in Section 8.","section":"§6 (Definitions 10–12) and §§12–13"}],"minor_comments":[{"comment":"In Table 4, the rule for agent identifiers (P s̄−→P′ implies A s̄−→A) is surprising at first reading because the target is A rather than P′; a sentence explaining the persistent-signal reading, consistent with the self-loop Pˆs s̄−→Pˆs, would remove potential confusion.","section":"§5.4 (Table 4)"},{"comment":"The 'Only if' direction of Theorem 4 is delegated to [16, Proof of Proposition E.4], which is a technical report rather than a published article; since Theorem 4 is one of the headline agreement results, the proof should be included or summarised in the main text so that the journal version is self-contained.","section":"§13 (Theorem 4)"},{"comment":"Figure 1's caption does not name Classes I–V or indicate which regions represent indicator transitions; the text introduces these labels only after the figure, so annotating the caption with the class names would help the reader.","section":"§6 (Figure 1)"},{"comment":"The extension to the infinitary choice operator in Section 10 is described in a few sentences, and the argument that the relevant ≡-equivalence classes are countable is compressed; adding the synchron clause for the new argument ∑j, alongside the existing clauses for +L and +R, would make the adaptation precise.","section":"§10"},{"comment":"The sentence after Example 8 ('it follows also that ⌣•c is incomparable with ⌣•') combines Example 8 with the earlier observation that some ⌣•-concurrent pairs are not ⌣•c-concurrent; stating this combination explicitly would aid readability.","section":"§7.3 (after Example 8)"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a journal consolidation of the FoSSaCS'19 extended abstract, with full proofs, the correction recorded in footnote 5, and the component-based and abstract-path analysis. The heavy citation of the author's own prior work is appropriate here, as the paper is a direct continuation of [16]–[18]. The paper fits the journal's scope well. My recommendation of major revision is driven by the proof-completeness gap in Lemma 6 rather than by any doubt about the claimed result; if the author supplies the missing proof of Lemma 6 (and, preferably, of Observation 1), I would support acceptance. I also recommend asking the author to respond to the correctness-risk concern about the derivation-tree interference model, and to include the proof of Theorem 4's 'Only if' direction rather than deferring to the technical report."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper does what it says: it defines a concurrency relation for CCS, ABC, and CCSS, shows it satisfies the closure property needed for a meaningful justness notion, proves feasibility, and proves agreement with the earlier coinductive definitions. The framework is a direct continuation of the author's own prior work, but the specific synchron-based construction, the static/dynamic component split, and the equivalence theorems (Theorems 2–4, Proposition 13) are new and substantially more general than what was in the literature.\n\nThe proofs are mostly detailed and honest. The footnote in v2 transparently correcting Propositions 11 and 12 is a good sign. The section on abstract paths is a nice addition: it shows the definition doesn't depend on distinguishing proof trees beyond what the liveness semantics needs.\n\nThe real soft spot is Lemma 6, exactly where the stress-test note points. The closure property (Corollary 3) depends on the claim that deleting marked dynamic nodes from a derivation yields another valid derivation. The consistency of the marking is asserted rather than proved, and the broadcast-partner case is a sketch. If that lemma fails, the synchron relation does not define an LTSC and Theorem 1 is not applicable. I did not find a counterexample, but the lemma is doing a lot of work and is the obvious place where the derivation-tree representation might miss some interference. The agreement theorems cannot catch this, because they compare versions of the same construction. So the central definition is plausible but rests on one unverified load-bearing step.\n\nThe circularity burden is real but not damning: the concept of justness is the author's, and the synchron machinery is tuned to reproduce the earlier coinductive definitions. That makes the equivalence theorems consistency checks rather than independent validation. Still, the formalization is internally coherent and the definitions are explicit; this is a competent within-subfield contribution.\n\nMinor issues: Lemma 6 deserves a full proof or a machine-checked or exhaustive finite verification. Some earlier lemmas are sketches but less critical. The paper is long and the notation is heavy, but the reading guide helps.\n\nWho is this for? Researchers working on liveness in process algebra, especially those using CCS or its extensions, and anyone building on the justness framework from [18]. It deserves serious peer review — the construction is original and mostly sound, and the one weak step is localized enough that a referee can check it. I'd accept it with a request to strengthen Lemma 6.","headline":"Solid, careful formalization of justness for CCS and extensions; the load-bearing Lemma 6 is the one soft spot worth checking before relying on the closure property.","tokens_in":38101,"tokens_out":605,"would_cite":false,"duration_ms":75834,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q85","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Justness becomes a precise, syntax-directed liveness criterion for CCS, ABC, and CCSS.","keywords":["justness","liveness","completeness criterion","concurrency relation","process algebra","CCS","broadcast communication","signals"],"falsifier":"Exhibit a transition pair t,u such that the synchron test says t is unaffected by u, yet performing u in the source state of t destroys every possible future variant of t through a conflict located below a static operator, such as a shared restriction \\L that the synchron test ignores. A concrete search over small CCS processes for such a pair would settle whether the synchron-based concurrency relation faithfully captures interference: if one exists, the definition of justness classifies some genuinely blocked path as complete.","tokens_in":37069,"feed_emoji":"⚖️","tokens_out":3773,"duration_ms":36399,"temperature":0.7,"pith_summary":"The paper argues that a transition system only becomes a model of a distributed system once we decide which paths count as complete runs. It advocates justness as the right completeness criterion: stronger than progress, weaker than fairness, and warranted by default rather than assumed. The paper's technical contribution is a concurrency relation between transitions, built from 'synchrons'—paths in derivation trees—defined for CCS and its extensions with broadcast communication and signals. With that relation, justness becomes a precise, syntax-directed predicate on paths, and the paper proves it is feasible, meaning every finite path extends to a just path, and that five different formulations all define the same just paths.","feed_headline":"One formal rule separates complete runs from stuck ones","feed_subtitle":"Justness for CCS, ABC, and CCSS makes liveness guarantees precise without assuming fairness.","key_machinery":"The load-bearing object is the synchron: a string of operator arguments leading from the root of a process to an atomic, unguarded subexpression, representing one leaf of a transition's derivation tree. Each transition derivation carries a set of necessary synchrons—all of them, except for broadcasts, where only the sending synchron is necessary. Two synchrons are concurrent when they sit on opposite sides of a parallel composition under the same prefix; the concurrency relation t ⌣ u holds when no active synchron of u interferes with a necessary synchron of t. This relation, extended to future variants, satisfies closure property (2), which is exactly what lets every finite path be extended to a just path.","core_discovery":"The central discovery is that an asymmetric concurrency relation—'transition u does not interfere with t'—can be defined compositionally for CCS, ABC, and CCSS by treating transitions as derivation trees and locating the atomic leaves, called synchrons, that a transition synchronises. A non-blocking transition is then just if, whenever it becomes enabled, eventually some transition occurs that interferes with one of its necessary synchrons. The paper proves this definition satisfies the closure property needed for feasibility (Corollary 3 with Theorem 1), shows that static and dynamic component versions give the same justness (Theorem 2), and proves agreement with the earlier coinductive definitions of justness for CCS, ABC, and CCSS (Theorems 3, 4, and Propositions 13–15).","pith_inferences":["The synchron/derivation-tree method will likely transfer to other process algebras whose structural operational semantics fits the same rule format; the main design choice is deciding which operators count as static.","If justness is accepted as the default completeness criterion, liveness verification could model-check against just paths instead of fair paths, yielding stronger guarantees that do not assume away real interference.","A testable extension: instrument an implementation of CCS to record derivation-tree identities at runtime, then compare the paths the definition calls just against actual blocked runs in a distributed environment, especially under broadcast and signal extensions.","The asymmetry of the concurrency relation suggests a hierarchy of justness for broadcast systems: sends can ignore receivers, but receives depend on senders, which may explain why broadcast protocols often need weaker liveness assumptions than handshake-based protocols."],"forward_implications":["For CCS, ABC, and CCSS, justness is now a fully syntax-directed completeness criterion, not an informal slogan: it can be checked on individual paths.","Every finite path can be extended to a B-just path, even in CCS with infinitary choice, so liveness properties verified under justness are not vacuous.","The five candidate definitions—synchron-based, dynamic components, static components, and the two component variants—all induce the same set of just paths, so any of them may be used in proofs or tools.","The new definition agrees with the earlier coinductive justness of [16] and [7], so existing examples and verification results for mutual exclusion and broadcast protocols carry over unchanged.","Because broadcast reception is treated as a blocking action and broadcasts as non-blocking, justness yields faithful liveness guarantees for reactive systems where progress is too weak."],"supporting_citations":[{"why":"Defines justness in terms of an asymmetric concurrency relation and introduces the feasibility requirement that the paper adopts.","marker":"[18]"},{"why":"Provides the original coinductive definitions of justness for CCS and ABC that the new definition must agree with.","marker":"[16]"},{"why":"Extends justness and signalling to CCSS, setting the target for the signal-aware version of justness.","marker":"[7]"},{"why":"Supplies the syntax and operational semantics of CCS, whose derivation trees the synchron construction reads.","marker":"[25]"},{"why":"Introduces the calculus of broadcasting systems that ABC builds on, including the discard-transition technique for avoiding negative premises.","marker":"[32]"},{"why":"Proposes feasibility as a requirement on completeness criteria, which Theorem 1 establishes for B-justness.","marker":"[1]"},{"why":"Calls the same feasibility property machine closure, reinforcing the requirement the paper satisfies.","marker":"[23]"}],"fun_headline_variants":["Justness: the missing criterion between progress and fairness","Synchrons make justness compositional for CCS, ABC, CCSS","Justness defined by non-interfering transitions for liveness","Justness: completeness for liveness without fairness","One asymmetric concurrency relation yields justness for process algebras"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that all real interference between transitions is visible in the shape of their derivation trees: two transitions are concurrent exactly when their synchrons sit on opposite sides of a parallel composition, and if two transitions can interfere without sharing such a syntactic position, justness will call some stuck runs complete and some live runs incomplete.","fun_headline_variants_meta":{"raw":{"variants":["Justness: the missing criterion between progress and fairness","Synchrons make justness compositional for CCS, ABC, CCSS","Justness defined by non-interfering transitions for liveness","Justness: completeness for liveness without fairness","One asymmetric concurrency relation yields justness for process algebras"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000817,"raw_usage":{"total_tokens":3505,"prompt_tokens":799,"completion_tokens":2706,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":415,"completion_tokens_details":{"reasoning_tokens":2624}},"tokens_in":415,"tokens_out":2706,"duration_ms":19599,"temperature":1.0,"reasoning_tokens":2624,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T05:56:19.487327+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a transition pair t,u such that the synchron test says t is unaffected by u, yet performing u in the source state of t destroys every possible future variant of t through a conflict located below a static operator, such as a shared restriction \\L that the synchron test ignores. A concrete search over small CCS processes for such a pair would settle whether the synchron-based concurrency relation faithfully captures interference: if one exists, the definition of justness classifies some genuinely blocked path as complete.","supporting_citations":[{"cited_title":"Progress, Fairness and Justness in Process Algebra","cited_arxiv_id":"1501.03268","evidence_quote":"Provides the original coinductive definitions of justness for CCS and ABC that the new definition must agree with."},{"cited_title":"Prasad (1991): A Calculus of Broadcasting Systems","cited_arxiv_id":null,"evidence_quote":"Introduces the calculus of broadcasting systems that ABC builds on, including the discard-transition technique for avoiding negative premises."},{"cited_title":"Lamport (2000): Fairness and hyperfairness","cited_arxiv_id":null,"evidence_quote":"Calls the same feasibility property machine closure, reinforcing the requirement the paper satisfies."}],"review_version":1}