# An Abstract Account of Up-to Techniques for Inductive Behavioural Relations

Davide Sangiorgi

► To cite this version:

Davide Sangiorgi. An Abstract Account of Up-to Techniques for Inductive Behavioural Relations. ISoLA 2024 - 12th International Symposium Leveraging Applications of Formal Methods Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola, Oct 2024, Crete Island, Greece. pp.62-74, 10.1007/978-3-031-73709-1_5 . hal-04827142

HAL Id: hal-04827142

https://hal.science/hal-04827142v1

Submitted on 9 Dec 2024

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>
# An abstract account of up-to techniques for inductive behavioural relations

Davide Sangiorgi

University of Bologna and INRIA

**Abstract.** 'Up-to techniques' represent enhancements of the coinduction proof method and are widely used on coinductive behavioural relations such as bisimilarity. Abstract formulations of these coinductive techniques exist, using fixed-points or category theory.

A proposal has been recently put forward [27] for transporting the enhancements onto the concrete realms of *inductive* behavioural relations, i.e., relations defined from inductive observables, such as traces or enriched forms of traces. The abstract meaning of such 'inductive enhancements', however, has not been explored. In this paper, we review the theory, and then propose an abstract account of it, using fixed-point theory in complete lattices.

# 1 Introduction

The recent paper [27] presents an attempt at transporting the well-known theory of enhancements for *coinductive* behavioural relations such as bisimilarity (the so-called ‘*up-to techniques*’) onto the realms of *inductive* behavioural relations, i.e., relations defined from inductive observables, such as traces or enriched forms of traces [8]. Abstract formulations of the theories of coinductive enhancements exist, using fixed-points or category theory [20]. However, the abstract meaning of the ‘inductive enhancements’ [27] is unclear, both because the observables are inductive and because of the coinductive flavour of some of the constructions at the heart of the theory. In this paper we give an overview of the concrete theory in [27], and then propose an abstract account of it, using fixed-point theory in complete lattices.

The motivation for transporting the bisimulation enhancements onto inductive behavioural relations is twofold. (We focus on the bisimulation enhancements, as bisimilarity is the most important coinductive behavioural relation and its enhancements are, by far, the most widely used.) First, the bisimulation enhancements can be very effective in proofs. The enhancements build on the bisimulation proof method, whereby, to prove two terms bisimilar, one finds a bisimulation relation, that is, a relation invariant under the observables of the language (i.e., what can be observed of the terms). In the enhancements, the invariance is allowed to hold ‘up-to’ certain functions on the relation. Examples of such ‘up-to functions’ include ‘up-to context’, ‘up-to transitive closure’, ‘up-to bisimilarity’, ‘up-to environment’ [20]. Most important, the theories of enhancements allow one to *combine* enhancements so to obtain, for free, the soundness
of more complex enhancements [23, 16, 17]. Sometimes the enhancements seem
essential to be able to carry out a proof: defining a full bisimulation, with all
needed pairs, can be considerably hard, let alone carrying out the necessary
checks (see e.g., [22]). This is frequent in languages for name mobility stemming
from the π-calculus and in languages including higher-order features such as
λ-calculi. Indeed, in these languages bisimilarity is hardly ever applied without
enhancements.

The other major motivation for transporting the bisimulation enhancements
onto inductive behavioural relations has to do with the criticism that has been
raised against bisimilarity. To begin with, bisimilarity is sometimes regarded
as too fine, discriminating processes that an external observer could not tell
apart. Thus, for instance, in the CSP community failure equivalence [3] is used
in place of bisimilarity. Another argument against bisimilarity is that it does
not have a natural associated preorder. For instance, similarity — the ‘one-
way’ bisimilarity — or variants of it, do not yield bisimilarity as their induced
equivalence [25]. Further, similarity as a behavioural preorder is often inadequate
because it does not respect deadlocks. Various inductive behavioural relations,
both preorders and equivalences, have been put forward and studied that improve
on such limitations: examples are preorders based on traces, failures, ready sets,
refusals, may and must testing, ready and failure traces, see, e.g., [3, 4, 6, 14, 15, 1,
11, 13, 9, 8]. We call these relations and their enhancements ‘inductive’ because
their observables are inductively defined, though this represents an abuse of
terminology as only the observables are inductive objects.

In abstract formulations of coinduction using fixed-point theory in complete
lattices, the coinductive objects are greatest fixed-points of monotone functions.
The coinductive enhancements can then be explained by means of composition
of these functions with auxiliary functions (the 'up-to' functions). Appropriate
conditions on the composition of the two functions guarantee that the post-fixed
points of the composed function remain below the initial coinductive object [19].

In the abstract presentation of inductive enhancements in this paper, a dif-
ference is that one reasons about meets (i.e., greatest lower bounds) of chains of
decreasing points in the lattice, starting from the top element. Then, the func-
tions of interest, the *valid* functions for a given chain, are those whose post-fixed
points are below the points of the chain – they need not be functions that produce
the points of the chain by iteration of the application of the function to the top
element. Valid functions are then enhanced by means of *approximant-preserving
functions*. These are, intuitively functions that ‘respect the approximants’ (i.e.,
the points in the chain). They are the analogous of the ‘up-to functions’ of the
coinductive setting.

