# Constructive characterisations of the must-preorder for asynchrony

Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, Léo Stefanesco

► To cite this version:

Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, Léo Stefanesco. Constructive characterisations of the must-preorder for asynchrony. ESOP, May 2025, Hamilton, Ontario, Canada, Canada. pp.88-116, 10.4230/LIPIcs.hal-04642776v2

HAL Id: hal-04642776

https://hal.science/hal-04642776v2

Submitted on 17 Jan 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Constructive characterisations of the
must-preorder for asynchrony

Giovanni Bernardi¹[0009-0008-3653-3040], Ilaria Castellani²[0000-0001-9820-0892],
Paul Laforgue¹,3[0009-0009-6688-4850], and Léo Stefanesco⁴[0000-0002-4719-2922]\*

¹ Université Paris Cité, CNRS, IRIF, F-75013, Paris, France

² INRIA, Université Côte d'Azur, France

³ Nomadic Labs, Paris, France

⁴ University of Cambridge, United Kingdom

**Abstract.** De Nicola and Hennessy's MUST-preorder is a liveness preserving refinement which states that a server *q* refines a server *p* if all clients satisfied by *p* are also satisfied by *q*. Owing to the universal quantification over clients, this definition does not yield a practical proof method, and alternative characterisations are necessary to reason over it. Finding these characterisations for asynchronous semantics, i.e. where outputs are non-blocking, has thus far proven to be a challenge, usually tackled via ad-hoc definitions.

We show that the standard characterisations of the MUST-preorder carry
over as they stand to asynchronous communication, if servers are en-
hanced to act as forwarders, i.e. they can input any message as long as
they store it back into the shared buffer. Our development is constructive,
is completely mechanised in Coq, and is independent of any calculus: our
results pertain to Selinger output-buffered agents with feedback. This is
a class of Labelled Transition Systems that captures programs that com-
municate via a shared unordered buffer, as in asynchronous CCS or the
asynchronous π-calculus.

We show that the standard coinductive characterisation lets us prove in
Coq that concrete programs are related by the MUST-preorder.

Finally, our proofs show that Brouwer's bar induction principle is a useful
technique to reason on liveness preserving program transformations.

# 1 Introduction

Code refactoring is a routine task to develop or update software, and it requires
methods to ensure that a program *p* can be safely replaced by a program *q*.
One way to address this issue is via refinement relations, *i.e.* preorders. For
programming languages, the most well-known one is Morris *extensional* preorder
[75, pag. 50], defined by letting *p* ≤ *q* if for all contexts *C*, whenever *C[p]* reduces
to a normal form *N*, then *C[q]* also reduces to *N*.

<footnote>* Work done at MPI-SWS, Germany.</footnote>
**Comparing servers** This paper studies a version of Morris preorder for nondeterministic asynchronous client-server systems. In this setting it is natural to reformulate the preorder by replacing reduction to normal forms (i.e. termination) with a suitable liveness property. Let $p \leqbar r$ denote a client-server system, that is a parallel composition in which the identities of the server $p$ and the client $r$ are distinguished, and whose computations have the form $p \leqbar r = p_0 \leqbar r_0 \longrightarrow p_1 \leqbar r_1 \longrightarrow p_2 \leqbar r_2 \longrightarrow \dots$, where each step represents either an internal computation of one of the two components, or an interaction between them. Interactions correspond to handshakes, where two components ready to perform matching input/output actions advance together. We express liveness by saying that $p$ *must pass* $r$, denoted $p \text{MUST} r$, if in every maximal computation of $p \leqbar r$ there exists a state $p_i \leqbar r_i$ such that $\text{GOOD}(r_i)$, where GOOD is a decidable predicate indicating that the client has reached a successful state. Servers are then compared according to their capacity to satisfy clients, i.e. via contexts of the form $[-] \leqbar r$ and the predicate MUST. Morris preorder then becomes the MUST-preorder by De Nicola and Hennessy [43] : $p \preceq_{\text{MUST}} q$ when $\forall r. p \text{MUST} r$ implies $q \text{MUST} r$.

**Advantages** The MUST-preorder is by definition liveness preserving, because $p \text{MUST} r$ literally means that “in every execution something good must happen (on the client side)”. Results on $\preceq_{\text{MUST}}$ thus shed light on liveness-preserving program transformations.

The MUST-preorder is independent of any particular calculus, as its definition requires simply (1) a reduction semantics for the parallel composition $p \leqbar r$, and (2) a predicate GOOD over programs. Hence $\preceq_{\text{MUST}}$ may relate servers written in different languages. For instance, servers written in OCAML may be compared to servers written in JAVA according to clients written in PYTHON, because all these languages use the same basic protocols for communication.

**Drawback** The definition of the MUST-preorder is *contextual*: proving $p \preceq_{\text{MUST}} q$ requires analysing an infinite amount of clients, and so the definition of the preorder does not entail an effective proof method. A solution to this problem is to define an *alternative (semantic) characterisation* of the preorder $\preceq_{\text{MUST}}$, i.e. a preorder $\prec_{alt}$ that coincides with $\preceq_{\text{MUST}}$ and does away with the universal quantification over clients (i.e. contexts). In *synchronous* settings, i.e. when both input and output actions are blocking, such alternative characterisations have been thoroughly investigated, typically via a behavioural approach based on labelled transition systems.

**Labelled transition systems** A program $p$ is associated with a labelled transition system (LTS) representing its behaviour, which we denote by $\text{LTS}(p)$. Figure 1 presents two instances of LTSs, where transitions are labelled by input actions such as `str`, output actions such as `str`, or the internal action $\tau$ (not featured in Figure 1), while dotted nodes represent successful states, i.e. those satisfying the predicate GOOD. There, the server $p_0$ is ready to input either a string or a float. It is the environment that, by offering an output of either type, will make $p$ move to either $p_1$ or $p_2$. The client $r_0$, on the other hand, is ready
<figure><img src="image_2.png" /><figcaption>Fig. 1. The behaviours of a server $p_0$ and of a client $r_0$.</figcaption></figure>

to either output a string, or input an integer. The input `int` makes the client move to the successful state $r_2$, while the output `str` makes the client move to the state $r_1$, where it can still perform the input `int` to reach the successful state $r_3$. In an asynchronous setting, output transitions enjoy a commutativity property on which we will return later. Programs $p$ are usually associated with their behaviours LTS($p$) via inference rules that we omit in the main body of the paper, as they are standard.

*Alternative preorders for synchrony* Program behaviours, i.e. LTSs, are used to define the alternative preorders for $\preceq_{MUST}$ following one of two different approaches: MUST-sets or acceptance sets.

Both approaches were originally proposed for Milner's Calculus of Communicating Systems (CCS) [74], where communication is synchronous. The first alternative preorder, which we denote by $\preceq_{MS}$, was put forth by De Nicola [43], and it compares server behaviours according to their MUST-sets, i.e. the sets of actions that they may perform after doing a given sequence of actions. The second alternative preorder, which we denote by $\preceq_{AS}$, was put forth by Hennessy [55], and it compares the acceptance sets of servers, i.e. how servers can be moved out of their potentially deadlocked states, namely, states from which the servers cannot evolve autonomously. Both these preorders characterise $\preceq_{MUST}$ in the following sense:

$$ \forall p, q \in \text{CCS. } p \preceq_{MUST} q \text{ iff } \text{LTS}(p) \preceq_{MS} \text{LTS}(q) \quad (1) $$

$$ \forall p, q \in \text{CCS. } p \preceq_{MUST} q \text{ iff } \text{LTS}(p) \preceq_{AS} \text{LTS}(q) \quad (2) $$

While these alternative preorders do away with the universal quantification over clients, they are not practical to use directly, as they still universally quantify over (finite) traces of actions. A more practical approach [2] is to use a coinductively defined preorder $\preceq_{co}$ based on $\preceq_{AS}$ [2,72,16]. This preorder has two advantages: first, its definition quantifies universally only on single actions; second, it allows the user to use standard coinductive methods, as found in the literature on bisimulation. In the case where the LTS is image-finite, such as for CCS and most process calculi, the coinductive preorder is sound and complete:

$$ \forall p, q \in \text{CCS. } p \preceq_{MUST} q \text{ iff } \text{LTS}(p) \preceq_{co} \text{LTS}(q) \quad (3) $$
<figure><img src="image_3.png" /><figcaption>**Fig. 2.** First-order axioms for output-buffered agents with feedback as given by Selinger [90], extended with the BACKWARD-OUTPUT-DETERMINACY axiom.</figcaption></figure>

**Asynchrony** In distributed systems, communication is inherently asynchronous. For instance, the standard TCP transmission on the Internet is asynchronous. Actor languages like ELIXIR and ERLANG implement asynchrony via mailboxes, and both PYTHON and JAVASCRIPT offer developers the constructs ASYNC/WAIT, to return promises (of results) or wait for them. In this paper we model asynchrony via output-buffered agents with feedback, as introduced by Selinger [90]. These are LTSs obeying the axioms in Figure 2, where *a* denotes an input action, *ā* denotes an output action, *τ* denotes the internal action, and *α* ranges over all these actions. For instance, the OUTPUT-COMMUTATIVITY axiom states that an output *ā* can always be postponed: if *ā* is followed by any action *α*, it can commute with it. In other words, outputs are non-blocking, as illustrated by the LTS for *r*₀ in Figure 1. We defer a more detailed discussion of these axioms to Section 2.

**Technical difficulties** The practical importance of asynchrony motivates a specific study of $\preceq_{MUST}$. Efforts in this direction have been made, all of which focussed on process calculi [38,23,94,57], while the axioms in Figure 2 apply to LTSs. Note that these axioms impose conditions only over outputs, and this asymmetric treatment of inputs and outputs substantially complicates the proofs of completeness and soundness of the alternative characterisations of $\preceq_{MUST}$. To underline the subtleties due to asynchrony, we note that the completeness result for asynchronous CCS given by Castellani and Hennessy in [38], and subsequently extended to the $\pi$-calculus by Hennessy [57], is false (see Appendix I).
## Contributions and paper structure.

Our main contributions may be summarised as follows (where for each of them, we indicate where it is presented in the paper):

- The first behavioural characterisations of the MUST-preorder (Theorem 1, Theorem 3) that are calculus independent, in that both our definitions and our proofs work directly on LTSs. Contrary to all the previous works on the topic, we show that the standard alternative preorders characterise the MUST-preorder also in Selinger asynchronous setting. To this end, it suffices to enrich the server semantics with forwarding, i.e. ensure that servers are ready to input any message, as long as they store it back in a global shared buffer. This idea, although we use it here in a slightly different form, was pioneered by Honda et al. [64]. In this paper we propose a construction that works on any LTS (Lemma 2) and we show the following counterparts of Equations (1), (2), and (3) where FDB denotes the LTSs of output-buffered agents with feedback, and FW is the function that enhances them with forwarding:

$$ \forall p, q \in \mathbf{FDB}. \ p \preceq_{\mathbf{MUST}} q \ \text{iff} \ \mathrm{FW}(p) \preceq_{\mathbf{MS}} \mathrm{FW}(q) \quad (a) $$

$$ \forall p, q \in \mathbf{FDB}. \ p \preceq_{\mathbf{MUST}} q \ \text{iff} \ \mathrm{FW}(p) \preceq_{\mathbf{AS}} \mathrm{FW}(q) \quad (b) $$

$$ \forall p, q \in \mathbf{FDB}. \ p \preceq_{\mathbf{MUST}} q \ \text{iff} \ \mathrm{FW}(p) \preceq_{\mathbf{CO}} \mathrm{FW}(q) \quad (c) $$

Quite surprisingly, the alternative preorders $\preceq_{\mathbf{AS}}$, $\preceq_{\mathbf{MS}}$ and $\preceq_{\mathbf{CO}}$ need not be changed. We present these results in Section 3. We use the coinductive preorder $\preceq_{\mathbf{CO}}$ to prove the correctness of a form of code hoisting (6).

- The first characterisations of the MUST-preorder that fully exploit asynchrony, i.e. disregard irrelevant (that is, non-causal) orders of visible actions in traces (Corollary 4).

- The first constructive account of the MUST-preorder. We show that if the MUST and termination predicates are defined *intensionally* (in the sense of Brede and Herbelin [28]), then $\preceq_{\mathbf{MUST}}$ can be characterised constructively. The original definitions of MUST and termination given by De Nicola [43], though, are *extensional*. We show how to use Brouwer bar induction principle to prove that the two approaches are logically equivalent (Corollary 2). Since Rahli et al. [81] have shown bar induction to be compatible with constructive type theory, we argue that our development is entirely constructive.

- The first mechanisation of the theory of MUST-preorder in a fully nondeterministic setting, which consists of around 8000 lines of Coq. In Appendix J we gather the Coq versions of all the definitions and the results presented in the main body of the paper.

In Section 6, we discuss the impact of the above contributions, as well as related and future work. In Section 2, we recall the necessary background definitions and illustrate them with a few examples.
<figure><img src="image_4.png" /><figcaption>Fig. 3. Highlights of our Sts and Lts typeclasses.</figcaption></figure>

# 2 Preliminaries

We model individual programs such as servers *p* and clients *r* as LTSs obeying Selinger axioms, while client-server systems *p* ⊲ r are modelled as state transition systems with a reduction semantics. We now formally define this two-level semantics.

Labelled transition systems A labelled transition system (LTS) is a triple $\mathcal{L} = \langle A, L, \rightarrow \rangle$ where A is the set of states, L is the set of labels and $\rightarrow \subseteq A \times L \times A$ is the transition relation. When modelling programs as LTSs, we use transition labels to represent program actions. The set of labels in Selinger LTSs has the same structure as the set of actions in Milner's calculus CCS: one assumes a set of names $\mathcal{N}$, denoting input actions and ranged over by *a*, *b*, *c*, a complementary set of conames $\overline{\mathcal{N}}$, denoting output actions and ranged over by $\overline{\text{a}}$, $\overline{\text{b}}$, $\overline{\text{c}}$, and an invisible action $\tau$, representing internal computation. The set of all actions, ranged over by $\alpha, \beta, \gamma$, is given by $\mathbf{Act}_{\tau} \stackrel{\text{def}}{=} \mathcal{N} \uplus \overline{\mathcal{N}} \uplus \{\tau\}$. We use $\mu, \mu'$ to range over the set of visible actions $\mathcal{N} \uplus \overline{\mathcal{N}}$, and we extend the complementation function $\bar{\cdot}$ to this set by letting $\overline{\text{a}} \stackrel{\text{def}}{=} \text{a}$. In the following, we will always assume $L = \mathbf{Act}_{\tau}$. Once the LTS is fixed, we write $p \xrightarrow{\alpha} p'$ to mean that $(p, \alpha, p') \in \rightarrow$ and $p \xrightarrow{\alpha} p'$ to mean $\exists p'$. $p \xrightarrow{\alpha} p'$.

We use $\mathcal{L}$ to range over LTSs. To reason simultaneously on different LTSs, we will use the symbols $\mathcal{L}_A$ and $\mathcal{L}_B$ to denote respectively the LTSs $\langle A, L, \rightarrow_A \rangle$ and $\langle B, L, \rightarrow_B \rangle$.

In our mechanisation LTSs are borne out by the typeclass Lts in Figure 3. The states of the LTS have type *A*, labels have type *L*, and *lts_step* is the characteristic function of the transition relation, which we assume to be decidable. We let $O(p) = \{\overline{\text{a}} \in \overline{\mathcal{N}} \mid p \xrightarrow{\overline{\text{a}}} \text{\textit{}}\}$ and $I(p) = \{\text{\textit{a}} \in \mathcal{N} \mid p \xrightarrow{\text{\textit{a}}} \text{\textit{}}\}$ be respectively the set of outputs and the set of inputs of state *p*. We assume that the set $O(p)$
<figure><img src="image_5.png" /><figcaption>Fig. 4. The STS of server-client systems.</figcaption></figure>

is finite for any $p$. In our mechanisation, the set $O(p)$ is rendered by the function `ltsougts`, and we shall also use a function `lts_performs` that lets us decide whether a state can perform a transition labelled by a given action.

*Client-server systems* A client-server system (or system, for short) is a pair $p \llbracket r$ in which $p$ is deemed to be the server of client $r$. In general, every system $p \llbracket r$ is the root of a state transition system (STS), $\langle S, \rightarrow \rangle$, where $S$ is the set of states and $\rightarrow$ is the reduction relation. For the sake of simplicity<fnref n="5" /> we derive the reduction relation from the LTS semantics of servers and clients as specified by the rules in Figure 4. In our mechanisation (Figure 3), `sts_step` is the characteristic function of the reduction relation $\rightarrow$, and `sts_stable` is the function that states whether a state can reduce or not. Both functions are assumed decidable.

**Definition 1 (Computation).** Given an STS $\langle S, \rightarrow \rangle$ and a state $s_0 \in S$, a computation of $s_0$ is a finite or infinite reduction sequence starting from $s_0$. A computation is maximal if either it cannot be extended or it is infinite.

To formally define the MUST-preorder, we assume a decidable predicate GOOD over clients. A computation $p \llbracket r = p_0 \llbracket r_0 \rightarrow p_1 \llbracket r_1 \rightarrow p_2 \llbracket r_2 \rightarrow \dots$ is successful if there exists a state $p_i \llbracket r_i$ such that GOOD($r_i$). We assume the predicate GOOD to be invariant under outputs:

$$ \text{If } r \xrightarrow{\bar{a}} r' \text{ then } \mathrm{GOOD}(r) \iff \mathrm{GOOD}(r') \quad (4) $$

All the previous works on asynchronous calculi implicitly make this assumption, since they rely on ad-hoc actions such as $\omega$ or $\checkmark$ to signal success and they treat them as outputs. In Appendix H we show that this assumption holds for the language `ACCS` (the asynchronous variant of `CCS`) extended with the process 1, which is used as a syntactic means to denote GOOD states. Moreover, when considering an equivalence on programs $\simeq$ that is compatible with transitions, in the sense of Figure 5, we assume the predicate `GOOD` to be preserved also by this equivalence. These assumptions are met by the frameworks in [38,23,57].

**Definition 2 (Client satisfaction).** We write $p \text{ MUST } r$ if every maximal computation of $p \llbracket r$ is successful.

<footnote n="5">⁵ In general the reduction semantics and the LTS of a calculus are defined independently, and connected via the Harmony lemma ([85], Lemma 1.4.15 page 51). We have a mechanised proof of it.</footnote>
**Definition 3 (must-preorder).** We let $p \preceq_{\text{MUST}} q$ whenever for every client $r$ we have that $p \text{ MUST } r$ implies $q \text{ MUST } r$.

*Example 1.* Consider the system $p_0 \leftrightharpoons r_0$, where $p_0$ and $r_0$ are the server and client given in Figure 1. The unique maximal computation of this system is $p_0 \leftrightharpoons r_0 \rightarrow p_1 \leftrightharpoons r_1 \rightarrow p_3 \leftrightharpoons r_3$. This computation is successful since it leads the client to the GOOD state $r_3$. Hence, client $r_0$ is satisfied by server $p_0$. Since OUTPUT-COMMUTATIVITY implies an absence of causality between the output *str* and the input *int* in the client, it is the order between the input *str* and the output *int* in the server that guides the order of client-server interactions. $\square$

*A closer look at Selinger axioms* Let us now discuss the axioms in Figure 2. The OUTPUT-COMMUTATIVITY axiom expresses the non-blocking behaviour of outputs: an output cannot be a cause of any subsequent transition, since it can also be executed after it, leading to the same resulting state. Hence, outputs are concurrent with any subsequent transition. The FEEDBACK axiom says that an output followed by a complementary input can also synchronise with it to produce a τ-transition. These first two axioms specify properties of outputs that are followed by another transition. Instead, the following three axioms, OUTPUT-CONFLUENCE, OUTPUT-DETERMINACY and OUTPUT-TAU, specify properties of outputs that are co-initial with another transition<fnref n="6" />. The OUTPUT-DETERMINACY and OUTPUT-TAU axioms apply to the case where the co-initial transition is an identical output or a τ-transition respectively, while the OUTPUT-CONFLUENCE axiom applies to the other cases. When taken in conjunction, these three axioms state that outputs cannot be in conflict with any co-initial transition, except when this is a τ-transition: in this case, the OUTPUT-TAU axiom allows for a confluent nondeterminism between the τ-transition on one side and the output followed by the complementary input on the other side.

We now explain the novel BACKWARD-OUTPUT-DETERMINACY axiom. It is the dual of OUTPUT-DETERMINACY, as it states that also backward transitions with identical outputs lead to the same state. The intuition is that if two programs arrive at the same state by removing the same message from the mailbox, then they must coincide. This axiom need not be assumed in [90] because it can be derived from Selinger axioms when modelling a calculus like ACCS equipped with a parallel composition operator $\parallel$ (see Lemma 53 in Appendix H). We use the BACKWARD-OUTPUT-DETERMINACY axiom only to prove a technical property of clients (Lemma 25) that is used to prove our completeness result.

*Calculi* A number of asynchronous calculi [64,24,38,61,77,86] have an LTS that enjoys the axioms in Figure 2, at least up to some structural equivalence $\equiv$. The reason is that these calculi syntactically enforce outputs to have no continuation, i.e. outputs can only be composed in parallel with other processes.<fnref n="7" /> For

<footnote n="6">⁶ Two transitions are co-initial if they stem from the same state.</footnote>

<footnote n="7">⁷ In the calculus TACCS (a variant of ACCS tailored for testing semantics) of [38] there is a construct of asynchronous output prefix, but its behaviour is to spawn the corresponding atom in parallel with the continuation, so it does not act as a prefix.</footnote>
example, Selinger [90] shows that the axioms of Figure 2 hold for the LTS of the calculus ACCS (the asynchronous variant of CCS<fnref n="8" />) modulo bisimulation, and in Appendix H (Lemma 55) we prove that they hold also for the LTS of ACCS modulo $≡$:

**Lemma 1.** We have that $\langle \text{ACCS}_{\equiv}, L, \rightarrow_{\equiv} \rangle \in \mathbf{FDB}$.

To streamline reasoning modulo some (structural) equivalence we introduce the typeclass LtsEq, whose instances are LTSs equipped with an equivalence $\simeq$ that satisfies the property in Figure 5. Defining output-buffered agents with feedback using LtsEq does not entail any loss of generality, because the equivalence $\simeq$ can be instantiated using the identity over the states A. Further details can be found in Appendix H.1.

When convenient we denote LTSs using the following minimal syntax for ACCS:

$$p, q, r ::= \bar{a} \mid g \mid p \parallel p \mid \text{rec} \cdot x \cdot p \mid x \qquad g ::= 0 \mid a \cdot p \mid \tau \cdot p \mid g + g \quad (5)$$

as well as its standard LTS<fnref n="9" /> whose properties we discuss in detail in Appendix H. This is exactly the syntax used in [90,23], without the operators of restriction and relabelling. Here the syntactic category g defines guards, i.e. the terms that may be used as arguments for the + operator. As in most process calculi, 0 denotes the terminated process that cannot do any action. Note that, apart from 0, only input-prefixed and $\tau$-prefixed terms are allowed as guards, and that the output prefix operator is replaced by atoms $\bar{a}$. In fact, this syntax is completely justified by Selinger axioms, which, as we argued above, specify that outputs cannot cause any other action, nor be in conflict with it.

<figure><img src="image_6.png" /><figcaption>**Fig. 5.** Axiom stating that equivalence $\simeq$ is compatible with a transition relation.</figcaption></figure>

**Definition 4 (Transition sequence).** Given an LTS $\langle A, L, \rightarrow \rangle$ and a state $p_0 \in A$, a transition sequence of $p_0$ is a finite or infinite sequence of the form $p_0 \alpha_1 p_1 \alpha_2 p_2 \cdots$ with $p_i \in A$ and $\alpha_i \in L$, and such that, for every $n \ge 1$ such that $p_n$ is in the sequence we have $p_{n-1} \xrightarrow{\alpha_n} p_n$.

<footnote n="8">⁸ The syntax of ACCS, which is closely inspired by that of the asynchronous $\pi$-calculus with input- and $\tau$-guarded choice [4,5], is given in Equation (5) and discussed later.</footnote>

<footnote n="9">⁹ Where the recursion rule is replaced by the one usually adopted for testing semantics, which introduces a $\tau$-transition before each unfolding.</footnote>
If a transition sequence is made only of $\tau$-transitions, it is called a computation by abuse of notation, the idea being that usually $\tau$-steps are related to reduction steps via the Harmony lemma (see footnote on page 7).

We give now an example that illustrates the use of the testing machinery in our asynchronous setting. This is also a counter-example to the completeness of the alternative preorder proposed in [38], as discussed in detail in Appendix I.

**Example 2.** Let $\Omega = \text{recx.}\tau.x$ and $\text{Pierre} = b.(\tau.\Omega + c.\bar{d})$. The LTS of Pierre is as follows:

<figure><img src="image_7.png" /></figure>

Pierre models a citizen confronted with an unpopular pension reform. To begin with, Pierre can only do the input $b$, which models his getting aware of the brute-force imposition of the reform by the government. After performing the input, Pierre reaches the state $\tau.\Omega + c.\bar{d}$, where he behaves in a nondeterministic manner. He can internally choose not to trust the government for any positive change, in which case he will diverge, refusing any further interaction. But this need not happen: in case the government offers the action $\bar{c}$, which models a positive change in political decision, Pierre can decide to accept this change, and then he expresses his agreement with the output $\bar{d}$, which stands for “done”. $\square$

**Example 3.** We prove now the inequality $\text{Pierre} \preceq_{\text{MUST}} 0$ by leveraging the possibility of divergence of Pierre after the input $b$. Fix an $r$ such that Pierre MUST $r$. Note that, since 0 is the terminated process, the condition for the server 0 to satisfy $r$ is that $r$ reaches by itself a successful state in each of its maximal computations. We distinguish two cases, according to whether $r \xrightarrow{\bar{b}}$ or $r \xrightarrow{\bar{b}}$.

