arxiv: 2605.02362 · v1 · submitted 2026-05-04 · 💻 cs.LO · cs.PL

Recognition: 2 theorem links

· Lean Theorem

A uniform characterisation of the (a)synchronous must-preorder

Giovanni Bernardi (UPCit\'e , IRIF (UMR\_8243)) , Hugo F\'er\'ee (UPCit\'e , Ga\"etan Lopez (UPCit\'e

Authors on Pith no claims yet

Pith reviewed 2026-05-08 18:34 UTC · model grok-4.3

classification 💻 cs.LO cs.PL

keywords must-preorderlabel abstractionsynchronousasynchronousmessage passingprocess calculussubstitutivitycharacterisation

0 comments

The pith

Label abstractions yield a uniform characterisation of the must-preorder across synchronous and asynchronous message-passing with or without values.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper seeks a single alternative relation that characterises the De Nicola-Hennessy must-preorder in all four combinations of synchronous versus asynchronous communication and value-passing versus pure communication. Separate characterisations have existed for each setting, which fragments the theory and makes proofs and tool support harder to maintain. An axiomatic, calculus-independent approach distinguishes blocking from non-blocking actions through the new notion of label abstraction, which encodes safe substitutivity with respect to interactions. This yields one definition together with one soundness proof and one completeness proof that cover every setting; the proofs are constructive and fully mechanised. A reader would care because the result promises a simpler, more general foundation for deciding when one program is an improvement over another in concurrent message-passing systems.

Core claim

The must-preorder is characterised by a relation defined using label abstractions. These abstractions capture the essence of safe substitutivity with respect to interactions and highlight the role of blocking and non-blocking actions. The same relation, together with a single proof of soundness and a single proof of completeness, applies to all four combinations of synchronous versus asynchronous communication and value-passing versus pure communication.

What carries the argument

Label abstraction, a novel construction that encodes the distinctions needed for safe substitutivity in interactions between processes.

Load-bearing premise

Label abstractions are sufficient to capture every necessary distinction between blocking and non-blocking actions in all four settings.

What would settle it

A concrete pair of processes in the asynchronous value-passing setting where the label-abstraction relation and the must-preorder disagree on whether one improves the other.

Figures

Figures reproduced from arXiv: 2605.02362 by Ga\"etan Lopez (UPCit\'e, Giovanni Bernardi (UPCit\'e, Hugo F\'er\'ee (UPCit\'e, IRIF (UMR\_8243)).

**Figure 1.** Figure 1: They define what it means for an action to be view at source ↗

read the original abstract

In the setting of message passing software, De Nicola and Hennessy must-preorder defines when a program improves on another one. Since this preorder does not come equipped with a viable proof method, using it requires an alternative relation that characterises it. The literature presents at least four different definitions of such alternative preorders, depending on whether communication is synchronous or asynchronous and on whether there is value-passing or not. The existence of these different definitions complicates the overall theory, hinders the development of tools, and, upon the whole, suggests a lack of understanding of the properties necessary and sufficient to reason on the must-preorder. This paper presents the first alternative characterisation that works at least in all the four settings mentioned above. We achieve this result thanks to an axiomatic approach that is calculus independent, by highlighting the role of blocking and non-blocking actions, and by introducing the novel notion of label abstraction. Label abstractions capture the essence of safe substitutivity w.r.t. interactions, and they let us obtain a unique proof of soundness and a unique proof of completeness that work in all the mentioned settings. We believe this generalises and simplifies the overall theory, while letting us present the existing results in a uniform way. Our proofs are constructive and our result is entirely mechanised in Rocq.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper unifies the must-preorder characterizations across sync/async and value/no-value settings with one axiomatic setup and mechanized proofs.

read the letter

The paper unifies characterizations of the must-preorder for message-passing programs across synchronous and asynchronous communication, both with and without value passing. It does so with a single axiomatic setup and one pair of soundness and completeness proofs. The new element is the concept of label abstraction, which captures safe substitutivity with respect to interactions by focusing on blocking and non-blocking actions. This allows an axiomatic approach that is independent of the specific calculus. The authors have mechanized the constructive proofs in Rocq, which is a strong point for verifiability. This approach does well in simplifying the theory. Instead of maintaining four different alternative preorders, there's now a uniform way to present and prove results about the must-preorder. That could help reduce duplication in future work on tools or extensions. The main soft spot is around the uniformity of the label abstraction. The claim is that one definition works for all four settings, but it would be important to check if the abstraction or the axioms need any tweaks for the asynchronous value-passing case, such as handling message queues. If the mechanized proofs use the exact same statements across cases, then it holds up. Otherwise, the unification might be less complete than it appears. The paper avoids circular definitions, which is positive. This work is aimed at researchers in concurrency theory and process algebra. Anyone studying testing preorders or developing proof methods for them would get value from seeing the results presented uniformly. It deserves a serious referee because the mechanization and the attempt at unification provide enough substance for detailed feedback. I recommend sending this to peer review.

Referee Report

2 major / 2 minor

Summary. The paper claims to provide the first alternative characterization of the De Nicola-Hennessy must-preorder that applies uniformly to all four combinations of synchronous/asynchronous communication and value-passing/no-value-passing. It uses a calculus-independent axiomatic approach, introduces the novel notion of label abstractions to capture safe substitutivity w.r.t. interactions, and supplies constructive soundness and completeness proofs that are mechanized in Rocq and claimed to be setting-independent.

Significance. If the uniformity claim holds, the work would consolidate previously separate characterizations in the process-algebra literature into a single framework with unified proofs, simplifying the theory and supporting tool development. The mechanized constructive proofs constitute a clear strength, supplying machine-checked evidence that can be inspected and extended.

major comments (2)

[§4.2] §4.2 (Definition of label abstraction): the definition is presented as uniform and free of setting-specific parameters, yet the completeness argument must be shown to rely on exactly the same axioms and lemmas for blocking/non-blocking distinctions in both the value-passing and non-value-passing cases; any hidden case distinction would undermine the central uniformity claim.
[§6] §6 (Completeness proof): the manuscript asserts a single proof works across all four settings, but the mechanization must be examined for any auxiliary lemmas about message queues or value matching that are proved separately per setting; if such splits exist, the 'unique proof' claim requires revision even if each individual case is correct.

minor comments (2)

[Abstract] The abstract states the result works 'at least in all the four settings'; the introduction should explicitly list which calculi were used for the mechanization and whether the proofs apply verbatim to each.
[§3] Notation for label abstractions could be introduced earlier with a small example illustrating how blocking versus non-blocking actions are abstracted in a concrete process.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for highlighting the potential of our uniform characterization. We address the major comments point by point below, defending the uniformity of our definitions and proofs while offering clarifications where appropriate.

read point-by-point responses

Referee: [§4.2] §4.2 (Definition of label abstraction): the definition is presented as uniform and free of setting-specific parameters, yet the completeness argument must be shown to rely on exactly the same axioms and lemmas for blocking/non-blocking distinctions in both the value-passing and non-value-passing cases; any hidden case distinction would undermine the central uniformity claim.

Authors: The definition of label abstraction in §4.2 is formulated in a purely axiomatic, calculus-independent manner with no setting-specific parameters. The completeness argument applies identical axioms and lemmas to handle blocking and non-blocking distinctions uniformly across value-passing and non-value-passing cases. These distinctions are resolved through the label abstraction mechanism itself, which encodes safe substitutivity without introducing hidden case splits. The Rocq mechanization uses a single set of definitions and lemmas for this purpose. revision: no
Referee: [§6] §6 (Completeness proof): the manuscript asserts a single proof works across all four settings, but the mechanization must be examined for any auxiliary lemmas about message queues or value matching that are proved separately per setting; if such splits exist, the 'unique proof' claim requires revision even if each individual case is correct.

Authors: Section 6 presents a single, setting-independent completeness proof that applies to all four combinations. In the Rocq mechanization, auxiliary lemmas on message queues and value matching are expressed generically via the parameterized label abstraction framework, with no separate per-setting proofs for the core results. Setting-specific behaviors appear only at the level of instantiation, preserving the unique proof structure. We will add a short clarification in the revised manuscript describing the modular organization of the mechanization to make this explicit. revision: partial

Circularity Check

0 steps flagged

Uniform axiomatic characterisation via label abstractions is self-contained and non-circular

full rationale

The paper introduces label abstractions as a novel but independently defined notion to characterise the pre-existing De Nicola-Hennessy must-preorder. The derivation proceeds via an axiomatic, calculus-independent approach with uniform soundness and completeness proofs across the four settings, all mechanised in Rocq. No equation or step equates the target preorder to a function of the new characterisation by construction, nor does any load-bearing premise reduce to a self-citation or fitted input. The mechanised proofs supply independent verification outside any definitional loop.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper relies on standard process-algebra axioms for the must-preorder and transition semantics. It introduces label abstraction as a new device with no free parameters or invented physical entities mentioned.

axioms (1)

domain assumption Standard transition semantics and must-preorder definition for message-passing calculi
Used to define the target relation being characterized.

invented entities (1)

label abstraction no independent evidence
purpose: Captures safe substitutivity with respect to interactions by abstracting labels while preserving blocking behavior
Novel notion introduced to obtain uniform proofs

pith-pipeline@v0.9.0 · 8838 in / 1121 out tokens · 52717 ms · 2026-05-08T18:34:52.029577+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

83 extracted references · 1 canonical work pages

[1]

Observation equivalence as a testing equivalence

Samson Abramsky. Observation equivalence as a testing equivalence. TCS , 1987

1987
[2]

Termination, Deadlock, and Divergence

Luca Aceto and Matthew Hennessy. Termination, Deadlock, and Divergence . J. ACM , 1992

1992
[3]

Testing Hennessy-Milner Logic with Recursion

Luca Aceto and Anna Ing \' o lfsd \' o ttir. Testing Hennessy-Milner Logic with Recursion . In FOSSACS , 1999

1999
[4]

Amadio, Ilaria Castellani, and Davide Sangiorgi

Roberto M. Amadio, Ilaria Castellani, and Davide Sangiorgi. On bisimulations for the asynchronous pi-calculus. TCS , 1998

1998
[5]

Processes against tests: On defining contextual equivalences

Cl \' e ment Aubert and Daniele Varacca. Processes against tests: On defining contextual equivalences. J. LAMP , 2022

2022
[6]

Asynchronous Traces and Open Petri Nets

Paolo Baldan, Filippo Bonchi, Fabio Gadducci, and Giacoma Valentina Monreale. Asynchronous Traces and Open Petri Nets . In Programming Languages with Applications to Biology and Security , 2015

2015
[7]

Monads and effects

Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In APPSEM
[8]

Input-output conformance testing for software product lines

Harsh Beohar and Mohammad Reza Mousavi. Input-output conformance testing for software product lines. J. LAMP , 2016

2016
[9]

Thompson

P \' e ter Bereczky, D \' a niel Horp \' a csi, and Simon J. Thompson. Program equivalence in the erlang actor model. Comput. , 2024

2024
[10]

Bernardi, O

G. Bernardi, O. Dardha, S. J. Gay, and D. Kouzapas. On Duality Relations for Session Types . In TGC , 2014

2014
[11]

Constructive characterisations of the must-preorder for asynchrony

Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, and L \' e o Stefanesco. Constructive characterisations of the must-preorder for asynchrony. In ESOP , 2025

2025
[12]

Mutually Testing Processes

Giovanni Bernardi and Matthew Hennessy. Mutually Testing Processes . LMCS , 2015

2015
[13]

Using higher-order contracts to model session types

Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types. LMCS , 2016

2016
[14]

Full-abstraction for client testing preorders

Giovanni Tito Bernardi and Adrian Francalanza. Full-abstraction for client testing preorders. Sci. Comput. Program. , 2018

2018
[15]

Modelling session types using contracts

Giovanni Tito Bernardi and Matthew Hennessy. Modelling session types using contracts. MSCS , 2016

2016
[16]

A complete normal-form bisimilarity for state

Dariusz Biernacki, Sergue \" Lenglet, and Piotr Polesiuk. A complete normal-form bisimilarity for state. In FOSSACS , 2019

2019
[17]

Brzozowski's and Up-To Algorithms for Must Testing

Filippo Bonchi, Georgiana Caltais, Damien Pous, and Alexandra Silva. Brzozowski's and Up-To Algorithms for Must Testing . In APLAS , 2013

2013
[18]

Trace and Testing Equivalence on Asynchronous Processes

Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Trace and Testing Equivalence on Asynchronous Processes . Inf. Comput. , 2002

2002
[19]

An abstract, certified account of operational game semantics

Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, and Yannick Zakowski. An abstract, certified account of operational game semantics. In ESOP , 2025

2025
[20]

Asynchrony and the Pi-calculus

G \' e rard Boudol. Asynchrony and the Pi-calculus . Research Report RR-1702, INRIA , 1992

1992
[21]

Representation of computations in concurrent automata by dependence orders

Felipe Bracho, Manfred Droste, and Dietrich Kuske. Representation of computations in concurrent automata by dependence orders. TCS , 1997

1997
[22]

On communicating finite-state machines

Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM , 1983

1983
[23]

The Mays and Musts of Concurrent Strategies

Simon Castellan, Pierre Clairambault, and Glynn Winskel. The Mays and Musts of Concurrent Strategies . In Samson Abramsky on Logic and Structure in Computer Science and Beyond , 2023

2023
[24]

Testing Theories for Asynchronous Languages

Ilaria Castellani and Matthew Hennessy. Testing Theories for Asynchronous Languages . In FSTTCS , 1998

1998
[25]

Quantum bisimilarity via barbs and contexts: Curbing the power of non-deterministic observers

Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Quantum bisimilarity via barbs and contexts: Curbing the power of non-deterministic observers. (POPL), 2024

2024
[26]

Testing quantum processes

Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Testing quantum processes. In ISoLA , 2024

2024
[27]

Choice trees: Representing nondeterministic, recursive, and impure programs in Coq.Proc

Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. Choice trees: Representing nondeterministic, recursive, and impure programs in coq. POPL , 2023. https://doi.org/10.1145/3571254 doi:10.1145/3571254

work page doi:10.1145/3571254 2023
[28]

Cleaveland, Z

R. Cleaveland, Z. Dayar, S. A. Smolka, and S. Yuen. Testing Preorders for Probabilistic Processes . Inf. Comput. , 1999

1999
[29]

Testing Equivalence as a Bisimulation Equivalence

Rance Cleaveland and Matthew Hennessy. Testing Equivalence as a Bisimulation Equivalence . In Joseph Sifakis, editor, Automatic Verification Methods for Finite State Systems , 1989

1989
[30]

Testing-based abstractions for value-passing systems

Rance Cleaveland and James Riely. Testing-based abstractions for value-passing systems. In CONCUR , 1994

1994
[31]

Linda-based applicative and imperative process algebras

Rocco De Nicola and Rosario Pugliese. Linda-based applicative and imperative process algebras. TCS , 2000

2000
[32]

The buffered \( \) -calculus: A model for concurrent languages

Xiaojie Deng, Yu Zhang, Yuxin Deng, and Farong Zhong. The buffered \( \) -calculus: A model for concurrent languages. In LATA , 2013

2013
[33]

Y. Deng, R. J. van Glabbeek, M. Hennessy, and C. Morgan. Characterising Testing Preorders for Finite Probabilistic Processes . Log. Methods Comput. Sci. , 2008

2008
[34]

Characterisations of testing preorders for a finite probabilistic \( \) -calculus

Yuxin Deng and Alwen Tiu. Characterisations of testing preorders for a finite probabilistic \( \) -calculus. Formal Aspects Comput. , 2012

2012
[35]

van Glabbeek, Carroll Morgan, and Chenyi Zhang

Yuxin Deng, Rob J. van Glabbeek, Carroll Morgan, and Chenyi Zhang. Scalar outcomes suffice for finitary probabilistic testing. In ESOP , 2007

2007
[36]

Directed Algebraic Topology and Concurrency

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raussen. Directed Algebraic Topology and Concurrency . 2016

2016
[37]

Wan J. Fokkink. Modelling Distributed Systems . Texts in Theoretical Computer Science. An EATCS Series. 2007

2007
[38]

Call-by-push-value in coq: operational, equational, and denotational theory

Yannick Forster, Steven Sch \" a fer, Simon Spies, and Kathrin Stark. Call-by-push-value in coq: operational, equational, and denotational theory. In CPP , 2019

2019
[39]

Gay, Peter Thiemann, and Vasco T

Simon J. Gay, Peter Thiemann, and Vasco T. Vasconcelos. Duality of session types: The final cut. In PLACES , EPTCS , 2020

2020
[40]

A fully abstract game semantics for finite nondeterminism

Russell Harmer and Guy McCusker. A fully abstract game semantics for finite nondeterminism. In LICS , 1999

1999
[41]

Composable memory transactions

Tim Harris, Simon Marlow, Simon Peyton Jones, and Maurice Herlihy. Composable memory transactions. In PPoPP , 2005

2005
[42]

Full abstractness for a functional/concurrent language with higher-order value-passing

Chrysafis Hartonas and Matthew Hennessy. Full abstractness for a functional/concurrent language with higher-order value-passing. Inf. Comput. , 1998

1998
[43]

Powerdomains and nondeterministic recursive definitions

Matthew Hennessy. Powerdomains and nondeterministic recursive definitions. In International Symposium on Programming , 1982

1982
[44]

Acceptance Trees

Matthew Hennessy. Acceptance Trees . J. ACM , 1985

1985
[45]

Algebraic theory of processes

Matthew Hennessy. Algebraic theory of processes . MIT Press series in the foundations of computing. MIT Press, 1988

1988
[46]

A model for the -calculus

Matthew Hennessy. A model for the -calculus. TCS , 1993

1993
[47]

A fully abstract denotational semantics for the pi-calculus

Matthew Hennessy. A fully abstract denotational semantics for the pi-calculus. TCS , 2002

2002
[48]

The security pi-calculus and non-interference

Matthew Hennessy. The security pi-calculus and non-interference. J. LAMP , 2005

2005
[49]

A distributed Pi-calculus

Matthew Hennessy. A distributed Pi-calculus . Cambridge University Press, 2007

2007
[50]

A theory of communicating processes with value passing

Matthew Hennessy and Anna Ing \' o lfsd \' o ttir. A theory of communicating processes with value passing. Inf. Comput. , 1993

1993
[51]

Scherer III

Maurice Herlihy, Victor Luchangco, Mark Moir, and William N. Scherer III. Software transactional memory for dynamic-sized data structures. In PODC , 2003

2003
[52]

C. A. R. Hoare. Communicating Sequential Processes (Reprint) . Commun. ACM , 1983

1983
[53]

An Object Calculus for Asynchronous Communication

Kohei Honda and Mario Tokoro. An Object Calculus for Asynchronous Communication . In Pierre America, editor, ECOOP , 1991

1991
[54]

Syteci: automating contextual equivalence for higher-order programs with references

Guilhem Jaber. Syteci: automating contextual equivalence for higher-order programs with references. POPL , 2020

2020
[55]

Beautiful concurrency

Simon Peyton Jones. Beautiful concurrency. In Beautiful Code . 2007

2007
[56]

Kanellakis and Scott A

Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. , 1990

1990
[57]

A Testing Theory for a Higher-Order Cryptographic Language - (Extended Abstract)

Vasileios Koutavas and Matthew Hennessy. A Testing Theory for a Higher-Order Cryptographic Language - (Extended Abstract) . In ESOP , 2011

2011
[58]

Fully abstract normal form bisimulation for call-by-value PCF

Vasileios Koutavas, Yu - Yang Lin, and Nikos Tzevelekos. Fully abstract normal form bisimulation for call-by-value PCF . J. ACM , 2025

2025
[59]

S ren B. Lassen. Bisimulation in untyped lambda calculus: B \" o hm trees and bisimulation up to context. In MFPS , 1999

1999
[60]

S ren B. Lassen. Eager normal form bisimulation. In LICS , 2005

2005
[61]

Mason and Carolyn L

Ian A. Mason and Carolyn L. Talcott. Equivalence in functional languages with effects. J. Funct. Program. , 1991

1991
[62]

Games and full abstraction for FPC

Guy McCusker. Games and full abstraction for FPC . Inf. Comput. , 2000

2000
[63]

Asynchronous games: Innocence without alternation

Paul - Andr \' e Melli \` e s and Samuel Mimram. Asynchronous games: Innocence without alternation. In CONCUR , 2007

2007
[64]

Concurrent separation logic meets template games

Paul - Andr \' e Melli \` e s and L \' e o Stefanesco. Concurrent separation logic meets template games. In LICS , 2020

2020
[65]

State monads and their algebras

François Metayer. State monads and their algebras. arXiv, CoRR, 2004

2004
[66]

Combining nondeterminism, probability, and termination: Equational and metric reasoning

Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In LICS , 2021

2021
[67]

Concurrent automata vs

R \' e mi Morin. Concurrent automata vs. asynchronous systems. In MFCS , 2005

2005
[68]

James H. Morris. Lambda-calculus models of programming languages . PhD thesis, Massachusetts Institute of Technology, 1969

1969
[69]

Towards a formal testing theory for quantum processes

Mohammad Reza Mousavi, Kirstin Peters, and Anna Schmitt. Towards a formal testing theory for quantum processes. In REoCAS Colloquium in Honor of Rocco De Nicola , 2024

2024
[70]

Testing equivalences for processes

Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theor. Comput. Sci. , 1984

1984
[71]

A hierarchy of equivalences for probabilistic processes

Manuel Núñez and Luis Llana. A hierarchy of equivalences for probabilistic processes. FORTE , 2008

2008
[72]

A. M. Pitts. Operationally-based theories of program equivalence. In Semantics and Logics of Computation . 1997

1997
[73]

Andrew M. Pitts. Operational semantics and program equivalence. In APPSEM , 2000

2000
[74]

Fair testing

Arend Rensink and Walter Vogler. Fair testing. Inf. Comput. , 2007

2007
[75]

Introduction to Static Analysis: An Abstract Interpretation Perspective

Xavier Rival and Kwangkeun Yi. Introduction to Static Analysis: An Abstract Interpretation Perspective . The MIT Press, 2020

2020
[76]

The Pi-Calculus - a Theory of Mobile Processes

Davide Sangiorgi and David Walker. The Pi-Calculus - a Theory of Mobile Processes . 2001

2001
[77]

First-Order Axioms for Asynchrony

Peter Selinger. First-Order Axioms for Asynchrony . In CONCUR , 1997

1997
[78]

Bonsangue, and Jan J

Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci. , 2013

2013
[79]

Michael B. Smyth. Power domains. J. Comput. Syst. Sci. , 1978

1978
[80]

Eugene W. Stark. Connections between a concrete and an abstract model of concurrent systems. In MFPS , 1989

1989

Showing first 80 references.