In the concrete setting of inductive behavioural relations [27], the inductive
observables are described by means of modal formulas, precisely subsets of the
positive fragment of Hennessy-Milner logic with the possible addition of atomic
observables. A *weight* can thus be associated to each observable, intuitively ex-
pressing the depth of the nesting of actions in the behaviour of a process that
may have be looked at when checking that observable. Approximants are then
obtained by placing bounds on the weights of the observables employed. The enhancements proposed in [27] are functions $\mathcal{F}$ on relations that are weight-preserving for a given preorder $\prec$, i.e., whenever a relation $\mathcal{R}$ complies with the $n$-th approximant $\prec_n$ of the preorder, then also $\mathcal{F}(\mathcal{R})$ complies (i.e., $\mathcal{R} \subseteq \prec_n$ implies $\mathcal{F}(\mathcal{R}) \subseteq \prec_n$). Such enhancements are used within semi-progressions between process relations. A semi-progression from $\mathcal{R}$ to $\mathcal{S}$ indicates a match in the immediate actions from pairs of processes in $\mathcal{R}$ (akin to the match required in a simulation relation) in which the derivatives (i.e., the processes resulting from performing such actions) are in $\mathcal{S}$. The soundness theorem states that, for any function $\mathcal{F}$ that is weight-preserving for a preorder $\prec$, a semi-progression from $\mathcal{R}$ to $\mathcal{F}(\mathcal{R})$ allows us to conclude that the relation $\mathcal{R}$ is contained in $\prec$.

When relating this concrete setting to the abstract one using fixed-points in complete lattices briefly described above: the set of all process relations is the complete lattice; the sequence of weight-based approximants of a behavioural preorder is a chain of decreasing points in the lattice; the preorder itself is the meet of the chain; the semi-progressions yield valid functions; and the weight-preserving functions are the approximant-preserving functions.

The theory in this paper, as well as that in [27], is parametrised on a set of inductive observables, that is, a preorder. See [27] for examples of proofs of results about behavioural preorders that are *parametric* on a preorder, hence applicable to a number of preorders. In this paper we only consider ‘strong’ semantics, i.e., Labeled Transition Systems in which all actions are equally visible.

*Structure of the paper* Sections 2 and 3 collect the main background. Section 4 presents the abstract setting based on complete lattices, post-fixed points, and chains of approximants. Finally, Section 5 reports the main related work and some possible directions for future work.

## 2 Inductive observables and weights

In this section we recall the definitions of inductive observables and preorders from [27], and their approximants using weights. We work on ordinary *Labeled Transition Systems (LTSs)*, i.e., triples $(Pr, Act, \rightarrow)$ with domain $Pr$, set of actions (or labels) $Act$, and transition relation $\rightarrow \subseteq Pr \times Act \times Pr$. We use $P, Q$ and $R$ to range over $Pr$ and call them *processes*; $\mu$ ranges over the actions. As usual $P \xrightarrow{\mu} Q$ stands for $(P, \mu, Q) \in \rightarrow$, to be interpreted as “$P$ may become $Q$ by performing an action $\mu$”. We write $P \xrightarrow{\mu} \lambda$ if there is $P'$ with $P \xrightarrow{\mu} P'$, and $P \xrightarrow{\lambda} \lambda$ if there is no $P'$ such that $P \xrightarrow{\lambda} P'$. We use $n$ to range over the natural numbers; letters $I$ and $J$ for countable indexing sets in unions, conjunctions, and similar; $i, j$ to range over countable sets.

### 2.1 Inductive observables

The observables are described by means of modal formulas. The operators include the ‘diamond’ $\langle \mu \rangle$. $\theta$, to detect the possibility of performing the action $\mu$, a
(possibly infinitary) 'and', to permit multiple observations, and a set of atomic observables. Without the atomic observables, this is the positive fragment of Hennessy-Milner logic [10].

**Definition 1.** Let Act and $\mathcal{A}$ be (countable) sets of actions and of atomic observables. A family of observables (over Act and $\mathcal{A}$) is a subset $\mathcal{O}$ of the formulas inductively generated by the following grammar:

$$ \theta := \langle \mu \rangle . \theta \mid \bigwedge_{j \in J} \theta_j \mid \mathbf{a} $$

where $\mu \in \text{Act}$, $\mathbf{a} \in \mathcal{A}$, $J$ is a countable set, and:

- (downward-closure) if $\langle \mu \rangle . \theta \in \mathcal{O}$ then also $\theta \in \mathcal{O}$, and similarly if $\bigwedge_{j \in J} \theta_j \in \mathcal{O}$ then also $\theta_j \in \mathcal{O}$ for each $j$.