i) Let $r \xrightarrow{\bar{b}} r'$ for some $r'$. Consider the maximal computation Pierre $\vdash r \rightarrow \tau.\Omega + c.\bar{d} \vdash r' \rightarrow \Omega \vdash r' \rightarrow \dots$ in which Pierre diverges and $r$ does not move after the first output. Since Pierre MUST $r$, either GOOD($r$) or GOOD($r'$). In case GOOD($r'$), by Equation (4) we get also GOOD($r$). Hence 0 MUST $r$.

ii) Let $r \xrightarrow{\bar{b}}$. Suppose $r = r_0 \xrightarrow{\tau} r_1 \xrightarrow{\tau} r_2 \xrightarrow{\tau} \dots$ is a maximal computation of $r$. Then Pierre $\vdash r$ has a maximal computation Pierre $\vdash r_0 \rightarrow Pierre \vdash r_1 \rightarrow Pierre \vdash r_2 \rightarrow \dots$. As Pierre MUST $r$, there must exist an $i \in \mathbb{N}$ such that GOOD($r_i$). Hence 0 MUST $r$. $\square$

The argument in Example 3 can directly use Definition 3 because it is very simple to reason on the process 0. The issues brought about by the contextuality of Definition 3, though, hinder showing general properties of $\preceq_{\text{MUST}}$. Consider the following form of code hoisting:

$$ \tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c}) \preceq_{\text{MUST}} \bar{a} \parallel (\tau.\bar{b} + \tau.\bar{c}) \quad (6) $$
If we see the above nondeterministic sums as representing the two branches of a conditional statement, this refinement corresponds to hoisting the shared action $\bar{a}$ before the conditional statement, a common compiler optimisation. Proving Equation (6) via the contextual definition of $\sqsubseteq_M$ is cumbersome. This motivates the study of alternative characterisations for $\sqsubseteq_M$, and in the rest of the paper we present several preorders that fit the purpose, in particular the coinductive preorder $\llcorner_{co}$, which we will use to establish Equation (6) in Section 3.3.

We conclude this section by recalling auxiliary and rather standard notions: given an LTS $\langle A, L, \rightarrow \rangle$, the weak transition relation $p \stackrel{s}{\Rightarrow} p'$, where $s \in \mathbf{Act}^*$, is defined via the rules

$$[\mathbf{wt-refl}] \quad p \stackrel{\epsilon}{\Rightarrow} p$$

$$[\mathbf{wt-tau}] \quad p \stackrel{s}{\Rightarrow} q \text{ if } p \xrightarrow{\tau} p' \text{ and } p' \stackrel{s}{\Rightarrow} q$$

$$[\mathbf{wt-mu}] \quad p \stackrel{\mu.s}{\Rightarrow} q \text{ if } p \xrightarrow{\mu} p' \text{ and } p' \stackrel{s}{\Rightarrow} q$$

We write $p \stackrel{s}{\Rightarrow}$ to mean $\exists p'. p \stackrel{s}{\Rightarrow} p'$.

We write $p \downarrow$ and say that $p$ converges if every computation of $p$ is finite, and we lift the convergence predicate to finite traces by letting the relation $\downarrow \subseteq A \times \mathbf{Act}^*$ be the least one that satisfies the following rules

$[\mathbf{cnv-epsilon}] \quad p \downarrow \epsilon \text{ if } p \downarrow,$

$[\mathbf{cnv-mu}] \quad p \downarrow \mu.s \text{ if } p \downarrow \text{ and } p \stackrel{\mu}{\Rightarrow} p' \text{ implies } p' \downarrow s.$

To understand the next section, one should keep in mind that all the predicates defined above have an implicit parameter: the LTS of programs. By changing this parameter, we may change the meaning of the predicates. For instance, letting $\Omega$ be the ACCS process $\mathit{recx.\tau.x}$, in the standard LTS $\langle \mathit{ACCS}, \rightarrow, \mathit{Act}_{\tau} \rangle$ we have $\Omega \xrightarrow{\tau} \Omega$ and $\neg(\Omega \downarrow)$, while in the LTS $\langle \mathit{ACCS}, \emptyset, \mathit{Act}_{\tau} \rangle$ we have $\Omega \xrightarrow{\tau} \Omega$ and thus $\Omega \downarrow$. In other words, the same predicates can be applied to different LTSs, and since the alternative characterisations of $\sqsubseteq_M$ are defined using such predicates, they can relate different LTSs.

# 3 Preorders based on acceptance sets

We first recall the definition of the standard alternative preorder $\llcorner_{AS}$, and show how to use it to characterise $\sqsubseteq_M$ in our asynchronous setting. We also present a new characterisation that disregards the order of non-causally related actions. We then explain the tools we use to prove these characterisations, and in particular their soundness. This section ends with the coinductive version $\llcorner_{co}$ of $\llcorner_{AS}$, which we use to prove the hoisting refinement (6).

## 3.1 Trace-based characterisations

