{"id":"cea09a11-c07a-4be6-87c2-cb9fb9a8f522","arxiv_id":"1912.05616","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A research agenda for a theory of concurrency that proves liveness properties using justness instead of fairness, because fairness assumptions can yield conclusions that do not hold in reality.","lead":"This paper argues that liveness proofs for distributed systems should rely on 'justness' rather than fairness assumptions, and lays out ten open problems for building a theory of concurrency on that basis. It matters because standard process algebras can equate systems that differ in crucial liveness guarantees, which can lead to false confidence in verification.","discovery_kind":"review","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the P/Q distinction is correct under the paper's explicit justness and demonic-choice definitions.","rationale":"The paper is an invited open-problems article, and the reader's ACCEPT verdict is appropriate. The P/Q example is the load-bearing illustration of the paper's thesis. I checked: the LTSs are identical (two states, initial y-loop plus x:=1 to second state, second state y-loop), so strong bisimilarity holds. Under Def. 5 of justness, for Q the infinite y-loop is just because every y-transition shares the left component with the enabled x:=1/tau transition; for P, the x:=1/tau transition has a disjoint right component, so the infinite y-loop is unjust. The only vulnerability is the demonic-choice interpretation, which the paper explicitly adopts after considering a referee objection. This is a philosophical assumption, not an internal inconsistency, and the paper's claim is explicitly framed 'when assuming justness... but not assuming fairness.' No change to the verdict.","tokens_in":28142,"tokens_out":9732,"duration_ms":102760,"concrete_test":"Encode the CCS versions of P and Q (P=(Y|tau) with Y=a.Y; Q=(X|b-bar)\\b with X=a.X+b-bar.X) in a component-labelled transition system tool, compute strong bisimulation to confirm P~Q, then apply the Appendix B justness criterion to check that some just run of Q avoids tau while every just run of P reaches tau. If the tool instead finds a just run of P avoiding tau, the example collapses; if it finds no distinguishing just run, the classification in Figure 3 is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is conditional on the author's definitions of justness (Appendix B) and on the demonic interpretation of nondeterministic choice (Section 2.2). Under those definitions, the P/Q example is technically sound: both programs have the same two-state LTS, hence are strongly bisimilar; under justness, P's x:=1 transition belongs to a separate component that must eventually progress, whereas Q's x:=1 transition belongs to the same component as y:=y+1, so an infinite y-only run is just. The weakest point is not a formal error but the philosophical stance that nondeterministic choice is external and demonic. The paper acknowledges referee counterarguments (Figure 1(d)) and defends the stance explicitly. A reader who instead adopts a probabilistic or fairness-flavored interpretation of choice will not get the distinction, but that is exactly the point the paper argues against, not a hidden assumption.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper is a position/research-agenda article. It argues that global fairness assumptions are by default unwarranted for establishing liveness properties of distributed systems, and that justness—a progress property strictly weaker than fairness—is the appropriate default completeness criterion. The central technical demonstration is the pair of programs P and Q in Section 5: both have the same two-state labelled transition system and are strongly bisimilar, yet under justness P guarantees that x eventually becomes 1 whereas Q does not, because in Q the choice between y:=y+1 and x:=1 is made by the same component and may forever select y:=y+1. The paper then explains why standard process algebras and temporal logics fail to make this distinction, discusses the dangers of fair abstraction, and lays out a ten-task research agenda covering equivalences, axiomatisations, congruence formats, Petri nets, expressiveness, time, probability, and applications.","tokens_in":28415,"tokens_out":16955,"duration_ms":177448,"significance":"If the central claim is accepted, the paper identifies a real blind spot in interleaving-based verification: semantic equivalences no finer than strong bisimilarity collapse systems that differ in a crucial liveness property under justness. The P/Q example is small, self-contained, and checkable from the definitions in Appendices A and B, and the paper is commendably explicit about the modeling assumption on which it rests: nondeterministic choice is interpreted as external, demonic choice (Section 2.2). The hierarchy in Section 4, supported by Proposition 1 in Appendix C, is a useful contribution. The main limitation is that the normative conclusion—that fairness is unwarranted by default—is a modeling position rather than a theorem; readers who adopt a probabilistic or fairness-flavored interpretation of internal choice will not obtain the P/Q separation. The paper openly acknowledges this in the Figure 1 discussion, so the assumption is stated rather than hidden. As a research agenda, the paper gives the justness program a compact and testable form.","major_comments":[],"minor_comments":[{"comment":"The row for 'progress' reports the liveness goal y=7 for Q as '−', but the text immediately above the table says that the progress assumption is sufficient to ensure that in P or Q the variable y will at some point reach the value 7; this row should presumably read '+ + − −' rather than '+ − − −'.","section":"Section 5, Figure 3"},{"comment":"The CCS rendering of the example needs the defining equations of the process constants: as written, it is not clear what process b (or ¯b) denotes, and after the τ-step P=(Y|τ) leaves a residual Y|0 with an a-loop whereas the residual of Q depends on the unspecified definition of b; please provide the defining equations or state the intended convention so that the claim that both systems are represented by the same labelled transition system can be checked.","section":"Section 5, 'Variations on this example'"},{"comment":"The claim that P and Q are both solutions of the guarded recursion U = (y:=y+1).U + (x:=1).V, V = (y:=y+1).V up to justness-preserving strong bisimilarity needs clarification: under the component-labelled semantics of Appendix A, the top-level choice in the right-hand side is executed by the empty component sequence, so the infinite y-run is just in the right-hand side but unjust in P; please specify whether the equations are intended over component-enriched behaviours, or restrict the RSP-soundness remark to a coarser equivalence.","section":"Task 2 (RSP discussion)"}],"recommendation":"minor_revision","confidential_remarks":"The paper is a good fit for a special issue on open problems in concurrency theory. The central P/Q argument is sound under the explicitly stated demonic-choice and justness assumptions, and the remaining issues are local: a table typo, a missing CCS defining equation, and a clarification of the recursive-specification sketch in Task 2. The paper relies heavily on the author's own prior work on justness, but this reliance is transparent and appropriate for a research agenda."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know: this is not a new-result paper. The load-bearing concepts—justness, the completeness hierarchy, the P/Q pair—come from van Glabbeek's earlier work with Hofner and others. What is new is the packaging: a ten-task research agenda plus a set of open problems. If you work on process algebra or liveness, this is a useful map of a serious program; if you don't, the main thing to know is that the claim \"strongly bisimilar yet different liveness under justness\" is real and works under the paper's explicit definitions.\n\nWhat it does well: the P/Q example is the centerpiece and it holds up. Both programs have the same two-state LTS, so they are strongly bisimilar. Under the component-labelled transition system and the justness definition in the appendices, P's x:=1 belongs to a separate component that must eventually progress, while Q's x:=1 belongs to the same component as y:=y+1, so an infinite y-only run is just. The paper also records referee counterarguments honestly, including the alternative model in Figure 1(d), and defends its position rather than hiding it. Proposition 1 restates a known ordering, but cleanly. The appendices give enough formal detail that the definitions are checkable.\n\nSoft spots: the central normative claim—that fairness assumptions are unwarranted by default and justness is the right completeness criterion—is a philosophical position, not a theorem. The whole distinction depends on interpreting nondeterministic choice as demonic and external (Section 2.2). If you adopt a probabilistic or fairness-flavored interpretation of choice, P and Q no longer differ. The author explicitly says this is the point under debate, so it is not a hidden flaw, but it means the paper argues a stance rather than proves it. The paper also leans heavily on the author's own prior work; that is natural for an agenda paper, but a reader new to the area will need to go to [GH18] and [Gla19a] for the full substance. The self-citation is transparent and the references are otherwise solid.\n\nWho this is for: anyone in concurrency theory or formal verification interested in liveness with progress-like assumptions but without fairness. I would bring it to reading group, and I would cite it if I were writing about justness or liveness in process algebra. It deserves to be sent to referees: it is an invited open-problems article that clearly frames a research program with concrete, checkable examples, and the weaknesses are acknowledged modeling choices rather than errors.","headline":"A well-built agenda paper: no new theorem, but a clear and honest synthesis of the justness program, with a checkable P/Q example worth engaging.","tokens_in":28792,"tokens_out":1607,"would_cite":true,"duration_ms":16227,"reading_group":"yes","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":"Under justness but not fairness, two strongly bisimilar programs differ in whether x necessarily reaches 1.","keywords":["liveness","justness","fairness assumptions","process algebra","temporal logic","strong bisimilarity","distributed systems","verification"],"falsifier":"Analyse the shared two-state transition system of $P$ and $Q$ with a justness-aware tool: the property 'eventually $x=1$' must hold for $P$ and fail for $Q$, because the infinite run that always chooses $y:=y+1$ in $Q$ is just. Any verification formalism that proves the property for both, or that declares $P$ and $Q$ equivalent while claiming to preserve liveness, contradicts the paper's central claim; exhibiting a standard equivalence that already separates them would falsify the claim that contemporary process algebras cannot.","tokens_in":27936,"feed_emoji":"⚖️","tokens_out":10197,"duration_ms":94420,"temperature":0.7,"pith_summary":"This paper argues that the standard formal toolbox for distributed systems—process algebras, temporal logics, and the equivalences built on them—cannot certify certain liveness properties without assuming fairness, and that fairness assumptions are often unwarranted. It exhibits two simple programs, $P$ and $Q$, that are strongly bisimilar, i.e. indistinguishable by the standard behavioural equivalence used across process algebra, yet under justness $P$ guarantees that $x$ will eventually be set to $1$ while $Q$ does not. The reason is structural: in $P$ the action $x:=1$ belongs to an independent parallel component, so justness forces that component to act, whereas in $Q$ both actions are branches of one repeated nondeterministic choice that an environment may resolve the same way forever. The paper therefore sets out a research agenda for a concurrency theory that takes justness, not fairness, as its completeness criterion, requiring new equivalences, proof principles, axiomatisations, congruence formats, and models.","feed_headline":"Two equivalent programs differ on a key liveness guarantee","feed_subtitle":"Under justness, one of two equivalent programs guarantees x = 1; the other can keep incrementing y forever.","key_machinery":"The load-bearing object is justness, a completeness criterion formalised on component-labelled transition systems. A transition is labelled with the set of parallel components that participate in it, and a run is just if every non-blocking transition enabled at some point is eventually taken or interfered with by a transition sharing at least one component. Justness is stronger than progress—a system with an enabled non-blocking transition will not idle forever—but weaker than fairness, which additionally demands that perpetually or relentlessly enabled tasks eventually occur. The component labels are what separate $P$ and $Q$: in $P$, the $x:=1$ transition belongs to a component of its own, while in $Q$ it is a guarded alternative inside the component that also performs $y:=y+1$. The paper's interpretation of nondeterministic choice as demonic and external supplies the last step: an environment may forever resolve the repeated choice in $Q$ towards $y:=y+1$, making the run just.","core_discovery":"The paper's central claim is that contemporary process algebras and temporal logics fail to distinguish systems whose liveness behaviour differs, once justness is assumed and fairness is not. The counterexample is the pair $P = x:=1 \\parallel \\text{repeat } y:=y+1$ and $Q = \\text{repeat }(\\text{if True then } y:=y+1 \\text{ else if } x=0 \\text{ then } x:=1)$, both starting with $x=y=0$. $P$ and $Q$ are strongly bisimilar—both reduce to a state with two looping transitions, $y:=y+1$ and $x:=1$—so virtually every process-algebraic equivalence identifies them. Under justness, however, every run of $P$ must eventually perform $x:=1$, because that action is enabled in an independent component and justness demands that an enabled non-blocking transition of a component is eventually taken or interfered with. In $Q$, the same action is only one branch of a choice inside a single component, and the run that always picks $y:=y+1$ is just; hence $x=1$ is not guaranteed. Any formalism that equates strongly bisimilar systems must therefore either credit $Q$ with a liveness property it lacks under justness or remain unable to establish that property for $P$.","pith_inferences":["A quick test for any proposed equivalence is whether it distinguishes $P$ and $Q$; any equivalence that identifies them cannot support justness-based liveness verification unless component information is added.","If the repeated choice in $Q$ carried a fixed positive lower probability, the run that always chooses $y:=y+1$ would have probability zero, suggesting that a probabilistic-justness hybrid could interpolate between the paper's demonic nondeterminism and full fairness.","The component-versus-choice distinction should transfer to real schedulers: an implementation that serialises two logically independent operations inside one scheduling decision silently loses the guarantee that the second operation will ever happen.","Temporal logics could be extended with a component-based modality expressing that every component eventually progresses, which might capture justness without abandoning standard model checking."],"forward_implications":["Verification by strong bisimilarity or coarser equivalences can silently erase liveness distinctions: a system shown equivalent to a specification may inherit a guarantee it does not actually possess under justness.","Proof rules built on fair abstraction, such as the Koomen Fair Abstraction Rule, need to be re-examined because they can validate liveness conclusions that fail in reality when fairness is unwarranted.","New semantic equivalences, finer than or incomparable with strong bisimilarity, are needed; candidates named in the paper include justness-preserving bisimilarity and structure-preserving bisimilarity.","Basic verification infrastructure must be rebuilt: complete axiomatisations, induction principles such as the recursive specification principle, and congruence formats all need versions that respect justness.","Even simple systems such as fair schedulers and mutual exclusion protocols cannot be specified faithfully in standard CCS or Petri nets without fairness, motivating extensions such as broadcast, priorities, and signals."],"supporting_citations":[{"why":"Supplies the formal definitions of progress, justness, and the fairness hierarchy that the paper adopts.","marker":"[GH18]"},{"why":"Establishes justness as a completeness criterion and provides the Alice-Cataline example motivating it.","marker":"[Gla19a]"},{"why":"Gives the original justness definition for CCS and the progress/justness/fairness distinction in process algebra.","marker":"[GH15b]"},{"why":"Documents the wireless-network packet-delivery case where justness without full fairness is needed.","marker":"[FGH+13]"},{"why":"Shows mutual exclusion cannot be implemented in standard languages without read arcs, supporting the expressiveness claim.","marker":"[Vog02]"},{"why":"Argues mutex needs fairness, supporting the claim that fair schedulers cannot be specified without extensions.","marker":"[KW97]"},{"why":"Introduces CCS and strong bisimulation, the equivalence relation the counterexample targets.","marker":"[Mil89]"},{"why":"Establishes the consistency of Koomen's Fair Abstraction Rule, the fairness-based proof principle the paper questions.","marker":"[BBK87]"}],"fun_headline_variants":["Bisimilar programs diverge on liveness under justness","Justness exposes liveness gap in bisimilar programs","Bisimilar but not live-same: justness matters","Equivalence hides liveness: justness reveals gap","Strong bisimilarity can't ensure liveness under justness"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The distinction between $P$ and $Q$ collapses unless nondeterministic choice is treated as demonic external choice—an environment may resolve the same branch forever—and unless justness is accepted as the right completeness criterion; both are assumptions about how systems behave, not theorems.","fun_headline_variants_meta":{"raw":{"variants":["Bisimilar programs diverge on liveness under justness","Justness exposes liveness gap in bisimilar programs","Bisimilar but not live-same: justness matters","Equivalence hides liveness: justness reveals gap","Strong bisimilarity can't ensure liveness under justness"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00063,"raw_usage":{"total_tokens":2957,"prompt_tokens":1039,"completion_tokens":1918,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":655,"completion_tokens_details":{"reasoning_tokens":1836}},"tokens_in":655,"tokens_out":1918,"duration_ms":13603,"temperature":1.0,"reasoning_tokens":1836,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T15:16:27.699712+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Analyse the shared two-state transition system of $P$ and $Q$ with a justness-aware tool: the property 'eventually $x=1$' must hold for $P$ and fail for $Q$, because the infinite run that always chooses $y:=y+1$ in $Q$ is just. Any verification formalism that proves the property for both, or that declares $P$ and $Q$ equivalent while claiming to preserve liveness, contradicts the paper's central claim; exhibiting a standard equivalence that already separates them would falsify the claim that contemporary process algebras cannot.","supporting_citations":[],"review_version":1}