We write true for the formula corresponding to the empty conjunction, and $\theta_1 \wedge \theta_2$ for a binary conjunction. We let $\mathcal{O}$ range over families of observables, and $\theta, \zeta$ over observables.

The observables of a family $\mathcal{O}$ are meant to be interpreted as predicates over the processes of an LTS over the same set of actions, and accordingly we write $P \models \theta$ when the observable $\theta$ holds on the process $P$. The interpretation is defined structurally over the observables, writing $\llbracket \mathbf{a} \rrbracket$ for the set of processes on which the atomic observable $\mathbf{a}$ holds:

$$ \text{AT} \quad \frac{P \in \llbracket \mathbf{a} \rrbracket}{P \models \mathbf{a}} \qquad \text{ACT} \quad \frac{P \xrightarrow{\mu} P' \qquad P' \models \theta}{P \models \langle \mu \rangle . \theta} \qquad \text{CONJ} \quad \frac{P \models \theta_j \quad \text{for all } j \in J}{P \models \bigwedge_{j \in J} \theta_j} $$

The observable true is satisfied by all processes. An example of atomic observable is the refusal $\mathbf{ref}_\mu$, which holds of a process $P$ and an action $\mu$ if $P \xrightarrow{\mu} \mathbf{a}$. All atomic observables should be local: they can be checked by looking only at the immediate outgoing transitions emanating from a process. That is, for each such observable, say $\mathbf{a}$, there are sets of actions $A$ and $B$ such that for all process $P$, we have $P \in \llbracket \mathbf{a} \rrbracket$ iff $(P \xrightarrow{\mu} A \qquad P \xrightarrow{\mu} B)$ for all $\mu \in A$, and $P \xrightarrow{\mu} B$ for all $\mu \in B)$. For instance, for the refusal $\mathbf{ref}_\mu$, we have $A = \emptyset$ and $B = \{\mu\}$.

**Definition 2 (preorder induced by $\mathcal{O}$).** A family $\mathcal{O}$ of observables induces a preorder $\preceq^\mathcal{O}$ on the processes, whereby $P \preceq^\mathcal{O} Q$ if $P \models \theta$ implies $Q \models \theta$ for all $\theta \in \mathcal{O}$.

The equivalence induced by a preorder is obtained by adding the symmetric requirement on pairs of related processes. All results below for preorders can be extended to equivalences in the expected manner. We will ignore equivalences in the remainder of the paper.

By varying the sets of observables, one can capture all inductive preorders and equivalences in van Glabbeek's spectrum [8] (collecting the main such relations in the literature), namely: trace, failure, failure trace, ready, ready trace preorders and equivalences [3, 4, 11, 14, 15, 1, 5]. Assuming image-finiteness of the LTSs,
meaning that for all P and $\mu$, the set $\{P' \mid P \xrightarrow{\mu} P'\}$ is finite, the set of such preorders also include the *may*, *must*, and *testing* preorders [6, 9], and the *refusal preorder* [13]. We refer to [27] for the details of the characterisations. The operators for observables in Definition 1 also capture some coinductive relations, such as simulation, and refinements of it such as ready simulation [27].

## 2.2 Weights

We are interested in observables that can be measured, that is, whenever $P \models \theta$ holds then a weight can be assigned to a proof of $P \models \theta$. Given an LTS $\mathcal{L}$ and a family $\mathcal{O}$ of observables over the same set of actions, a process $P$ of $\mathcal{L}$, and an observable $\theta \in \mathcal{O}$, an assertion $P \models^n \theta$ holds if $P \models \theta$ and the depth of nesting of diamond operators in $\theta$ is not greater than $n$ (See [27] for a definition in terms of rules). For instance, we have $P \models^n \langle a \rangle . \langle b \rangle$. true, for any $n \ge 2$, whereas $P \models^1 \langle a \rangle . \langle b \rangle$. true does not hold.

**Definition 3.** A family of observables $\mathcal{O}$ and the corresponding preorder $\lesssim^{\mathcal{O}}$ are measurable if, for any LTS (over the same set of actions) and process $P$ of the LTS, and for any observable $\theta \in \mathcal{O}$, whenever $P \models \theta$ then also $P \models^n \theta$ holds, for some $n \ge 0$.

The introduction of weights allows us to define approximations of the behavioural preorders.

**Definition 4 (stratification).** Two processes $P, Q$ are in the $n$-th approximant of $\lesssim^{\mathcal{O}}$, written $P \lesssim_n^{\mathcal{O}} Q$, if $P \models^n \theta$ implies $Q \models \theta$, for all $\theta$.

In the above definition, $Q \models \theta$ could be replaced by $Q \models^n \theta$. Relations $\lesssim_n^{\mathcal{O}}$ are preorders.

**Lemma 1.** If $\mathcal{O}$ is measurable, then $\lesssim_n^{\mathcal{O}} = \cap_n \lesssim_n^{\mathcal{O}}$.

All preorders discussed at the end of Section 2.1 are measurable. In the remainder, it is intended that all family of observables and all preorders are measurable.