The ready set of a program $p$ is defined as $R(p) = I(p) \cup O(p)$, and it contains all the visible actions that $p$ can immediately perform. If a program $p$ is stable, i.e. it cannot perform any $\tau$-transition, we say that it is a potential deadlock. In general,
the ready set of a potential deadlock *p* shows how to make *p* move to a different state, possibly one that can perform further computation: if *R(p)* = ∅ then there is no way to make *p* move on, while if *R(p)* contains some action, then *p* is a state waiting for the environment to interact with it. Indeed, potential deadlocks are called *waiting states* in [64]. In particular, in an asynchronous setting the outputs of a potential deadlock *p* show how it can unlock the inputs of a client, which in turn may lead the client to a novel state that can make *p* move, possibly to a state that can perform further computation. A standard manner to capture all the ways out of the potential deadlocks that a program *p* encounters after executing a trace *s* is its acceptance set: *A(p, s, →) = {R(p') | p ⇝ p' τ→}*.

In our presentation we indicate explicitly the third parameter of $\mathcal{A}$, i.e. the transition relation of the LTS at hand, because when necessary we will manipulate this parameter. For any two LTSs $\mathcal{L}_A, \mathcal{L}_B$ and servers $p \in \mathcal{A}, q \in \mathcal{B}$, we write $\mathcal{A}(p, s, \rightarrow_A) \ll \mathcal{A}(q, s, \rightarrow_B)$ if for every $R \in \mathcal{A}(q, s, \rightarrow_B)$ there exists $\hat{R} \in \mathcal{A}(p, s, \rightarrow_A)$ such that $\hat{R} \subseteq R$. We can now recall the definition of the behavioural preorder à la Hennessy, $\preceq_{\text{AS}}$, which is based on acceptance sets [55].

**Definition 5.** We write

- $p \preceq_{\text{cnv}} q$ whenever $\forall s \in \mathcal{A}^* . p \Downarrow_A s$ implies $q \Downarrow_B s$,

- $p \preceq_{\text{acc}} q$ whenever $\forall s \in \mathcal{A}^* . p \Downarrow_A s$ implies $\mathcal{A}(p, s, \rightarrow_A) \ll \mathcal{A}(q, s, \rightarrow_B)$,

- $p \preceq_{\text{AS}} q$ whenever $p \preceq_{\text{cnv}} q$ and $p \preceq_{\text{acc}} q$.

In the synchronous setting, the behavioural preorder $\preceq_{\text{AS}}$ is closely related to the denotational semantics based on Acceptance Trees proposed by Hennessy in [54,55]. There the predicates need not be annotated with the LTS that they are used on, because those works treat a unique LTS. Castellani and Hennessy [38] show in their Example 4 that the condition on acceptance sets, i.e. $\preceq_{\text{acc}}$, is too demanding in an asynchronous setting.

Letting $p = a.0$ and $q = 0$, they show that $p \preceq_{\text{MUST}} q$ but $p \not\preceq_{\text{AS}} q$, because $\mathcal{A}(p, \epsilon) = \{\{a\}\}$ and $\mathcal{A}(q, \epsilon) = \{\emptyset\}$, and corresponding to the ready set $\emptyset \in \mathcal{A}(q, \epsilon)$ there is no ready set $\hat{R} \in \mathcal{A}(p, s)$ such that $\hat{R} \subseteq \emptyset$. Intuitively this is the case because acceptance sets treat inputs and outputs similarly, while in an asynchronous setting only outputs can be tested.

Nevertheless $\preceq_{\text{AS}}$ characterises $\preceq_{\text{MUST}}$, if servers are enhanced as with forwarding. We now introduce this concept.

*Forwarders* We say that an LTS $\mathcal{L}$ is of output-buffered agents with forwarding, for short is FWD, if it satisfies all the axioms in Figure 2 except FEEDBACK, and also the two following axioms:

$$ \begin{array}{ccc} \text{INPUT-BOOMERANG} & p \underset{\bar{a}}{\stackrel{a}{\rightleftharpoons}} p' & p \xrightarrow{\bar{a}} p' \\ & & \downarrow_a \Rightarrow p \xrightarrow{\tau} q \text{ or } p = q \\ & & q \end{array} \quad (7) $$

FWD-FEEDBACK
The INPUT-BOOMERANG axiom states a kind of input-enabledness property, which is however more specific as it stipulates that the target state of the input should loop back to the source state via a complementary output. This is the essence of the behaviour of a forwarder, whose role is simply to pass on a message and then get back to its original state. The FWD-FEEDBACK axiom is a weak form of Selinger's FEEDBACK axiom, which is better understood in conjunction with the INPUT-BOOMERANG axiom: if the transition sequence $p \xrightarrow{\bar{a}} p' \xrightarrow{a} q$ in the FWD-FEEDBACK axiom is taken to be the transition sequence $p' \xrightarrow{\bar{a}} p \xrightarrow{a} p'$ in the INPUT-BOOMERANG axiom, then we see that it must be $q = p$ in the FWD-FEEDBACK axiom. Moreover, no $\tau$ action is issued when moving from $p$ to $q$, since no synchronisation occurs in this case: the message is just passed on.

To prove that $\preceq_{AS}$ is sound and complete with respect to $\preceq_{MUST}$:

1. we define a function FW: FDB $\rightarrow$ FWD that lifts any LTS $\mathcal{L} \in$ FDB into a suitable LTS FW($\mathcal{L}$) $\in$ FWD, and

2. we check the predicates $\Downarrow$ and $\mathcal{A}(-, -, -)$ over the LTS FW($\mathcal{L}$).

Let MO denote the set of all finite multisets of output actions, for instance we have $\emptyset, \{\overline{a}\}, \{\overline{a}, \overline{a}\}, \{\overline{a}, \overline{b}, \overline{a}, \overline{b}\} \in$ MO. We let $M, N, \dots$ range over MO. The symbol $M$ stands for mailbox. We denote with $\uplus$ the multiset union.

**Definition 6.** Let $\text{FW}(\mathcal{L}) = \langle A \times MO, L, \rightarrow_{fw} \rangle$ for every $\mathcal{L} = \langle A, L, \rightarrow \rangle$, where the states in $\text{FW}(\mathcal{L})$ are pairs denoted $p \triangleright M$, such that $p \in A$ and $M \in MO$, and the transition relation $\rightarrow_{fw}$ is defined via the rules in Figure 6.

$$ \text{[L-PROC]} \quad \frac{p \xrightarrow{\alpha} p'}{p \triangleright M \xrightarrow{\alpha} \overline{fw} \ p' \triangleright M} $$

$$ \text{[L-COMM]} \quad \frac{p \xrightarrow{a} p'}{p \triangleright (\{\overline{a}\} \uplus M) \xrightarrow{\tau} \overline{fw} \ p' \triangleright M} $$

$$ \text{[L-MOUT]} \quad \frac{p \triangleright (\{\overline{a}\} \uplus M) \xrightarrow{\bar{a}} \overline{fw} \ p \triangleright M}{p \triangleright M \xrightarrow{a} \overline{fw} \ p \triangleright (\{\overline{a}\} \uplus M)} $$

$$ \text{[L-MINP]} \quad \frac{p \triangleright M \xrightarrow{a} \overline{fw} \ p \triangleright (\{\overline{a}\} \uplus M)}{p \triangleright M \xrightarrow{a} \overline{fw} \ p \triangleright (\{\overline{a}\} \uplus M)} $$

<caption>**Fig. 6.** Lifting of an LTS to an LTS with forwarding.</caption>

Let us briefly comment on Definition 6 and the rules in Figure 6. The pair $p \triangleright M$ is a kind of asymmetric parallel composition between a process $p$ and a mailbox $M$. Rule [L-PROC] says that the process can evolve independently of the mailbox. Rule [L-COMM] says that an input in the process can synchronise with a complementary output in the mailbox. Rules [L-MINP] and [L-MOUT] express the essence of the forwarding behaviour: the pair $p \triangleright M$ may input any message from the environment and store it into the mailbox $M$ (Rule [L-MINP]); dually, the pair $p \triangleright M$ may output any message in the mailbox $M$ towards the environment (Rule [L-MOUT]). Note that in both cases, the interaction occurs between the mailbox $M$ and the environment, without any participation of the process $p$.
### 3. PREORDERS BASED ON ACCEPTANCE SETS

**Example 4.** If a calculus is fixed, then the function FW may have a simpler definition. For instance Castellani and Hennessy [38] define it in their calculus TACCS by letting $\xrightarrow{\alpha}_{\rightarrow_{fw}}$ be the least relation over TACCS such that (1) for every $\alpha \in \text{Act}_\tau$. $\xrightarrow{\alpha} \subseteq \xrightarrow{\alpha}_{\rightarrow_{fw}}$, and (2) for every $a \in \mathcal{N}$. $p \xrightarrow{a} \rightarrow_{fw} p \parallel \bar{a}$. $\square$

The transition relation $\rightarrow_{fw}$ is reminiscent of the one introduced in Definition 8 by Honda and Tokoro in [64]. The construction given in our Definition 6, though, does not yield the LTS of Honda and Tokoro, as $\rightarrow_{fw}$ adds the forwarding capabilities to the states only at the top-level, instead of descending structurally into terms. As a consequence, in the LTS of [64] $a.0+0 \xrightarrow{b} \bar{b}$, while $a.0+0 \triangleright M \xrightarrow{b} \rightarrow_{fw} M \uplus \{\bar{b}\}$.

**Example 5.** As the set $\mathcal{N}$ is countable, every process $p$ that belongs to the LTS $\langle \text{ACCS} \times \text{MO}, \text{Act}_\tau, \rightarrow_{fw} \rangle$ is infinitely-branching: for every mailbox $M$ we have $p \triangleright M \xrightarrow{a_i} \rightarrow_{fw} p \triangleright (\{\bar{a}_i\} \uplus M)$ for every $a_i \in \mathcal{N}$. This is illustrated by the following picture, where for simplicity we omit the subscript fw under the arrows.

<figure><img src="image_8.png" /></figure>

<figure><img src="image_9.png" /></figure>

The intuition behind Definition 6 is that, when a client interacts with a server asynchronously, the client can send any message it likes, regardless of the inputs that the server can actually perform. In fact, asynchronous clients behave as if the server was saturated with *forwarders*, namely processes of the form $a.\bar{a}$, for any $a \in \mathcal{N}$.

The function FW enjoys two crucial properties: it lifts any LTS of output-buffered agents with feedback to an LTS with forwarding, and the lifting preserves the MUST predicate. We can thus reason on $\sqsubseteq_{MUST}$ using LTSs in FWD.

**Lemma 2.** For every LTS $\mathcal{L} \in \text{FDB}$, $\text{FW}(\mathcal{L}) \in \text{FWD}$.

*Proof.* See Appendix C. $\square$

<figure><img src="image_10.png" /></figure>

**Lemma 3.** For every $\mathcal{L}_A, \mathcal{L}_B, \mathcal{L}_C \in \text{FDB}, p \in A, q \in B, r \in C$,

1. $p \sqsubseteq_{MUST} r$ if and only if $\text{FW}(p) \sqsubseteq_{MUST} r$,

2. $p \sqsubseteq_{MUST} q$ if and only if $\text{FW}(p) \sqsubseteq_{MUST} \text{FW}(q)$.

We now simplify the definition of acceptance sets to reason on LTSs that are in FWD: for any LTS $\mathcal{L} = \langle A, \text{Act}, \rightarrow \rangle \in \text{FWD}$ and program $p \in A$ we let $A_{fw}(p, s, \rightarrow) = \{O(p') | p \xrightarrow{s} p' \xrightarrow{\tau} \rightarrow\}$. This definition suffices to characterize $\sqsubseteq_{MUST}$ because in each LTS that is FWD every state performs every input,
thus comparing inputs has no impact on the preorder ≲<sub>acc</sub> of Definition 5. More formally, for every L<sub>A</sub>, L<sub>B</sub> ∈ FWD and every p ∈ A and q ∈ B, we let

$$p \preceq_{acc}^{fw} q \text{ iff } \forall s \in \mathbf{Act}^*. p \downarrow s \text{ implies } A_{fw}(p, s, \rightarrow_A) \ll A_{fw}(q, s, \rightarrow_B)$$

We have the following logical equivalence.

**Lemma 4.** Let L<sub>A</sub>, L<sub>B</sub> ∈ FWD. For every p ∈ A, q ∈ B, p ≲<sub>acc</sub> q if and only if p ≲<sub>acc</sub><sup>fw</sup> q.

*Proof.* The only if implication is trivial, so we discuss the if one. Suppose that p ≲<sub>acc</sub><sup>fw</sup> q and that for some s we have that R ∈ A(q, s, →<sub>B</sub>). Let X be the possibly empty subset of R that contains only output actions. Since L<sub>B</sub> is FWD we know by definition that R = X ∪ N. By definition X ∈ A<sub>fw</sub>(q, s, →<sub>B</sub>), and thus by hypothesis there exists a set of output actions Y ∈ A<sub>fw</sub>(p, s, →<sub>A</sub>) such that Y ⊆ X. It follows that the set Y ∪ N ∈ A(p, s, →<sub>A</sub>), and trivially Y ∪ N ⊆ X ∪ N = R. □

In view of the second point of Lemma 3, to prove completeness it suffices to show that ≲<sub>AS</sub> includes ≲<sub>MUST</sub> over LTSs with forwarding. This is indeed true:

**Lemma 5.** For every L<sub>A</sub>, L<sub>B</sub> ∈ FWD and p ∈ A, q ∈ B, if p ≲<sub>MUST</sub> q then we have p ≲<sub>AS</sub> q.

By a slight abuse of notation, given an LTS L = ⟨A, L, →⟩ and a state p ∈ A, we denote with FW(p) the LTS rooted at p ▷ ∅ in FW(L).

**Theorem 1.** For every L<sub>A</sub>, L<sub>B</sub> ∈ FDB and p ∈ A, q ∈ B,

$$p \preceq_{MUST} q \text{ iff } \mathrm{FW}(p) \preceq_{AS} \mathrm{FW}(q).$$

This theorem is the linchpin of this paper, as all other results presented in this paper are corollaries. To begin with, instantiating this theorem to a calculus which can be given an LTS that satisfies the axioms for output-buffered agents with feedback such as ACCS (Lemma 1), the core join-calculus [48] or KLAIM [42], we get a characterisation of the MUST-preorder essentially for free. In our Coq development, we instantiate it with ACCS:

**Corollary 1.** For every p, q ∈ ACCS<sub>≡</sub>, p ≲<sub>MUST</sub> q iff FW(p) ≲<sub>AS</sub> FW(q).

Another application of Theorem 1 is a novel behavioural characterisation of the MUST-preorder, which fully exploits asynchrony, i.e. disregards irrelevant non-causal orders of visible actions in traces. For space reasons, we defer the discussion of this result to Appendix G.

So far, we have seen the more direct applications of Theorem 1. Before we explain two other applications, namely the coinductive characterisation of the MUST-preorder and the relation of ≲<sub>MUST</sub> with the failure refinement, we outline the proof of Theorem 1, and, in particular, the technical tools we used.
## 3.2 Proof of Theorem 1

The full proof of Theorem 1, which is given in the Appendix, as well as in the Coq development, comprises two parts: Appendix D deals with completeness, where the main aim is to show Lemma 5, and Appendix E deals with soundness. Here we outline the main tools we use to prove the soundness of the $\llcorner AS$ preorder: *Bar-induction*, which allows us to relate the standard definition of MUST with an inductive one that is more practical to use, especially in a constructive setting, and the *LTS of sets*, which is derived from the LTS of the processes.

**Bar induction: from extensional to intensional definitions** We present the inductive characterisations of $\downarrow$ and MUST in any state transition system (STS) $\langle S, \rightarrow \rangle$ that is countably branching. In practice, this condition is satisfied by most concrete LTS of programming languages, which usually contain countably many terms; this is the case for ACCS and for the asynchronous $\pi$-calculus.

Following the terminology of [28] we introduce extensional and intensional predicates associated to any decidable predicate $Q: S \to \mathbb{B}$ over an STS $\langle S, \rightarrow \rangle$, where $\mathbb{B}$ denotes the set of booleans.

**Definition 7.** The extensional predicate $ext_Q(s)$ is defined, for $s \in S$, as

$$ \forall \eta \text{ maximal execution of } S. \eta_0 = s \text{ implies } \exists n \in \mathbb{N}, Q(\eta_n) $$

The intensional predicate $int_Q$ is the inductive predicate (least fixpoint) defined by the following rules:

$$ \text{[AXIOM]} \quad \frac{Q(s)}{\text{int}_Q(s)} \qquad \text{[IND-RULE]} \quad \frac{s \rightarrow \quad \forall s'. s \rightarrow s' \text{ implies } \text{int}_Q(s')}{\text{int}_Q(s)} $$

For instance, by letting

$$ Q_1(p) \iff p \dashv\dashv Q_2(p,r) \iff \text{GOOD}(r) $$

we have by definition that

$$ p \downarrow \iff ext_{Q_1}(p) \qquad p \text{ MUST } r \iff ext_{Q_2}(p,r) \qquad (\text{ext-preds}) $$

that is the standard definitions of $\downarrow$ and MUST are extensional. Our aim now is to prove that they coincide with their intensional counterparts. The reader not familiar with this terminology may find in Appendix B an informal and hopefully intuitive explanation. Since we will use the intensional predicates in the rest of the paper a little syntactic sugar is in order, let

$$ p \downarrow_i \iff ext_{Q_1}(p) \qquad p \text{ MUST}_i r \iff ext_{Q_2}(p,r) \qquad (\text{int-preds}) $$

The proofs of soundness, i.e. that the inductively defined predicates imply the extensional ones, are by rule induction:
**Lemma 6.** For $p \in S$,

(a) $p \downarrow_i$ implies $p \downarrow$,

(b) for every $r$. $p \text{MUST}_i r$ implies $p \text{MUST} r$.

The proofs of completeness are more delicate. To the best of our knowledge, the ones about CCS [39,12] proceed by induction on the greatest number of steps necessary to arrive at termination or at a successful state. Since the STS of $\langle \text{CCS}, \xrightarrow{\tau} \rangle$ is finite branching, Kőnig's lemma guarantees that such a bound exists. This technique does not work on infinite-branching STSs, for example the one of CCS with infinite sums [14]. If we reason in classical logic, we can prove completeness without Kőnig's lemma and also over infinite-branching STSs via a proof *ad absurdum*: suppose $p \downarrow$. If $\neg(p \downarrow_i)$ no finite derivation tree exists to prove $p \downarrow_i$, and then we construct an infinite sequence of $\tau$ moves starting with $p$, thus $\neg(p \downarrow)$. Since we strive to be constructive we replace reasoning *ad absurdum* with a constructive axiom: (decidable) *bar induction*. In the rest of this section we discuss this axiom, and adapt it to our client-server setting. This requires a little terminology.

**Bar induction** The axiom we want to use is traditionally stated using natural numbers. We use the standard notations $\mathbb{N}^*$ for finite sequences of natural numbers, $\mathbb{N}^\omega$ for infinite sequences, and $\mathbb{N}^\infty = \mathbb{N}^* \cup \mathbb{N}^\omega$ for finite or infinite sequences. Remark that, in constructive logics, given $u \in \mathbb{N}^\infty$, we cannot do a case analysis on whether $u$ is finite or infinite. The set $\mathbb{N}^\infty$ equipped with the prefix order can be seen as a *tree*, denoted $T_\mathbb{N}$, in the sense of set theory: a tree is an ordered set $(A, \le)$ such that, for each $a \in A$, the set $\{b \mid b < a\}$ is well-ordered by $<$. A *path* in a tree $A$ is a maximal element in $A$. In the tree $\mathbb{N}^\infty$, each node has $\omega$ children, and the paths are exactly the infinite sequences $\mathbb{N}^\omega$.

A predicate $P \subseteq \mathbb{N}^*$ over finite words is a *bar* if every infinite sequence of natural numbers has a finite prefix in $P$. Note that a bar defines a subtree of $T_\mathbb{N}$ *extensively*, because it defines each path of the tree, as a path $u \in \mathbb{N}^\omega$ is in the tree if and only if there exists a finite prefix which is in the bar $P$.

A predicate $Q \subseteq \mathbb{N}^*$ is *hereditary* if

$$ \forall w \in \mathbb{N}^*, \text{ if } \forall n \in \mathbb{N}, w \cdot n \in Q \text{ then } w \in Q. $$

Bar induction states that the extensional predicate associated to a bar implies its *intensional* counterpart: a predicate $P_{\text{int}} \subseteq \mathbb{N}^*$ which contains $Q$ and which is hereditary.

**Axiom 8 (Decidable bar induction over $\mathbb{N}$)** Given two predicates $P_{\text{int}}$, $Q$ over $\mathbb{N}^*$, such that:

1. for all $\pi \in \mathbb{N}^\omega$, there exists $n \in \mathbb{N}$ such that $(\pi_1, \dots, \pi_n) \in Q$;

2. for all $w \in \mathbb{N}^*$, it is decidable whether $Q(w)$ or $\neg Q(w)$;

3. for all $w \in \mathbb{N}^*$, $Q(w) \Rightarrow P_{\text{int}}(w)$;

4. $P_{\text{int}}$ is hereditary;
### 3. PREORDERS BASED ON ACCEPTANCE SETS

then $P_{int}$ holds over the empty word: $P_{int}(\varepsilon)$.

Bar induction is a generalisation of the fan theorem, i.e. the constructive version of Kőnig's lemma [47, pag. 56], and states that any extensionally well-founded tree $T$ can be turned into an inductively-defined tree $t$ that realises $T$ [28,68].

Our mechanisation of bar induction principle is formulated as a Proposition that is proved using classical reasoning, since it is not provable directly in the type theory of Coq. Unfortunately, while bar induction is a constructive principle, mainstream proof assistants do not support it yet, which is why on the one hand we had to postulate it as a proof principle while on the other hand we proved it in classical logic using the Excluded Middle axiom. This principle though has a computational content, Spector bar recursion<fnref n="10" />, which, currently, cannot be used in mainstream proof assistants such as Coq. Developing a type theory with a principle of bar induction is recent and ongoing work [50,81].

**Encoding states** The version of bar induction we just outlined is not directly suitable for our purposes, as we need to reason about sequences of reductions rather than sequences of natural numbers. The solution is to encode STS states by natural numbers. This leads to the following issue: the nodes of the tree $T_N$ have a fixed arity, namely $N$, while processes have variably many reducts, including zero if they are stable. To deal with this glitch, it suffices to assume that there exists the following family of surjections:

$$F(p) : \mathbb{N} \to \{q \mid p \to q\} \qquad (8)$$

where a surjection is defined as follows.

**Definition 9.** A map $f : A \to B$ is a surjection if it has a section $g : B \to A$, that is, $f \circ g = \text{Id}_B$.

This definition implies the usual one which states the existence of an antecedent $x \in A$ for any $y \in B$, and it is equivalent to it if we assume the Axiom of Choice.

Using this map $F$ as a decoding function, any sequence of natural numbers corresponds to a path in the STS. Its subjectivity means that all paths of the LTS can be represented as such a sequence. This correspondence allows us to transport bar induction from sequences of natural numbers to executions of processes.

Note that such a family of surjections $F$ exists for ACCS processes, and generally to most programming languages, because the set $\text{Act}_\tau$ is countable, and so are processes. This leads to the following version of bar induction where words and sequences are replaced by finite and infinite executions.

**Proposition 1 (Decidable bar induction over an STS).** Let $\langle S, \to \rangle$ be an STS such that a surjection as in (8) exists. Given two predicates $Q, P_{int}$ over finite executions, if

<footnote n="10">¹⁰ https://en.wikipedia.org/wiki/Bar_recursion</footnote>
1. for all infinite execution $\eta$, there exists $n \in \mathbb{N}$ such that $(\eta_1, \dots, \eta_n) \in Q$;

2. for all finite execution $\zeta$, $Q(\zeta)$ or $\neg Q(\zeta)$ is decidable;

3. for all finite execution $\zeta$, $Q(\zeta) \Rightarrow P_{\text{int}}(\zeta)$;

4. $P_{\text{int}}$ is hereditary, as defined above except that $\zeta \cdot q$ is a partial operation defined when $\zeta$ is empty or its last state is $p$ and $p \to q$;

then $P_{\text{int}}$ holds over the empty execution: that is $P_{\text{int}}(\varepsilon)$ holds.

The last gap towards a useful principle is the requirement that every state in our STS has an outgoing transition. This condition is necessary to ensure the existence of the surjection in Equation (8). To ensure this requirement given any countably-branching STS, we enrich it by adding a sink state, which (a) is only reachable from stable states of the original STS, and (b) loops. This is a typical technique, see for instance [71, pag. 17].

**Definition 10.** Define $\text{Sink}(S, \to) := \langle S \cup \{\top\}, \to^{\top} \rangle$, where $\to^{\top}$ is defined inductively as follows:

$$p \to q \implies p \to^{\top} q \qquad p \leftrightarrow \implies p \to^{\top} \top \qquad \top \to^{\top} \top$$

A maximal execution of $\text{Sink}(S, \to)$ is always infinite, and it corresponds (in classical logic) to either an infinite execution of $S$ or a maximal execution of $S$ followed by infinitely many $\top$. We finally prove the converse of Lemma 6.

**Proposition 2.** Given a countably branching STS $\langle S, \to \rangle$, and a decidable predicate $Q$ on $S$, we have that, for all $s \in S$, $\text{ext}_Q(s)$ implies $\text{int}_Q(s)$.

Now we thus obtain completeness of the intensional predicates.

**Corollary 2.** For every $p \in A$ we have

1. $p \downarrow$ if and only if $p \downarrow_i$, and

2. for every $r$ we have that $p_{\text{MUST}} r$ if and only if $p_{\text{MUST}_i} r$.

*Proof.* Direct consequence of Proposition 2, and Equation (ext-preds) and Equation (int-preds) above.

As we have outlined why Corollary 2 is true, from now on we use $\downarrow_i$ and $\text{MUST}_i$ instead of $\downarrow$ and $\text{MUST}$. In Appendix B.2 we prove the properties of these predicates, that we use in the rest of the paper.

**The LTS of sets** Recall that soundness of $\ll_{\text{AS}}$ means that $\ll_{\text{AS}} \subseteq \ll_{\text{MUST}}$. The naïve reasoning does not work. Fix two servers $p$ and $q$ such that $p \ll_{\text{AS}} q$. We need to prove that for every client $r$, if $p_{\text{MUST}_i} r$ then $p_{\text{MUST}_i} r$. Rule induction on the predicate $p_{\text{MUST}_i} r$ fails, as demonstrated by the following example.

*Example 6.* Consider the two servers $p = \tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c})$ and $q = \bar{a} \parallel (\tau.\bar{b} + \tau.\bar{c})$ of Equation (6). Fix a client $r$ such that $p_{\text{MUST}_i} r$. Rule induction yields the following inductive hypothesis:
### 3. PREORDERS BASED ON ACCEPTANCE SETS

$$ \forall p', q'. \ p \llbracket r \xrightarrow{\tau} p' \rrbracket r' \wedge p' \preceq_{AS} q' \Rightarrow q' \ \mathit{MUST}_i r'. $$

In the proof of $q \ \mathit{MUST}_i \ r$ we have to consider the case where there is a communication between $q$ and $r$ such that, for instance, $q \xrightarrow{\bar{a}} \tau \cdot \bar{b} + \tau \cdot \bar{c}$ and $r \xrightarrow{a} r'$. In that case, we need to show that $\tau \cdot \bar{b} + \tau \cdot \bar{c} \ \mathit{MUST}_i \ r'$. Ideally, we would like to use the inductive hypothesis. This requires us to exhibit a $p'$ such that $p \llbracket r \xrightarrow{\tau} p' \rrbracket r'$ and $p' \preceq_{acc} \tau \cdot \bar{b} + \tau \cdot \bar{c}$. However, note that there is no way to derive $p \llbracket r \xrightarrow{\tau} p' \rrbracket r'$, because $p \xrightarrow{\bar{a}}$. The inductive hypothesis thus cannot be applied, and the naïve proof does not go through. □

This example suggests that defining an auxiliary predicate $\mathit{MUST}_{aux}$ in some sense equivalent to $\mathit{MUST}_i$, but that uses explicitly weak outputs of servers, should be enough to prove that $\preceq_{AS}$ is sound with respect to $\preceq_{\mathit{MUST}_i}$. Unfortunately, though, there is an additional nuisance to tackle: server nondeterminism.

**Example 7.** Assume that we defined the predicate $\mathit{MUST}_i$ using weak transitions on the server side. Recall the argument put forward in the previous example. The inductive hypothesis now becomes the following:

For every $p', q', \mu$ such that $p \stackrel{\mu}{\Rightarrow} p'$ and $r \stackrel{\mu}{\Rightarrow} r'$, $p' \preceq_{AS} q'$ implies $q' \ \mathit{MUST}_i \ r'$.

To use the inductive hypothesis we have to choose a $p'$ such that $p \stackrel{\bar{a}}{\Rightarrow} p'$ and $p' \preceq_{AS} \tau \cdot \bar{b} + \tau \cdot \bar{c}$. This is still not enough for the entire proof to go through, because (modulo further $\tau$-moves) the particular $p'$ we pick has to be related also to either $\bar{b}$ or $\bar{c}$. It is not possible to find such a $p'$, because the two possible candidates are either $\bar{b}$ or $\bar{c}$; neither of which can satisfy $p' \preceq_{AS} \tau \cdot \bar{b} + \tau \cdot \bar{c}$, as the right-hand side has not committed to a branch yet.

If instead of a single state $p$ in the novel definition of $\mathit{MUST}_i$ we used a set of states and a suitable transition relation, the choice of either $\bar{b}$ or $\bar{c}$ would be suitably delayed. It suffices for instance to have the following states and transitions: $\{p\} \stackrel{\bar{a}}{\Rightarrow} \{\bar{b}, \bar{c}\}$. □

Now that we have motivated the main intuitions behind the definition of our novel auxiliary predicate $\mathit{MUST}_{aux}$, we proceed with the formal definitions.

**Definition 11 (LTS of sets).** Let $\mathcal{P}^+(Z)$ be the set of non-empty parts of $Z$. For any LTS $\langle A, L, \rightarrow \rangle$, $X \in \mathcal{P}^+(A)$ and $\alpha \in L$, we define the sets

$$ D(\alpha, X) = \{p' \mid \exists p \in X. p \xrightarrow{\alpha} p'\}, \quad WD(\alpha, X) = \{p' \mid \exists p \in X. p \stackrel{\alpha}{\Rightarrow} p'\}. $$

We construct the LTS $\langle \mathcal{P}^+(A), \mathit{Act}_\tau, \rightarrow \rangle$ by letting $X \stackrel{\alpha}{\Rightarrow} D(\alpha, X)$ whenever $D(\alpha, X) \neq \emptyset$. Similarly, we have $X \stackrel{\alpha}{\Rightarrow} WD(\alpha, X)$ whenever $WD(\alpha, X) \neq \emptyset$.

Intuitively, this definition lifts the standard notion of state derivative to sets of states. This construction is standard [41,19,20] and goes back to the determination of nondeterministic automata.

Let $\mathit{MUST}_{aux}$ be defined via the rules in Figure 7. This predicate lets us reason on $\mathit{MUST}_i$ via sets of servers, in the following sense:
<figure><img src="image_11.png" /><figcaption>Fig. 7. Rules to define inductively the predicate MUST<sub>aux</sub>.</figcaption></figure>

**Lemma 7.** For every LTSs $\mathcal{L}_A$, $\mathcal{L}_B$ and every set of servers $X \in \mathcal{P}^+(A)$, we have that $X \text{ MUST}_{\text{aux}} r$ if and only if for every $p \in X$. $p \text{ MUST}_i r$.

The LTS of sets has two important applications in this paper: first, it is used to define the MUST<sub>aux</sub> relation, on which we rely to prove the soundness of the characterisation (see Appendix E). Additionally, it is used in the definition of the coinductive characterisation, which is the topic of the next section.

### 3.3 The action-based coinductive characterisation

We conclude this section by introducing a characterisation of the MUST-preorder that is more practical than $\leq_{AS}$, as it allows one to use the usual coinductive techniques. In addition, in the asynchronous case where processes are enhanced with forwarding, being able to use the coinductive proof method allows us to deal easily with the additional transitions due to forwarding. As a demonstration, we use this preorder to prove the code hoisting refinement shown in (6).

First, we recall the definition of this alternative preorder, which, like the other ones, is the same as in the synchronous case [2,72,16].

**Definition 12 (Coinductive preorder).** For all image-finite LTSs $\mathcal{L}_A$, $\mathcal{L}_B$ and all $X \in \mathcal{P}^+(A)$, $q \in B$, we let the coinductive preorder $\leq_{co}$ be defined as the greatest relation such that whenever $X \leq_{co} q$, the following requirements hold:

1. $X \downarrow$ implies $q \downarrow$,

2. For each $q'$ such that $q \xrightarrow{\tau} q'$, we have that $X \leq_{co} q'$,

3. $X \downarrow$ and $q \xrightarrow{\tau} \tau$ imply that there exist $p \in X$ and $p' \in A$ such that $p \implies p' \xrightarrow{\tau} \tau$ and $R(p') \subseteq R(q)$,

4. For any $\mu \in \text{Act}$, if $X \Downarrow \mu$, then for every $X'$ and $q'$ such that $X \xrightarrow{\mu} X'$ and $q \xrightarrow{\mu} q'$, we have that $X' \leq_{co} q'$.

This preorder characterises $\sqsubseteq_{MUST}$ when the set $X$ of servers is a singleton.

**Theorem 2.** For every image-finite LTS $\mathcal{L}_A$, $\mathcal{L}_B \in \text{FDB}$, every $p \in A$ and $q \in B$, we have that $p \sqsubseteq_{MUST} q$ if and only if $\{\text{FW}(p)\} \leq_{co} \text{FW}(q)$.
## 4. PREORDERS BASED ON MUST-SETS AND FAILURE REFINEMENT

The idea of the proof is to establish that the coinductive preorder characterises a version of the MUST-preorder that also has a set of servers on its LHS, and is defined as follows:

$$X \sqsubseteq_{\text{MUST}}^{\text{Set}} q \iff \forall t. (\forall p \in X, p \text{ MUST}_i t) \text{ implies } q \text{ MUST}_i t.$$

Observe that Definition 12 is based on single actions, instead of traces like $\leq_{AS}$, thus it gives us a practical proof method. To make this point, we now prove the code hoisting refinement (6). According to Theorem 2, it suffices to prove:

$$\{\tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c})\} \leq_{\text{co}} \bar{a} \parallel (\tau.\bar{b} + \tau.\bar{c}) \quad (9)$$

As for proofs by induction, when using coinduction it is helpful to prove a more general statement, which yields a useful *coinductive hypothesis*. This vocabulary corresponds to the proof theoretic point of view of coinduction, which matches how Coq implements coinductive proofs using cofix. In practice, the prover can use the coinductive hypothesis after the predicate defined coinductively has been unfolded at least once. In the set-theoretic setting used in Definition 12, this corresponds to choosing a relation $R$ that is closed under the operations given in the definition. This is borne out by Lemma 47 in Appendix F.

# 4 Preorders based on must-sets and failure refinement

We now establish the second *standard* characterisation of the MUST-preorder, defined using MUST-sets, again thanks to Theorem 1. As an application, we relate the *failure refinement* used by the CSP community to the MUST-preorder.

We begin by defining formally the $\leq_{MS}$ preorder, and we relate it to the MUST-preorder. For every $X \subseteq_{fin} \text{Act}$, that is for every finite set of visible actions, with a slight abuse of notation we write $p \text{ MUST } X$ whenever $p \stackrel{e}{\Rightarrow} p'$ implies that $p' \stackrel{\mu}{\Rightarrow} p$ for some $\mu \in X$, and we say that $X$ is a MUST-set of $p$. Let $(p \text{ after } s, \rightarrow) = \{p' | p \stackrel{s}{\Rightarrow} p'\}$. For every $\mathcal{L}_A, \mathcal{L}_B$ and $p \in A, q \in B$, let $p \leq_M q$ whenever $\forall s \in \text{Act}^* \text{ we have that } p \downarrow s$ implies that $(\forall X \subseteq_{fin} \text{Act} \text{ if } (p \text{ after } s, \rightarrow_A) \text{ MUST } X \text{ then } (q \text{ after } s, \rightarrow_B) \text{ MUST } X)$.

**Definition 13.** For all $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$ and servers $p \in A$ and $q \in B$, we let $p \leq_{MS} q$ whenever $p \leq_{cnv} q \wedge p \leq_M q$.

**Lemma 8.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$. For all $p \in A$ and $q \in B$ such that $\text{FW}(p) \leq_{cnv} \text{FW}(q)$, we have that $\text{FW}(p) \leq_M \text{FW}(q)$ if and only if $\text{FW}(p) \leq_{acc} \text{FW}(q)$.

As a direct consequence, we obtain the following result.

**Theorem 3.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$. For all $p \in A$ and $q \in B$, we have that $p \sqsubseteq_{\text{MUST}} q$ if and only if $\text{FW}(p) \leq_{MS} \text{FW}(q)$.
*Failure refinement* MUST-sets have been used mainly by De Nicola and collaborators, for instance in [44,23], and are closely related to the failure refinement proposed in [33] by Hoare, Brookes and Roscoe for TCSP (the process algebra based on Hoare's language CSP [63,31]). Following [33], a *failure* of a process *p* is a pair (*s*, *X*) such that *p* ⇝*s* *p'* and *p'* ↛*µ* for all *µ* ∈ *X*. Then, failure refinement is defined by letting *p* ≲*fail* *q* whenever the failures of *q* are also failures of *p*. This refinement was designed to give a denotational semantics to processes, and mechanisations in Isabelle/HOL have been developed to ensure that the refinement is well defined [91,11]. Both Hennessy [55, pag. 260] and [37] highlight that the failure model can be justified operationally via the MUST testing equivalence: it is folklore dating back to [43, Section 4] that failure equivalence and ≁<sub>MUST</sub> coincide. Thanks to Theorem 3 we conclude that in fact ⊑<sub>MUST</sub> coincides with the *failure divergence refinement* [92], that is, the intersection of ≲<sub>fail</sub> and ≲<sub>cnv</sub>.

**Corollary 3.** Let $\mathcal{L}_A, \mathcal{L}_B \in \mathbf{FDB}$. For every $p \in A$ and $q \in B$, we have that $p \preceq_{\mathbf{MUST}} q$ if and only if $\mathrm{FW}(p) \preceq_{\mathrm{cnv}} \mathrm{FW}(q)$ and $\mathrm{FW}(p) \leq_{\mathrm{fail}} \mathrm{FW}(q)$.

Thanks to Corollary 4, we obtain ≲<sub>MS</sub><sup>NF</sup>, the analogous of Definition 16 based on normal forms, and we prove that it characterises ⊑<sub>MUST</sub>.

**5 Related work**

Here we discuss in detail the works more closely related to the results of this paper. Further discussion on related work may be found in Appendix A.

The first investigation on the MUST-preorder in an asynchronous setting was put forth by [38]. While their very clear examples shed light on the preorder, their alternative preorder (Definition 6 in that paper) is more complicated than necessary: it uses the standard LTS of TACCS, its lifting to an LTS with forwarding, and two somewhat ad-hoc notions: a predicate $\stackrel{I}{\rightleftharpoons}$ and a condition on multisets of inputs. Moreover that preorder is not complete because of a glitch in the treatment of divergence. The details of the counter-example we found to that completeness result are given in Appendix I.

In [57] Hennessy outlines how to adapt the approach of [38] to a typed asynchronous π-calculus. While the LTS with forwarding is replaced by a Context LTS, the predicates to define the alternative preorder are essentially the same as those used in the preceding work with Castellani. Acceptance sets are given in Definition 3.19 there, and the predicate $\stackrel{I}{\rightleftharpoons}$ is denoted $\searrow$, while the generalised acceptance sets of [38] are given in Definition 3.20. Owing to the glitch in the completeness of [38], it is not clear that Theorem 3.28 of [57] is correct either.

Also the authors of [23] consider the MUST-preorder in ACCS. There is a major difference between their approach and ours. When studying theories for asynchronous programs, one can either

(1) keep the definitions used for synchronous programs, and enhance the LTS with forwarders; or

(2) adapt the definitions, and keep the standard LTS.
In the first case, the complexity is moved into the LTS, which becomes infinite-
branching and infinite-state. In the second case, the complexity is moved into
the definitions used to reason on the LTS (i.e. in the meta-language), and in
particular in the definition of the alternative preorder, which deviates from the
standard one. The authors of [23] follow the second approach. This essentially
explains why they employ the standard LTS of CCS and to tackle asynchrony
they reason on traces via (1) a preorder $\preceq$ (Table 2 of that paper) that defines
on *input* actions the phenomena due to asynchrony; and (2) a rather technical
operation on traces, namely $s \ominus s' = (\{s\}_i \setminus \{s'\}_i) \setminus (\{s\}_o \setminus \{s'\}_o)$. We favour
instead the approach in (1), for it helps achieve a modular mechanisation.

The authors of [45] give yet another account of the MUST-preorder. Even
though non-blocking outputs can be written in their calculus, they use a left-
merge operator that allows writing blocking outputs. The contexts that they use
to prove the completeness of their alternative preorder use such blocking outputs,
consequently their arguments need not tackle the asymmetric treatment of input
and output actions. This explains why they can use smoothly a standard LTS,
while [38] and [23] have to resort to more complicated structures.

Theorem 5.3 of the PhD thesis by [94] states an alternative characterisation
of the MUST-preorder, but it is given with no proof. The alternative preorder
given in Definition 5.8 of that thesis turns out to be a mix of the ones by [38]
and [23]. In particular, the definition of the alternative preorder relies on the
LTS with forwarding, there denoted $\rightarrow_A$ (Point 1. in Definition 5.1 defines
exactly the input transitions that forward messages into the global buffer). The
condition that compares convergence of processes is the same as in [38], while
server actions are compared using MUST-sets, and not acceptance sets. In fact,
Definition 5.7 there is titled "acceptance sets" but it actually defines MUST-sets.

**6 Conclusion**

In this paper we have shown that the standard characterisations of the MUST-
preorder by De Nicola and Hennessy [43,55] are sound and complete also in an
asynchronous setting, provided servers are enhanced with the forwarding ability.
Lemma 2 shows that this lifting is always possible. We have also shown that
the standard coinductive characterisation carries over to the asynchronous set-
ting. Our results are supported by the first mechanisation of the MUST-preorder,
and increase proof (i.e. code) factorisation and reusability since the alternative
preorders do not need to be changed when shifting between synchronous and
asynchronous semantics: it is enough to parameterise the proofs on the set of
non-blocking actions. Corollary 3 states that MUST-preorder and failure refine-
ment essentially coincide. This might spur further interest in the mechanisations
of failure refinement, carried out so far in Isabelle/HOL [91,11], possibly opening
up opportunities of joint efforts for automated checking.

*Proof method for* MUST-*preorder* Theorems 1, 2 and 3 endow researchers in programming languages for message-passing software with a proof method for $\sqsubseteq_{\mathrm{MUST}}$,
namely: to define for their calculi an LTS that enjoys the axioms of output-
buffered agents with feedback. An example of this approach is Corollary 1.

*Live programs have barred trees* We argued that a proof of *p<sub>MUST</sub>r* is a proof of liveness (of the client). This paper is thus de facto an example that proving liveness amounts to prove that a computational tree has a bar (identified by the predicate *GOOD*), and hence bar induction is a natural way to reason constructively on liveness-preserving manipulations on programs. While this fact seems to be by and large unexploited by the PL community, we believe that it may be of interest to practitioners reasoning on liveness properties in theorem provers in particular, and to the PL community at large.

*Mechanisation* Boreale and Gadducci [21] remark that the MUST-preorder lacks a tractable proof method. In constrast, we argue that our contributions, in particular the coinductive characterisation (Theorem 2), being fully mechanised in Coq, let practitioners pursue non-trivial results about testing preorders for real-world programming languages. To make this point, we have proved a form of code-hoisting using this characterisation. Our mechanisation lowers the barrier to entry for researchers versed into theorem provers and wishing to use testing preorders; adds to the toolkit of Coq users an alternative to the well-known (and already mechanised) bisimulation equivalence [78]; and provides a starting point for researchers willing to study testing preorders and analogous refinements within type theory. Researchers working on testing preorders may benefit from it, as there are analogies between reasoning techniques for MAY, MUST, COMPLIANCE, SHOULD, and FAIR testing. For instance Baldan et al. show with pen and paper that a technique similar to forwarding works to characterise the MAY-preorder [8].

*Future work* Thanks to Theorems 1, 2 and 3 we can now set out to (1) devise an axiomatisation of $\sqsubseteq_{MUST}$ for asynchronous calculi, as done in [59,22,55,56] for synchronous ones; (2) study for which asynchronous calculi $\sqsubseteq_{MUST}$ is a pre-congruence; (3) machine-check semantic models of subtyping for session types [16]; (4) study the decidability of $\sqsubseteq_{MUST}$.

More in general, given the practical relevance of asynchronous communica-
tion, it seems crucial not only to adapt the large body of theory for synchronous
communication to the asynchronous setting but also to resort to machine sup-
ported reasoning to do it. This paper is meant to be a step in this direction.

*Data availability* The mechanised proofs have been archived on Zenodo[13].

***Acknowledgments.*** We thank the anonymous reviewers for their helpful com-
ments, and Roberto Amadio for useful remarks. The first author would like to
acknowledge his “N+1 honoris causa” Pierre-Evariste Dagand for the systematic
and useful feedback, Guillaume Geoffroy for suggesting the use of bar induction,
and Hugo Herbelin for discussions on the topic. This work has received funding
from the European Research Council (ERC) under the European Union’s Hori-
zon 2020 research and innovation programme (grant agreement No. 101003349).
References

1. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Ad-ventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. **3**(POPL), 52:1–52:29 (2019). https://doi.org/10.1145/3290365, https://doi.org/10.1145/3290365

2. Aceto, L., Hennessy, M.: Termination, Deadlock, and Divergence. J. ACM **39**(1), 147–187 (1992). https://doi.org/10.1145/147508.147527, https://doi.org/10.1145/147508.147527

3. Affeldt, R., Kobayashi, N.: A Coq Library for Verification of Concurrent Programs. In: Schürmann, C. (ed.) Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, LFM@IJCAR 2004. Cork, Ireland, July 5, 2004. Electronic Notes in Theoretical Computer Science, vol. 199, pp. 17–32. Elsevier (2004). https://doi.org/10.1016/J.ENTCS.2007.11.010, https://doi.org/10.1016/j.entcs.2007.11.010

4. Amadio, R.M., Castellani, I., Sangiorgi, D.: On Bisimulations for the Asynchronous pi-calculus. In: Montanari, U., Sassone, V. (eds.) Proceedings CONCUR 96, Pisa. Lecture Notes in Computer Science, vol. 1119, pp. 147–162. Springer Verlag (1996)

5. Amadio, R.M., Castellani, I., Sangiorgi, D.: On Bisimulations for the Asynchronous pi-calculus. Theoretical Computer Science **195**, 291–324 (1998)

6. Athalye, A.: CoqIOA: A Formalization of IO Automata in the Coq Proof Assistant. Master's thesis, Massachusetts Institute of Technology (Jun 2017)

7. Aubert, C., Varacca, D.: Processes against tests: On defining contextual equiva-lences. J. Log. Algebraic Methods Program. **129**, 100799 (2022). https://doi.org/10.1016/J.JLAMP.2022.100799, https://doi.org/10.1016/j.jlamp.2022.100799

8. Baldan, P., Bonchi, F., Gadducci, F., Monreale, G.V.: Asynchronous Traces and Open Petri Nets. In: Bodei, C., Ferrari, G., Priami, C. (eds.) Programming Lan-guages with Applications to Biology and Security - Essays Dedicated to Pier-paolo Degano on the Occasion of His 65th Birthday. Lecture Notes in Com-puter Science, vol. 9465, pp. 86–102. Springer (2015). https://doi.org/10.1007/978-3-319-25527-9_8, https://doi.org/10.1007/978-3-319-25527-9_8

9. Barbanera, F., de'Liguoro, U.: Two notions of sub-behaviour for session-based client/server systems. In: Kutsia, T., Schreiner, W., Fernández, M. (eds.) Pro-ceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria. pp. 155–164. ACM (2010). https://doi.org/10.1145/1836089.1836109, https://doi.org/10.1145/1836089.1836109

10. Barendregt, H., Manzonetto, G.: A Lambda Calculus Satellite. College Publications (2022), https://www.collegepublications.co.uk/logic/mlf/?00035, chapter 11

11. Baxter, J., Ribeiro, P., Cavalcanti, A.: Sound reasoning in tock-CSP. Acta Informatica **59**(1), 125–162 (2022). https://doi.org/10.1007/s00236-020-00394-3, https://doi.org/10.1007/s00236-020-00394-3

12. Bernardi, G.: Behavioural equivalences for Web services. Ph.D. thesis, Trinity College Dublin (2013), http://www.tara.tcd.ie/handle/2262/77595

13. Bernardi, G., Castellani, I., Laforgue, P., Stefanesco, L.: Artifact for constructive characterisations of the must-preorder for asynchrony (jan 2025). https://doi.org/10.5281/zenodo.14617145, https://doi.org/10.5281/zenodo.105281/zenodo.14617145
14. Bernardi, G., Hennessy, M.: Mutually Testing Processes. Log. Methods Comput. Sci. 11(2) (2015). https://doi.org/10.2168/LMCS-11(2:1)2015, https://doi.org/10.2168/LMCS-11(2:1)2015

15. Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types. Log. Methods Comput. Sci. 12(2) (2016). https://doi.org/10.2168/LMCS-12(2:10)2016, https://doi.org/10.2168/LMCS-12(2:10)2016

16. Bernardi, G.T., Hennessy, M.: Modelling session types using contracts. Math. Struct. Comput. Sci. 26(3), 510–560 (2016). https://doi.org/10.1017/S0960129514000243, https://doi.org/10.1017/S0960129514000243

17. Berry, G., Boudol, G.: The Chemical Abstract Machine. Theor. Comput. Sci. 96(1), 217–248 (1992). https://doi.org/10.1016/0304-3975(92)90185-I, https://doi.org/10.1016/0304-3975(92)90185-I

18. Bizjak, A., Birkedal, L., Miculan, M.: A model of countable nondeterminism in guarded type theory. In: Dowek, G. (ed.) Rewriting and Typed Lambda Calculi. pp. 108–123. Springer International Publishing, Cham (2014)

19. Bonchi, F., Caltais, G., Pous, D., Silva, A.: Brzozowski's and Up-To Algorithms for Must Testing. In: Shan, C. (ed.) Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8301, pp. 1–16. Springer (2013). https://doi.org/10.1007/978-3-319-03542-0_1, https://doi.org/10.1007/978-3-319-03542-0_1

20. Bonchi, F., Sokolova, A., Vignudelli, V.: The Theory of Traces for Systems with Nondeterminism, Probability, and Termination. Log. Methods Comput. Sci. 18(2) (2022). https://doi.org/10.46298/LMCS-18(2:21)2022, https://doi.org/10.46298/lmcs-18(2:21)2022

21. Boreale, M., Gadducci, F.: Processes as formal power series: A coinductive approach to denotational semantics. Theor. Comput. Sci. (2006). https://doi.org/10.1016/j.tcs.2006.05.030, https://doi.org/10.1016/j.tcs.2006.05.030

22. Boreale, M., Nicola, R.D.: Testing Equivalence for Mobile Processes. Inf. Comput. 120(2), 279–303 (1995). https://doi.org/10.1006/inco.1995.1114, https://doi.org/10.1006/inco.1995.1114

23. Boreale, M., Nicola, R.D., Pugliese, R.: Trace and Testing Equivalence on Asynchronous Processes. Inf. Comput. 172(2), 139–164 (2002). https://doi.org/10.1006/inco.2001.3080, https://doi.org/10.1006/inco.2001.3080

24. Boudol, G.: Asynchrony and the Pi-calculus. Research Report RR-1702, INRIA (1992), https://hal.inria.fr/inria-00076939

25. Boudol, G.: The pi-Calculus in Direct Style. High. Order Symb. Comput. 11(2), 177–208 (1998). https://doi.org/10.1023/A:1010064516533, https://doi.org/10.1023/A:1010064516533

26. Boudol, G., Lavatelli, C.: Full Abstraction for Lambda Calculus with Resources and Convergence Testing. In: Kirchner, H. (ed.) Trees in Algebra and Programming - CAAP’96, 21st International Colloquium, Linköping, Sweden, April, 22-24, 1996, Proceedings. Lecture Notes in Computer Science, vol. 1059, pp. 302–316. Springer (1996). https://doi.org/10.1007/3-540-61064-2_45, https://doi.org/10.1007/3-540-61064-2_45

27. Bravetti, M., Lange, J., Zavattaro, G.: Fair Refinement for Asynchronous Session Types. In: FOSSACS (2021)

28. Brede, N., Herbelin, H.: On the logical structure of choice and bar induction principles. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1–13. IEEE
6. CONCLUSION

(2021). https://doi.org/10.1109/LICS52264.2021.9470523, https://doi.org/10.1109/LICS52264.2021.9470523

29. Breuvart, F., Manzonetto, G., Polonsky, A., Ruoppolo, D.: New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. In: Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. LIPIcs, vol. 52, pp. 15:1–15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPIcs.FSCD.2016.15, https://doi.org/10.4230/LIPIcs.FSCD.2016.15

30. Breuvart, F., Manzonetto, G., Ruoppolo, D.: Relational Graph Models at Work. Log. Methods Comput. Sci. 14(3) (2018). https://doi.org/10.23638/LMCS-14(3:2)2018, https://doi.org/10.23638/LMCS-14(3:2)2018

31. Brookes, S.D.: On the Relationship of CCS and CSP. In: Díaz, J. (ed.) Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18-22, 1983, Proceedings. Lecture Notes in Computer Science, vol. 154, pp. 83–96. Springer (1983). https://doi.org/10.1007/BFb0036899, https://doi.org/10.1007/BFb0036899

32. Brookes, S.D.: Deconstructing CCS and CSP Asynchronous Communication, Fairness, and Full Abstraction (2016), http://www.cs.cmu.edu/afs/cs/Web/People/brookes/papers/mfps16paper.pdf

33. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. J. ACM 31(3), 560–599 (1984). https://doi.org/10.1145/828.833, https://doi.org/10.1145/828.833

34. Caruana, C.: Compositional Reasoning about Actor Based Systems. Master thesis, University of Malta (2019)

35. Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: Porto, A., López-Fraguas, F.J. (eds.) Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pp. 219–230. ACM (2009). https://doi.org/10.1145/1599410.1599437, https://doi.org/10.1145/1599410.1599437

36. Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for Web services. ACM Trans. Program. Lang. Syst. 31(5), 19:1–19:61 (2009). https://doi.org/10.1145/1538917.1538920, https://doi.org/10.1145/1538917.1538920

37. Castellan, S., Clairambault, P., Winskel, G.: The Mays and Musts of Concurrent Strategies. In: Palmigiano, A., Sadrzadeh, M. (eds.) Samson Abramsky on Logic and Structure in Computer Science and Beyond. pp. 327–361. Springer International Publishing, Cham (2023). https://doi.org/10.1007/978-3-031-24117-8_9, https://doi.org/10.1007/978-3-031-24117-8_9

38. Castellani, I., Hennessy, M.: Testing Theories for Asynchronous Languages. In: Arvind, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1530, pp. 90–101. Springer (1998). https://doi.org/10.1007/978-3-540-49382-2_9, https://doi.org/10.1007/978-3-540-49382-2_9

39. Cerone, A., Hennessy, M.: Process Behaviour: Formulae vs. Tests. Tech. rep., Trinity College Dublin, School of Computer Science and Statistics (2010)

40. Cleaveland, R., Zwarico, A.E.: A Theory of Testing for Real-Time. In: LICS (1991)

41. Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings. Lecture
Notes in Computer Science, vol. 407, pp. 11–23. Springer (1989). https://doi.org/10.1007/3-540-52148-8_2, https://doi.org/10.1007/3-540-52148-8_2

42. De Nicola, R., Ferrari, G., Pugliese, R.: Klaim: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering 24(5), 315–330 (1998). https://doi.org/10.1109/32.685256

43. De Nicola, R., Hennessy, M.: Testing Equivalences for Processes. Theor. Comput. Sci. 34, 83–133 (1984). https://doi.org/10.1016/0304-3975(84)90113-0, https://doi.org/10.1016/0304-3975(84)90113-0

44. De Nicola, R., Melgratti, H.C.: Multiparty testing preorders. Log. Methods Comput. Sci. 19(1) (2023). https://doi.org/10.46298/lmcs-19(1:1)2023, https://doi.org/10.46298/lmcs-19(1:1)2023

45. De Nicola, R., Pugliese, R.: Linda-based applicative and imperative process algebras. Theor. Comput. Sci. 238(1-2), 389–437 (2000). https://doi.org/10.1016/S0304-3975(99)00339-4, https://doi.org/10.1016/S0304-3975(99)00339-4

46. Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22(4-5), 477–528 (2012). https://doi.org/10.1017/S095679681200024X, https://doi.org/10.1017/S095679681200024X

47. Dummett, M.: Elements of Intuitionism. Oxford logic guides, Clarendon Press (2000), https://books.google.fr/books?id=JVFzknbGBVAC

48. Fournet, C., Gonthier, G.: The join calculus: A language for distributed mobile programming. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) Applied Semantics. pp. 268–332. Springer Berlin Heidelberg, Berlin, Heidelberg (2002)

49. Francalanza, A.: A theory of monitors. Inf. Comput. 281, 104704 (2021). https://doi.org/10.1016/j.ic.2021.104704, https://doi.org/10.1016/j.ic.2021.104704

50. Fridlender, D.: An Interpretation of the Fan Theorem in Type Theory. In: TYPES (1998), https://doi.org/10.1007/3-540-48167-2_7

51. Frumin, D., Krebbers, R., Birkedal, L.: ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 442–451. ACM (2018). https://doi.org/10.1145/3209108.3209174, https://doi.org/10.1145/3209108.3209174

52. Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2-3), 191–225 (2005). https://doi.org/10.1007/s00236-005-0177-z, https://doi.org/10.1007/s00236-005-0177-z

