{"id":"6d51adbd-f2af-4ffe-9f8d-ee67fa004b6f","arxiv_id":"1908.08633","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":1.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A survey of encodability criteria for process calculi, showing that the criteria are numerous and incomparable, and outlining frameworks and a relation-based formal analysis to compare them.","lead":"This paper surveys the many criteria used to judge when one process calculus can be encoded in another, and argues that the lack of a standard choice makes results hard to compare. It also presents a formal method, based on relations between source and target terms, for analyzing and comparing those criteria.","discovery_kind":"review","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Section 5's relation-based 'iff' characterizations carry unstated side conditions on ≍T and omit the definition of correspondence simulation, so the mapping does not cover Definition 3.1 as written.","rationale":"The reader's weakest assumption targets the imported Lemmas 5.1-5.3 as possibly wrong. My reading agrees that Section 5 is the load-bearing part, but the more precise concern is not that the lemmas are false; the external Isabelle/HOL formalization [51] is genuine independent support. The issue is that the survey presents the reduction as an 'exact' capture of the criteria as defined in Section 3, while Lemma 5.2 applies only when ≍T is itself a bisimulation and Lemma 5.3 relies on an undefined 'correspondence simulation'. The finite-LTS counterexample shows the qualification is not cosmetic: for a perfectly ordinary non-bisimulation preorder, operational correspondence holds but the relation-based bisimulation characterization fails. This does not refute the paper's overall survey content or its central observation that criteria are numerous and incomparable, nor does it require rejecting the formalized results. It does mean the proposed analysis technique is narrower than the surrounding text suggests, and the paper is not self-contained enough for the reader to verify the scope of Lemma 5.3 without going to [50,51]. Since the reader already set CONDITIONAL for the related self-containedness gap, my analysis does not change that verdict, but it sharpens the reason: the conditional should be discharged by stating the missing definitions and side conditions explicitly, not by re-proving the lemmas. I therefore leave the verdict unchanged, with partial agreement because my concrete concern differs from 'the lemmas might be wrong' and instead concerns their stated hypotheses and missing definitions.","tokens_in":21985,"tokens_out":15281,"duration_ms":149835,"concrete_test":"Retrieve the Isabelle/HOL formalization [51] and inspect the statements of Lemmas 5.2 and 5.3. Then run a finite-LTS check: PS={S,S'} with S⇒S'; PT={C1,C1',C2} with C1⇒C1' and C2 having no steps; enc(S)=C1, enc(S')=C1'; ≍T = reflexive closure ∪ {(C1,C2)}. Verify (a) that the encoding is operationally corresponding per Definition 3.1, and (b) whether any relation R satisfying the right-hand side of Lemma 5.2 exists. If (a) holds and (b) fails, the side condition that ≍T be a bisimulation is essential, and the survey's claim that operational correspondence 'exactly' describes bisimilarity is valid only for bisimulation-valued ≍T.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central methodological claim of Section 5 is that encodability criteria can be mapped exactly to conditions on a relation R between source and target terms, making criteria formally comparable. The lemmas that carry this claim for operational correspondence, however, do not apply to all instances of Definition 3.1. Lemma 5.2 states an equivalence only for encodings that are operationally corresponding with respect to a preorder ≍T that is itself a bisimulation; Definition 3.1 imposes no such requirement. If ≍T is a preorder but not a bisimulation, the claimed bisimulation characterization can fail: let PS={S,S'} with S⇒S', PT={C1,C1',C2} with C1⇒C1' and C2 having no steps, enc(S)=C1, enc(S')=C1', and ≍T the reflexive closure of {(C1,C2)}. This encoding satisfies Definition 3.1, yet any R with R↾PT=≍T contains (C1,C2), so R cannot be a bisimulation because C2 cannot match C1's step. Thus operational correspondence yields reduction bisimilarity only under a side condition not stated in the criterion itself. Lemma 5.3 is even more problematic: its right-hand side uses 'correspondence simulation', a notion the paper explicitly declines to define ('We omit the definition of correspondence simulation'), so the lemma is uncheckable from the paper alone and the conclusion that weak operational correspondence ensures coupled similarity rests on an undefined concept. The survey therefore does not fully support the claim that the relation-based mapping 'completely capture[s] the effect' of these criteria as introduced in Section 3.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper is a short survey of encodability criteria used to compare process calculi. After setting up reduction semantics, encodings, and renaming policies, it surveys criteria under four headings: direct comparison via a behavioural relation, full abstraction, operational correspondence, and success/termination/barb preservation; it then covers structural criteria such as compositionality, name invariance, and homomorphic translation, and discusses a domain-specific criterion for preservation of distribution. Three general frameworks for unified notions of encoding quality are outlined: Gorla's five-criterion framework, Fu's theory of interaction, and van Glabbeek's theory of encodings. Section 5 presents the approach from [50] of mapping encodability criteria to conditions on the relation induced by the encoding, restating lemmas for full abstraction and (weak) operational correspondence. The paper concludes that criteria and variants are incomparable, that frameworks differ, and that formal analysis of criteria is still incomplete.","tokens_in":22251,"tokens_out":9068,"duration_ms":87726,"significance":"This is a useful expository paper for the EXPRESS/SOS audience. Its main contribution is a structured taxonomy of criteria, with explicit definitions, and a comparative discussion of existing general frameworks. The paper honestly attributes the formal results of Section 5 to [50] and points to the Isabelle/HOL formalization [51], which is machine-checked; this is a genuine strength. If the relation-based characterizations are correct under suitable side conditions, they provide a promising model-independent way to compare criteria and to identify the semantic content of full abstraction and operational correspondence. However, the formal claims in Section 5 are not fully supported as written: the lemmas are stated for restricted classes of target preorders that are absent from the criteria of Section 3, and one key notion is left undefined. These gaps are load-bearing for the paper's methodological claim and need to be repaired.","major_comments":[{"comment":"The claim that the first two variants of Definition 3.1 \"exactly describe\" strong and weak bisimilarity up to ≍T is too strong. Definition 3.1 does not require ≍T to be a preorder, let alone a bisimulation; Lemma 5.2 only applies to encodings that are operationally corresponding w.r.t. a preorder ≍T that is itself a bisimulation. This is a substantive side condition, not a notational convenience. A concrete instance showing the gap: let PS={S,S'} with S⇒S', PT={C1,C1',C2} with C1⇒C1' and C2 inert, and set enc(S)=C1, enc(S')=C1', and ≍T to the reflexive closure of {(C1,C2)}. This encoding satisfies the sound and complete clauses of operational correspondence from Definition 3.1, yet no relation R with R↾PT=≍T can be a bisimulation, since C2 cannot match the step C1⇒C1'. Thus Lemma 5.2 does not capture Definition 3.1 as written. The text should either strengthen Definition 3.1 explicitly or qualify the \"exactly\" claim and state the restricted scope of Lemma 5.2.","section":"Section 5, Lemma 5.2 and preceding paragraph"},{"comment":"The lemma's right-hand side refers to \"correspondence simulation\", but the paper explicitly says \"We omit the definition of correspondence simulation\". As a result, the claimed characterization of weak operational correspondence is uncheckable from the paper alone, and the conclusion that weak operational correspondence ensures coupled similarity rests on an undefined concept. The definition, or a precise statement of the lemma from [50], should be included together with the conditions under which it applies before this part of the central claim can be assessed.","section":"Section 5, Lemma 5.3"}],"minor_comments":[{"comment":"Definition 3.2 defines full abstraction with respect to two behavioural equivalences, while Lemma 5.1 states the characterization for preorders; the text should clarify whether preorders are intended as a generalization or as a different criterion, since the two formulations do not literally coincide.","section":"Section 3.2 and Section 5, Lemma 5.1"},{"comment":"The prose preceding Definition 3.1 calls ≍T \"some equivalence on the target language\", but the formal definition only states ≍T ⊆ P_T^2 and imposes no reflexivity, transitivity, or symmetry requirement; the prose and the formal definition should be aligned.","section":"Section 3.3, Definition 3.1"},{"comment":"The discussion immediately after Definition 3.5 claims that when a component Si can reduce on its own, its translation Ti can emulate the reduction modulo ≍T; this derivative-emulation property is not part of Definition 3.5 as stated and appears to come from a combination with operational completeness rather than from the definition alone.","section":"Section 3.6, Definition 3.5"},{"comment":"The paper says the relation-based mapping \"completely capture[s]\" the semantic effect of criteria, but the lemmas are imported from [50] without proof sketches; a brief note that full proofs and the Isabelle/HOL formalization appear in [50,51] would help the reader calibrate the strength of the claims.","section":"Section 5, introductory paragraph"},{"comment":"The running header reads \"EXPRES S/SOS\" and should read \"EXPRESS/SOS\".","section":"Page 1, running header"}],"recommendation":"major_revision","confidential_remarks":"For the editor: the paper is a competent survey and the Section 5 material is already published and machine-checked in [50,51]. My main concern is technical presentation: the formal claims in Section 5 are stated more broadly than the definitions in Section 3 justify, and one central notion is left undefined. These are fixable in revision and do not undermine the survey's overall value, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Good survey, with a real caveat in Section 5. It gives a clear map of encodability criteria, the three unified frameworks, and the relation-based analysis from Peters and van Glabbeek. That mapping is the most interesting part: it reduces questions about criteria to questions about relations, and the fact that it is backed by an Isabelle/HOL formalization is a strength. I would point anyone new to the area here.\n\nThe soft spots are real but not fatal. The stress-test concern is fair. Definition 3.1 allows arbitrary target equivalences, but Lemma 5.2 only works when ≍T is a preorder and a bisimulation. The counterexample in the note (C1 related to C2 by ≍T while C2 has no step) indeed satisfies weak operational correspondence, yet no relation extending ≍T can be a bisimulation. So the sentence 'operational correspondence ensures that source terms and their translations are reduction bisimilar' is too broad: it holds only under side conditions on ≍T. Similarly, Lemma 5.3 relies on 'correspondence simulation,' which the paper declines to define, so a reader cannot check the claim without digging into [50]. That is acceptable in a workshop survey if it is clearly a pointer, but the surrounding text should say so more loudly.\n\nEverything else holds up. The survey is honest about its own limits, does not overclaim the novelty of the frameworks, and covers the relevant literature. The claim that criteria are numerous and often incomparable is justified by the citations.\n\nThis paper does not change practice, but it is a good resource for anyone who needs to choose criteria or understand why results do not compose. I would accept it for peer review, with the expectation that the author tighten Section 5: either state the side conditions in the main claims, or add the missing definition, or mark the lemmas more clearly as 'for a restricted class of target equivalences.'","headline":"A useful survey of encodability criteria whose Section 5 overclaims the reach of its relation-based 'iff' characterizations; worth a referee pass to tighten the side conditions.","tokens_in":22808,"tokens_out":4024,"would_cite":true,"duration_ms":38963,"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":"One relation can make encoding results comparable","keywords":["process calculi","encodings","encodability criteria","full abstraction","operational correspondence","expressiveness","separation results","bisimulation"],"falsifier":"A single counterexample within the machine-checked formalisation [51] — a pair of calculi and an encoding that is fully abstract with respect to preorders $R_S$ and $R_T$ but for which no transitive relation $R$ with $(S,\\llbracket S\\rrbracket)$ and $(\\llbracket S\\rrbracket,S)$ in $R$ and $R_S = R\\upharpoonright P_S$, $R_T = R\\upharpoonright P_T$ exists — would refute Lemma 5.1 and with it the claim that full abstraction imposes almost no semantic constraint. More broadly, producing any commonly used encodability criterion that cannot be expressed as a condition on the encoding-induced relation would falsify the paper's central methodological thesis.","tokens_in":21738,"feed_emoji":"🔗","tokens_out":8349,"duration_ms":73567,"temperature":0.7,"pith_summary":"This paper is a survey of the many criteria used to judge whether an encoding from one process calculus into another is meaningful, and of the frameworks that try to unify them. It claims that the field is fragmented: because criteria and their variants are tailored to different settings, encodability and separation results are often incomparable, and it is not always clear that a criterion actually fits the setting in which it is used. The way out, the survey argues, is to translate every semantic criterion into a condition on the relation that an encoding induces between source terms and their translations, turning the problem of comparing criteria into the well-studied problem of comparing relations on processes. On this basis the paper reports that full abstraction alone, without fixed source and target equivalences, has very little semantic effect, while operational correspondence is exactly a bisimulation condition. A fair reader would care because a relation-based reading promises to make expressiveness hierarchies and separation proofs comparable across different calculi.","feed_headline":"One relation can make encoding results comparable","feed_subtitle":"A survey maps encodability criteria to conditions on the source-target relation induced by an encoding.","key_machinery":"The central device is the encoding-induced relation $R_{\\llbracket\\cdot\\rrbracket} \\subseteq (P_S \\uplus P_T)^2$: the smallest relation containing $(S,\\llbracket S\\rrbracket)$ for every source term $S$. Each encodability criterion is reformulated as a property of such a relation (totality, transitivity, bisimulation-like simulation conditions, divergence reflection, success respect), so comparing criteria reduces to comparing relations on processes — a domain with a mature theory. The three iff-lemmas of [50] (full abstraction, operational correspondence, and a new correspondence simulation) do the bridge-work; correspondence simulation is the named new relation, intermediate between coupled similarity and bisimilarity, that captures weak operational correspondence.","core_discovery":"The paper's central claim is that the proliferation of encodability criteria — different criteria, different variants, fine-tuned to different settings — has made encodability and separation results in process calculi largely incomparable, and that the path to comparability is to map each criterion onto a condition on the relation between source and target terms induced by an encoding. For any encoding $\\llbracket\\cdot\\rrbracket$ it defines the relation $R_{\\llbracket\\cdot\\rrbracket} \\subseteq (P_S \\uplus P_T)^2$ that relates each source term to its literal translation; a criterion then becomes a property of such relations. Following the method of [50], full abstraction with respect to preorders $R_S$ and $R_T$ becomes exactly the existence of a transitive relation containing $(S,\\llbracket S\\rrbracket)$ and $(\\llbracket S\\rrbracket,S)$ whose restrictions are $R_S$ and $R_T$ — so, without fixing the equivalences, full abstraction says almost nothing. Operational correspondence becomes bisimilarity up to the target equivalence, and weak operational correspondence becomes a new notion, correspondence simulation, situated strictly between coupled similarity and bisimilarity. Thus the survey locates the semantic core of each commonly used criterion and makes criteria comparable as relations on processes.","pith_inferences":["Editorial inference: the relation-based mapping suggests a natural taxonomy project — classify every encodability criterion ever proposed by the class of relations it induces (reflexive, transitive, bisimulation-like, divergence-respecting), yielding a lattice of criteria and a principled way to choose them for a given expressiveness question.","Editorial inference: if the full-abstraction lemma is right, many published full-abstraction proofs carry less weight than their titles suggest; re-examining classical full-abstraction results (for instance encodings into the asynchronous $\\pi$-calculus) through the relation-based lens could show which ones actually fix the equivalences enough to be informative.","Editorial inference: the method covers semantic criteria; extending it to structural criteria like compositionality and name invariance would require formalising contexts, and the paper explicitly leaves this open — a concrete next step would be to represent compositionality as a condition on the contextual closure of the induced relation.","Editorial inference: crediting the machine-checked formalisation [51] with the lemmas' correctness, the remaining risk is the gap between the abstract calculus model and real process calculi; testing the lemmas on calculi with unusual operators (such as the join-calculus) could reveal hidden assumptions."],"forward_implications":["Encodability and separation results proven under different criterion sets are incomparable, so building an expressiveness hierarchy requires fixing a single criterion set first.","Full abstraction without a fixed, canonical pair of equivalences imposes almost no semantic constraint; fully abstract encodings exist as soon as a transitive relation can combine the chosen source and target preorders.","Operational correspondence is exactly bisimilarity up to $\\asymp_T$; its weak variant is exactly coupled similarity, so these criteria are simulation conditions in disguise.","In the five-criteria framework surveyed, a 'good' encoding is exactly one that relates source and target terms by a coupled simulation that reflects divergence and respects success.","Adding domain-specific criteria can strengthen encodability results but weakens separation results and makes comparison with existing results harder; they should be added only when necessary."],"supporting_citations":[{"why":"Supplies the relation-based method for analysing encodability criteria and the three iff-lemmas that the survey's Section 5 conclusions rest on.","marker":"[50]"},{"why":"Provides the five-criteria framework used as the principal example of a general notion of encoding quality.","marker":"[22]"},{"why":"Introduces the labelled-semantics framework with subbisimulation, one of the three general approaches surveyed.","marker":"[13]"},{"why":"Extends [13] into a general theory of interaction with four fundamental principles, the second general framework discussed.","marker":"[12]"},{"why":"Defines expressiveness via validity and correctness up to a semantic relation, the third general framework surveyed.","marker":"[18]"},{"why":"Discusses pitfalls and misunderstandings of full abstraction, supporting the paper's claim that full abstraction is not well understood.","marker":"[23]"},{"why":"States general conditions for full abstraction, used alongside [23] to argue that full abstraction needs fixed equivalences to be meaningful.","marker":"[46]"},{"why":"Supplies the terminology of relative expressive power and several structural criteria that the survey revises.","marker":"[45]"},{"why":"Classic separation result requiring the homomorphic translation of the parallel operator, used as the running example of domain-specific structural criteria.","marker":"[43]"}],"fun_headline_variants":["Encodability criteria united through source-target relations","Mapping criteria to relations makes encodings comparable","One relation to compare process calculi encodings","Survey reduces encoding criteria to relation conditions","How encoding criteria become relation properties"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The decisive premise is that the three lemmas quoted from [50] really do capture full abstraction and (weak) operational correspondence as relation-based conditions, because this survey imports those lemmas without reproof and the Section 5 analysis stands or falls with them.","fun_headline_variants_meta":{"raw":{"variants":["Encodability criteria united through source-target relations","Mapping criteria to relations makes encodings comparable","One relation to compare process calculi encodings","Survey reduces encoding criteria to relation conditions","How encoding criteria become relation properties"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001084,"raw_usage":{"total_tokens":4515,"prompt_tokens":909,"completion_tokens":3606,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":525,"completion_tokens_details":{"reasoning_tokens":3539}},"tokens_in":525,"tokens_out":3606,"duration_ms":26158,"temperature":1.0,"reasoning_tokens":3539,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:33:05.083190+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A single counterexample within the machine-checked formalisation [51] — a pair of calculi and an encoding that is fully abstract with respect to preorders $R_S$ and $R_T$ but for which no transitive relation $R$ with $(S,\\llbracket S\\rrbracket)$ and $(\\llbracket S\\rrbracket,S)$ in $R$ and $R_S = R\\upharpoonright P_S$, $R_T = R\\upharpoonright P_T$ exists — would refute Lemma 5.1 and with it the claim that full abstraction imposes almost no semantic constraint. More broadly, producing any commonly used encodability criterion that cannot be expressed as a condition on the encoding-induced relation would falsify the paper's central methodological thesis.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces the labelled-semantics framework with subbisimulation, one of the three general approaches surveyed."},{"cited_title":"Parrow (2008): Expressiveness of Process Algebras","cited_arxiv_id":null,"evidence_quote":"Supplies the terminology of relative expressive power and several structural criteria that the survey revises."}],"review_version":1}