# 3 Functions for inductive enhancements

We recall here the concrete definitions of the functions for inductive enhancements, namely the weight-preserving functions [27]. Unless otherwise stated, a relation is meant to be a (binary) relation on processes. We let $\mathcal{R}$ and $\mathcal{S}$ range over relations. The union of relations $\mathcal{R}$ and $\mathcal{S}$ is $\mathcal{R} \cup \mathcal{S}$, and their composition is $\mathcal{R}\mathcal{S}$ (i.e., $(P, P') \in \mathcal{R}\mathcal{S}$ holds if for some $P''$, both $(P, P'') \in \mathcal{R}$ and $(P'', P') \in \mathcal{S}$ hold). We often use the infix notation for relations; hence $P \mathcal{R} Q$ means $(P, Q) \in \mathcal{R}$.

The definition below of semi-progression is essentially the “one-way” version of the progressions in the theory of enhanced coinduction [23]. The converse clause is missing, as we are dealing with preorders, rather than equivalences as in enhanced coinduction.
**Definition 5 (semi-progression).** Given two relations $\mathcal{R}$ and $\mathcal{S}$, we say that $\mathcal{R}$ semi-progresses to $\mathcal{S}$, written $\mathcal{R} \to \mathcal{S}$, if $\mathcal{P}\mathcal{R}\mathcal{Q}$ implies:

- whenever $P \xrightarrow{\mu} P'$, there exists $Q'$ such that $Q \xrightarrow{\mu} Q'$ and $P' S Q'$. $\square$

We need semi-progressions of the form $\mathcal{R} \to \mathcal{F}(\mathcal{R})$ where $\mathcal{F}$ is a function on process relations. Below, $\mathcal{F}$ and $\mathcal{G}$ range over such functions. To handle atomic observables such as refusals, the following compliance requirement is needed.

**Definition 6 (compliance).** A relation $\mathcal{R}$ is compliant with $\mathcal{O}$ (or simply compliant, if $\mathcal{O}$ is clear) if, for all atomic observables $\mathcal{a}$ in $\mathcal{O}$ and for all $\mathcal{P}\mathcal{R}\mathcal{Q}$, $\mathcal{P} \models \mathcal{a}$ implies $\mathcal{Q} \models \mathcal{a}$.

Separating compliance and (semi-)progression allows us to maintain the standard notion of progression in the literature, which only refers to action transitions. Moreover, in this way progressions and semi-progressions are defined without reference to any family of observables.

**Definition 7 (soundness).** A function $\mathcal{F}$ is sound for $\lesssim^{\mathcal{O}}$ if $\mathcal{R} \to \mathcal{F}(\mathcal{R})$ implies $\mathcal{R} \subseteq \lesssim^{\mathcal{O}}$, for any compliant $\mathcal{R}$.

Not all functions are sound. An example is the function that maps every relation onto the universal relation (the set of all pairs of processes). One then looks for a class of sound functions for which membership is easy to check, which includes interesting functions, and which satisfies interesting properties. For this the notion of weight-preserving function is proposed [27].

**Definition 8 (weight-preserving function).** A function $\mathcal{F}$ preserves weights on $\lesssim^{\mathcal{O}}$ when, for all $n$ and for all $\mathcal{R}$, if $\mathcal{R} \subseteq \lesssim_n^{\mathcal{O}}$, then also $\mathcal{F}(\mathcal{R}) \subseteq \lesssim_n^{\mathcal{O}}$.

Any weight-preserving function is indeed sound, as stated in the following theorem. A direct proof of the theorem is presented in [27]; in this paper we will derive it from the fixed-point theory of Section 4.

**Theorem 1 (soundness of weight-preserving functions for preorders).** If $\mathcal{F}$ preserves weights on $\lesssim^{\mathcal{O}}$, then $\mathcal{F}$ is sound for $\lesssim^{\mathcal{O}}$.

Thus the proof technique stemming from the theory above goes as follows. Let $\lesssim^{\mathcal{O}}$ be the preorder resulting from the set of observables $\mathcal{O}$. Take a function $\mathcal{F}$ that preserves weights. Then for any relation $\mathcal{R}$ that is compliant with $\mathcal{O}$, whenever $\mathcal{R} \to \mathcal{F}(\mathcal{R})$, we also have $\mathcal{R} \subseteq \lesssim^{\mathcal{O}}$.

A number of examples of weight-preserving functions are reported in [27]: the identity function, various useful constant functions, the transitive-closure function, the closure under contexts (for specific languages). Moreover, the set of weight-preserving functions is closed under useful constructors such as function composition, union, chaining (that yields relational composition); these allow one to derive a number of more sophisticated weight-preserving functions, e.g., the transitive-closure function, the closure under $\lesssim^{\mathcal{O}}$ (analogous to the 'up-to bisimilarity' enhancement for bisimilarity), the closure under contexts and $\lesssim^{\mathcal{O}}$ (analogous to the 'up-to context and bisimilarity' enhancement for bisimilarity).
# 4 Complete lattices and chains of approximants