53. van Glaabeek, R.: Just Testing. In: Kupferman, O., Sobocinski, P. (eds.) Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13992, pp. 498–519. Springer (2023). https://doi.org/10.1007/978-3-031-30829-1_24, https://doi.org/10.1007/978-3-031-30829-1_24

54. Hennessy, M.: Acceptance Trees. J. ACM 32(4), 896–928 (1985). https://doi.org/10.1145/4221.4249, https://doi.org/10.1145/4221.4249

55. Hennessy, M.: Algebraic theory of processes. MIT Press series in the foundations of computing, MIT Press (1988)

56. Hennessy, M.: A fully abstract denotational semantics for the pi-calculus. Theor. Comput. Sci. 278(1-2), 53–89 (2002). https://doi.org/10.1016/S0304-3975(00)00331-5, https://doi.org/10.1016/S0304-3975(00)00331-5
57. Hennessy, M.: The security pi-calculus and non-interference. J. Log. Algebraic Methods Program. (2005). https://doi.org/10.1016/j.jlap.2004.01.003, https://doi.org/10.1016/j.jlap.2004.01.003

58. Hennessy, M.: A distributed Pi-calculus. Cambridge University Press (2007)

59. Hennessy, M., Ingólfsdóttir, A.: Communicating Processes with Value-passing and Assignments. Formal Aspects Comput. 5(5), 432–466 (1993). https://doi.org/10.1007/BF01212486, https://doi.org/10.1007/BF01212486

60. Hennessy, M., Plotkin, G.D.: A Term Model for CCS. In: Dembinski, P. (ed.) Mathematical Foundations of Computer Science 1980 (MFCS’80), Proceedings of the 9th Symposium, Rydzyna, Poland, September 1-5, 1980. Lecture Notes in Computer Science, vol. 88, pp. 261–274. Springer (1980). https://doi.org/10.1007/BFb0022510, https://doi.org/10.1007/BFb0022510

61. Hennessy, M., Riely, J.: Information flow vs. resource access in the asynchronous pi-calculus. ACM Trans. Program. Lang. Syst. 24(5), 566–591 (2002). https://doi.org/10.1145/570886.570890, https://doi.org/10.1145/570886.570890

62. Hirschkoff, D., Jaber, G., Prebet, E.: Deciding Contextual Equivalence of $\nu$-Calculus with Effectful Contexts. In: Kupferman, O., Sobocinski, P. (eds.) Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13992, pp. 24–45. Springer (2023). https://doi.org/10.1007/978-3-031-30829-1_2, https://doi.org/10.1007/978-3-031-30829-1_2

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

64. Honda, K., Tokoro, M.: An Object Calculus for Asynchronous Communication. In: America, P. (ed.) ECOOP’91 European Conference on Object-Oriented Programming, Geneva, Switzerland, July 15-19, 1991, Proceedings. Lecture Notes in Computer Science, vol. 512, pp. 133–147. Springer (1991). https://doi.org/10.1007/BFb0057019, https://doi.org/10.1007/BFb0057019

65. Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: Necula, G.C., Wadler, P. (eds.) POPL. pp. 273–284. ACM Press, New York (2008)

66. Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. Journal of ACM 63(1), 9:1–9:67 (2016)

67. Intrigila, B., Manzonetto, G., Polonsky, A.: Degrees of extensionality in the theory of Böhm trees and Sallé’s conjecture. Log. Methods Comput. Sci. 15(1) (2019). https://doi.org/10.23638/LMCS-15(1:6)2019, https://doi.org/10.23638/LMCS-15(1:6)2019

68. Kleene, S.C., Vesley, R.E.: The Foundations of Intuitionistic Mathematics: Especially in Relation to Recursive Functions. Studies in logic and the foundations of mathematics, North-Holland Publishing Company (1965), https://books.google.fr/books?id=2EHVxQEACAAJ

69. Koutavas, V., Tzevelekos, N.: Fully Abstract Normal Form Bisimulation for Call-by-Value PCF. In: LICS (2023)

70. Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 205–217. ACM (2017). https://doi.org/10.1145/3009837.3009855, https://doi.org/10.1145/3009837.3009855
71. Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002), http://research.microsoft.com/users/lamport/tla/book.html

72. Laneve, C., Padovani, L.: The Must Preorder Revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4703, pp. 212-225. Springer (2007). https://doi.org/10.1007/978-3-540-74407-8_15, https://doi.org/10.1007/978-3-540-74407-8_15

73. Milner, R.: Functions as Processes. In: Paterson, M. (ed.) Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, UK, July 16-20, 1990, Proceedings. Lecture Notes in Computer Science, vol. 443, pp. 167-180. Springer (1990). https://doi.org/10.1007/BFb0032030, https://doi.org/10.1007/BFb0032030

74. Milner, R.: Communicating and Mobile Systems - the Pi-Calculus. Cambridge University Press (1999)

75. Morris, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology (1969), https://dspace.mit.edu/handle/1721.1/64850

76. Nicola, R.D., Hennessy, M.: CCS without tau's. In: Ehrig, H., Kowalski, R.A., Levi, G., Montanari, U. (eds.) TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP '87). Lecture Notes in Computer Science, vol. 249, pp. 138-152. Springer (1987). https://doi.org/10.1007/3-540-17660-8_53, https://doi.org/10.1007/3-540-17660-8_53

77. Palamidessi, C.: Comparing the Expressive Power of the Synchronous and Asynchronous pi-calculi. Mathematical Structures in Computer Science 13(5), 685-719 (2003). https://doi.org/10.1017/S0960129503004043

78. Pous, D.: Coinduction All the Way Up. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016. pp. 307-316. ACM (2016). https://doi.org/10.1145/2933575.2934564, https://doi.org/10.1145/2933575.2934564

79. Prebet, E.: Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques. In: Bojanczyk, M., Merelli, E., Woodruff, D.P. (eds.) 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France. LIPIcs, vol. 229, pp. 130:1-130:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.ICALP.2022.130, https://doi.org/10.4230/LIPIcs.ICALP.2022.130

80. Pugliese, R.: Semantic Theories for Asynchronous Languages. Ph.D. thesis, Università di Roma "La Sapienza" (1996)

81. Rahli, V., Bickford, M., Cohen, L., Constable, R.L.: Bar Induction is Compatible with Constructive Type Theory. J. ACM 66(2), 13:1-13:35 (2019). https://doi.org/10.1145/3305261, https://doi.org/10.1145/3305261

82. Ravara, A., Resende, P., Vasconcelos, V.T.: An Algebra of Behavioural Types. Inf. Comput. 212, 64-91 (2012)

83. Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125-198 (2007). https://doi.org/10.1016/j.ic.2006.06.002, https://doi.org/10.1016/j.ic.2006.06.002
84. Sabel, D., Schmidt-Schauß, M.: A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations. Math. Struct. Comput. Sci. 18(3), 501–553 (2008). https://doi.org/10.1017/S0960129508006774, https://doi.org/10.1017/S0960129508006774

85. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011)

86. Sangiorgi, D.: Asynchronous pi-calculus at Work: The Call-by-Need Strategy. In: Alvim, M.S., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds.) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday. Lecture Notes in Computer Science, vol. 11760, pp. 33–49. Springer (2019). https://doi.org/10.1007/978-3-030-31175-9_3, https://doi.org/10.1007/978-3-030-31175-9_3

87. Sangiorgi, D., Walker, D.: The Pi-Calculus - a Theory of Mobile Processes. Cambridge University Press (2001)

88. Schmidt-Schauß, M., Sabel, D.: Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars. In: Dardha, O., Rot, J. (eds.) Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020, and 17th Workshop on Structural Operational SemanticsOnline, 31 August 2020. EPTCS, vol. 322, pp. 88–105 (2020). https://doi.org/10.4204/EPTCS.322.8, https://doi.org/10.4204/EPTCS.322.8

89. Schmidt-Schauß, M., Sabel, D., Dallmeyer, N.: Sequential and Parallel Improvements in a Concurrent Functional Programming Language. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018. pp. 20:1–20:13. ACM (2018). https://doi.org/10.1145/3236950.3236952, https://doi.org/10.1145/3236950.3236952

90. Selinger, P.: First-Order Axioms for Asynchrony. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) CONCUR '97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1243, pp. 376–390. Springer (1997). https://doi.org/10.1007/3-540-63141-0_26, https://doi.org/10.1007/3-540-63141-0_26

91. Taha, S., Ye, L., Wolff, B.: HOL-CSP Version 2.0. Archive of Formal Proofs (April 2019)

92. Taha, S., Wolff, B., Ye, L.: The hol-csp refinement toolkit. Archive of Formal Proofs (November 2020), https://isa-afp.org/entries/CSP_RefTK.html, Formal proof development

93. Tanti, E., Francalanza, A.: Towards Sound Refactoring in Erlang (2015), https://api.semanticscholar.org/CorpusID:63046364

94. Thati, P.: A Theory of Testing for Asynchronous Concurrent Systems. Ph.D. thesis, University of Illinois Urbana-Champaign, USA (2003), https://hdl.handle.net/2142/81630

95. Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical Relations for Fine-Grained Concurrency. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013. pp. 343–356. ACM (2013). https://doi.org/10.1145/2429069.2429111, https://doi.org/10.1145/2429069.2429111
A Further related works

*Contextual preorders in functional languages* Morris preorder is actively studied in the pure λ-calculus [29,30,67,10], λ-calculus with references [79,62], in PCF [69] as well as in languages supporting shared memory concurrency [95], and mutable references [46]. The more sophisticated the languages, the more intricate and larger the proofs. The need for mechanisation became thus apparent, in particular to prove that complex logical relations defined in the framework Iris (implemented in Coq) are sound, i.e. included in the preorder [70,51]. The paper [7] provides a framework to study contextual equivalences in the setting of process calculi. It is worth noting, though, that as argued in [25, Section 3], Morris equivalence coincides with MAY-equivalence, at least if the operational semantics at hand enjoys the Church-Rosser property. In fact [26] define Morris preorder literally as a testing one, via tests for convergence. The studies of the MUST-preorder in process calculi can thus be seen as providing proof methods to adapt Morris equivalence to nondeterministic settings, and using contexts that are really external observers. To sum up, one may say that Morris equivalence coincides with MAY-equivalence when nondeterminism is confluent and all states are viewed as accepting states, while it coincides with MUST equivalence in the presence of true nondeterminism and when only successful states are viewed as accepting states.

In the setting of nondeterministic and possibly concurrent applicative programming languages [89,88,18], also a contextual preorder based on may and must-termination has been studied [84,18]. Our preorder ≲<sub>env</sub> is essentially a generalisation of the must-termination preorder of [84] to traces of visible actions.

*Theories for synchronous semantics* Both [72] and [36] employed LTSs as a model of contracts for web-services (i.e. WSCL), and the MUST-preorder as refinement for contracts. The idea is that a search engine asked to look for a service described by a contract $p_1$ can actually return a service that has a contract $p_2$, provided that $p_1 \preceq_{\text{MUST}} p_2$.

The MUST-preorder for clients proposed by [14] has partly informed the theory of monitors by [1], in particular the study of preorders for monitors by [49]. Our results concern LTSs that are more general than those of monitors, and thus our code could provide the basis to mechanise the results of [1].

The first subtyping relation for binary session types was presented in [52] using a syntax-oriented definition. The semantic model of that subtyping is a refinement very similar to the MUST-preorder. The idea is to treat types as CCS terms, assign them an LTS [35,9,82,16], and use the resulting testing preorders as semantic models of the subtyping. In the setting of coinductively defined higher-order session types, the correspondence is implicitly addressed in [35]. In the setting of recursive higher-order session types, it is given by Theorem 4.10 of [15].
*Models of asynchrony* While synchronous (binary) communication requires the simultaneous occurrence of a send and a receive action, asynchronous communication allows a delay between a send action and the corresponding receive action. Different models of asynchrony exist, depending on which medium is assumed for storing messages in transit. In this paper, following the early work on the asynchronous π-calculus [64,24,4], we assume the medium to be an unbounded unordered mailbox, shared by all processes. Thus, no process needs to wait to send a message, namely the send action is non-blocking. This model of communication is best captured via the output-buffered agents with feedback of [90]. The early style LTS of the asynchronous π-calculus is a concrete example of this kind of LTSs. A similar global unordered mailbox is used also in Chapter 5 of [94], by [32], which relies explicitly on a mutable global state, and by [77], which manipulates it via two functions *get* and *set*.

More deterministic models of asynchrony are obtained assigning a data structure to every channel. For example [65,66] use an even more deterministic model in which each ordered pair of processes is assigned a dedicated channel, equipped with an *ordered* queue. Hence, messages along such channels are received in the same order in which they were sent. This model is used for asynchronous session calculi, and mimics the communication mode of the TCP/IP protocol. The obvious research question here is how to adapt our results to the different communication mechanisms and different classes of LTSs. For instance, both [93] and [34] define LTSs for ERLANG. We will study whether at least one of these LTSs is an instance of output-buffered agents with feedback. If this is not the case, we will first try to adapt our results to ERLANG LTSs.

*May-preorder* MAY testing and the MAY-preorder, have been widely studied in asynchronous settings. The first characterisation for ACCS appeared in [38] and relies on comparing traces and asynchronous traces of servers. Shortly after [23] presented a characterisation based on operation on traces. A third characterisation appeared in [8], where the saturated LTS $\rightarrow_s$ is essentially our $\rightarrow_{fw}$. That characterisation supports our claim that results about synchronous semantics are true also for asynchronous ones, modulo forwarding. Compositionality of trace inclusion, i.e. the alternative characterisation of the MAY-preorder, has been partly investigated in Coq by [6] in the setting of IO-automata. The MAY-preorder has also been studied in the setting of actor languages by [34,93].

*Fairness* Van Glabbeek [53] argues that by amending the semantics of parallel composition (i.e. the scheduler) different notions of fairness can be embedded in the MUST-preorder. We would like to investigate which notion of fairness makes the MUST-preorder coincide with the FAIR-preorder of [83].

*Mutable state* Prebet [79] has recently shown an encoding of the asynchronous π-calculus into a λ-calculus with references, which captures Morris equivalence via a bisimulation. This renders vividly the intuition that output-buffered agents manipulate a shared common state. We therefore see our work also as an analysis of the MUST-preorder for a language in which programs manipulate a global
<figure><img src="image_12.png" /><figcaption>Fig. 8. The state transition system of client-server system.</figcaption></figure>

mutable store. Since the store is what contains output messages, and our formal development shows that only outputs are observable, our results suggest that characterisations of testing preorders for impure programming languages should predicate over the content of the mutable store, i.e. the values written by programs. Another account of π-calculus synchronisation via a functional programming language is provided in [88], that explains how to use Haskell M-VARS to implement π-calculus message passing.

## B Bar-Induction

Section B.1 is an informal introduction to the intuitions behind bar induction, together with a comment on the admissibility of this principle in Coq. In Section B.2 we gather the properties of the predicates $\Downarrow$ and `MUST` that we use throughout our technical development.

### B.1 A visual introduction

We explain the difference between extensional definitions of predicates and intensional ones, by discussing how the two different approaches make us reason on computational trees.

