{"id":"00a75dce-7db1-425f-81ab-4f190005e826","arxiv_id":"2411.14583","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Concurrent reversible processes are given sound and complete expansion laws for forward, reverse, and forward-reverse bisimilarities by annotating action prefixes with backward ready sets in proved encodings.","lead":"These scientists added the parallel operator to a reversible version of CCS and wrote complete algebraic rewrite rules for three notions of equivalence: forward-only, reverse-only, and forward-plus-reverse. Their new encoding labels each action with the set of actions that can be undone next, and the rewrite rules let any parallel composition be expanded into a purely sequential form.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The expansion law in Definition 5.3 depends on an unspecified total order ≤†; different linearizations of concurrent executed actions yield non-FRB-bisimilar encodings, so the encoding is not well-defined and Theorems 5.7-5.14 are not well-formed.","rationale":"The reader identified the unspecified total order ≤† as the weakest assumption; I agree that this is the load-bearing point. The concern is not merely that a proof is missing but that the construction appears to be genuinely ill-defined. The concrete counterexample based on a†.0 ∥/0 b†.0 shows that two different linearizations of the same concurrent history produce encodings that are not forward-reverse bisimilar. Since the syntax of P does not record any linearization of independent executed actions, the encoding eP is not a function of P. This undermines Theorem 5.7, Corollary 5.8, and the two completeness theorems (5.11 and 5.14), as their statements quantify over an encoding that is not uniquely determined. The paper gives no way to choose a canonical order nor a proof that the chosen order is irrelevant. I therefore regard this as a fatal flaw in the central claim as written, rather than a merely cosmetic gap, and I recommend REJECT rather than CONDITIONAL: the issue is not a missing proof of a true statement but a false well-definedness claim. A repair would require a fundamentally different encoding that avoids linearizing concurrent executed actions, or an enrichment of the process syntax with explicit history information—both beyond the scope of a minor revision.","tokens_in":22955,"tokens_out":17701,"duration_ms":142819,"concrete_test":"For a ≠ b, let P = a†.0 ∥/0 b†.0 and P' = b†.0 ∥/0 a†.0. Compute the two encodings prescribed by Definition 5.3 under the two possible orders: E_ab (Ua ≤† Tb) = <a†,{a}>.<b†,{a,b}>.0 + <b,{b}>.<a,{a,b}>.0 and E_ba (Tb ≤† Ua) = <b†,{b}>.<a†,{a,b}>.0 + <a,{a}>.<b,{a,b}>.0. Check whether E_ab ∼FRB:ℓbrs E_ba. If not, Definition 5.3 is not well-defined. Also check whether P ∼FRB P' (it should hold by isomorphism); if E_ab and E_ba are not FRB:ℓbrs-related, then Corollary 5.8 fails for this pair under any fixed linearization.","verdict_should_be":"REJECT","load_bearing_attack":"The central construction is Definition 5.3, whose fourth case ('both non-initial') chooses a sequencing of already executed actions based on a 'total order ≤† over Θ induced by the trace of actions executed so far'. This order is never defined, and no invariance lemma is proved. The problem is not merely a missing definition: the choice of order can change the FRB-equivalence class of the encoding. Consider P = a†.0 ∥/0 b†.0 with a ≠ b. With order Ua ≤† Tb, Definition 5.3 and Example 5.4 give EP = <a†,{a}>.<b†,{a,b}>.0 + <b,{b}>.<a,{a,b}>.0. With Tb ≤† Ua, one obtains EQ = <b†,{b}>.<a†,{a,b}>.0 + <a,{a}>.<b,{a,b}>.0. These two Pbrs processes are not forward-reverse bisimilar: EP has an outgoing transition labeled (a,{a}) (undoing a), while EQ has no outgoing transition labeled (a,{a})-its only a-labelled outgoing transition carries (a,{a,b}). Hence the encoding is not a function of P. Moreover, the processes P and P' = b†.0 ∥/0 a†.0 are FRB-equivalent (their LTSs are isomorphic), yet any fixed left-to-right order yields EP and EQ respectively, which are not FRB:ℓbrs-equivalent. Thus Corollary 5.8, and with it the completeness theorems for AR and AFR, fail as stated. The paper supplies no mechanism (e.g., enriching processes with histories or proving invariance under a canonicalization) to remove this dependence.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper extends the reversible process calculus of [13] with a CSP-style parallel composition and develops equational axiomatizations of past-sensitive forward bisimilarity (∼FB:ps), reverse bisimilarity (∼RB), and forward-reverse bisimilarity (∼FRB). The method follows the proved-trees approach of Degano and Priami: transitions are labelled with proof terms, observation functions map proof terms to the information relevant to each bisimilarity, and the observation function is lifted to a syntactic encoding eP of processes. For ∼FB:ps the encoding is the identity on action prefixes and the expansion law is interleaving (Section 4). For ∼RB and ∼FRB the paper claims that the needed extra information is the backward ready set brs of the reached process, so prefixes are annotated with such sets, and expansion laws are given in Definition 5.3. The main theorems are Theorem 4.3 (AF is sound and ground-complete for ∼FB:ps), Corollary 5.8 (P1 ∼B P2 iff eP1 ∼B:ℓbrs eP2 for B ∈ {RB, FRB}), and Theorems 5.11 and 5.14 (AR and AFR are sound and ground-complete for the encoded equivalences).","tokens_in":23374,"tokens_out":11463,"duration_ms":111995,"significance":"If correct, the paper would give a uniform, fully equational treatment of a truly concurrent reversible semantics, and it would identify backward ready sets as the discriminating information needed for expansion laws under reverse and forward-reverse bisimilarity. The congruence result for parallel composition (Theorem 2.8), the clean interleaving axiomatization for ∼FB:ps, and the systematic use of proved transitions are valuable components. However, the central construction for the truly concurrent cases is not well-defined as written: it relies on an unspecified total order, and the choice of that order changes the FRB:ℓbrs equivalence class of the encoding. Since Corollary 5.8 and the completeness theorems for AR and AFR depend on the encoding, the paper's main claims for reverse and forward-reverse bisimilarities are not established and, in the form stated, fail.","major_comments":[{"comment":"The expansion law for the both-non-initial parallel case is not well-defined. The text says the sequencing of already executed actions is chosen 'based on a total order ≤† over Θ induced by the trace of actions executed so far', but no definition of ≤† is ever given, and no invariance lemma is proved. The choice matters. For P = a†.0 ∥/0 b†.0 with a ≠ b, the calculation in Example 5.4 with Ua ≤† Tb gives eP = <a†,{a}>.<b†,{a,b}> + <b,{b}>.<a,{a,b}>.0; with the reversed order Tb ≤† Ua the same Definition 5.3 gives eQ = <b†,{b}>.<a†,{a,b}> + <a,{a}>.<b,{a,b}>.0. These two Pbrs processes are not ∼FRB:ℓbrs-equivalent: through the backward clause, eP has an incoming transition labelled (b,{b}) but no incoming transition labelled (a,{a}), whereas eQ has the dual behaviour. Since the original processes a†.0 ∥/0 b†.0 and b†.0 ∥/0 a†.0 are FRB-equivalent (their proved LTSs are isomorphic with the same action labels), any fixed deterministic reading of ≤† makes Corollary 5.8 false. This is a load-bearing defect, not a missing detail: the encoding is not a function of the process up to FRB-equivalence, and the completeness theorems for AR and AFR inherit the problem.","section":"Definition 5.3, fourth case"},{"comment":"These results are stated without proof bodies in the submitted text, but more importantly they are not well-formed as consequences of Definition 5.3. Corollary 5.8 asserts P1 ∼B P2 iff eP1 ∼B:ℓbrs eP2; the counterexample above shows that the right-hand side depends on the unspecified order, not only on the FRB-equivalence class of the source process. Theorems 5.11 and 5.14 also quantify over eP1 and eP2, so their statements are indeterminate until the encoding is fixed. The paper needs either a concrete definition of ≤† with a proof that all admissible orders yield provably equivalent encodings, or a redesigned encoding that is canonical (for example, by carrying the full history or by constructing all legal linearizations rather than selecting one). Without such a mechanism, the central claims for reverse and forward-reverse bisimilarities cannot be accepted.","section":"Corollary 5.8 and Theorems 5.11, 5.14"},{"comment":"The paper itself concedes the problematic case. Proposition 5.6(2) states that brs(eP) = brs(P) fails when P has a subprocess P1 ∥L P2 with both components non-initial and different last executed actions outside L, and the subsequent example with a†.0 ∥/0 b†.0 shows brs(eP) = {b} while brs(P) = {a,b}. The explanation that '{a,b} occurs next to the last executed action b†' does not repair the invariance failure: in the bisimulation game on Pbrs the label of an incoming transition is determined by the backward ready set of the target state, and the asymmetric choice of which executed action counts as 'last' is exactly the arbitrary order that is never defined. The mismatch between brs(P) and brs(eP) is thus not a harmless technicality but a symptom of the non-canonicity of the encoding.","section":"Proposition 5.6(2)"}],"minor_comments":[{"comment":"There is a typo in the phrase 'by induction on the syntactical structural of its first argument'; it should read 'syntactical structure'.","section":"Definition 5.1"},{"comment":"Several axiom names and symbols in Table 4 appear corrupted in the rendered text (e.g., 'Â', 'fl', 'ga', '‡'); these should be typeset uniformly so that axioms AR,1–AR,5 and AFR,1–AFR,5 are readable.","section":"Table 4"},{"comment":"The description of the general expansion law for sequential processes is only a sketch, and the notation for the lifted encoding ℓσ is dense; a short example explicitly showing how the environment process E is threaded through the encoding would substantially improve readability.","section":"Section 3"},{"comment":"The proofs of the normal-form lemmas and of Theorems 4.3, 5.11, and 5.14 are omitted from the submitted text; if the version of record has an appendix, it should be included in the submission for refereeing.","section":"Lemma 4.2 and Lemmas 5.10, 5.13"}],"recommendation":"reject","confidential_remarks":"The forward-bisimilarity part may be salvageable, and the paper identifies an interesting phenomenon (backward ready sets as needed information). But the reverse/forward-reverse part hinges on an undefined and non-invariant ordering, and the provided counterexample shows Corollary 5.8 is false for any fixed choice of that ordering. This is not a proof-completeness issue; it requires redesigning the encoding or the expansion law. I therefore recommend rejection, despite the paper's useful observations and clean presentation in Sections 2 and 4."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read this if you care about equational axiomatizations of reversible concurrent processes. The paper extends Bernardo–Rossi's sequential axiomatizations to parallel composition using Degano–Priami proved trees. The forward-bisimilarity part (Section 4) is fine and new. The more interesting claim is that reverse and forward-reverse bisimilarities can be captured by annotating every action prefix with the backward ready set of the reached process. That observation is plausible and works for sequential processes and for the cases where only one side of a parallel composition has executed actions.\n\nThe problem is the case where both sides have executed independent actions. Definition 5.3 introduces a 'total order ≤† over Θ induced by the trace of actions executed so far' and uses it to linearize already-executed actions. No definition of ≤† is given, and the encoding is not invariant. Take P = a†.0 ∥/0 b†.0. With one linearization the encoding is <a†,{a}>.<b†,{a,b}>.0 + <b,{b}>.<a,{a,b}>.0; with the other it is the mirror image. These two Pbrs processes are not forward-reverse bisimilar: their incoming transitions carry (b,{a,b}) versus (a,{a,b}). Meanwhile P and b†.0 ∥/0 a†.0 are FRB-equivalent in the original calculus. So any fixed choice of order makes Corollary 5.8 false. The stress-test note states this with an example that mislabels the difference as outgoing vs. incoming, but the underlying objection stands.\n\nTheorems 5.7–5.14 therefore do not hold as stated. The paper supplies no history in the process syntax, so there is no principled way to pick the order; the encoding is not a function of the process. This is not a small gap—it is the heart of the claimed extension to true concurrency.\n\nOn the positive side: the paper is carefully written, the sequential encoding (Example 5.2) is correct, Proposition 5.6 shows the encoding preserves initiality and backward ready sets in the cases it can, and the literature engagement is honest. The proof bodies for the main theorems are not in the text, which compounds the problem.\n\nVerdict: the forward-bisimilarity axiomatization is a real contribution; the reverse/forward-reverse parallel results need a different treatment—either a canonical history in the source syntax, a proof of invariance under a defined order, or a restriction to processes with unique causal histories. As it stands, the paper should not be accepted without major revision. Yes, send to a serious referee: the mistake is subtle and the correct part of the paper is worth preserving, but I would not cite the main theorems until the encoding is repaired.","headline":"Clever observation, broken encoding: the parallel non-initial case in Definition 5.3 makes the main theorems fail as stated.","tokens_in":23930,"tokens_out":12645,"would_cite":false,"duration_ms":107662,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q85"],"pacs":[],"model":"deepseek-v4-flash","headline":"Concurrent reversible processes can be axiomatized by expansion laws, provided reverse and forward-reverse bisimilarities annotate every action prefix with the backward ready set of the reached process.","keywords":["reversible process calculi","bisimilarity","expansion laws","proved trees","backward ready sets","true concurrency","axiomatization","parallel composition"],"falsifier":"Take the process $a^{\\dagger}.0 \\parallel_{\\emptyset} b^{\\dagger}.0$ with $a \\neq b$ and compute its $\\ell_{brs}$-encoding under two different admissible orders, for instance with $Ua \\leq^{\\dagger} Tb$ or with $Tb \\leq^{\\dagger} Ua$. If the two resulting processes are not bisimilar under $\\sim_{RB}$ or $\\sim_{FRB}$, then the encoding of Theorem 5.7 is not well-defined; if they are bisimilar but not provably equal in $A_R$ or $A_{FR}$, then the completeness theorems would need a proof of order-independence.","tokens_in":22753,"feed_emoji":"♻️","tokens_out":9158,"duration_ms":79616,"temperature":0.7,"pith_summary":"This paper extends a reversible process calculus with parallel composition and asks whether the three standard behavioural equivalences — forward, reverse, and forward-reverse bisimilarity — can be captured by equational axioms. The authors establish that all three have sound and ground-complete axiomatizations, obtained by expansion laws that eliminate parallel composition. For the two truly concurrent equivalences, reverse and forward-reverse bisimilarity, the key new ingredient is that every action prefix in the encoded process must be annotated with the backward ready set of the process reached by that action, that is, the set of actions labelling its incoming transitions. The result matters because it gives a fully equational account of behaviour in reversible concurrent systems, allowing algebraic reasoning about systems that can undo computations.","feed_headline":"Backward-ready sets turn reversible concurrency into equations","feed_subtitle":"Expansion laws give sound and complete axiomatizations for forward, reverse, and forward-reverse bisimilarities.","key_machinery":"The machinery is the proved trees approach, in which every transition is labelled by a proof term — the action preceded by the sequence of operator contexts in whose scope it occurs — and an observation function maps proof terms to whatever the semantics under study should see. The paper instantiates this with three observation functions: $\\ell_F(\\theta) = act(\\theta)$ for forward bisimilarity, and $\\ell_R(\\theta)_{P'} = \\ell_{FR}(\\theta)_{P'} = \\langle act(\\theta), brs(P')\\rangle$ for the reverse and forward-reverse cases, where $brs(P')$ is the backward ready set of the reached process. The lifting of $\\ell_{brs}$ to a process encoding $\\widehat{P}$ annotates every action prefix with the backward ready set of the process reached so far, maintained by an environment-process update function. For parallel compositions where both sides have already executed non-synchronizing actions, the encoding orders the executed actions by a total order $\\leq^{\\dagger}$ over proof terms, because executed actions cannot both appear on either side of an alternative composition in a well-formed process.","core_discovery":"The central claim is that proving the three bisimilarities equal over concurrent reversible processes reduces to choosing the right process encoding. For forward bisimilarity the observation function is the identity on actions, so the classical interleaving expansion law suffices, yielding the axiom system $A_F$ and Theorem 4.3: $P_1 \\sim_{FB:ps} P_2$ iff $A_F \\vdash P_1 = P_2$. For reverse and forward-reverse bisimilarities, the paper shows that the original transition labels carry no discriminating information about concurrency, and that the additional information needed is the backward ready set of the reached process: the observation is $\\ell_{brs}(\\theta)_{P'} = \\langle act(\\theta), brs(P')\\rangle$. The encoding $\\widehat{P}$ lifts this observation into action prefixes, and the main theorems state that $\\widehat{P_1} \\sim_{RB:\\ell_{brs}} \\widehat{P_2}$ iff $A_R \\vdash \\widehat{P_1} = \\widehat{P_2}$ and $\\widehat{P_1} \\sim_{FRB:\\ell_{brs}} \\widehat{P_2}$ iff $A_{FR} \\vdash \\widehat{P_1} = \\widehat{P_2}$. If correct, this gives sound and ground-complete equational characterizations of both truly concurrent reversible equivalences over the full calculus with parallel composition.","pith_inferences":["A natural extension of the paper's closing suggestion is that switching from backward ready sets to backward ready multisets may characterize hereditary history-preserving bisimilarity; counting occurrences of executed actions rather than just their presence would separate $a \\parallel a$ from $a$ alone, a distinction the set version collapses.","The total order $\\leq^{\\dagger}$ in the non-initial parallel case is the only non-constructive point in the construction; proving order-independence would make the axiomatization fully syntactic.","The same observation-function method should transfer to weak ($\\tau$-abstracting) versions of the three bisimilarities, with backward ready sets weakened by $\\tau$-closure, giving expansion laws for weak reversible concurrency."],"forward_implications":["$\\sim_{FB:ps}$ over concurrent reversible processes is soundly and ground-completely axiomatized by the system $A_F$, whose single expansion law is the interleaving one.","$\\sim_{RB}$ and $\\sim_{FRB}$ are soundly and ground-completely axiomatized by $A_R$ and $A_{FR}$, whose expansion laws are expressed through the $\\ell_{brs}$-encoding with backward ready sets in every action prefix.","$P_1 \\sim_B P_2$ holds exactly when $\\widehat{P_1} \\sim_{B:\\ell_{brs}} \\widehat{P_2}$ for $B \\in \\{RB, FRB\\}$, so the backward ready set is precisely the information needed to tell concurrent from sequential reversible behaviour.","All four bisimilarities are congruences with respect to parallel composition, so the axiomatizations compose with the rest of the calculus.","A fully equational account of truly concurrent reversible behaviour exists: algebraic derivations can replace bisimulation games for these equivalences."],"supporting_citations":[{"why":"Supplies the proved trees method that generates proof-term-labelled transitions and observation functions, the basis of all three encodings.","marker":"[27]"},{"why":"Provides the sequential reversible process calculus, the definitions of the four bisimilarities, and the axioms that this paper extends to parallel composition.","marker":"[13]"},{"why":"Introduces forward-reverse bisimilarity and the static style of reversibility used for the syntax with $\\dagger$-decorated actions.","marker":"[45]"},{"why":"Originates the expansion-law technique for eliminating parallel composition in interleaving semantics, which $A_F$ adapts.","marker":"[32]"},{"why":"Supplies the back-and-forth single-transition view of reversibility on which the symmetric transition relation and incoming-transition matching rely.","marker":"[26]"}],"fun_headline_variants":["Backward-ready sets yield complete axioms for reversible bisimulations","Proved encodings with backward-ready sets axiomatize reversible concurrency","Uniform expansion laws for forward, reverse, and forward-reverse bisimilarity","Backward-ready sets make reversible concurrency equational","Sound and complete equations for reversible concurrency via backward-ready sets"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the expansion laws for parallel composition of two non-initial processes use a total order $\\leq^{\\dagger}$ over proof terms, induced by the trace of actions executed so far; the paper does not give a concrete definition of this order and does not prove the encoding independent of the chosen linearization.","fun_headline_variants_meta":{"raw":{"variants":["Backward-ready sets yield complete axioms for reversible bisimulations","Proved encodings with backward-ready sets axiomatize reversible concurrency","Uniform expansion laws for forward, reverse, and forward-reverse bisimilarity","Backward-ready sets make reversible concurrency equational","Sound and complete equations for reversible concurrency via backward-ready sets"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001141,"raw_usage":{"total_tokens":4766,"prompt_tokens":1006,"completion_tokens":3760,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":622,"completion_tokens_details":{"reasoning_tokens":3670}},"tokens_in":622,"tokens_out":3760,"duration_ms":27380,"temperature":1.0,"reasoning_tokens":3670,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:08:46.585109+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the process $a^{\\dagger}.0 \\parallel_{\\emptyset} b^{\\dagger}.0$ with $a \\neq b$ and compute its $\\ell_{brs}$-encoding under two different admissible orders, for instance with $Ua \\leq^{\\dagger} Tb$ or with $Tb \\leq^{\\dagger} Ua$. If the two resulting processes are not bisimilar under $\\sim_{RB}$ or $\\sim_{FRB}$, then the encoding of Theorem 5.7 is not well-defined; if they are bisimilar but not provably equal in $A_R$ or $A_{FR}$, then the completeness theorems would need a proof of order-independence.","supporting_citations":[{"cited_title":"De Nicola, U","cited_arxiv_id":null,"evidence_quote":"Supplies the back-and-forth single-transition view of reversibility on which the symmetric transition relation and incoming-transition matching rely."}],"review_version":1}