In this section we present the abstract account for the enhancements of inductive behavioural relations, using complete lattices, chains of approximants, and post-fixed points.

## 4.1 Post-fixed points and chains

We recall that a poset $L$ is a non-empty set equipped with a relation $\leq$ on its elements that is a partial order (that is, reflexive, antisymmetric, and transitive).

**Definition 9.** Let $\mathcal{F}$ be an endofunction on a poset $L$.

- $\mathcal{F}$ is monotone if $x \leq y$ implies $\mathcal{F}(x) \leq \mathcal{F}(y)$, for all $x, y$.

- An element $x$ of the poset is a post-fixed point of $\mathcal{F}$ if $x \leq \mathcal{F}(x)$.

- A fixed point of $\mathcal{F}$ is an element $x$ with $\mathcal{F}(x) = x$.

□

The greatest lower bound of a subset $S \subseteq L$ is also called the meet of $S$; dually, the least upper bound of $S$ is also called the join of $S$. We write $\cup_{x_n} x_n$ for the join of a subset $\{x_n\}_n$ of elements of the poset, and similarly $\cap_{x_n} x_n$ for its meet.

**Definition 10 (Complete lattice).** A complete lattice is a poset with all joins (i.e., all the subsets of the poset have a join). □

The above implies that a complete lattice has also all meets. Further, it implies that there are bottom and top elements, which will be indicated by $\bot$ and $\top$, respectively. The key ingredient for our abstract theory of up-to techniques are chains of approximants in complete lattices.

**Definition 11.** In a complete lattice, a chain of approximants is a sequence of points $\{x_n\}_n$, $n \geq 0$ in the lattice with $x_0 = \top$ and $x_{n+1} \leq x_n$, for all $n$.

We wish to reason about meets of chains of approximants. As we shall see, these meets represent inductive behavioural relations, obtained as the intersection of their approximants. We sometimes simply call *chain* a chain of approximants.

**Definition 12.** An endofunction $\mathcal{B}$ on a complete lattice $L$ is valid for a chain of approximants $\{x_n\}_n$ in $L$ if, for all $y \in L$ and $n \geq 0$, if $y \leq x_n$ then $\mathcal{B}(y) \leq x_{n+1}$.

Intuitively, $\mathcal{B}$ is valid for a chain if an application of $\mathcal{B}$ allows us to move (at least) one step down in the chain. Below, for readability we often omit reference to the complete lattice. It is intended that all points and functions are points and endofunctions on a lattice.

Valid functions for a chain allow us to reason about the meet of the chain.

**Theorem 2.** If $\mathcal{B}$ is valid for the chain $\{x_n\}_n$, then for any post-fixed point $z$ of $\mathcal{B}$ we have $z \leq \cap_n x_n$.
*Proof.* We show that $z \le x_n$, for each $n$, using induction on $n$. For $n=0$, this follows from $x_0 = \top$. Otherwise, suppose $z \le x_n$; by validity of $\mathcal{B}$ we derive $\mathcal{B}(z) \le x_{n+1}$. As $z$ is a post-fixed point of $\mathcal{B}$, we have $z \le \mathcal{B}(z)$. We can thus conclude that also $z \le x_{n+1}$. $\square$

We seek ways of enhancing valid functions, i.e., obtain other valid functions (with the intention of obtaining, concretely, 'larger' functions). For this we use the approximant-preserving functions.

**Definition 13.** An endofunction $\mathcal{F}$ is approximant-preserving for a chain of approximants $\{x_n\}_n$ if, for all $y$ and $n \ge 0$, if $y \le x_n$ then also $\mathcal{F}(y) \le x_n$.

Intuitively, application of approximant-preserving functions respects the level of approximation. We write $\mathcal{F}_1 \circ \mathcal{F}_2$ for the composition of the two functions, where $(\mathcal{F}_1 \circ \mathcal{F}_2)(z) = \mathcal{F}_1(\mathcal{F}_2(z)))$.

**Theorem 3.** If $\mathcal{B}$ is valid, and $\mathcal{F}$ is approximant-preserving, for the same chain $\{x_n\}_n$, then also $\mathcal{B} \circ \mathcal{F}$ is valid for $\{x_n\}_n$, which means that $\mathcal{B}$ is indeed valid.

*Proof.* Suppose $y \le x_n$, for some $n$ and $y$. As $\mathcal{F}$ is approximant-preserving, we have $\mathcal{F}(y) \le x_n$; and since $\mathcal{B}$ is valid, $\mathcal{B}(\mathcal{F}(y)) \le x_{n+1}$. $\square$

The set of approximant-preserving functions is closed under composition, join, and contains a few useful constant functions.

**Proposition 1.** For any chain of approximants $\{x_n\}_n$,

- the identity function is approximant-preserving;

- for any $y$ with $y \le \cap_n x_n$ the constant function mapping each point onto $y$ is approximant-preserving;