Suppose that we have a client-server system $p \llcorner r$ and that we want to prove either $p \ \mathsf{MUST} \ r$ or $p \ \mathsf{MUST}_i \ r$. For both proofs, what matters is the state transition system (STS) of $p \llcorner r$, i.e. the computation steps performed by the client-server system at issue. In fact it is customary to treat this STS as a computational tree, as done for instance in the proofs of [55, Lemma 4.4.12] and [39, Theorem 2.3.3]. In the rest of this subsection we discuss the tree depicted in Figure 8. It contains three maximal computations, the middle one being infinite. In the figures of this subsection, the states in which the client is successful (i.e. in the predicate `GOOD`) contain the symbol $\checkmark$.
<figure><img src="image_13.png" /><figcaption>**Fig. 9.** Extensional approach: finding successful prefixes in every maximal path of the computational tree.</figcaption></figure>

*The extensional approach* To prove *p MUST r*, the extensional definition of MUST requires checking that every maximal path in the tree in Figure 8 starts with a finite prefix that leads to a successful state. The proof that *p MUST r* amounts to looking for a suitable prefix maximal path by maximal path, via a loop whose iterations are suggested in Figure 9. There at every iteration a different maximal path (highlighted by dashed arrows) is checked, and each time a successful prefix is found (indicated by a red arrow), the loop moves on to the next maximal path. Once a maximal path is explored, it remains dashed, to denote that there a successful prefix has been found. The first iteration looks for a successful prefix in the left-most maximal path, while the last iteration looks for a successful prefix in the right-most path. In the current example the loop terminates because the tree in Figure 8 has conveniently a finite number of maximal paths, but in general the mathematical reasoning has to deal with an infinite amount of maximal path. An archetypal example is the tree in Figure 11: it has countably many maximal paths, each one starting with a successful prefix.

*The intensional approach* Consider now the predicate $MUST_i$ - which is defined intensional ly - and a proof that $p MUST_i r$. The base case of $MUST_i$ ensures that all the nodes that contain a successful client (i.e. that satisfies the predicate $Q_2$, defined on line 553 of the submission) are in $MUST_i$. Pictorially, this is the step from (1) to (2) in Figure 10, where the nodes in $MUST_i$ are drawn using dashed borders, and the freshly added ones are drawn in red. Once the base case is established, the inductive rule of $MUST_i$ ensures that any node that inevitably goes to nodes that are in $MUST_i$, is also in the predicate $MUST_i$. This leads to the step from (2) to (3) and then from (3) to (4). Note that the argument is concise, for in the tree the depth at which successful states can be found is finite. In general though is may not be the case. The tree in Figure 11 is again the archetypal example: every maximal path there contains a finite prefix that leads to a successful state, but there is no upper bound on the length on those prefixes.
<figure><img src="image_14.png" /><figcaption>**Fig. 10.** Intensional approach: visiting the tree bottom-up, starting from the bar.</figcaption></figure>

*Do extensional and intensional predicates coincide?* Extensional and intensional definitions make us reason on computational trees in strikingly different fashions: * extensionally * we reason maximal path by maximal path, while * intensionally * we reason bottom-up, starting from the nodes in a predicate that bars the tree.<fnref n="11" /> It is natural to ask whether reasoning in these different manners ultimately leads to the same outcomes. In our setting this amounts to proving that the predicates MUST and MUSTᵢ are logically equivalent, and similarly for the convergence predicates ↓ and ↓ᵢ. The proof that p MUSTᵢ r implies p MUST r is - obviously - by induction on the derivation of p MUSTᵢ r. Proving that the extensional predicates imply the intensional ones is, on the other hand, delicate, because we may have to deal with unbounded structures. The tree in Figure 11 is once more the archetypal example: it has countably many maximal paths, and there is no upper bound on the depth at which successful states (i.e. nodes in the *bar*) are found.

In classical logic one can prove that *p* MUST *r* implies *p* MUSTᵢ *r* by contradiction. As we wish to avoid this reasoning principle, the only tool we have is the axiom of Bar induction, which states exactly that under suitable hypotheses, extensionally defined predicates imply their intensional ly defined counter-parts.

<footnote n="11">¹¹ Whence the name *bar*-induction.</footnote>
<figure><img src="image_15.png" /><figcaption>**Fig. 11.** An infinite branching computational tree where the bar ✓ is at unbounded depth.</figcaption></figure>

*Admissibility.* To show that the principle is admissible, we prove that it follows from the Classical Epsilon (CE) axiom of the Coq standard library. In short, CE gives a choice function $\epsilon$ such that if $p$ is a proof of $\exists x : A, P x$, then $\epsilon(p)$ is an element of $A$ such that $P(\epsilon(p))$ holds. It implies Excluded Middle, and thus classical reasoning, because $A \lor \neg A$ is equivalent to $\exists b : \mathbf{bool}, (b = \mathbf{true} \land A) \lor (b = \mathbf{false} \land \neg A)$. Since CE is guaranteed by the Coq developers to be admissible, our statement of bar induction is also admissible.

## B.2 Properties of inductively defined predicates

Convergence along traces is preserved by the strong transitions $\to$.

**Lemma 9.** In every LTS, for every $p, p' \in C$ and $s \in \mathbf{Act}^*$ the following facts are true,

1. if $p \Downarrow s$ and $p \xrightarrow{\tau} p'$ then $p' \Downarrow s$,

2. for every $\mu \in \mathbf{Act}$. $p \Downarrow \mu.s$ and $p \xrightarrow{\mu} p'$ imply $p \Downarrow s$.

**Lemma 10.** For every $s \in \mathbf{Act}^*$ and $p \in \mathbf{ACCS}$, if $p \Downarrow s$ then $|\{q | p \xrightarrow{s} q\}| \in \mathbb{N}$.

The hypothesis of convergence in Lemma 10 is necessary. This is witnessed by the process $p = \mathbf{recx}.(x \parallel \bar{a})$, which realises an ever lasting addition of a message to the mailbox:

$$p \xrightarrow{\tau} p \parallel \bar{a} \xrightarrow{\tau} p \parallel \bar{a} \parallel \bar{a} \xrightarrow{\tau} p \parallel \bar{a} \parallel \bar{a} \parallel \bar{a} \xrightarrow{\tau} \dots$$
In more general languages also image-finiteness may fail. An example is given on page 267 of [60].

The predicate $MUST_i$ is preserved by atoms freely changing their locations in systems. This is coherent with the intuition that the mailbox is a global and shared one. For instance the systems $a.0 \parallel \bar{d} \parallel d.1$ and $a.0 \parallel \bar{d} \parallel d.1 \parallel d$, which in the mechanisation are respectively

(pr_par (pr_input a prNil) (pr_out d), pr_input d prSucces)

and

(pr_input a prNil, pr_par (pr_input a prSucces) (pr_out d))

have the same mailbox, namely $\bar{d}$.

The predicate $MUST_i$ enjoys three useful properties: it ensures convergence of servers interacting with clients that are not in a good state; it is preserved by internal computation of servers; and it is preserved also by interactions with unhappy clients. The arguments to show these facts are by rule induction on the hypothesis $p MUST_i r$. The last fact is a consequence of a crucial property of $MUST_i$, namely Lemma 14.

**Lemma 11.** Let $\mathcal{L}_A \in \text{FWD}$ and $\mathcal{L}_B \in \text{FDB}$. For every $p \in A$, $r \in B$ we have that $p MUST_i r$ implies that $p \downarrow_i$ or GOOD(r).

**Lemma 12.** Let $\mathcal{L}_A \in \text{FWD}$ and $\mathcal{L}_B \in \text{FDB}$. For every $p, p' \in A$, $r \in B$ we have that $p MUST_i r$ and $p \xrightarrow{\tau} p'$ imply $q MUST_i r$.

**Lemma 13.** For every $\mathcal{L}_B \in \text{OBA}$, $r \in B$ and name $a \in \mathcal{N}$ such that $p \xrightarrow{\bar{a}} p'$ then GOOD($p$) iff GOOD($p'$).

*Proof.* This is a property of Good, more specifically good_preserved_by_lts_output and good_preserved_by_lts_output_converse.

The next lemma states that when reasoning on $MUST_i$, outputs can be freely moved from the client to the server side of systems, if servers have the forwarding ability. Its proof uses *all* the axioms for output-buffered agents with feedback, and the lemma itself is used in the proof of the main result on acceptance sets, namely Lemma 19.

**Lemma 14 (Output swap).** Let $\mathcal{L}_A \in \text{FWD}$ and $\mathcal{L}_B \in \text{FDB}$. For every $p_1, p_2 \in A$, every $r_1, r_2 \in B$ and name $a \in \mathcal{N}$ such that $p_1 \xrightarrow{\bar{a}} p_2$ and $r_1 \xrightarrow{\bar{a}} r_2$, if $p_1 MUST_i r_2$ then $p_2 MUST_i r_1$.

*Proof.* We proceed by induction on $p_1 MUST_i r_2$. In the base case $p_1 MUST_i r_2$ is derived using the rule [AXIOM] and thus GOOD($r_2$). Lemma 13 implies that GOOD($r_1$), and so we prove $p_2 MUST_i r_1$ using rule [AXIOM]. We are done with the base case.

In the inductive case, the hypothesis $p_2 MUST_i r_1$ has been derived via an rule [IND-RULE], and we therefore know the following facts:
1. $p_1 \llbracket r_2 \xrightarrow{\tau} \hat{p} \rrbracket \hat{r}$, and

2. For every $p', r'$ such that $p_1 \llbracket r_2 \xrightarrow{\tau} p' \rrbracket r'$ we have that $p' \text{ MUST}_i r'$.

We prove $p_2 \text{ MUST}_i r_1$ by applying rule [IND-RULE]. In turn this requires us to show that

(i) $p_2 \llbracket r_1 \xrightarrow{\tau} \hat{r} \rrbracket$, and that

(ii) for each $p'$ and $r'$ such that $p_2 \llbracket r_1 \xrightarrow{\tau} p' \rrbracket r'$, we have $p' \text{ MUST}_i r'$.

We prove (i). The argument starts with a case analysis on how the transition (1) has been derived. There are the following three cases:

[S-Srv] a $\tau$-transition performed by the server such that $p_1 \xrightarrow{\tau} \hat{p}$ and that $\hat{r} = r_2$, or

[S-Clt] a $\tau$-transition performed by the client such that $r_2 \xrightarrow{\tau} \hat{r}$ and that $\hat{p} = p_1$, or

[S-com] an interaction between the server $p_1$ and the client $r_2$ such that $p_1 \xrightarrow{\mu} \hat{p}$ and that $r_2 \xrightarrow{\bar{\mu}} \hat{r}$.

In case [S-SRV] we use the OUTPUT-TAU axiom together with the transitions $p_1 \xrightarrow{\bar{a}} p_2$ and $p_1 \xrightarrow{\tau} \hat{p}$ to obtain that either:

- there exists a $p_3$ such that $p_2 \xrightarrow{\tau} p_3$ and $\hat{p} \xrightarrow{\bar{a}} p_3$, or

- $p_2 \xrightarrow{a} p_3$.

In the first case $p_2 \xrightarrow{\tau} p_3$ let us construct the transition $p_2 \llbracket r_1 \xrightarrow{\tau} p_3 \rrbracket r_1$ as required. In the second case recall that by hypothesis $r_1 \xrightarrow{\bar{a}} r_2$, and thus the transition $p_2 \xrightarrow{a} \hat{p}$ and rule [S-COM] let us construct the desired reduction $p_2 \llbracket r_1 \xrightarrow{\tau} \hat{p} \rrbracket r_2$.

In case [S-Clt] we use the OUTPUT-COMMUTATIVITY axiom together with the transitions $r_1 \xrightarrow{\bar{a}} r_2 \xrightarrow{\tau} \hat{r}$ to obtain a $r_3$ such that $r_1 \xrightarrow{\tau} r_3 \xrightarrow{\bar{a}} \hat{r}$ and it follows that there exists the silent move $p_2 \llbracket r_1 \xrightarrow{\tau} p_2 \rrbracket r_3$.

In case [S-COM] we have that $p_1 \xrightarrow{\mu} \hat{p}$ and $r_2 \xrightarrow{\bar{\mu}} \hat{r}$. We distinguish whether $\mu = \bar{a}$ or not. If $\mu = \bar{a}$ then observe that $r_1 \xrightarrow{\bar{a}} r_2 \xrightarrow{a} \hat{r}$. Since by hypothesis $r_1, r_2 \in B$ and $\mathcal{L}_B \in \text{FDB}$ we apply FEEDBACK axiom to these transitions and obtain $r_1 \xrightarrow{\tau} \hat{r}$. An application of [S-COM] let us construct the desired transition $p_2 \llbracket r_1 \xrightarrow{\tau} p_2 \rrbracket \hat{r}$.

If $\mu \neq \bar{a}$ we apply the OUTPUT-CONFLUENCE axiom to the transitions $p_1 \xrightarrow{\bar{a}} p_2$ and $p_1 \xrightarrow{\mu} \hat{p}$ to obtain a $p_3$ such that $p_2 \xrightarrow{\mu} p_3$ and $\hat{p} \xrightarrow{\bar{a}} p_3$. We then apply the OUTPUT-COMMUTATIVITY axiom to obtain $r_1 \xrightarrow{\bar{\mu}} r_3 \xrightarrow{\bar{a}} \hat{r}$ for some $r_3$. Finally, we have the desired $p_2 \llbracket r_1 \xrightarrow{\tau} \hat{p} \rrbracket r_3$ thanks to the existence of an interaction between $p_2$ and $r_1$ that follows from $p_2 \xrightarrow{\mu} p_3$ and $r_1 \xrightarrow{\bar{\mu}} r_2$. This concludes the proof of (i).

We now tackle (ii). First of all, note that the inductive hypothesis states the following fact,
For every $p', r', p_0$ and $r_0$, such that $p_1 \underset{r_2}{\overset{\tau}{\rightleftharpoons}} p' \underset{r'}{\overset{\tau}{\rightleftharpoons}} p', p' \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p_0$ and $r_0 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} r'$ then $p_0 \text{ MUST}_i r_0$.

Fix a transition

$$p_2 \underset{r_1}{\overset{\tau}{\rightleftharpoons}} p' \underset{r'}{\overset{\tau}{\rightleftharpoons}} r,$$

we must show $p' \text{ MUST}_i r'$. We proceed by case analysis on the rule used to derive the transition at issue, and the cases are as follows,

(a) a $\tau$-transition performed by the server such that $p_2 \underset{\tau}{\overset{\tau}{\rightleftharpoons}} p'$ and that $r' = r_1$, or

(b) a $\tau$-transition performed by the client such that $r_1 \underset{\tau}{\overset{\tau}{\rightleftharpoons}} r'$ and that $p' = p_2$, or

(c) an interaction between the server $p_2$ and the client $r_1$ such that $p_2 \underset{r_1}{\overset{\bar{\mu}}{\rightleftharpoons}} p'$ and that $r_1 \underset{r_1}{\overset{\bar{\mu}}{\rightleftharpoons}} r'$.

In case (a) we have $p_2 \underset{\tau}{\overset{\tau}{\rightleftharpoons}} p'$ and $r' = r_1$ and hence we must show $p' \text{ MUST}_i r_1$. We apply the OUTPUT-COMMUTATIVITY axiom to the transitions $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p_2 \underset{\tau}{\overset{\tau}{\rightleftharpoons}} p'$ to obtain a $p_3$ such that $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p_3 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p'$. We apply the inductive hypothesis with $p' = p_3, r' = r_2, p_0 = p'$ and $r_0 = r_1$ and obtain $p_2 \text{ MUST}_i r_1$ as required.

In case (b) we have $r_1 \underset{\tau}{\overset{\tau}{\rightleftharpoons}} r'$ and $p' = p_2$, we therefore must show $p_2 \text{ MUST}_i r'$. We apply the OUTPUT-TAU axiom to the transitions $r_1 \underset{r_1}{\overset{\tau}{\rightleftharpoons}} r'$ and $r_1 \underset{r_1}{\overset{\bar{a}}{\rightleftharpoons}} r_2$ to obtain that

- either there exists a $\hat{r}$ such that $r_2 \underset{\tau}{\overset{\tau}{\rightleftharpoons}} \hat{r}$ and $r' \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} \hat{r}$,

- or $r_2 \underset{a}{\overset{a}{\rightleftharpoons}} r'$.

In the first case we apply the inductive hypothesis with $p' = p_1, r' = \hat{r}, p_0 = p_2$ and $r_0 = r'$ and obtain $p_2 \text{ MUST}_i r'$ as required. In the second case, the transitions $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p_2$ and $r_2 \underset{a}{\overset{a}{\rightleftharpoons}} r'$ and rule [S-COM] let us prove $p_1 \underset{r_2}{\overset{\tau}{\rightleftharpoons}} p_2 \underset{r'}{\overset{\tau}{\rightleftharpoons}} r'$. We apply part (2) to obtain $p_2 \text{ MUST}_i r'$ as required.

We now consider the case (c) in which $p_2 \underset{\mu}{\overset{\mu}{\rightleftharpoons}} p'$ and $r_1 \underset{\bar{\mu}}{\overset{\bar{\mu}}{\rightleftharpoons}} r'$. We must show $p' \text{ MUST}_i r'$ and to do so we distinguish whether $\mu = a$ or not.

If $\mu = a$ then we apply the OUTPUT-DETERMINACY axiom to the transitions $r_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} r_2$ and $r_1 \underset{\bar{\mu}}{\overset{\bar{\mu}}{\rightleftharpoons}} r'$ to obtain that $r_2 = r'$. Since by hypothesis $p_1, p_2 \in A$ and $\mathcal{L}_A \in \text{FWD}$ we apply the FWD-FEEDBACK axiom to the transitions $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p_2 \underset{a}{\overset{\tau}{\rightleftharpoons}} p'$ to prove that either $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p'$ or $p_1 = p'$ must hold. If $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p'$ then we have that $p_1 \underset{r_2}{\overset{\tau}{\rightleftharpoons}} r_2 \underset{r_2}{\overset{\tau}{\rightleftharpoons}} p' \underset{r_2}{\overset{\tau}{\rightleftharpoons}} r_2$. The property in (2) ensures that $p' \text{ MUST}_i r_2$ and from $r_2 = r'$ we have that the required $p' \text{ MUST}_i r'$ holds too. If $p_1 = p'$ then $p' \text{ MUST}_i r_2$ is a direct consequence of the hypothesis $p_1 \text{ MUST}_i r_2$.

If $\mu \neq a$ then we are allowed to apply the OUTPUT-CONFLUENCE axiom to the transitions $r_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} r_2$ and $r_1 \underset{\bar{\mu}}{\overset{\bar{\mu}}{\rightleftharpoons}} r'$ to obtain a $\hat{r}$ such that $r_2 \underset{\bar{\mu}}{\overset{\bar{\mu}}{\rightleftharpoons}} \hat{r}$ and $r' \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} \hat{r}$. An application of the OUTPUT-COMMUTATIVITY axiom to the transitions $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p_2 \underset{\bar{\mu}}{\overset{\bar{\mu}}{\rightleftharpoons}} p'$ provides us with a $\hat{p}$ such that $p_1 \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} \hat{p} \underset{\bar{a}}{\overset{\bar{a}}{\rightleftharpoons}} p'$. We now apply the inductive hypothesis with $p' = \hat{p}, r' = \hat{r}, p_0 = p'$ and $r_0 = r'$ and obtain $p_2 \text{ MUST}_i r'$ as required. This concludes the proof of (ii), and therefore of the lemma.
**Lemma 15.** Let $\mathcal{L}_A \in \text{FWD}$ and $\mathcal{L}_B \in \text{FDB}$. For every $p, p' \in A$, $r, r' \in B$ and every action $\mu \in \text{Act}$ such that $p \xrightarrow{\mu} p'$ and $r \xrightarrow{\bar{\mu}} r'$ we have that $p \text{MUST}_i r$ and $\neg \text{GOOD}(r)$ implies $p' \text{MUST}_i r'$.

*Proof.* By case analysis on the hypothesis that $p \text{MUST}_i r$.

## C Forwarders

The intuition behind forwarders, quoting [64], is that “any message can come into the configuration, regardless of the forms of inner receptors. [...] As the experimenter is not synchronously interacting with the configuration [...] , he may send any message as he likes.”

In this appendix we give the technical results to ensure that the function FW builds an LTS that satisfies the axioms of the class LtsEq.

For any LTS $\mathcal{L} = (A, L, \longrightarrow)$ of output-buffered agents we assume a function $\text{mbox} : A \to MO$

(i) $\bar{a} \in O(p)$ if and only if $\bar{a} \in \text{mbox}(p)$, and

(ii) for every $p'$, if $p \xrightarrow{\bar{a}} p'$ then $\text{mbox}(p) = \{[\bar{a}]\} \cup \text{mbox}(p')$.

Note that by definition $\text{mbox}(p)$ is a finite multiset.

**Definition 14.** For any LTS $\mathcal{L} = (C, L, \longrightarrow) \in \text{FDB}$, we define the function strip : $C \longrightarrow C$ by induction on $\text{mbox}(p)$ as follows: if $\text{mbox}(p) = \emptyset$ then strip($p$) = $p$, while if $\exists \bar{a} \in \text{mbox}(p)$ and $p \xrightarrow{\bar{a}} p'$ then strip($p$) = strip($p'$). Note that strip($p$) is well-defined thanks to the OUTPUT-DETERMINACY and the OUTPUT-COMMUTATIVITY axioms.

We now wish to show that $\text{FW}(\mathcal{L}) \in \text{FWD}$ for any LTS $\mathcal{L}$ of output-buffered agents with feedback. Owing to the structure of our typeclasses, we have first to construct an equivalence $\simeq$ over $\text{FW}(\mathcal{L})$ that is compatible with the transition relation, i.e. satisfies the axiom in Figure 5. We do this in the obvious manner, i.e. by combining the equivalence $\simeq$ over the states of $\mathcal{L}$ with an equivalence over mailboxes.

**Definition 15.** For any LTS $\mathcal{L} \in \text{FDB}$, two states $p \triangleright M$ and $q \triangleright N$ of $\text{FW}(\mathcal{L})$ are equivalent, denoted $p \triangleright M \doteq q \triangleright N$, if $\text{strip}(p) \simeq \text{strip}(q)$ and $M \uplus \text{mbox}(p) = N \uplus \text{mbox}(q)$.

**Lemma 16.** For every $\mathcal{L}_A$ and every $p \triangleright M, q \triangleright N \in A \times MO$, and every $\alpha \in L$, if $p \triangleright M (\doteq \xrightarrow{\alpha} \text{fw}) q \triangleright N$ then $p \triangleright M (\xrightarrow{\alpha} \text{fw} \cdot \doteq) q' \triangleright N'$.

**Lemma 17.** For every $\mathcal{L}_A \in \text{FDB}$ and every $p, q \in A$, $M \in MO$, if $p \simeq q$ then $p \triangleright M \doteq q \triangleright M$.

*Proof.* This follows from the fact that if $p \simeq q$ then $\text{strip}(p) \simeq \text{strip}(q)$ and $\text{mbox}(p) = \text{mbox}(q)$.
**Lemma 2.** For every LTS $\mathcal{L} \in \mathcal{FDB}$, $FW(\mathcal{L}) \in \mathcal{FWD}$.

*Proof.* We must show that, given an LTS $\mathcal{L} = \langle C, L, \rightarrow \rangle \in \mathcal{FDB}$, we have that $FW(\mathcal{L}) \in \mathcal{FWD}$. To do so, we need to show that $FW(\mathcal{L})$ obeys to the axioms given in Equation (7), namely INPUT-BOOMERANG and FWD-FEEDBACK. We first show that $FW(\mathcal{L})$ obeys to the INPUT-BOOMERANG axiom.

We pick a process $p \in C$, a mailbox $M \in MO$ and a name $a \in \mathcal{N}$. The axiom INPUT-BOOMERANG requires us to exhibit a process $p' \in A$ and a mailbox $M' \in MO$ such that the following transitions hold.

$$p \triangleright M \xrightarrow{a} \mathcal{Fw} p' \triangleright M' \xrightarrow{\bar{a}} \mathcal{Fw} p \triangleright M$$

We choose $p' = p$ and $M' = (\{\bar{a}\} \uplus M)$. An application of the rule [L-MINP] and then the rule [L-MOUT] from Figure 6 allows us to derive the required sequence of transitions as shown below.

$$p \triangleright M \xrightarrow{a} \mathcal{Fw} p \triangleright (\{\bar{a}\} \uplus M) \xrightarrow{\bar{a}} \mathcal{Fw} p \triangleright M$$

We now show that $FW(\mathcal{L})$ obeys to the FWD-FEEDBACK axiom. To begin we pick three processes $p_1, p_2, p_3 \in C$, three mailboxes $M_1, M_2, M_3 \in MO$ and a name $a \in \mathcal{N}$ such that:

$$p_1 \triangleright M_1 \xrightarrow{\bar{a}} \mathcal{Fw} p_2 \triangleright M_2 \xrightarrow{a} \mathcal{Fw} p_3 \triangleright M_3$$

We need to show that either:

1. $p_1 \triangleright M_1 \xrightarrow{\tau} \mathcal{Fw} p_3 \triangleright M_3$, or

2. $p_1 \triangleright M_1 \doteq p_3 \triangleright M_3$

We proceed by case analysis on the last rule used to derive the transition $p_1 \triangleright M_1 \xrightarrow{\bar{a}} \mathcal{Fw} p_2 \triangleright M_2$. This transition can either be derived by the rule [L-MOUT] or the rule [L-PROC].

We first consider the case where the transition has been derived using the rule [L-MOUT]. We then have that $p_1 = p_2$ and $M_1 = (\{\bar{a}\} \uplus M_2)$. We continue by case analysis on the last rule used to derive the transition $p_2 \triangleright M_2 \xrightarrow{a} \mathcal{Fw} p_3 \triangleright M_3$. If this transition has been derived using the rule [L-MINP] then it must be the case that $p_2 = p_3$ and that $(\{\bar{a}\} \uplus M_2) = M_3$. This lets us conclude by the following equality to show that $p_1 \triangleright M_1 \doteq p_3 \triangleright M_3$.

$$p_1 \triangleright M_1 = p_2 \triangleright (\{\bar{a}\} \uplus M_2) = p_3 \triangleright M_3$$