- if $\mathcal{F}_1$ and $\mathcal{F}_2$ are approximant-preserving then so is $\mathcal{F}_1 \circ \mathcal{F}_2$;

- if $\{\mathcal{F}_j\}_j$ is a set of approximant-preserving functions, then $\cup_j \mathcal{F}_j$, i.e., the function that maps a point $z$ onto $\cup_j \mathcal{F}_j(z)$ is approximant-preserving too.

## 4.2 Monotone functions

The conditions of validity and approximant-preserving can be simplified if we require the functions to be monotone.

**Proposition 2.** If $\mathcal{B}$ is monotone, then, for any chain of approximants $\{x_n\}_n$, $\mathcal{B}$ is valid for $\{x_n\}_n$ iff, for all $n$, we have $\mathcal{B}(x_n) \le x_{n+1}$.

*Proof.* If $\mathcal{B}$ is valid, then from $x_n \le x_n$ we infer $\mathcal{B}(x_n) \le x_{n+1}$. Conversely, if $y \le x_n$, then by monotonicity we derive $\mathcal{B}(y) \le \mathcal{B}(x_n)$; then, from $\mathcal{B}(x_n) \le x_{n+1}$, also $\mathcal{B}(y) \le x_{n+1}$. $\square$

A similar result holds for approximant-preserving functions:

**Proposition 3.** If $\mathcal{F}$ is monotone, then, for any chain of approximants $\{x_n\}_n$, $\mathcal{F}$ is approximant-preserving for $\{x_n\}_n$ iff, for all $n$, we have $\mathcal{F}(x_n) \le x_n$.
## 4.3 From complete lattices to behavioural relations

We now show that the results recalled in Section 3 are instances of the abstract setting based on fixed-points in Sections 4.1 and 4.2.

The complete lattice to be used in the case of behavioural relations on a set $Pr$ of processes is obtained from the powerset construction on $Pr \times Pr$. Thus $\emptyset$ (the empty set) and $Pr \times Pr$ are the bottom and top elements; join is given by set union, and meet by set intersection. We write $L_{Pr}$ for this complete lattice.

We recall that the behavioural preorders of Section 2 are obtained as the meet of their approximants, as for each set $O$ of observables, we have $\preceq^{O} = \cap_n \preceq^{O}_n$ (Lemma 1). The approximants $\{\preceq^{O}_n\}_n$ form a chain of approximants (Definition 11), as $\preceq^{O}_0 = Pr \times Pr$ and, for each $n$, we have $\preceq^{O}_{n+1} \subseteq \preceq^{O}_n$.

Next, we need to express the semi-progressions of Section 3 as functions $S^O$ on the lattice, for a given set $O$ of observables. The only difference with respect to the ordinary functional for simulation is the compliance condition:

$$ S^O(\mathcal{R}) \stackrel{\text{def}}{=} \{(P, Q) \mid \begin{array}{l} 1. \text{ whenever } P \xrightarrow{\mu} P', \text{ there exists } Q' \text{ s.t. } Q \xrightarrow{\mu} Q' \text{ and } P' \mathcal{R} Q'; \\ 2. \text{ for all atomic observables } \mathbf{a} \text{ in } O \text{ if } P \models \mathbf{a} \text{ then also } Q \models \mathbf{a.} \end{array} \} $$

**Theorem 4.** For all $O$, function $S^O$ is valid for $\{\preceq^{O}_n\}_n$.

*Proof.* We omit $O$, abbreviating $\preceq^{O}_n$ as $\preceq_n$, and $S^O$ as $S$. The function $S$ is monotone. Hence, by Proposition 2, to show that $S$ is valid for $\{\preceq_n\}_n$ it suffices to show that, for any $n$, we have $S(\preceq_n) \le \preceq_{n+1}$.

Thus take any $n \ge 0$, and suppose $(P, Q) \in S(\preceq_n)$. We have to show that also $(P, Q) \in \preceq_{n+1}$. For this, assume $P \models \theta$ and the depth of nesting of diamond operators in $\theta$ is not greater than $n+1$. We check that also $Q \models \theta$ holds. We proceed by rule induction on the proof of $P \models \theta$, using a case analysis on the last rule applied.

**Rule AT** For atomic observables, $Q \models \theta$ holds by the compliance condition on $S$ (clause (2) in the definition of $S$).

**Rule CONJ** If the last rule applied is

$$ \frac{P \models \theta_j \text{ for each } j}{P \models \bigwedge_{j \in J} \theta_j} $$

then since, for each $j$, by the downward-closure property on $O$ we have $\theta_j \in O$. We can use rule induction to infer $Q \models \theta_j$, and then conclude $Q \models \bigwedge_{j \in J} \theta_j$.

**Rule ACT** Suppose that the last rule applied is

$$ \frac{P \xrightarrow{\mu} P' \qquad P' \models \theta}{P \models \langle \mu \rangle . \theta} $$

where, by the downward-closure property on $O$ we have $\theta \in O$, and the depth of diamond operators in $\theta$ is not greater than $n$; that is, $P' \models^n \theta$ holds. From
$P \xrightarrow{\mu} P'$ and clause (1) of the definition of $\mathcal{S}$, we infer that $Q \xrightarrow{\mu} Q'$ with $P' \preceq_n Q'$, for some $Q'$. From $P' \preceq_n Q'$ and $P' \models^n \theta$, by definition of $\preceq_n$, we obtain $Q' \models \theta$. In summary, we can infer

$$ \frac{Q \xrightarrow{\mu} Q' \qquad Q' \models \theta}{Q \models \langle \mu \rangle . \theta} $$

□

Finally, we notice that, on the lattice $L_{Pr}$, the definition of weight-preserving function matches that of approximant-preserving functions. That is, a function is preserves weights on $\preceq^O$ precisely when it is approximant-preserving for $\{\preceq^O_n\}_n$.

We thus derive the soundness of weight-preserving functions, i.e., Theorem 1, stating that if $\mathcal{F}$ preserves weights on $\preceq^O$, then $\mathcal{F}$ is sound for $\preceq^O$.

*Proof (of Theorem 1).* Soundness of $\mathcal{F}$ for $\preceq^O$ means that any post-fixed point of $S^{O} \circ \mathcal{F}$ is contained in $\preceq^O$.

Since weight-preserving on $\preceq^O$ is the same as approximant-preserving for $\{\preceq^O_n\}_n$, by Theorems 4 and 3, function $S^{O} \circ \mathcal{F}$ is valid for $\{\preceq^O_n\}_n$. Therefore for any post-fixed point $\mathcal{R}$ of $S^{O} \circ \mathcal{F}$, we have $\mathcal{R} \subseteq \bigcap_n \preceq^O_n = \preceq^O$. □

Similarly, properties of weight-preserving functions, such as closure under composition and union, can be derived from the properties of approximant-preserving functions in the abstract setting (e.g., Proposition 1).

# 5 Concluding remarks

## 5.1 Related work

The idea of developing a theory of enhancements, for the bisimulation proof method, is put forward in [23], introducing the notion of progression (roughly the symmetric version of the semi-progression of Section 3) and of respectful function (roughly, functions that preserve regressions). Later [16, 17] the theory has been both generalised to the coinduction proof method, using complete lattices, and refined, first using a variant of respectfulness called compatibility, then focusing on the largest compatible function, called the *companion* (that also coincides with the largest respectful function). The companion can also be obtained using Kleene's construction of the greatest fixed-point [12]. The theory of enhancements for inductive behavioural relations [27] follows the schema for the bisimulation enhancements based on respectfulness and compatibility [19]. In contrast, the chains of approximants and the approximant-preserving functions, on which the abstract theory in Section 4 is based, closely resemble the approximations of the greatest fixed-point of monotone functions from the top element of the lattice using Kleene's construction, and the corresponding account of 'up-to' techniques, as studied in papers such as [17, 12, 28, 18].

Abstract formulations of the meaning of coinductive enhancements have also been given using category theory. The main technical tools are final semantics, coalgebras, spans of coalgebra homomorphisms, fibrations, and corecursion
schemes; see, e.g., [18, 2, 21]. For more details and references on coinductive enhancements, we refer to the technical survey [19] and to the historical review [20].

Proof techniques for (weak) bisimilarity akin to the up-to techniques of coin-
ductive enhancements have also been studied using unique solutions of equations
and special inequations called contractions [7, 26]. In particular, these techniques
offer one the power of some of the most important bisimulation enhancements,
namely ‘up-to context’. Moreover, the authors transport them onto inductive
equivalences and preorders such as trace equivalence and trace preorder.

## 5.2 Further developments

We have given an interpretation, using complete lattices and fixed-points, of the
enhancements and the ‘up-to’ techniques for inductive behavioural relations [27].

In the paper, we have confined ourselves to ‘strong’ semantics, i.e., to transition systems where all actions are treated in the same manner. It would be useful to extend the setting to ‘weak’ forms of behavioural relations, in which a special action denoting internal activity is partly or completely ignored. Theories of weak coinductive enhancements are rather more involved than the strong theories. For instance, auxiliary relations such as *expansion* [24] and *contraction* [26] are usually needed. Similar issues show up in enhancements for inductive behavioural relations. For instance, two forms of weights have been proposed [27], distinguishing the contribution of internal and visible actions, with their relative advantages and disadvantages. In addition, some weak behavioural relations make use of state predicates such as *stability*, which do not appear in the strong case.

A challenging direction might be to study lifting of the theory presented in
this paper to a probabilistic setting and labelled Markov processes. We would
like also to examine abstract settings capable of accommodating behavioural
relations defined from both *inductive* and *coinductive* observables. Examples of
coinductive observables that may appear together with the inductive ones are
infinite traces and divergence.

## Acknowledgments

I am very glad and honoured to have paper in his volume dedicated to Rocco
De Nicola. This also gives me an opportunity for expressing my gratitude to
him. Not only for many fruitful scientific discussions, but also (and possibly
even more!) for his constant and generous friendship, including frequent pieces
of personal advice, beginning with the recommendation to go to Edinburgh for
carrying out a PhD ! Furthermore, meeting Rocco has always been a guarantee
for joyful and pleasant moments: conversation would quickly and invariably take
a broad span (from science, to life, and to politics...), with Rocco brilliantly
seizing all opportunities for jokes and laughter.

Thanks also to the anonymous referees for useful observations and comments
on the content of the paper. This work has been partly supported by the MIUR-
PRIN project 'Resource Awareness in Programming: Algebra, Rewriting, and Analysis' (RAP, ID P2022HXNSC).

## References

1. Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Ready-trace semantics for concrete process algebra with the priority operator. Comput. J. 30(6), 498–506 (1987)

2. Basold, H., Pous, D., Rot, J.: Monoidal company for accessible functors. In: Proc. CALCO. LIPIcs, vol. 72. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

3. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)

4. Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating processes. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) Seminar on Concurrency. Lecture Notes in Computer Science, vol. 197, pp. 281–305. Springer Verlag (1984)

5. De Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24, 211–237 (1987)

6. De Nicola, R., Hennessy, R.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)

7. Durier, A., Hirschkoff, D., Sangiorgi, D.: Divergence and unique solution of equations. Logical Methods in Computer Science 15(3) (2019), https://doi.org/10.23638/LMCS-15(3:12)2019

8. Glabbeek, R.v.: The linear time–branching time spectrum I. In: J. Bergstra, A.P., Smolka, S. (eds.) Handbook of Process Algebra. pp. 3–99. Elsevier (2001)

9. Hennessy, M.: Algebraic Theory of Processes. The MIT Press, Cambridge, Mass. (1988)

10. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137–161 (1985)

11. Olderog, E.R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes. Acta Inf. 23(1), 9–66 (1986)

12. Parrow, J., Weber, T.: The largest respectful function. Logical Methods in Computer Science 12(2) (2016)

13. Phillips, I.: Refusal testing. Theor. Comput. Sci. 50, 241–284 (1987), a preliminary version in Proc. ICALP’86, Lecture Notes in Computer Science 226, Springer Verlag.

14. Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) 12th ICALP. Lecture Notes in Computer Science, vol. 194, pp. 15–32. Springer Verlag (1985)

15. Pomello, L.: Some equivalence notions for concurrent systems. An overview. In: Rozenberg, G. (ed.) Advances in Petri Nets 1985. Lecture Notes in Computer Science, vol. 222, pp. 381–400. Springer (1985), https://doi.org/10.1007/BFb0016202

16. Pous, D.: Complete lattices and up-to techniques. In: Proc. APLAS ’07. Lecture Notes in Computer Science, vol. 4807, pp. 351–366. Springer Verlag (2007)

17. Pous, D.: Coinduction all the way up. In: Proc. LICS. pp. 307–316. ACM (2016)

18. Pous, D., Rot, J.: Companions, Codensity, and Causality. In: Proc. FoSSaCS. Lecture Notes in Computer Science, vol. 10203, pp. 106–123. Springer Verlag (2017)

19. Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cambridge University Press (2012)
20. Pous, D., Sangiorgi, D.: Bisimulation and coinduction enhancements: A historical perspective. Formal Asp. Comput. 31(6), 733–749 (2019)

21. Rot, J., Bonchi, F., Bonsangue, M.M., Pous, D., Rutten, J., Silva, A.: Enhanced coalgebraic bisimulation. Mathematical Structures in Computer Science 27(7), 1236–1264 (2017)

22. Sangiorgi, D.: An investigation into functions as processes. In: Proc. Math. Foundations of Programming Semantics (MFPS). Lecture Notes in Computer Science, vol. 802, pp. 143–159. Springer Verlag (1993)

23. Sangiorgi, D.: On the bisimulation proof method. Journal of Mathematical Structures in Computer Science 8, 447–479 (1998)

24. Sangiorgi, D., Milner, R.: The problem of “Weak Bisimulation up to”. In: Cleveland, W. (ed.) Proc. CONCUR ’92. Lecture Notes in Computer Science, vol. 630, pp. 32–46. Springer Verlag (1992)

25. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012)

26. Sangiorgi, D.: Equations, contractions, and unique solutions. ACM Trans. Comput. Log. 18(1), 4:1–4:30 (2017), http://doi.acm.org/10.1145/2971339

27. Sangiorgi, D.: From enhanced coinduction towards enhanced induction. Proc. ACM Program. Lang. 6(POPL), 1–29 (2022), https://doi.org/10.1145/3498679

28. Schäfer, S., Smolka, G.: Tower induction and up-to techniques for CCS with fixed points. In: Höfner, P., Pous, D., Struth, G. (eds.) Proc. Relational and Algebraic Methods in Computer Science. Lecture Notes in Computer Science, vol. 10226, pp. 274–289 (2017)