Otherwise, this transition has been derived using the rule [L-PROC], which implies that $p_2 \xrightarrow{a} p_3$ together with $M_2 = M_3$. An application of the rule [L-COMM] ensures the following transition and allows us to conclude this case with $p_1 \triangleright M_1 \xrightarrow{\tau} \mathcal{Fw} p_3 \triangleright M_3$.

$$p_1 \triangleright M_1 = p_2 \triangleright (\{\bar{a}\} \uplus M_2) \xrightarrow{\tau} p_3 \triangleright M_2 = p_3 \triangleright M_3$$
We now consider the case where the transition $p_1 \triangleright M_1 \xrightarrow{\bar{a}}_{fw} p_2 \triangleright M_2$ has been derived using the rule [L-PROC] such that $p_1 \xrightarrow{\bar{a}} p_2$ and $M_1 = M_2$.

Again, we continue by case analysis on the last rule used to derive the transition $p_2 \triangleright M_2 \xrightarrow{a}_{fw} p_3 \triangleright M_3$. If this transition has been derived using the rule [L-MINP] then it must be the case that $p_2 = p_3$ and $(\{\bar{a}\} \uplus M_2) = M_3$. Also, note that, as $\mathcal{L} \in \mathcal{FDB}$, the transition $p_1 \xrightarrow{\bar{a}} p_2$ implies $mbox{$p_1$} = \mathcal{Mbox}(p_2) \uplus \{\bar{a}\}$. In order to prove $p_1 \triangleright M_1 \doteq p_3 \triangleright M_3$, it suffices to show the following:

(a) $\mathit{strip}(p_1) \simeq \mathit{strip}(p_3)$, and

(b) $M_1 \uplus \mathit{mbox}(p_1) = M_3 \uplus \mathit{mbox}(p_3)$

We show that $\mathit{strip}(p_1) \simeq \mathit{strip}(p_3)$ by definition of $\mathit{strip()}$ together with the transition $p_1 \xrightarrow{\bar{a}} p_2$ and the equality $p_2 = p_3$.

The following ensures that $M_1 \uplus \mathit{mbox}(p_1) = M_3 \uplus \mathit{mbox}(p_3)$.

$$
\begin{align*}
& M_1 \uplus \mathit{mbox}(p_1) \\
&= M_1 \uplus \mathit{mbox}(p_2) \uplus \{\bar{a}\} \quad \text{from } \mathit{mbox}(p_1) = \mathit{mbox}(p_2) \uplus \{\bar{a}\} \\
&= M_2 \uplus \mathit{mbox}(p_3) \uplus \{\bar{a}\} \quad \text{from } M_1 = M_2, p_2 = p_3 \\
&= (M_2 \uplus \{\bar{a}\}) \uplus \mathit{mbox}(p_3) \\
&= M_3 \uplus \mathit{mbox}(p_3) \quad \text{from } M_3 = M_2 \uplus \{\bar{a}\}
\end{align*}
$$

If the transition $p_2 \triangleright M_2 \xrightarrow{a}_{fw} p_3 \triangleright M_3$ has been derived using the rule [L-PROC] then it must be the case that $p_2 \xrightarrow{a} p_3$ and $M_2 = M_3$. As $\mathcal{L} \in \mathcal{FDB}$, we are able to call the axiom FEEDBACK together with the transitions $p_1 \xrightarrow{\bar{a}} p_2$ and $p_2 \xrightarrow{a} p_3$ to obtain a process $p'_3$ such that $p_1 \xrightarrow{\bar{a}} p'_3$ and $p'_3 \simeq p_3$. An application of Lemma 17 and rule [L-PROC] allows us to conclude that $p_1 \triangleright M_1 (\xrightarrow{\bar{a}}_{fw} \cdot \doteq) p_3 \triangleright M_3$. $\square$

D Completeness

This section is devoted to the proof that the alternative preorder given in Definition 5 includes the MUST-preorder. First we present a general outline of the main technical results to obtain the proof we are after. Afterwards, in Subsection (D) we discuss in detail on all the technicalities.

Proofs of completeness of characterisations of contextual preorders usually require using, as the name suggests, syntactic contexts. Our calculus-independent setting, though, does not allow us to define them. Instead we phrase our arguments using two functions $tc : \mathit{Act}^* \to C$, and $ta : \mathit{Act}^* \times \mathcal{P}(\mathcal{N}) \to C$ where $\langle C, L, \longrightarrow \rangle$ is some LTS of FDB. In Table 1 we gather all the properties of $tc$ and $ta$ that are sufficient to give our arguments. The properties (1) - (5) must hold for both $tc$ and $ta(\varepsilon, -)$ for every set of names $O$, the properties (c1) - (c2) must hold for $tc$, and (t1) - (t4) must hold for $ta$.

We use the function $tc$ to test the convergence of servers, and the function $ta$ to test the acceptance sets of servers.

A natural question is whether such $tc$ and $ta$ can actually exist. The answer depends on the LTS at hand. In Appendix H.2, and in particular Figure 16, we
$$
\forall s \in \mathbf{Act}^*, \forall a \in \mathcal{N},
$$

$$
(1) \neg_{\text{GOOD}}(f(s))
$$

$$
(2) \forall \mu \in \mathbf{Act}, f(\mu.s) \xrightarrow{\bar{\mu}} f(s)
$$

$$
(3) f(\bar{a}.s) \xrightarrow{\tau} r
$$

$$
(4) \forall r \in C, f(\bar{a}.s) \xrightarrow{\tau} r \text{ implies } \mathbf{GOOD}(r)
$$

$$
(5) \quad \forall r \in C, \mu \in \mathbf{Act}, f(\bar{a}.s) \xrightarrow{\mu} r \text{ implies } \mu = a \text{ and } r = f(s)
$$

$$
\forall E \subseteq \mathcal{N},
$$

$$
(t1) \quad ta(\epsilon, E) \xrightarrow{\tau} \epsilon
$$

$$
(t2) \quad \forall a \in \mathcal{N}, ta(\epsilon, E) \xrightarrow{\bar{a}} \epsilon
$$

$$
(t3) \quad \forall a \in \mathcal{N}, ta(\epsilon, E) \xrightarrow{a} \text{ if and only if } a \in E
$$

$$
(t4) \quad \forall \mu \in \mathbf{Act}, r \in C, ta(\epsilon, E) \xrightarrow{\mu} r \text{ implies } \mathbf{GOOD}(r)
$$

$$
(c1) \quad \forall \mu \in \mathbf{Act}, tc(\epsilon) \xrightarrow{\mu} \epsilon
$$

$$
(c2) \exists r, tc(\epsilon) \xrightarrow{\tau} r
$$

$$
(c3) \quad \forall r, tc(\epsilon) \xrightarrow{\tau} r \text{ implies } \text{GOOD}(r)
$$

<caption>**Table 1.** Properties of the functions that generate clients.</caption>

define these functions for the standard LTS of **ACCS**, and it should be obvious
how to adapt those definitions to the asynchronous π-calculus [57].

In short, our proofs show that ≲<sub>AS</sub> is complete with respect to ⊊<sub>MUST</sub> in any LTS of output-buffered agents with feedback wherein the functions *tc* and *ta* enjoying the properties in Table 1 can be defined.

First, converging along a finite trace *s* is logically equivalent to passing the client *tc*(*s*). In other words, there exists a bijection between the proofs (i.e. finite derivation trees of *p* MUST<sub>*i*</sub> *tc*(*s*)) and the ones of *p* ⇓ *s*. We first give the proposition, and then discuss the auxiliary lemmas to prove it.

**Proposition 3.** For every $\mathcal{L}_A \in \text{FWD}$, $p \in A$, and $s \in \text{Act}^*$ we have that $p \text{ MUST}_i tc(s)$ if and only if $p \downarrow s$.

The *if* implication is Lemma 31 and the *only if* implication is Lemma 28. The
hypothesis that $\mathcal{L}_A \in \text{FWD}$, i.e. the use of forwarders, is necessary to show that
convergence implies passing a client, as shown by the next example.

Example 8. Consider a server *p* in an LTS *L* ∈ FDB whose behaviour amounts
to the following transitions: *p* − b − Ω − τ − Ω − τ − ... Note that this entails that
*L* does not *not* enjoy the axioms of forwarders.

Now let $s = a.b$. Since $p \downarrow$ and $p \stackrel{a}{\Rightarrow}$ we know that $p \downarrow a.b$. On the other hand Table 1(2) implies that the client $tc(s)$ performs the transitions $tc(s) \xrightarrow{\bar{a}} tc(b) \xrightarrow{\bar{b}} tc(\epsilon)$. Thanks to the OUTPUT-COMMUTATIVITY axiom we
obtain $tc(s) \xrightarrow{\bar{b}} \bar{a} \xrightarrow{\bar{a}} tc(\varepsilon)$. Table 1(1) implies that the states reached by the client are unsuccessful, and so by zipping the traces performed by $p$ and by $tc(s)$ we build a maximal computation of $p \Vdash tc(s)$ that is unsuccessful, and thus $p \models_{\mathcal{L}_A} tc(s)$. $\square$

This example explains why in spite of Lemma 3 output-buffered agents with feedback do not suffice to use the standard characterisations of the MUST-preorder.

We move on to the more involved technical results, i.e. the next two lemmas, that we use to reason on acceptance sets of servers.

**Lemma 18.** Let $\mathcal{L}_A \in \text{FWD}$. For every $p \in A$, $s \in \text{Act}^*$, and every $L, E \subseteq \mathcal{N}$, if $\bar{L} \in \mathcal{A}_{\text{fw}}(p, s)$ then $p \models_{\mathcal{L}_A} ta(s, E \setminus L)$.

**Lemma 19.** Let $\mathcal{L}_A \in \text{FWD}$. For every $p \in A$, $s \in \text{Act}^*$, and every finite set $O \subseteq \bar{\mathcal{N}}$, if $p \Vdash s$ then either

(i) $p \models_{\text{MUST}_i} ta(s, \bigcup \mathcal{A}_{\text{fw}}(p, s) \setminus O)$, or

(ii) there exists $\hat{O} \in \mathcal{A}_{\text{fw}}(p, s)$ such that $\hat{O} \subseteq O$.

We can now show that the alternative preorder $\preceq_{\text{AS}}$ includes $\preceq_{\text{MUST}}$ when used over LTSs of forwarders.

**Lemma 20.** For every $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$ and servers $p \in A, q \in B$, if $p \preceq_{\text{MUST}} q$ then $p \preceq_{\text{AS}} q$.

*Proof.* Let $p \preceq_{\text{MUST}} q$. To prove that $p \preceq_{\text{cnv}} q$, suppose $p \Vdash s$ for some trace $s$. Proposition 3 implies $p \models_{\text{MUST}_i} tc(s)$, and so by hypothesis $q \models_{\text{MUST}_i} tc(s)$. Proposition 3 ensures that $q \Vdash s$.

We now show that $p \preceq_{\text{acc}} q$. Thanks to Lemma 4, it is enough to prove that $p \preceq_{\text{acc}}^{\text{fw}} q$. So, we show that for every trace $s \in \text{Act}^*$, if $p \Vdash s$ then $\mathcal{A}_{\text{fw}}(p, s) \ll \mathcal{A}_{\text{fw}}(q, s)$. Fix an $O \in \mathcal{A}_{\text{fw}}(q, s)$. We have to exhibit a set $\hat{O} \in \mathcal{A}_{\text{fw}}(p, s)$ such that $\hat{O} \subseteq O$.

By definition $O \in \mathcal{A}_{\text{fw}}(q, s)$ means that for some $q'$ we have $q \stackrel{s}{\Rightarrow} q' \xrightarrow{\tau} O$ and $O(q') = O$. Let $E = \bigcup \mathcal{A}_{\text{fw}}(p, s)$ and $X = E \setminus O$. The hypothesis that $p \Vdash s$, and the construction of the set $X$ let us apply Lemma 19, which implies that either

(a) $p \models_{\text{MUST}_i} ta(s, \bar{X})$, or

(b) there exists a $\hat{O} \in \mathcal{A}_{\text{fw}}(p, s)$ such that $\hat{O} \subseteq O(q')$.

Since (b) is exactly what we are after, to conclude the argument it suffices to prove that (a) is false. This follows from Lemma 18, which proves $q \models_{\text{MUST}_i} ta(s, \bar{X})$, and the hypothesis $p \preceq_{\text{MUST}} q$, which ensures $p \models_{\text{MUST}_i} ta(s, \bar{X})$.

The fact that the MUST-preorder can be captured via the function $\text{FW}(-)$ and $\preceq_{\text{AS}}$ is a direct consequence of Lemma 3 and Lemma 20.

**Proposition 4 (Completeness).** For every $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$ and servers $p \in A, q \in B$, if $p \preceq_{\text{MUST}} q$ then $\text{FW}(p) \preceq_{\text{AS}} \text{FW}(q)$.
We now gather all the technical auxiliary lemmas and then discuss the proofs of the main ones.

By assumption, outputs preserve the predicate GOOD. For stable clients, they also preserve the negation of this predicate.

**Lemma 21.** For all $r, r' \in A$ and trace $s \in \overline{\mathcal{N}}^*$, $r \xrightarrow{\tau} r'$, $\neg GOOD(r)$ and $r \stackrel{s}{\implies} r'$ implies $\neg GOOD(r')$.

## D.1 Testing convergence

We start with preliminary facts, in particular two lemmas that follow from the properties in Table 1.

A process $p$ converges along a trace $s$ if for every $p'$ reached by $p$ performing any prefix of $s$, the process $p'$ converges.

**Lemma 22.** For every $\langle A, L, \rightarrow \rangle$, $p \in A$, and $s \in \mathbf{Act}^*$, $p \downarrow s$ if and only if $p \stackrel{s'}{\implies} p'$ implies $p' \downarrow$ for every $s'$ prefix of $s$.

Traces of output actions impact neither the stability of servers, nor their input actions.

**Lemma 23.** For every $\mathcal{L}_A$, every $p, p' \in A$ and every trace $s \in \overline{\mathcal{N}}^*$,

1. $p \xrightarrow{\tau} p$ and $p \stackrel{s}{\implies} p'$ implies $p' \xrightarrow{\tau} p$.

2. $p \xrightarrow{\tau} p$ and $p \stackrel{s}{\implies} p'$ implies $I(p) = I(p')$.

**Lemma 24.** For every $s \in \mathbf{Act}^*$, $tc(s) \xrightarrow{\tau} p$.

The BACKWARD-OUTPUT-DETERMINACY axiom is used in the proof of the next lemma.

**Lemma 25.** For every $s \in \mathbf{Act}^*$, if $tc(s) \xrightarrow{\mu} r$ then either

(a) GOOD($r$), or

(b) $s = s_1 \bar{\mu} s_2$ for some $s_1 \in \mathcal{N}^*$ and $s_2 \in \mathbf{Act}^*$ such that $r \simeq tc(s_1 s_2)$.

**Lemma 26.** For every $s \in \mathbf{Act}^*$, if $tc(s) \xrightarrow{\tau} r$ then either:

(a) GOOD($r$), or

(b) there exist $b, s_1, s_2$ and $s_3$ with $s_1.b.s_2 \in \mathcal{N}^*$ such that $s = s_1.b.s_2.b.s_3$ and $r \simeq tc(s_1.s_2.s_3)$.

**Lemma 27.** Let $\mathcal{L}_A \in \text{FWD}$. For every server $p, p' \in A$, trace $s \in \mathbf{Act}^*$ and action $\mu \in \mathbf{Act}$ such that $p \stackrel{\mu}{\implies} p'$ we have that $p_{\text{MUST}_i} tc(\mu.s)$ implies $p'_{\text{MUST}_i} tc(s)$.

*Proof.* By rule induction on the reduction $p \stackrel{\mu}{\implies} p'$ together with Lemma 12 and Lemma 15.

**Lemma 28.** Let $\mathcal{L}_A \in \text{FWD}$. For every server $p \in A$, trace $s \in \mathbf{Act}^*$ we have that $p_{\text{MUST}_i} tc(s)$ implies $p \downarrow s$.
*Proof.* We proceed by induction on the trace *s*. In the base case *s* is ε. Table 1(1) states that $\neg\text{GOOD}(tc(\varepsilon))$ and we apply Lemma 11 to obtain $p \downarrow_i$, and thus $p \Downarrow \varepsilon$. In the inductive case *s* is $\mu.s'$ for some $\mu \in \text{Act}$ and $s' \in \text{Act}^*$. We must show the following properties,

1. $p \downarrow_i$, and

2. for every $p'$ such that $p \stackrel{\mu}{\Longrightarrow} p'$, $p' \Downarrow s'$.

We prove the first property as we did in the base case, and we apply Lemma 27 to prove the second property.

**Lemma 29.** Let $\mathcal{L}_A \in \text{FWD}$. For every $p \in A$, $s_1 \in \mathcal{N}^*$ and $s_3 \in \text{Act}^*$ we have that

1. for every $\mu \in \text{Act}$, if $p \Downarrow s_1.\mu.s_3$ and $p \stackrel{\mu}{\Longrightarrow} q$ then $q \Downarrow s_1.s_3$,

2. for every $a.s_2 \in \mathcal{N}^*$ if $p \Downarrow s_1.a.s_2.\bar{a}.s_3$ then $p \Downarrow s_1.s_2.s_3$.

**Lemma 30.** For every LTS $\mathcal{L}_A$ and every $p \in A$, $p \downarrow_i$ implies $p_{\text{MUST}_i} tc(\varepsilon)$.

*Proof.* Rule induction on the derivation of $p \downarrow_i$.

**Lemma 31.** For every $\mathcal{L}_A \in \text{FWD}$, every $p \in A$, and $s \in \text{Act}^*$, if $p \Downarrow s$ then $p_{\text{MUST}_i} tc(s)$.

*Proof.* The hypothesis $p \Downarrow s$ ensures $p \downarrow_i$. We show that $p_{\text{MUST}_i} tc(s)$ reasoning by complete induction on the length of the trace *s*. The base case is Lemma 30 and here we discuss the inductive case, i.e. when $\text{len}(s) = n + 1$ for some $n \in \mathbb{N}$.

We proceed by rule induction on $p \downarrow_i$. In the base case $p \stackrel{\tau}{\Longrightarrow}$, and the reduction at hand is due to either a $\tau$ transition in $tc(s)$, or a communication between $p$ and $tc(s)$.

In the first case $tc(s) \stackrel{\tau}{\Longrightarrow} r$, and so Lemma 26 ensures that one of the following conditions holds,

1. GOOD($r$), or

2. there exist $a \in \mathcal{N}$, $s_1, s_2$ and $s_3$ with $s = s_1.a.s_2.\bar{a}.s_3$ and $r \simeq tc(s_1.s_2.s_3)$.

If GOOD($r$) then we conclude via rule [AXIOM]; otherwise Lemma 29(2) and the hypothesis that $p \Downarrow s$ imply $p \Downarrow s_1.s_2.s_3$, thus prove $p_{\text{MUST}_i} r$ via the inductive hypothesis of the complete induction on *s*.

We now consider the case when the transition is due to a communication, i.e. $p \stackrel{\mu}{\Longrightarrow} p'$ and $tc(s) \stackrel{\bar{a}}{\Longrightarrow} r$. Lemma 25 tells us that either GOOD($r$) or there exist $s_1$ and $s_2$ such that $s = s_1.\mu.s_2$ and $r \simeq tc(s_1.s_2)$. In the first case we conclude via rule [AXIOM]. In the second case we apply Lemma 29(1) to prove $p' \Downarrow s_1.s_2$, and thus $p'_{\text{MUST}_i} r$ follows from the inductive hypothesis of the complete induction. In the inductive case of the rule induction on $p \downarrow_i$, we know that $p \stackrel{\tau}{\Longrightarrow} p'$ for some process $p'$. We reason again by case analysis on how the reduction we fixed has been derived, i.e. either via a $\tau$ transition in $tc(s)$, or via a communication between $p$ and $tc(s)$, or via a $\tau$ transition in $p$. In the first two cases we reason as we did for the base case of the rule induction. In the third case $p \Downarrow s$ and $p \stackrel{\tau}{\Longrightarrow} p'$ imply $p' \Downarrow s$, we thus obtain $p'_{\text{MUST}_i} tc(s)$ thanks to the inductive hypothesis of the rule induction which we can apply because the tree to derive $p' \downarrow_i$ is smaller than the tree to derive that $p \downarrow_i$.
## D.2 Testing acceptance sets

In this section we present the properties of the function $ta(-, -)$ that are sufficient to obtain completeness. To begin with, $ta(-, -)$ function enjoys a form of monotonicity with respect to its second argument.

**Lemma 32.** Let $\mathcal{L}_A \in \mathbf{FDB}$. For every $p \in A$, trace $s \in \mathbf{Act}^*$, and sets of outputs $O_1, O_2$, if $p_{\mathbf{MUST}_i} ta(s, O_1)$ and $O_1 \subseteq O_2$ then $p_{\mathbf{MUST}_i} ta(s, O_2)$.

*Proof.* Induction on the derivation of $p_{\mathbf{MUST}_i} ta(s, O_1)$.

Let OBA denote the set of LTS of output-buffered agents. Note that any $\mathcal{L} \in \mathbf{OBA}$ need not enjoy the FEEDBACK axiom.

**Lemma 33.** Let $\mathcal{L}_A \in \mathbf{OBA}$, and $\mathcal{L}_B \in \mathbf{OBA}$. For every $p \in A$, trace $s \in \mathbf{Act}^*$, set of outputs $O$ and name $a \in \mathcal{N}$, such that

(i) $p \downarrow_i$ and,

(ii) For every $p' \in A$, $p \xrightarrow{\bar{a}} p'$ implies $p'_{\mathbf{MUST}_i} ta(s, \bar{O})$,

we have that $p_{\mathbf{MUST}_i} ta(\bar{a}.s, \bar{O})$.

*Proof.* We proceed by induction on the hypothesis $p \downarrow_i$.

(Base case: $p$ is stable) We prove $p_{\mathbf{MUST}_i} ta(\bar{a}.s, \bar{O})$ by applying rule [IND-RULE]. Since Table 1(3) implies that $p \| ta(\bar{a}.s, \bar{O}) \xrightarrow{\tau} r$, all we need to prove is the following fact,

$$ \forall p' \in A, r \in B. \text{ if } p \| ta(\bar{a}.s, \bar{O}) \xrightarrow{\tau} p' \| r \text{ then } p'_{\mathbf{MUST}_i} r. \quad (\star) $$

Fix a transition $p \| ta(\varepsilon, \bar{O}) \xrightarrow{\tau} p' \| r$. As $p$ is stable, this transition can either be due to:

1. a $\tau$-transition performed by the client such that $ta(\bar{a}.s, \bar{O}) \xrightarrow{\tau} r$, or

2. an interaction between the server $p$ and the client $ta(\bar{a}.s, \bar{O})$.

In the first case Table 1(4) implies GOOD($r$), and hence we obtain $p'_{\mathbf{MUST}_i} r$ via rule [AXIOM]. In the second case there exists an action $\mu$ such that

$$ p \xrightarrow{\mu} p' \quad \text{and} \quad ta(\bar{a}.s, \bar{O}) \xrightarrow{\bar{\mu}} r $$

Table 1(5) implies $\mu$ is $\bar{a}$ and $r = ta(s, \bar{O})$. We then have $p \xrightarrow{\bar{a}} p'$ and thus the reduction $p \xrightarrow{\bar{a}} p'$, which allows us to apply the hypothesis (ii) and obtain $p'_{\mathbf{MUST}_i} r$ as required.
(Inductive case: $p \xrightarrow{\tau} p'$ implies $p'$) The argument is similar to one for the base case, except that we must also tackle the case when the transition $p \llcorner ta(\bar{a}.s, \bar{O}) \xrightarrow{\tau} p' \llcorner r$ is due to a $\tau$ action performed by $p$, i.e. $p \xrightarrow{\tau} p'$ and $r = ta(\bar{a}.s, \bar{O})$. The inductive hypothesis tells us the following fact:

For every $p_1$ and $a$, such that $p \xrightarrow{\tau} p_1$, for every $p_2$, if $p_1 \stackrel{\bar{a}}{\implies} p_2$ then $p_2 \text{ MUST}_i ta(s, O)$.

To apply the inductive hypothesis we have to show that for every $p_2$ such that $p' \stackrel{\bar{a}}{\implies} p_2$ we have that $p_2 \text{ MUST}_i ta(s, \bar{O})$. This is a consequence of the hypothesis (ii) together with the reduction $p \xrightarrow{\tau} p' \stackrel{\bar{a}}{\implies} p_2$, and thus concludes the proof.

**Lemma 34.** Let $\mathcal{L}_A \in \mathbf{FDB}$. For every $p \in A$ and set of outputs $O$, if $p$ is stable then either

(a) $p \text{ MUST}_i ta(\varepsilon, \overline{O(p) \setminus O})$, or

(b) $O(p) \subseteq O$.

*Proof.* We distinguish whether $O(p) \setminus O$ is empty or not. In the first case, $O(p) \setminus O = \emptyset$ implies $O(p) \subseteq O$, and we are done.

In the second case, there exists $\bar{a} \in O(p)$ such that $\bar{a} \notin O$. Note also that Table 1(1) ensures that $\neg \text{GOOD}(ta(\varepsilon, \overline{O(p) \setminus O}))$, and thus we construct a derivation of $p \text{ MUST}_i ta(\varepsilon, \overline{O(p) \setminus O})$ by applying the rule [IND-RULE]. This requires us to show the following facts,

1. $p \llcorner ta(s, \overline{O(p) \setminus O}) \longrightarrow$, and

2. for each $p'$, $r$ such that $p \llcorner ta(s, \overline{O(p) \setminus O}) \xrightarrow{\tau} p' \llcorner r$, $p' \text{ MUST}_i r$ holds.

To prove (1), we show that an interaction between the server $p$ and the test $ta(s, \overline{O(p) \setminus O})$ exists. As $\bar{a} \in O(p)$, we have that $p \xrightarrow{\bar{a}}$. Then $\bar{a} \in O(p) \setminus O$ together with (3) ensure that $ta(s, \overline{O(p) \setminus O}) \xrightarrow{\bar{a}}$. An application of the rule [S-COM] gives us the required transition $p \llcorner ta(s, \overline{O(p) \setminus O}) \longrightarrow$.

To show (2), fix a silent transition $p \llcorner ta(s, \overline{O(p) \setminus O}) \xrightarrow{\tau} p' \llcorner r$. We proceed by case analysis on the rule used to derive the transition under scrutiny. Recall that the server $p$ is stable by hypothesis, and that $ta(s, \overline{O(p) \setminus O})$ is stable thanks to Table 1(1). This means that the silent transition must have been derived via rule [S-COM]. Furthermore, Table 1(2) implies that the test $ta(s, \overline{O(p) \setminus O})$ does not perform any output. As a consequence, if there is an interaction it must be because the test performs an input and becomes $r$. Table 1(4) implies that GOOD($r$), and hence we obtain the required $p' \text{ MUST}_i r$ applying rule [AXIOM].

**Lemma 18** Let $\mathcal{L}_A \in \mathbf{FWD}$. For every $p \in A$, $s \in \text{Act}^*$, and every $L, E \subseteq \mathcal{N}$, if $\bar{L} \in \mathcal{A}_{\text{fw}}(p, s)$ then $p \text{ MUST}_i ta(s, E \setminus L)$.

*Proof.* By hypothesis there exists a set $\bar{L} \in \mathcal{A}_{\text{fw}}(p, s)$, i.e. for some $p'$ we have $p \stackrel{s}{\implies} p' \xrightarrow{\tau} \bar{L}$ and $O(p') = \bar{L}$. We have to show that $p \text{ MUST}_i ta(s, E \setminus L)$, i.e. $p \text{ MUST}_i ta(s, E \setminus L)$ implies $\perp$. For convenience, let $X = E \setminus L$.
We proceed by induction on the derivation of the weak transitions $p \stackrel{s}{\Rightarrow} p'$. In the base case the derivation consists in an application of rule [WT-REFL], which implies that $p = p'$ and $s = \varepsilon$. We show that there exists no derivation of judgement $p_{MUST_i} ta(s, X)$. By definition, $\neg GOOD(ta(s, X))$ and thus no tree that ends with [AXIOM] can have $p_{MUST_i} ta(s, X)$ as conclusion. The hypotheses ensure that $p$ is stable, and $ta(\varepsilon, X)$ is stable by definition. The set of inputs of $ta(\varepsilon, X)$ is $X$, which prevents an interaction between $p$ and $ta(s, X)$, i.e. an application of rule [S-COM]. This proves that $p \Vdash ta(s, X)$ is stable, thus a side condition of [IND-RULE] is false, and the rule cannot be employed to prove $p_{MUST_i} ta(s, X)$.

In the inductive cases $p \stackrel{s}{\Rightarrow} p'$ is derived using either:

(i) rule [WT-TAU] such that $p \xrightarrow{\tau} \hat{p} \stackrel{s}{\Rightarrow} p'$, or

(ii) rule [WT-MU] such that $p \xrightarrow{\mu} \hat{p} \stackrel{t}{\Rightarrow} p'$, with $s = \mu.t$.

In the first case, applying the inductive hypothesis requires us to show $\hat{p}_{MUST_i} ta(s, X)$, which is true since $p_{MUST_i} ta(s, X)$ is preserved by the $\tau$-transitions performed by the server.

In the second case, applying the inductive hypothesis requires us to show $\hat{p}_{MUST_i} ta(t, X)$. Table 1(2) implies that $ta(\mu.t, X) \xrightarrow{\bar{\mu}} ta(t, X)$. Then we derive via [S-COM] the transition $p \Vdash ta(\mu.t, E) \xrightarrow{\tau} \hat{p} \Vdash ta(t, E)$. Since $p_{MUST_i} ta(s, X)$ is preserved by the interactions occurring between the server and the client, which implies $\hat{p}_{MUST_i} ta(t, X)$ as required.

**Lemma 19** Let $\mathcal{L}_A \in \text{FWD}$. For every $p \in A$, $s \in \text{Act}^*$, and every finite set $O \subseteq \tilde{N}$, if $p \downarrow s$ then either

(i) $p_{MUST_i} ta(s, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O})$, or

(ii) there exists $\tilde{O} \in \mathcal{A}_{fw}(p, s)$ such that $\tilde{O} \subseteq O$.

*Proof.* We proceed by induction on the trace $s$.

(Base case, $s = \varepsilon$) The hypothesis $p \downarrow \varepsilon$ implies $p \downarrow_i$ and we continue by induction on the derivation of $p \downarrow_i$.<fnref n="12" /> In the base case $p \downarrow_i$ was proven using rule [AXIOM], and hence $p \xrightarrow{\tau}$. We apply Lemma 34 to obtain either:

(i) $p_{MUST_i} ta(\varepsilon, \overline{O(p) \setminus O})$, or

(ii) $O(p) \subseteq O$.

In case (i) we are done. In case (ii), as $p$ is stable we have $\{p' | p \stackrel{\varepsilon}{\Rightarrow} p' \xrightarrow{\tau} \} = \{p\}$ and thus $\mathcal{A}_{fw}(p, \varepsilon) = \{O(p)\}$ and we conclude by letting $\tilde{O} = O(p)$.

In the inductive case $p \downarrow_i$ was proven using rule [IND-RULE]. We know that $p \xrightarrow{\tau}$, and the inductive hypothesis states that for any $p'$ such that $p \xrightarrow{\tau} p'$, either:

(a) $p'_{MUST_i} ta(\varepsilon, \overline{O(p') \setminus O})$, or

<footnote n="12">¹² Recall that the definition of $\downarrow_i$ is in Equation (int-preds)</footnote>
(b) there exists $\hat{O} \in \mathcal{A}_{fw}(p', s)$ such that $\hat{O} \subseteq O$.

It follows that either

(∀) for each $p' \in \{p' | p \xrightarrow{\tau} p'\}$, $p' \text{ MUST}_i ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p', s) \setminus O})$, or

(∃) there exists a $p' \in \{p' | p \xrightarrow{\tau} p'\}$ and a $\hat{O} \in \mathcal{A}_{fw}(p', \varepsilon)$ such that $\hat{O} \subseteq O$,

We discuss the two cases. If (∃) the argument is straightforward: we pick the existing $p'$ such that $p \xrightarrow{\tau} p'$. The definition of $\mathcal{A}_{fw}(-, -)$ ensures that and show that $\mathcal{A}_{fw}(p', \varepsilon) \subseteq \mathcal{A}_{fw}(p, \varepsilon)$, and thus we conclude by choosing $\hat{O}$.

Case (∀) requires more work. We are going to show that $p \text{ MUST}_i ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O})$ holds. To do so we apply the rule [IND-RULE] and we need to show the following facts,

(a) $p \Vdash ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O}) \xrightarrow{\tau}$, and

(b) for each $p' \Vdash r'$ such that $p \Vdash ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O}) \xrightarrow{\tau} p' \Vdash r'$, we have $p' \text{ MUST}_i r'$.

The first requirement follows from the fact that $p$ is not stable. To show the second requirement we proceed by case analysis on the transition $p \Vdash ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O}) \xrightarrow{\tau} p' \Vdash r'$. As $ta(\varepsilon, \overline{O}(p) \setminus O)$ is stable by (1), it can either be due to:

1. a $\tau$-transition performed by the server $p$ such that $p \xrightarrow{\tau} p'$, or

2. an interaction between the server $p$ and the client $ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O})$.

In the first case we apply the first part of the inductive hypothesis to prove that $p' \text{ MUST}_i ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p', s) \setminus O})$, and we conclude via Lemma 32 to get the required

$$p' \text{ MUST}_i ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O}).$$

In the second case, there exists a $\mu \in \text{Act}$ such that

$$p \xrightarrow{\mu} p' \text{ and } ta(\varepsilon, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O}) \xrightarrow{\mu} r$$

Thanks to Table 1(4) we apply rule [AXIOM] to prove that $p' \text{ MUST}_i r$ and we are done with the base case of the main induction on the trace $s$.

(Inductive case, $s = \mu.s'$) By induction on the set $\{p' | p \xrightarrow{\mu} p'\}$ and an application of the inductive hypothesis we know that either:

(i) there exists $p' \in \{p' | p \xrightarrow{\mu} p'\}$ and $\hat{O} \in \mathcal{A}_{fw}(p', s')$ such that $\hat{O} \subseteq O$, or

(ii) for each $p' \in \{p' | p \xrightarrow{\mu} p'\}$ we have that $p' \text{ MUST}_i ta(s', \bigcup \overline{\mathcal{A}_{fw}(p', s')})$.

In the first case, the inclusion $\mathcal{A}_{fw}(p', s') \subseteq \mathcal{A}_{fw}(p, \mu.s')$ and $\hat{O} \in \mathcal{A}_{fw}(p', s')$ imply $\hat{O} \in \mathcal{A}_{fw}(p, s)$ and we are done.

In the second case, we show $p \text{ MUST}_i ta(s, \bigcup \overline{\mathcal{A}_{fw}(p, s)})$ by case analysis on the action $\mu$, which can be either an input or an output.
- If $\mu$ is an input, $\mu = a$ for some $a \in \mathcal{N}$. An application of the axiom of forwarders gives us a $p'$ such that $p \xrightarrow{a} p'$ $\xrightarrow{\bar{a}} p$. An application of Table 1(2) gives us the following transition,

$$ta(a.s', \bigcup \overline{\mathcal{A}_{fw}(p, a.s') \setminus O}) \xrightarrow{\bar{a}} ta(s', \bigcup \overline{\mathcal{A}_{fw}(p, a.s') \setminus O})$$

By an application of Lemma 14 it is enough to show

$$p'_{\text{MUST}_i} ta(s', \bigcup \overline{\mathcal{A}_{fw}(p, a.s') \setminus O})$$

to obtain the required $p_{\text{MUST}_i} ta(a.s', \bigcup \overline{\mathcal{A}_{fw}(p, a.s') \setminus O})$.

- If $\mu$ is an output, $\mu = \bar{a}$ for some $a \in \mathcal{N}$ and we must show that

$$p_{\text{MUST}_i} ta(\bar{a}.s', \bigcup \overline{\mathcal{A}_{fw}(p, \bar{a}.s') \setminus O}).$$

We apply Lemma 33 together with (ii) to obtain $p_{\text{MUST}_i} ta(\bar{a}.s', \bigcup \overline{\mathcal{A}_{fw}(p', s') \setminus O})$. Again, Lemma 32 together with the inclusion $\mathcal{A}_{fw}(p', s') \subseteq \mathcal{A}_{fw}(p, \bar{a}.s')$ ensures the required $p_{\text{MUST}_i} ta(s, \bigcup \overline{\mathcal{A}_{fw}(p, s) \setminus O})$.

## E Soundness

In this section we prove the converse of Proposition 4, i.e. that $\ll_{AS}$ is included in $\ll_{MUST}$. We remark immediately that a naïve reasoning does not work. Fix two servers $p$ and $q$ such that $p \ll_{AS} q$.

To lift the predicates $\ll_{cnv}$ and $\ll_{acc}$ to sets of servers, we let $\mathcal{A}_{fw}(X, s) = \{O \mid \exists p \in X. O \in \mathcal{A}_{fw}(p, s)\}$, and for every finite $X \in \mathcal{P}^+(A)$, we write $X \downarrow$ to mean $\forall p \in X. p \downarrow$, we write $X \downarrow s$ to mean $\forall p \in X. p \downarrow s$, and let

- $X \ll_{cnv}^{\text{set}} q$ to mean $\forall s \in \text{Act}^*$, if $X \downarrow s$ then $q \downarrow s$,

- $X \ll_{acc}^{\text{set}} q$ to mean $\forall s \in \text{Act}^*, X \downarrow s$ implies $\mathcal{A}_{fw}(X, s) \ll \mathcal{A}_{fw}(q, s)$,

- $X \ll_{AS}^{\text{set}} q$ to mean $X \ll_{cnv}^{\text{set}} q \wedge X \ll_{acc}^{\text{set}} q$.

These definitions imply immediately the following equivalences, $\{p\} \ll_{acc}^{\text{set}} q \iff p \ll_{cnv}^{\text{set}} q, \{p\} \ll_{cnv}^{\text{set}} q \iff p \ll_{acc}^{\text{set}} q$ and thereby the following lemma.

**Lemma 35.** For every LTS $\mathcal{L}_A, \mathcal{L}_B, p \in A, q \in B, p \ll_{AS} q$ if and only if $\{p\} \ll_{AS}^{\text{set}} q$.

The preorder $\ll_{AS}^{\text{set}}$ is preserved by $\tau$-transitions on its right-hand side, and by visible transitions on both sides. We reason separately on the two auxiliary preorders $\ll_{cnv}^{\text{set}}$ and $\ll_{acc}^{\text{set}}$. We need one further notion.

**Lemma 36.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$. For every set $X \in \mathcal{P}^+(A)$, and $q \in B$, such that $X \ll_{cnv}^{\text{set}} q$,

1. $q \xrightarrow{\tau} q'$ implies $X \ll_{cnv}^{\text{set}} q'$,
2. $X \downarrow_i, X \stackrel{\mu}{\Rightarrow} X'$ and $q \stackrel{\mu}{\rightarrow} q'$ imply $X' \preceq_{\text{cnv}}^{\text{set}} q'$.

**Lemma 37.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$. For every $X, X' \in \mathcal{P}^+(A)$ and $q \in B$, such that $X \preceq_{\text{acc}}^{\text{set}} q$, then

1. $q \xrightarrow{\tau} q'$ implies $X \preceq_{\text{acc}}^{\text{set}} q'$,

2. if $X \downarrow_i$ then for every $\mu \in \text{Act}$, every $q'$ and $X'$ such that $q \stackrel{\mu}{\rightarrow} q'$ and $X \stackrel{\mu}{\Rightarrow} X'$ we have $X' \preceq_{\text{acc}}^{\text{set}} q'$.

The main technical work for the proof of soundness is carried out by the next lemma.

**Lemma 38.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$ and $\mathcal{L}_C \in \text{FDB}$. For every set of servers $X \in \mathcal{P}^+(A)$, server $q \in B$ and client $r \in C$, if $X \text{MUST}_{\text{aux}} r$ and $X \preceq_{\text{AS}}^{\text{set}} q$ then $q \text{MUST}_i r$.

**Proposition 5 (Soundness).** For every $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$ and servers $p \in A, q \in B$, if $\text{FW}(p) \preceq_{\text{AS}}^{\text{}} \text{FW}(q)$ then $p \preceq_{\text{MUST}}^{\text{}} q$.

*Proof.* Lemma 3 ensures that the result follows if we prove that $\text{FW}(p) \preceq_{\text{MUST}}^{\text{}} \text{FW}(q)$. Fix a client $r$ such that $\text{FW}(p) \text{MUST}_i r$. Lemma 38 implies the required $\text{FW}(q) \text{MUST}_i r$, if we show that

(i) $\{\text{FW}(p)\} \text{MUST}_{\text{aux}} r$, and that

(ii) $\{\text{FW}(p)\} \preceq_{\text{AS}}^{\text{set}} \text{FW}(q)$.

The first fact follows from the assumption that $\text{FW}(p) \text{MUST}_i r$ and Lemma 7 applied to the singleton $\{\text{FW}(p)\}$. The second fact follows from the hypothesis that $\text{FW}(p) \preceq_{\text{AS}}^{\text{}} \text{FW}(q)$ and Lemma 35.

## E.1 Technical results to prove soundness

We now discuss the proofs of the main technical results behind Proposition 5. The predicate $\text{MUST}_{\text{aux}}$ is monotonically decreasing with respect to its first argument, and it enjoys properties analogous to the ones of $\text{MUST}_i$ that have been shown in Lemma 11 and Lemma 12.

**Lemma 39.** For every LTS $\mathcal{L}_A, \mathcal{L}_B$ and every set $X_1 \subseteq X_2 \subseteq A$, client $r \in B$, if $X_2 \text{MUST}_{\text{aux}} r$ then $X_1 \text{MUST}_{\text{aux}} r$.

**Lemma 40.** Let $\mathcal{L}_A \in \text{FWD}$ and $\mathcal{L}_B \in \text{FDB}$. For every set $X \in \mathcal{P}^+(A)$, client $r \in B$, if $\neg \text{GOOD}(r)$ and $X \text{MUST}_{\text{aux}} r$ then $X \downarrow_i$.

**Lemma 41.** For every $\mathcal{L}_A, \mathcal{L}_B$, every set $X_1, X_2 \in \mathcal{P}^+(A)$, and client $r \in B$, if $X_1 \text{MUST}_{\text{aux}} r$ and $X_1 \stackrel{\varepsilon}{\Rightarrow} X_2$ then $X_2 \text{MUST}_{\text{aux}} r$.

**Lemma 42.** For every LTS $\mathcal{L}_A, \mathcal{L}_B$ and every $X \in \mathcal{P}^+(A)$ and $r \in B$, if $X \text{MUST}_{\text{aux}} r$ then for every $X'$ such that

(a) If $X \stackrel{\varepsilon}{\Rightarrow} X'$ then $X' \text{MUST}_{\text{aux}} r$,
(b) For any $\mu \in \text{Act}$ and client $r'$, if $X \stackrel{\mu}{\Longrightarrow} X'$, $r \xrightarrow{\bar{\mu}} r'$ and $\neg\text{GOOD}(r)$, then $X' \text{MUST}_{\text{aux}} r'$.

**Lemma 43.** Given two LTS $\mathcal{L}_A$ and $\mathcal{L}_B$ then for every $X \in \mathcal{P}^+(A)$ and $r \in B$, if for each $p \in X$ we have that $p \text{MUST}_i r$, then $X \text{MUST}_{\text{aux}} r$.

**Lemma 44.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$ and $\mathcal{L}_C \in \text{FDB}$. For every $X \in \mathcal{P}^+(A)$ and $q \in B$ such that $X \preceq_{\text{AS}}^{\text{set}} q$, for every $r \in C$ if $\neg\text{GOOD}(r)$ and $X \text{MUST}_{\text{aux}} r$ then $q \Vdash r \xrightarrow{\tau} \bar{r}$.

*Proof.* If either $q \xrightarrow{\tau} \bar{r}$ or $r \xrightarrow{\tau} \bar{r}$ then we prove that $q \Vdash r$ performs a $\tau$-transition vis [S-SRV]or [S-CLT], so suppose that both $q$ and $r$ are stable. Since $q$ is stable we know that

$$ \mathcal{A}_{\text{fw}}(q, \varepsilon) = \{O(q)\} $$

The hypotheses $\neg\text{GOOD}(r)$ and $X \text{MUST}_{\text{aux}} r$ together with Lemma 40 imply $X \downarrow_i$ and thus $X \downarrow \varepsilon$. The hypothesis $X \preceq_{\text{acc}}^{\text{set}} q$ with $s = \varepsilon$, gives us a $p'$ such that $p \stackrel{\varepsilon}{\Longrightarrow} p' \xrightarrow{\tau} \bar{p}$ and $O(p') \subseteq O(q)$. By definition there exists the weak silent trace $X \Longrightarrow X'$ for some set $X'$ such that $\{p'\} \subseteq X'$. The hypothesis $X \text{MUST}_{\text{aux}} r$ together with Lemma 41 and Lemma 39 ensure that $\{p'\} \text{MUST}_{\text{aux}} r$.

As $\neg\text{GOOD}(r)$, $\{p'\} \text{MUST}_{\text{aux}} r$ must have been derived using rule [IND-RULE] which implies that $p' \Vdash r \xrightarrow{\tau} \bar{r}$. As both $r$ is stable by assumption, and $p'$ is stable by definition, this $\tau$-transition must have been derived using [S-COM], and so $p' \xrightarrow{\mu} \bar{p}$ and $r \xrightarrow{\bar{\mu}} \bar{r}$ for some $\mu \in \text{Act}$. Now we distinguish whether $\mu$ is an input or an output. In the first case $\mu$ is an input. Since $\mathcal{L}_B \in \text{FWD}$ we use the INPUT-BOOMERANG axiom to prove $q \xrightarrow{\mu} \bar{q}$, and thus $q \Vdash r \xrightarrow{\tau} \bar{r}$ via rule [S-COM]. In the second case $\mu$ is an output, and so the inclusion $O(p') \subseteq O(q)$ implies that $q \xrightarrow{\mu} \bar{q}$, and so we conclude again applying rule [S-COM].

**Lemma 45.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$. For every $X \in \mathcal{P}^+(A)$ and $q, q' \in B$, such that $X \preceq_{\text{AS}}^{\text{set}} q$, then for every $\mu \in \text{Act}$, if $X \downarrow \mu$ and $q \xrightarrow{\mu} \bar{q}$ then $X \stackrel{\mu}{\Longrightarrow} \bar{q}$.

*Proof.* Then, from $X \preceq_{\text{cnv}}^{\text{set}} q$ and $X \downarrow \mu$ we have that $q \downarrow \mu$ and thus $q' \downarrow_i$. As $q'$ converges, there must exist $q''$ such that

$$ q \stackrel{\mu}{\Longrightarrow} q' \stackrel{\varepsilon}{\Longrightarrow} q'' \xrightarrow{\tau} \bar{q} $$

and so $\mathcal{A}_{\text{fw}}(q, \mu, \to_B) \neq \emptyset$. An application of the hypothesis $X \preceq_{\text{acc}}^{\text{set}} q$ implies that there exists a set $\hat{O} \in \mathcal{A}_{\text{fw}}(X, \mu, \to_A)$, and thus there exist two servers $p' \in X$ and $p''$ such that $p' \stackrel{\mu}{\Longrightarrow} p'' \xrightarrow{\tau} \bar{p}$. Since $p' \in X$ it follows that $X \stackrel{\mu}{\Longrightarrow} \bar{q}$.

**Lemma 36** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$. For every set $X \in \mathcal{P}^+(A)$, and $q \in B$, such that $X \preceq_{\text{cnv}}^{\text{set}} q$ then

1. $q \xrightarrow{\tau} q'$ implies $X \preceq_{\text{cnv}}^{\text{set}} q'$,

2. if $X \downarrow_i$ and $q \xrightarrow{\mu} \bar{q}'$ then for every set $X \stackrel{\mu}{\Longrightarrow} X'$ we have that $X' \preceq_{\text{cnv}}^{\text{set}} q'$.
*Proof.* We first prove part (1). Let us fix a trace $s$ such that $X \downarrow s$. We must show $q' \downarrow s$. An application of the hypothesis $X \preceq_{\text{cnv}}^{\text{set}} q$ ensures $q \downarrow s$. From the transition $q \xrightarrow{\tau} q'$ and the fact that convergence is preserved by the $\tau$-transitions we have that $q' \downarrow s$ as required.

We now prove part (2). Fix a trace $s$ such that $X' \downarrow s$. Since $q \xrightarrow{\mu} q'$, the required $q' \downarrow s$ follows from $q \downarrow \mu.s$. Thanks to the hypothesis $X \preceq_{\text{cnv}}^{\text{set}} q$ it suffices to show that $X \downarrow \mu.s'$, i.e. that

$$ \forall p \in X. p \downarrow \mu.s' $$

Fix a server $p \in X$. We must show that

1. $p \downarrow_i$ and that

2. for any $p'$ such that $p \xrightarrow{\mu} p'$ we have $p' \downarrow s$.

The first requirement follows from the hypothesis $X \downarrow_i$. The second requirement follows from the transition $p \xrightarrow{\mu} p'$, from the assumption $X' \downarrow s$, and the hypothesis that $X \xrightarrow{\mu} X'$, which ensures that $p' \in X'$ and thus by definition of $X' \downarrow s$ that $p' \downarrow s$.

**Lemma 37** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$. For every $X, X' \in \mathcal{P}^+(A)$ and $q \in B$, such that $X \preceq_{\text{acc}}^{\text{set}} q$, then

1. $q \xrightarrow{\tau} q'$ implies $X \preceq_{\text{acc}}^{\text{set}} q'$,

2. for every $\mu \in \text{Act}$, if $X \downarrow_i$, then for every $q \xrightarrow{\mu} q'$ and set $X \xrightarrow{\mu} X'$ we have $X' \preceq_{\text{acc}}^{\text{set}} q'$.

*Proof.* To prove part (1) fix a trace $s \in \text{Act}^*$ such that $X \downarrow s$. We have to explain why $\mathcal{A}_{\text{fw}}(X, s) \ll \mathcal{A}_{\text{fw}}(q', s)$. By unfolding the definitions, this amounts to showing that

$$ \forall O \in \mathcal{A}_{\text{fw}}(q', s). \exists p_{\text{attaboy}} \in X. \exists \hat{O} \in \mathcal{A}_{\text{fw}}(p_{\text{attaboy}}, s). \hat{O} \subseteq O \quad (*) $$

Fix a set $O \in \mathcal{A}_{\text{fw}}(q', s)$. By definition there exists some $q''$ such that $q' \xrightarrow{s} q'' \xrightarrow{\tau},$ and that $O = O(q'')$. The definition of $\mathcal{A}_{\text{fw}}(-, -)$ and the silent move $q \xrightarrow{\tau} q'$ ensures that $O \in \mathcal{A}_{\text{fw}}(q, s)$. The hypothesis $X \preceq_{\text{acc}}^{\text{set}} q$ and that $X \downarrow s$ now imply that $\mathcal{A}_{\text{fw}}(X, s) \ll \mathcal{A}_{\text{fw}}(q, s)$, which together with $O \in \mathcal{A}_{\text{fw}}(q, s)$ implies exactly Equation $(\star)$.

We now prove part (2). To show $X' \preceq_{\text{acc}}^{\text{set}} q'$ fix a trace $s \in \text{Act}^*$ such that $X' \downarrow s$.

We have to explain why $\mathcal{A}_{\text{fw}}(X, s) \ll \mathcal{A}_{\text{fw}}(q', s)$. By unfolding the definitions we obtain our aim,

$$ \forall O \in \mathcal{A}_{\text{fw}}(q', s). \exists p_{\text{attaboy}} \in X'. \exists \hat{O} \in \mathcal{A}_{\text{fw}}(p_{\text{attaboy}}, s). \hat{O} \subseteq O \quad (\star\star) $$

To begin with, we prove that $X \downarrow \mu.s$. Since $X \xrightarrow{\mu} X'$ we know that $X \xrightarrow{\mu} X'$. This, together with $X \downarrow_i$ and $X' \downarrow s$ implies the convergence property we are after.
Now fix a set $O \in \mathcal{A}_{fw}(q', s)$. Thanks to the transition $q \xrightarrow{\mu} q'$, we know that $O \in \mathcal{A}_{fw}(q, \mu.s)$. The hypothesis $X \preceq_{acc}^{\text{set}} q$ together with $X \Downarrow \mu.s$ implies that there exists a server $p_{\text{attaboy}} \in X$ such that there exists an $\hat{O} \in \mathcal{A}_{fw}(p_{\text{attaboy}}, \mu.s)$. This means that $p_{\text{attaboy}} \overset{\mu}{\implies} p'_{\text{attaboy}}$ and that $\hat{O} \in \mathcal{A}_{fw}(p'_{\text{attaboy}}, s)$. Since $X \implies X'$ we know that $p'_{\text{attaboy}} \in X'$ and this concludes the argument.

**Lemma 46.** For every $\mathcal{L}_A \in \text{FWD}$, $\mathcal{L}_B \in \text{FDB}$, every set of processes $X \in \mathcal{P}^+(A)$, every $r \in B$, and every $\mu \in \text{Act}$, if $X_{\text{MUST}_{\text{aux}} r}$, $\neg\text{GOOD}(r)$ and $r \xrightarrow{\mu} X \Downarrow \bar{\mu}$ then $X \Downarrow \bar{\mu}$.

**Lemma 38** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$ and $\mathcal{L}_C \in \text{FDB}$. For every set of processes $X \in \mathcal{P}^+(A)$, server $q \in B$ and client $r \in C$, if $X_{\text{MUST}_{\text{aux}} r}$ and $X \preceq_{\text{AS}}^{\text{set}} q$ then $q_{\text{MUST}_i r}$.

*Proof.* We proceed by induction on the derivation of $X_{\text{MUST}_{\text{aux}} r}$. In the base case, $\text{GOOD}(r)$ so we trivially derive $q_{\text{MUST}_i r}$. In the inductive case the proof of the hypothesis $X_{\text{MUST}_{\text{aux}} r}$ terminates with an application of [MSET-STEP]. Since $\neg\text{GOOD}(r)$, we show the result applying [IND-RULE]. This requires us to prove that

(1) $q \Vdash r \xrightarrow{\tau},$ and that

(2) for all $q', r'$ such that $q \Vdash r \xrightarrow{\tau} q' \Vdash r'$ we have $q'_{\text{MUST}_i r'}$.

The first fact is a consequence of Lemma 44, which we can apply because $\neg\text{GOOD}(r)$ and thanks to the hypothesis $X \preceq_{\text{acc}}^{\text{set}} q$ and $X_{\text{MUST}_{\text{aux}} r}$. To prove the second fact, fix a transition $q \Vdash r \xrightarrow{\tau} q' \Vdash r'$. We have to explain why the following properties are true,

(a) for every $q'$. $q \xrightarrow{\tau} q'$ implies $q'_{\text{MUST}_i r}$,

(b) for every $r$. $r \xrightarrow{\tau} r'$ implies $q_{\text{MUST}_i r'}$,

(c) for every $q', r'$ and $\mu \in \text{Act}$, $q \xrightarrow{\mu} q'$ and $r \xrightarrow{\bar{\mu}} r'$ imply $q'_{\text{MUST}_i r'}$.

First, note that $X_{\text{MUST}_{\text{aux}} r}$, $\neg\text{GOOD}(r)$, and Lemma 40 imply $X \downarrow$. Second, the inductive hypotheses state that for every $r'$, non-empty set $X'$, and $q$ the following facts hold,

(i) $X \xrightarrow{\tau} X'$ and $X' \preceq_{\text{AS}}^{\text{set}} q$ implies $q_{\text{MUST}_i r}$,

(ii) $r \xrightarrow{\tau} r'$ and $X \preceq_{\text{AS}}^{\text{set}} q$ implies $q_{\text{MUST}_i r'}$,

(iii) for every and $\mu \in \text{Act}$, $X \xrightarrow{\bar{\mu}} X'$ and $r \xrightarrow{\mu} r'$, and $X' \preceq_{\text{AS}}^{\text{set}} q$ implies $q_{\text{MUST}_i r'}$.

To prove (a) we use $X \downarrow$ and the hypothesis $X \preceq_{\text{cnv}}^{\text{set}} q$ to obtain $q \downarrow_i$. A rule induction on $q \downarrow_i$ now suffices: in the base case (a) is trivially true and in the inductive case (a) follows from Lemma 36(1) and Lemma 37(1), and the inductive hypothesis.

The requirement (b) follows directly from the hypothesis $X \preceq_{\text{AS}}^{\text{set}} q$ and part (ii) of the inductive hypothesis.
To see why (c) holds, fix an action $\mu$ such that $q \xrightarrow{\mu} q'$ and $r \xrightarrow{\bar{\mu}} r'$. Since $\neg GOOD(r)$ Lemma 46 implies that $X \downarrow \mu$, and so Lemma 45 proves that $X \xrightarrow{\mu}$. In turn this implies that there exists a $X'$ such that $X \xrightarrow{\mu} X'$, and thus Lemma 36(2) and Lemma 37(2) prove that $X' \preceq_{\text{AS}}^{\text{set}} q'$ holds, and (iii) ensures the result, i.e. that $q'_{\text{MUST}_i} r'$.

## F Technical details about coinduction

Here we outline the lemma that lets us prove Equation (9).

**Lemma 47.** For every mailbox M and every set X of processes, we have

$$ \{\tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c}) \triangleright M\} \cup X \preceq_{\text{co}} \bar{a} \parallel (\tau.\bar{b} + \tau.\bar{c}) \triangleright M. \quad (\text{CH}) $$

*Proof (sketch).* Let M be a mailbox and X be a set of processes. We focus on the last point of Definition 12, for the other cases are similar. Consider an arbitrary reduction of the RHS of Equation (CH):

$$ \bar{a} \parallel (\tau.\bar{b} + \tau.\bar{c}) \triangleright M \xrightarrow{\mu} q \quad (10) $$

We proceed by case analysis.

1. The cases that correspond to a reduction of the mailbox M are dealt with directly using the coinductive hypothesis (CH), since the mailbox is quantified universally in (CH). In more detail, consider the case where the reduction (10) is of the form:

$$ \bar{a} \parallel (\tau.\bar{b} + \tau.\bar{c}) \triangleright M \xrightarrow{b} \bar{a} \parallel (\tau.\bar{b} + \tau.\bar{c}) \triangleright \{\bar{b}\} \uplus M $$

Let $X'$ be $WD(b, \{\tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c}) \triangleright M\} \uplus X)$, that is, the unique set of processes such that

$$ \{\tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c}) \triangleright M\} \cup X \xrightarrow{b} X' $$

It is easy to prove that $\{\tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c}) \triangleright \{\bar{b}\} \uplus M\} \in X'$ and thus we conclude by applying the coinductive hypothesis (CH).

2. If (10) corresponds to a transition of the process, it must be that $\mu = \bar{a}$ and $q = \tau.\bar{b} + \tau.\bar{c} \triangleright M$. In that case, the set $X'$ of processes reached from $\{\tau.(\bar{a} \parallel \bar{b}) + \tau.(\bar{a} \parallel \bar{c}) \triangleright M\} \uplus X$ while outputting a contains $\bar{b}$ and $\bar{c}$, so that $X' \preceq_{\text{co}} q$ follows from the general fact that $\{p, q\} \subset_{\text{MUST}}^{\text{Set}} \tau.p + \tau.q$. $\square$

## G Traces in normal form

Let $MI$ be the set of multisets of input actions, and let $nf: \text{Act}^* \to (MI \times MO)^*$ be the function

$$ \text{nf}(s) = (I_0, M_0), (I_1, M_2), \dots, (I_n, M_n) $$
$$nf(\varepsilon) = \varepsilon$$

$$nf(s) = nf'(s, \emptyset, \emptyset)$$

$$nf'(\varepsilon, I, M) = (I, M)$$

$$nf'(a.s, I, M) = nf'(s, \{\emptyset\} \uplus I, M)$$

$$nf'(\bar{a}.s, I, M) = \begin{cases} (I, \{\emptyset\} \uplus M), nf'(s, I, \emptyset) & \text{if } s = b.s' \text{ for some } b, s' \\ nf'(s, I, \{\emptyset\} \uplus M) & \text{otherwise} \end{cases}$$

<caption>**Fig. 12.** Definition of the trace normalisation function nf</caption>

which is defined inductively in Figure 12. The intuition is that given a trace s, the function nf forgets the order of actions in sequences of consecutive inputs, and in sequences of consecutive outputs, thereby transforming them in multisets. On the other hand nf preserves the causal order in the trace, in the sense that the execution of all inputs in $I_k$ is necessary to execute any of the outputs in $M_k$, as well as the actions in the multisets at index h with $k < h$. For instance:

$$nf(cabddae\overline{e}f\overline{e}) = (\{\emptyset, a\}, \{\emptyset, \bar{b}, \bar{d}, \overline{d}\}), (\{\emptyset, a\}, \{\emptyset, \bar{c}, \overline{f}\}), (\{\emptyset, e\}, \emptyset)$$

Let $\sigma$ range over the set $(MI \times MO)^*$. We say that $\sigma$ is a trace in normal form, and we write $p \stackrel{\sigma}{\implies} q$, whenever there exists $s \in \text{Act}^*$ such that $p \stackrel{s}{\implies} q$ and $nf(s) = \sigma$.

**Definition 16.** We lift in the obvious way the predicates $\leq_{\text{cnv}}$, $\leq_{\text{acc}}$, and $\leq_{\text{fw}}^{\text{acc}}$ to traces in normal forms. For every $\mathcal{L}_A, \mathcal{L}_B$ and $p \in A, q \in B$, let

$$- p \leq_{\text{asyn}}^{\text{cnv}} q \text{ to mean } \forall \sigma \in (MI \times MO)^*. p \downarrow \sigma \text{ implies } q \downarrow \sigma,$$

$$- p \leq_{\text{asyn}}^{\text{acc}} q \text{ to mean } \forall \sigma \in (MI \times MO)^*. p \downarrow \sigma \text{ implies } \mathcal{A}_{\text{fw}}(p, \sigma) \ll \mathcal{A}_{\text{fw}}(q, \sigma),$$

$$- p \leq_{\text{AS}}^{\text{NF}} q \text{ whenever } q \leq_{\text{asyn}}^{\text{cnv}} p \wedge p \leq_{\text{asyn}}^{\text{acc}} q.$$

In LTSs with forwarding, the transition relation $\to$ is input-receptive (Axiom (IB4), Table 2 of [90]), and thus Lemma 48 shows that $\to$ enjoys a restricted version of INPUT-COMMUTATIVITY, and that so does its weak version. Sequences of input actions $s \in \mathcal{N}^*$ enjoy a form of diamond property in $\implies$. The crucial fact pertains consecutive input actions. Recall that $\simeq$ denotes any equivalence that satisfies the compatibility property depicted in Figure 5.

**Lemma 48.** For every $\mathcal{L} = (A, \text{Act}, \to) \in \text{FWD}$, every $p, q \in A$ and $a, b \in \mathcal{N}$, if $p \stackrel{a.b}{\implies} q$ then $p \stackrel{b.a}{\implies} \cdot \simeq q$.

Lemma 48, together with an induction on traces, allows us to prove that nf preserves convergence and acceptance sets.

**Lemma 49.** For every $\mathcal{L} = (A, \text{Act}, \to) \in \text{FWD}$, every $p \in A$ and $s \in \text{Act}^*$ we have that
<figure><img src="image_16.png" /><figcaption>Fig. 13. The LTS of processes. The meta-variables are $a \in \mathcal{N}$, $\mu \in \text{Act}$, and $\alpha \in \text{Act}_\tau$.</figcaption></figure>

1. $p \stackrel{s}{\rightleftharpoons} q \text{ iff } p \stackrel{\text{nf}(s)}{\rightleftharpoons} \cdot \approx q$, and if the first trace does not pass through a successful state then the normal form does not either,

2. $p \Downarrow \text{nf}(s) \text{ iff } p \Downarrow s$,

3. $A_{\text{fw}}(p, s) = A_{\text{fw}}(p, \text{nf}(s))$.

We thereby obtain two other characterisations of the contextual preorder $\preceq_{\text{MUST}}$: Theorem 1 and Lemma 49 ensure that the preorders $\preceq_{\text{MUST}}$ and $\preceq_{\text{AS}}^{\text{NF}}$ coincide.

**Corollary 4.** For every $\mathcal{L}_A$, $\mathcal{L}_B \in \text{FDB}$, every $p \in A$ and $q \in B$,

$$p \preceq_{\text{MUST}} q \text{ iff } \text{FW}(p) \preceq_{\text{AS}}^{\text{NF}} \text{FW}(q).$$

## H Asynchronous CCS

Here we recall the syntax and the LTS of asynchronous CCS, or ACCS for short, a version of CCS where outputs have no continuation and sum is restricted to input- and $\tau$-guards.

$$p, q, r ::= \underline{a} \mid g \mid p \parallel p \mid \text{recx.p} \mid x, \quad g ::= 0 \mid 1 \mid a.p \mid \tau.p \mid g + g$$

This calculus, which is inspired by the variant of the asynchronous $\pi$-calculus considered by [4,5] for their study of asynchronous bisimulation, was first investigated by [90], and subsequently resumed by other authors such as [23]. Different asynchronous variants of CCS were studied in the same frame of time by [80], whose calculus included output prefixing and operators from ACP, and by [38], whose calculus TACCS included asynchronous output prefixing and featured
two forms of choice, internal and external, in line with previous work on testing semantics [76].

The syntax of terms is given in Equation (5). As usual, recx.p binds the variable *x* in *p*, and we use standard notions of free variables, open and closed terms. Processes, ranged over by *p*, *q*, *r*,... are *closed* terms. The operational semantics of processes is given by the LTS $\langle \mathit{ACCS}, \mathit{Act}_\tau, \rightarrow \rangle$ specified by the rules in Figure 13.

The prefix *a.p* represents a *blocked* process, which waits to perform the input *a*, i.e. to interact with the atom $\bar{a}$, and then becomes *p*; and atoms $\bar{a}$, $\bar{b}$, ... represent output messages. We will discuss in detail the role played by atoms in the calculus, but we first overview the rest of the syntax. We include 1 to syntactically denote successful states. The prefix $\tau.p$ represents a process that does one step of internal computation and then becomes *p*. The sum $g_1 + g_2$ is a process that can behave as $g_1$ or $g_2$, but not both. Thus, for example $\tau.p + \tau.q$ models an *if ... then ... else*, while *a.p + b.q* models a *match ... with*. Note that the sum operator is only defined on *guards*, namely it can only take as summands 0, 1 or input-prefixed and $\tau$-prefixed processes. While the restriction to guarded sums is a standard one, widely adopted in process calculi, the restriction to input and $\tau$ guards is specific to asynchronous calculi. We will come back to this point after discussing atoms and mailboxes. Parallel composition $p \parallel q$ runs *p* and *q* concurrently, allowing them also to interact with each other, thanks to rule [COM]. For example

$$ b.a. 0 \parallel b.c. 0 \parallel (\bar{a} \parallel \bar{b} \parallel \bar{c}) \qquad (11) $$

represents a system in which two concurrent processes, namely *b.a. 0* and *b.c. 0*, are both ready to consume the message $\bar{b}$ from a third process, namely $\bar{a} \parallel \bar{b} \parallel \bar{c}$. This last process is a parallel product of atoms, and it is not guarded, hence it is best viewed as an unordered mailbox shared by *all* the processes running in parallel with it. For instance in (11) the terms *b.a. 0* and *b.c. 0* share the mailbox $\bar{a} \parallel \bar{b} \parallel \bar{c}$. Then, depending on which process consumes $\bar{b}$, the overall process will evolve to either *b.c. 0* $\parallel \bar{c}$ or *b.a. 0* $\parallel \bar{a}$, which are both stuck.<fnref n="13" />

Concerning the sum construct, we follow previous work on asynchronous calculi ([4,5,87,23]) and only allow input-prefixed or $\tau$-prefixed terms as summands. The reason for forbidding atoms in sums is that the nondeterministic sum is essentially a synchronising operator: the choice is solved by executing an action in one of the summands and *simultaneously* discarding all the other summands. Then, if an atom were allowed to be a summand, this atom could be discarded by performing an action in another branch of the choice. This would mean that a

<footnote n="13">¹³ The global shared mailbox that we treat is reminiscent but less general than the chemical “soup” of [17]. In that context the components of the soup are not just atoms, but whole parallel components: in fact, the chemical soup allows parallel components to come close in order to react with each other, exactly as the structural congruence of [73], which indeed was inspired by the Chemical Abstract Machine.</footnote>
process would have the ability to withdraw a message from the mailbox without consuming it, thus contradicting the intuition that the mailbox is a shared entity which is out of the control of any given process, and with which processes can only interact by feeding a message into it or by consuming a message from it. In other words, this restriction on the sum operator ensures that atoms indeed represent messages in a global mailbox. For further details see the discussion on page 191 of [87].

A structural induction on the syntax ensures that processes perform only a finite number of outputs:

**Lemma 50.** For every $p \in \mathbf{ACCS}$. $|O(p)| \in \mathbb{N}$.

Together with Lemma 53, this means that at any point of every execution the global mailbox contains a finite number of messages. Since the LTS is image-finite under any visible action, a consequence of Lemma 50 is that the number of reducts of a program is finite.

**Lemma 51.** For every $p \in \mathbf{ACCS}$. $|\{p' \in \mathbf{ACCS} | p \xrightarrow{\tau} p'\}| \in \mathbb{N}$.

*Proof.* Structural induction on $p$. The only non-trivial case is if $p = p_1 \parallel p_2$. In this case the result is a consequence of the inductive hypothesis, of Lemma 50 and of the following fact: $p \xrightarrow{\tau} q$ iff

1. $p_1 \xrightarrow{\tau} p'_1$ and $q = p'_1 \parallel p_2$,

2. $p_2 \xrightarrow{\tau} p'_2$ and $q = p_1 \parallel p'_2$,

3. $p_1 \xrightarrow{a} p'_1$ and $p_2 \xrightarrow{\bar{a}} p'_2$ and $q = p'_1 \parallel p'_2$,

4. $p_1 \xrightarrow{\bar{a}} p'_1$ and $p_2 \xrightarrow{a} p'_2$ and $q = p'_1 \parallel p'_2$.

In the third case the number of possible output actions $\bar{a}$ is finite thanks to Lemma 50, and so is the number of reducts $p'_1$ and $p'_2$, so the set of term $p'_1 \parallel p'_2$ is decidable. The same argument works for the fourth case.

Thanks to Lemma 50 and Lemma 51, Lemma 51 holds also for the LTS modulo structural congruence, i.e. $\langle \mathbf{ACCS}_{\equiv}, \rightarrow_{\equiv}, \mathbf{Act}_{\tau} \rangle$.

## H.1 Structural equivalence and its properties

To manipulate the syntax of processes we use a standard structural congruence denoted $\equiv$, stating that $\mathbf{ACCS}$ is a commutative monoid with identity $0$ with respect to both sum and parallel composition.

A first fact is the following one.

**Lemma 52.** For every $\mu \in \overline{\mathcal{N}}$ and $\alpha \in \mathbf{Act}_{\tau}$, if $p \stackrel{\mu.\alpha}{\implies} q$ then $p \stackrel{\alpha.\mu}{\implies} \cdot \equiv q$.

As sum and parallel composition are commutative monoids, we use the notation

$\Sigma\{g_0, g_1, \dots, g_n\}$ to denote $g_0 + g_1 + \dots + g_n$

$\Pi\{p_0, p_1, \dots, p_n\}$ to denote $p_0 \parallel p_1 \parallel \dots \parallel p_n$
Class LtsEq (A L : Type) ˘{Lts A L} := {
  eq_rel : A Æ A Æ Prop;
  eq_rel_refl p : eq_rel p p;
  eq_symm p q : eq_rel p q Æ eq_rel q p;
  eq_trans p q r :
    eq_rel p q Æ eq_rel q r Æ eq_rel p r;
  eq_spec p q (α : Act L) :
    (∃ p', (eq_rel p p') ∧ p' —> {α} q)
    →
    (∃ q', p —> {α} q' ∧ (eq_rel q' q))
}.

<caption>**Fig. 14.** A typeclass for LTSs where a structural congruence exists over states.</caption>

This notation is useful to treat the global shared mailbox. In particular, if
{µ₀, µ₁, ..., µₙ} is a multiset of output actions, then the syntax Π{µ₀, µ₁, ..., µₙ}
represents the shared mailbox that contains the messages µᵢ; for instance we have
Π{ā, a, c} = |ā||a||c|. We use the colour — to highlight the content of the
mailbox. Intuitively a shared mailbox contains the messages that are ready to
be read, i.e. the outputs that are immediately available (i.e. not guarded by any
prefix operation). For example in

$$
\bar{c} \parallel a.(\bar{b} \parallel c.d. 1) \parallel \bar{d} \parallel \tau.\bar{c}
$$

the mailbox is $\bar{c} \parallel \bar{d}$. The global mailbox that we denote with $-$ is exactly the buffer $B$ in the configurations of [94], and reminiscent of the $\omega$ used by [27]. The difference is that $\omega$ represents an unbounded ordered queue, while our mailbox is an unbounded unordered buffer.

As for the relation between output actions in the LTS and the global mailbox,
an output $\bar{a}$ can take place if and only if the message $\bar{a}$ appears in the mailbox:

**Lemma 53.** For every $p \in \mathbf{ACCS}$,

1. for every $a \in \mathcal{N}$. $p \xrightarrow{\bar{a}} p'$ implies $p \equiv p' \parallel \bar{a}$,

2. there exists $p'$ such that $p \equiv p' \parallel \Pi M$, and $p'$ performs no output action.

This lemma and Lemma 52 essentially hold, because, as already pointed out in
Section 2, the syntax enforces outputs to have no continuation.

The following lemma states a fundamental fact ([58, Lemma 2.13], [74, Proposition 5.2], [87, Lemma 1.4.15]). Its proof is so tedious that even the references we have given only sketch it. In this paper we follow the masters example, and give merely a sketch. However, we have a complete machine-checked proof.
$$
\begin{align*}
& [S\text{-SZERO}] \quad p + 0 \equiv p \\
& [S\text{-SCOM}] \quad p + q \equiv q + p \\
& [S\text{-SASS}] \quad (p + q) + r \equiv p + (q + r)
\end{align*}
$$

$$
\begin{align*}
& [S\text{-PZERO}] \quad p \parallel 0 \equiv p \\
& [S\text{-PCOM}] \quad p \parallel q \equiv q \parallel p \\
& [S\text{-PASS}] \quad (p \parallel q) \parallel r \equiv p \parallel (q \parallel r)
\end{align*}
$$

$$
\begin{align*}
& [S-REFL] \quad p \equiv p \\
& [S-SYMM] \quad p \equiv q && \text{if } q \equiv p \\
& [S-TRANS] \quad p \equiv q && \text{if } p \equiv p' \text{ and } p' \equiv q
\end{align*}
$$

$$
\begin{align*}
& [S-PREFIX] \quad \alpha.p \equiv \alpha.q && \text{if } p \equiv q \\
& [S-SUM] \quad p + q \equiv p' + q && \text{if } p \equiv p' \\
& [S-PPAR] \quad p \parallel q \equiv p' \parallel q && \text{if } p \equiv p'
\end{align*}
$$

<caption>Fig. 15. Rules to define structural congruence on ACCS.</caption>

**Lemma 54.** For every $p, q \in \mathbf{ACCS}$ and $\alpha \in \mathbf{Act}_\tau$, $p \equiv \alpha \xrightarrow{\alpha} q$ implies $p \xrightarrow{\alpha} \equiv q$.

*Proof (Proof sketch).* We need to show that if there exists a process $p'$ such that $p \equiv p'$ and $p' \xrightarrow{\alpha} q$ then there exists a process $q'$ such that $p \xrightarrow{\alpha} p'$ and $p' \equiv q$. The proof is by induction on the derivation $p \equiv p'$.

We illustrate one case with the rule [S-TRANS]. The hypotheses tell us that
there exists $\hat{p}$ such that $p \equiv \hat{p}$ and $\hat{p} \equiv p'$, that $p' \xrightarrow{\alpha} q$, and the inductive
hypotheses that

(a) for all $q' \text{ s.t } \hat{p} \xrightarrow{\alpha} q'$ implies that there exists a $\hat{q}$ such that $p \xrightarrow{\alpha} \hat{q}$ and
$\hat{q} \equiv q'$

(b) for all $q' \text{ s.t } p' \xrightarrow{\alpha} q'$ implies that there exists a $\hat{q}$ such that $\hat{p} \xrightarrow{\alpha} \hat{q}$ and
$\hat{q} \equiv q'$

By combining part (b) and $p' \xrightarrow{\alpha} q$ we obtain a $\hat{q}_1$ such that $\hat{p} \xrightarrow{\alpha} \hat{q}_1$ and
$\hat{q}_1 \equiv q$. Using part (a) together with $\hat{p}_1 \xrightarrow{\alpha} \hat{q}_1$ we have that there exists a $\hat{q}_2$
such that $p \xrightarrow{\alpha} \hat{q}_2$ and $\hat{q}_2 \equiv \hat{q}_1$. We then have that $p \xrightarrow{\alpha} \hat{q}_2$ and it remains to
show that $\hat{q}_2 \equiv q$. We use the transitivity property of the structural congruence
relation to show that $\hat{q}_2 \equiv \hat{q}_1$ and $\hat{q}_1 \equiv q$ imply $\hat{q}_2 \equiv q$ as required and we are
done with this case.

Time is a finite resource. The one spent to machine check Lemma 54 would
have been best invested into bibliographical research. Months after having im-
plemented the lemma we realised that [3] already had an analogous result for
a mechanisation of the π-calculus. Lemma 54 is crucial to prove the Harmony
Lemma, which states that τ-transitions coincide with the standard reduction