# The Coarsest Precongruences Respecting Safety and Liveness Properties

Robert Jan Glabbeek

► To cite this version:

Robert Jan Glabbeek. The Coarsest Precongruences Respecting Safety and Liveness Properties. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. pp.32-52, 10.1007/978-3-642-15240-5_3 . hal-01054444

HAL Id: hal-01054444

https://inria.hal.science/hal-01054444

Submitted on 6 Aug 2014

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
# The Coarsest Precongruences
Respecting Safety and Liveness Properties

Rob van Glabbeek¹,²

¹ NICTA, Sydney, Australia

² School of Computer Sc. and Eng., Univ. of New South Wales, Sydney, Australia

**Abstract.** This paper characterises the coarsest refinement preorders on labelled transition systems that are precongruences for renaming and partially synchronous interleaving operators, and respect all safety, liveness, and conditional liveness properties, respectively.

## 1 Introduction

The goal of this paper is to define and characterise certain semantic equivalences $\equiv$ and refinement preorders $\sqsubseteq$ on processes. The idea is that $p \equiv q$ says, essentially, that for practical purposes processes $p$ and $q$ are equally suitable, i.e. one can be replaced for by the other without untoward side effects. Likewise, $p \sqsubseteq q$ says that for all practical purposes under consideration, $q$ is at least as suitable as $p$, i.e. it will never harm to replace $p$ by $q$. Thus, one should have that $p \equiv q$ iff both $p \sqsubseteq q$ and $q \sqsubseteq p$.

Naturally, the choice of $\equiv$ and $\sqsubseteq$ depends on how one models a process, and what range of practical purposes one considers. I this paper I restrict myself to one of the most basic process models: *labelled transition systems*. I study processes that merely perform actions *a*, *b*, *c*, ... which themselves are not subject to further investigations. These actions may be instantaneous or durational, but they may not last forever; moreover, in a finite amount of time only finitely many actions can be carried out. I distinguish between *visible* actions, that can be observed by the environment of a process, and whose occurrence can be influenced by this environment, and *invisible* actions, that cannot be observed of influenced. Since there is no need to distinguish different invisible actions, I can just as well consider all of them to be occurrences of the same invisible action, which is traditionally called $\tau$. Furthermore, I abstract from real-time and probabilistic aspects of processes.

This choice of process model already rules out many practical purposes for which one process could be more suitable than another. I can for instance not compare processes on speed, since this is an issue that my process model has already abstracted from. In fact, the only aspects of processes that are captured by such a model and that may matter in practical applications, are the sequences of actions that a process may perform in a, possibly infinite, run, performed in, or in collaboration with, a certain environment. As the invisible action is by definition unobservable, it moreover suffices to consider sequences of *visible*
actions. A sequence of visible actions that a process *p* may perform is called a *trace* of *p*; it is a *complete trace* if it is performed during a maximal run of *p*, one that cannot be further extended. Obviously, the traces of *p* are completely determined by the complete traces of *p*, namely as their prefixes.

Based on the considerations above, it is tempting to postulate that the relevant behaviour of a process, as far as discernible in terms of labelled transition systems, is completely determined by its set of complete traces; hence two processes should be equivalent if they have the same competed traces. However, this argument bypasses the role of the environment in influencing the behaviour of a process. Often, one allows the actions a process performs to be synchronisations with the environment, and the environment can influence the course of action of a process by synchronising with some actions but not with others. Therefore, a safe over-approximation of the relevant behaviour of a process is not merely its set of complete traces, but rather its set of complete traces obtained as a function of the environment the process is running in.

In this paper I consider a neutral environment in which all courses of action are possible and the behaviour of a process is indeed determined by its complete traces. All other ways in which the environment may influence the behaviour of a process are given in terms of *contexts* build from other processes and certain composition operators. It could for instance be that in the neutral environment there is no way to tell the difference between processes *p* and *q*; maybe because they have the same set of complete traces. However, for a suitable parallel composition operator $\|$ and other process *r* it may be that there is a manifest practical difference between $p\|r$ and $q\|r$, so that one has $p\|r \neq q\|r$. Now that fact alone is taken to be enough reason to postulate that $p \neq q$. Namely the difference between *p* and *q* can be spotted by placing them in a context $\underline{\|}r$. This context can be regarded as an environment in which the behaviours of *p* and *q* differ.

Following this programme, a suitable semantic equivalence on processes is defined in terms of two requirements. First of all the behaviour of processes is compared in the neutral environment. This entails isolating a class *C* of properties $\varphi$ of processes that are deemed relevant in a given range of applications. One then requires for $p \equiv q$ to hold that *p* and *q* have the same properties from this class:

$$p \equiv q \Rightarrow \forall \varphi \in C. (p \models \varphi \Leftrightarrow q \models \varphi) \quad (1)$$

where $p \models \varphi$ denotes that process *p* has the property $\varphi$. An equivalence $\equiv$ that satisfies this last requirement is said to *respect* or *preserve* the properties in *C*. The second requirement entails selecting a class *O* of useful operators for combining processes. One then requires that for any context $C[\underline{\cdot}]$ (such as $\underline{\|}r$) built from operators from *O* and arbitrary processes, that

$$p \equiv q \Rightarrow C[p] \equiv C[q]. \quad (2)$$

An equivalence $\equiv$ that satisfies this last requirement is called a *congruence* for *O*. For the sake of intuition it may help to consider the contrapositive formulation of these implications: if there exists a property $\varphi$ in *C* that holds for *p* but not for *q*,
or vice versa, then $p$ and $q$ cannot be considered equivalent. Likewise $C[p] \not\equiv C[q]$ implies $p \not\equiv q$.

These two requirements merely insist that the desired equivalence $\equiv$ does not identify processes that in some context differ on their relevant properties. They are satisfied by many equivalence relations, including the identity relation, that distinguishes all processes. In order to characterise precisely when two systems have the same relevant properties in any relevant context, one takes the coarsest equivalence satisfying (1) and (2); the one making the most identifications. This equivalence is called fully abstract w.r.t. $\mathcal{C}$ and $\mathcal{O}$. It always exists, and, as is straightforward to check, is characterised by

$$p \equiv q \Leftrightarrow \forall \mathcal{O}\text{-context } C[\underline{\phantom{}}]. \forall \varphi \in \mathcal{C}. (C[p] \models \varphi \Leftrightarrow C[q] \models \varphi).$$

When, for a certain application, the choice of $\mathcal{C}$ and $\mathcal{O}$ is clear, the unique equivalence relation that is fully abstract w.r.t. $\mathcal{C}$ and $\mathcal{O}$ is the right semantic equivalence for that application. However, when the choice of $\mathcal{C}$ and $\mathcal{O}$ is not clear, or when proving results that may be re-used in future applications that may call for extending $\mathcal{C}$ or $\mathcal{O}$, it is better to err on the side of caution, and use equivalences that satisfy (1) and (2) but need not be fully abstract; instead the finest equivalence $\equiv_{\text{fine}}$ for which a result $p \equiv_{\text{fine}} q$ can be proved is often preferable, because this immediately entails that $p \equiv q$ for any coarser equivalence relation $\equiv$, in particular for an $\equiv$ that may turn out to be fully abstract for some future choice of $\mathcal{C}$ and $\mathcal{O}$. It is for this reason that much actual verification work employes the finest equivalences that lend themselves for verification purposes, such as the various variants of bisimulation equivalence [12], see e.g. [1]. Nevertheless, this paper is devoted to the characterisation of fully abstract equivalences, and preorders, for a few suitable choices of $\mathcal{C}$ and $\mathcal{O}$.

The programme for refinement preorders proceeds along the same lines, but here it is important to distinguish between good and bad properties of processes. The counterpart of (1) is

$$p \sqsubseteq q \Rightarrow \forall \varphi \in \mathcal{G}. (p \models \varphi \Rightarrow q \models \varphi) \qquad (3)$$

where $\mathcal{G}$ is the set of good properties within $\mathcal{C}$, those that for some applications may be required of a process. If this holds, $\sqsubseteq$ respects or preserves the properties in $\mathcal{G}$. When dealing with bad properties, those that in some applications should be avoided, the implication between $p \models \varphi$ and $q \models \varphi$ is oriented in the other direction. Since every bad property $\varphi$ can be reformulated as a good property $\neg\varphi$, there is no specific need add a variant of (3) for the bad properties. The counterpart of (2) is simply

$$p \sqsubseteq q \Rightarrow C[p] \sqsubseteq C[q]. \qquad (4)$$

and a preorder $\sqsubseteq$ that satisfies this requirement is called a *precongruence* for $\mathcal{O}$. Now the preorder that is fully abstract w.r.t. $\mathcal{G}$ and $\mathcal{O}$ always exists, and is characterised by

$$p \sqsubseteq q \Leftrightarrow \forall \mathcal{O}\text{-context } C[\underline{\phantom{}}]. \forall \varphi \in \mathcal{G}. (C[p] \models \varphi \Rightarrow C[q] \models \varphi).$$
It is the coarsest precongruence for $\mathcal{O}$ that respects the properties in $\mathcal{G}$. A characterisation of the preorder $\sqsubseteq$ that is fully abstract w.r.t. a certain $\mathcal{G}$ and $\mathcal{O}$ automatically yields a characterisation of the equivalence $\equiv$ that is fully abstract w.r.t. $\mathcal{G}$ and $\mathcal{O}$, as one has $p \equiv q$ iff both $p \sqsubseteq q \wedge q \sqsubseteq p$.

In this paper I will propose three main candidates for the set $\mathcal{G}$ of good properties: safety properties in Section 3, liveness properties in Section 4 and conditional liveness properties in Section 5. For the sake of theoretical completeness I moreover address general linear time properties in Section 6.

In Section 2 I will define my model of labelled transition systems and propose a class of $\mathcal{C}$ of operators that appear useful in applications to combine processes. My favourite selection contains

* the partially synchronous interleaving operator of CSP [15],

* abstraction or concealment [3,15]

* and the state operator [2],

or any other basis that is equally expressive. With each of the four choices for $\mathcal{G}$ this set of operators determines a fully abstract preorder, which will be characterised in Sections 3, 4, 5 and 6. It turns out that the resulting preorders are somewhat robust under the precise choice of operators for which one imposes a precongruence requirement: the same ones are obtained already without using concealment, and using merely injective renaming instead of the more general state operator. In the other direction, I could just as well have used all operators of CSP.

## 2 Labelled Transition Systems and a Selection of Composition Operators

Let $\Sigma^*$ denote the set of finite sequences over a given set $\Sigma$, and $\Sigma^\infty$ the set of infinite ones; $\Sigma^\omega := \Sigma^* \cup \Sigma^\infty$. Write $\epsilon$ for the empty sequence, $\sigma\rho$ for the concatenation of sequences $\sigma \in \Sigma^*$ and $\rho \in \Sigma^\omega$, and $a$ for the sequence consisting of the single symbol $a \in \Sigma$. Write $\sigma \le \rho$ for “$\sigma$ is a prefix of $\rho$”, i.e. “$\rho = \sigma \lor \exists \nu \in \Sigma^*. \sigma\nu = \rho$”, and $\rho < \sigma$ for “$\sigma \le \rho$ and $\sigma \ne \rho$”.

I presuppose an infinite action alphabet $A$, not containing the silent action $\tau$, and set $A_\tau = A \cup \{\tau\}$.

**Definition 1** A labelled transition system (LTS) is a pair $(\mathbb{P}, \rightarrow)$, where $\mathbb{P}$ is a class of processes or states and $\rightarrow \subseteq \mathbb{P} \times A_\tau \times \mathbb{P}$ is a set of transitions, such that for each $p \in \mathbb{P}$ and $\alpha \in A_\tau$ the class $\{q \in \mathbb{P} \mid (p, \alpha, q) \in \rightarrow\}$ is a set.

Assuming a fixed transition system $(\mathbb{P}, \rightarrow)$, I write $p \xrightarrow{\alpha} q$ for $(p, \alpha, q) \in \rightarrow$; this means that process $p$ can evolve into process $q$, while performing the action $\alpha$. The ternary relation $\overset{\epsilon}{\Rightarrow} \subseteq \mathbb{P} \times A^* \times \mathbb{P}$ is the least relation satisfying

$$ p \stackrel{\epsilon}{\Rightarrow} p, \quad \frac{p \xrightarrow{\tau} q}{p \xrightarrow{\epsilon} q}, \quad \frac{p \xrightarrow{a} q, a \neq \tau}{p \xrightarrow{a} q} \quad \text{and} \quad \frac{p \stackrel{\sigma}{\Rightarrow} q \stackrel{\rho}{\Rightarrow} r}{p \stackrel{\sigma\rho}{\Rightarrow} r} . $$

This enables a formalisation of the concepts of traces and complete traces from the introduction.
**Definition 2** Let $p \in \mathbb{P}$.

* $p$ is deterministic if, for any $\sigma \in A^*$, $p \stackrel{\sigma}{\Longrightarrow} q_1$ and $p \stackrel{\sigma}{\Longrightarrow} q_2$ implies that $q_1 = q_2$ and $q_1 \xrightarrow{\tau} r$.

* $p$ deadlocks, notation $p \nparallel r$, if there are no $\alpha \in A_\tau$ and $q \in \mathbb{P}$ with $p \xrightarrow{\alpha} q$.

* $p$ is locked if it can never do a visible action, i.e. if $p \stackrel{a}{\Longrightarrow} q$ for no $a \in A$ and $q \in \mathbb{P}$.

* $p$ diverges, notation $p \Uparrow$, if there are $p_i \in \mathbb{P}$ for all $i > 0$ such that $p \xrightarrow{\tau} p_1 \xrightarrow{\tau} p_2 \xrightarrow{\tau} \dots$.

* $a_1 a_2 a_3 \dots \in A^\infty$ is an infinite trace of $p$ if there are $p_1, p_2, \dots \in \mathbb{P}$ such that $p \stackrel{a_1}{\Longrightarrow} p_1 \stackrel{a_2}{\Longrightarrow} p_2 \stackrel{a_3}{\Longrightarrow} \dots$.

* $\inf(p)$ denotes the set of infinite traces of $p$.

* $\text{ptraces}(p) := \{\sigma \in A^* \mid \exists q. p \stackrel{\sigma}{\Longrightarrow} q\}$ is the set of partial traces of $p$.

* $\text{traces}(p) := \inf(p) \cup \text{ptraces}(p)$ is the set of traces of $p$.

* $\text{deadlocks}(p) := \{\sigma \in A^* \mid \exists q. p \stackrel{\sigma}{\Longrightarrow} q \nparallel r\}$ is the set of deadlock traces of $p$.

* $\text{diverg}(p) := \{\sigma \in A^* \mid \exists q. p \stackrel{\sigma}{\Longrightarrow} q \Uparrow\}$ is the set of divergence traces of $p$.

* $\text{CT}(p) := \inf(p) \cup \text{diverg}(p) \cup \text{deadlocks}(p)$ is the set of complete traces of $p$.

Note that $\text{traces}(p) = \{\sigma \in A^\omega \mid \exists \rho \in \text{CT}(p). \sigma \le \rho\}$.

To justify that $\text{CT}(p)$ is indeed a correct formalisation of the set of complete traces of $p$, I postulate that in a neutral environment, if a process $p \in \mathbb{P}$ has any outgoing transition $p \xrightarrow{\alpha} q$, then within a finite amount of time it will do one of its outgoing transitions. This is called a *progress property*; it says that a process will continue to make progress if possible.

As explained in the introduction, whether a fully abstract equivalence identifies processes $p$ and $q$ may depend on the existence of a third process $r$ such that $p \parallel r$ can be distinguished from $q \parallel r$. When restricting attention to a particular labelled transition system $(\mathbb{P}, \rightarrow)$ it might happen that a perfectly reasonable candidate $r$ happens not to be a member of $\mathbb{P}$, and thus that the conclusion $p \equiv q$ is arrived at solely as a result underpopulation of $\mathbb{P}$. To obtain the most robust notions of equivalence, I therefore assume my LTS to be *universal*, in the sense that up to isomorphism it contains *any* process one can imagine.

**Definition 3** An LTS $(\mathbb{P}, \rightarrow_{\mathbb{P}})$ is *universal* if for any other LTS $(\mathcal{Q}, \rightarrow_{\mathcal{Q}})$ there exists an injective mapping $f: \mathcal{Q} \rightarrow \mathbb{P}$, called an *embedding*, such that, for any $q \in \mathcal{Q}$ and $p' \in \mathbb{P}$ one has $f(q) \xrightarrow{\alpha} \mathbb{P}$ iff $p' \in \mathbb{P}$ has the form $f(q')$ for some $q' \in \mathcal{Q}$ with $q \xrightarrow{\alpha} \mathcal{Q} \setminus q'$.

The existence of a universal LTS has been established in [7]. Here one needs $\mathbb{P}$ to be a proper class. All preorders $\sqsubseteq$ that I consider in this paper are defined on arbitrary LTSs and have the property that $q \sqsubseteq q' \Leftrightarrow f(p) \sqsubseteq f(q')$, for any embedding $f$. This means that they are precongruences for isomorphism, and only take into account the future behaviour of processes, i.e. in determining whether $p \sqsubseteq q$ transitions leading to $p$ or $q$ play no rôle. Thus, a definition of such a preorder on a universal LTS, implicitly also defines it on any other LTS.

I will now do a proposal for the set $\mathcal{O}$ that will be my default choice in this paper. It consists of three operators for combining processes that appear useful in practical applications.
$$
\begin{align*}
& \frac{p \xrightarrow{\alpha} p'}{p \|_S q \xrightarrow{\alpha} p' \|_S q} \quad \frac{q \xrightarrow{\alpha} q'}{p \|_S q \xrightarrow{\alpha} p \|_S q'} \quad \frac{p \xrightarrow{a} p' \xrightarrow{a} q'}{p \|_S q \xrightarrow{a} p \|_S q'} \quad \frac{q \xrightarrow{a} q'}{(a \in S)} \\
& \frac{p \xrightarrow{\alpha} p'}{\tau_I(p) \xrightarrow{\alpha} \tau_I(p')} \quad \frac{p \xrightarrow{a} p'}{\tau_I(p) \xrightarrow{\tau} \tau_I(p')} \quad \frac{(\alpha \notin I)}{(a \in I)} \\
& \frac{p \xrightarrow{\tau} p'}{\lambda_s^m(p) \xrightarrow{\tau} \lambda_s^m(p')} \quad \frac{p \xrightarrow{a} p'}{\lambda_s^m(p) \xrightarrow{a^{(m,s)}} \lambda_{s(m,a)}^m(p')} \tag*{\text{Table 1. Partially synchronous interleaving, abstraction, and the state operator}}
\end{align*}
$$

<caption>Table 1. Partially synchronous interleaving, abstraction, and the state operator</caption>

The first is the *partially synchronous interleaving operator* of CSP [15]. It is parametrised with a set $S \subseteq A$ of visible actions on which it synchronises: the composition $p\|_S q$ can perform an action from $S$ only when both $p$ and $q$ perform it. All other actions from $p$ and $q$ are interleaved: whenever one of the two components can perform such an action, so can the composition, while the other component doesn't change its state. Formally, for any choice of $S \subseteq A$, $\|_S: \mathbb{P} \times \mathbb{P} \to \mathbb{P}$ is a binary operator on $\mathbb{P}$ such that a process $p\|_S q$ can make an $\alpha$-transition iff this can be inferred by the first three rules of Table 1 from the transitions that $p$ and $q$ can make. Here $a$ ranges over $A$ and $\alpha$ over $A_\tau$.

A context $\underline{\|}_S r$ is widely regarded as a plausible way of modelling an environment that partially synchronises with processes under investigation. It is for this reason I include it in $\mathcal{O}$. This argument does not hold for many other process algebraic operators, such as the choice operator $+$ of CCS [12]. This is an example of an operator that is useful for *describing* particular processes, but a context $\underline{+}r$ does not really model a reasonable environment in which one wants to run processes under investigation. For reasons of algebraic convenience, being a precongruence for the $+$ is an optional desideratum of refinement preorders, but it is not such an overriding requirement as being a precongruence for $\|_S$.

The second operator nominated for membership of $\mathcal{O}$ is the unary *abstraction operator* $\tau_I$ of ACP$_\tau$ [3], also known as the *concealment* operator of CSP [4,15]. This operator models a change in the level of abstraction at which processes are regarded, by reclassifying visible actions as hidden ones. It is parametrised with the set $I \subseteq A$ of visible actions that one chooses to abstract from, and formally defined by the next two rules of Table 1. Abstraction from internal actions by such a mechanism is an essential part of most work on verification in a process algebraic setting, and a context $\tau_I(\underline{\phantom{x}})$ represents a reasonable environment in which to evaluate processes.

My final nominee for the set $\mathcal{O}$ of useful composition operators is the state operator $\lambda_s^m$ of [2]. This unary operator formalises an interface between a process and its environment that is able to rename actions: if its argument process performs an action $b$, the interface $\lambda_s^m(\underline{\phantom{x}})$ may pass on this action to the environment as $c$, thereby opening up the possibility of synchronisation with another occurrence of $c$ when using a composed context $\lambda_s^m(\underline{\phantom{x}})\|_S r$. Furthermore, the in-
terface may remember the actions that have been performed to far, and make
its renaming behaviour dependent on this history. For instance, if its argument
$p$ performs two $a$-actions in a row, $\lambda_s^m(p)$ may pass these on to the environment
as $a_1$ and $a_2$, respectively.

The state operator $\lambda_s^m$ is parametrised with an *interface specification*
$m = (S, \ACTION, \EFFECT)$, consisting of set $S$ of *internal states*, and functions
$\ACTION: S \times A \to A$ and $\EFFECT: S \times A \to S$, as well as a *current state* $s \in S$.
Here $\ACTION$ is a function that renames actions performed by an argument process $p$ into actions performed by the interface $\lambda_s^m(p)$; the renaming depends on the internal state of the state operator, and thus is of type $S \times A \to A$. $\EFFECT$ specifies the transformation of one internal state of the state operator into another, as triggered by the encounter of an action of its argument process; it thus is of type $S \times A \to S$. Traditionally, one writes $a(m, s)$ for $\ACTION(s, a)$ and $s(m, a)$ for $\EFFECT(s, a)$. So $a(m, s)$ denotes the action $a$, as modified by the interface $m$ in state $s$, whereas $s(m, a)$ denotes the internal state $s$, as modified by the occurrence of action $a$ of the argument process within the scope of the interface $m$. With this notation, the formal definition of the state operator is given by the last two rules of Table 1.

The special case of a state operator with a singleton set of internal states is
known as a *renaming operator*. Renaming operators occur in the languages CCS
[12] and CSP [4,15]. Here I denote a renaming operator as $\lambda^m$, where the re-
dundant subscript $s$ is omitted, and $m$ trivialises to a function $\ACTION: A \to A$.
I speak of an *injective* renaming operator if $\ACTION(a) = \ACTION(b)$ implies
$a = b$. For any injective renaming operator $\lambda^m$ there exists an inverse renaming
operator $\lambda^{-m}$ (not necessarily injective) such that for all $p \in \mathbb{P}$, the process
$\lambda^{-m}(\lambda^m(p))$ behaves exactly the same as $p$—they are equivalent under all no-
tions of equivalence considered in this paper.

3 Safety Properties

A *safety property* [9] is a property that says that

something bad will never happen.

To formulate a canonical safety property, assume that my alphabet of visible
actions contains one specific action *b*, whose occurrence is *bad*. The canonical
safety property now says that *b* **will never happen**.

**Definition 4** A process *p* satisfies the *canonical safety property*, notation *p* = *safety*(*b*), if no trace of *p* contains the action *b*.

To arrive at a general concept of safety property for labelled transition systems,
assume that some notion of *bad* is defined. Now, to judge whether a process
*p* satisfies this safety property, one should judge whether *p* can reach a state
in which one would say that something bad had happened. But all observable
behaviour of *p* that is recorded in a labelled transition system until one comes
to such a verdict, is the sequence of visible actions performed until that point.
Thus the safety property is completely determined by the set sequences of visible
actions that, when performed by *p*, lead to such a judgement. Therefore one can
just as well define the concept of a safety property in terms of such a set.

**Definition 5** A safety property of processes in an LTS is given by a set $B \subseteq A^*$.
A process *p* satisfies this safety property, $p \models safety(B)$, when $ptraces(p) \cap B = \emptyset$.

This formalisation of safety properties is essentially the same as the one in [9]
and all subsequent work on safety properties; the only, non-essential, difference is
that I work with transition systems in which the transitions are labelled, whereas
[9] and most related work deals with state-labelled transition systems.

A property is called *trivial* if it either always holds or always fails. Trivial
properties are respected by any equivalence. The sets $B := \emptyset$ and $B := \{\epsilon\}$
specify trivial safety properties.

**Theorem 1** A precongruence for the state operator respects every safety property iff it respects the canonical safety property.

**Proof:** *"Only if"* follows because the canonical safety property is in fact a safety
property, namely the one with *B* being the set of those sequences that contain
the action *b*.

"If": I use here a state operator that remembers exactly what sequence of actions
has occurred so far. Thus the set of internal states of its interface specification
*m* is *A*\*, and furthermore *σ*(*m*,*a*) := *σ*a for all *σ* ∈ *A*\* and *a* ∈ *A*. Now given a
safety property *B* ⊆ *A*\*, let *b* ∈ *A* be the special "bad" action, and *d* ∈ *A* be a
different "neutral" action. Define *a*(*m*,*σ*) :=
{ b if *σ*a ∈ *B*
  d otherwise.

Then $\lambda_{\epsilon}^{m}(p) \models safety(b)$ iff $p \models safety(B)$. Thus, if $p \sqsubseteq q$ and $p \models safety(B)$, then $\lambda_{\epsilon}^{m}(p) \sqsubseteq \lambda_{\epsilon}^{m}(q)$ and $\lambda_{\epsilon}^{m}(p) \models safety(b)$. Hence $\lambda_{\epsilon}^{m}(q) \models safety(b)$, so $q \models safety(B)$. $\square$

Being locked (see Definition 2) is a safely property, namely with *B* the set
of all sequences over *A*\* of length 1. It can be understood this way by regarding
any occurrence of an action as bad.

**Theorem 2** A precongruence for abstraction that respects the property of being
locked, respects the canonical safety property.

**Proof:** Let $\sqsubseteq$ be a precongruence for abstraction that respects the property of being locked, and suppose that $p \sqsubseteq q$. Let $I := A \setminus \{b\}$. Then $\tau_I$ is an operator that renames all actions other than $b$ into $\tau$; thus if a process of the form $\tau_I(r)$ ever performs a visible action, it must be $b$. Now $p \models safety(b) \Leftrightarrow \tau_I(p) \models safety(b) \Leftrightarrow \tau_I(p)$ is locked $\Rightarrow \tau_I(q)$ is locked $\Leftrightarrow \tau_I(q) \models safety(b) \Leftrightarrow q \models safety(b)$. $\square$

By combining Theorems 1 and 2 one obtains:

**Corollary 1** A precongruence for abstraction and for the state operator that
respects the property of being locked, respects all safety properties.
**Theorem 3** Any precongruence for $\mathcal{O}$ that respects a single nontrivial safety property, respects every safety property.

**Proof:** Let $\sqsubseteq$ be a precongruence for $\mathcal{O}$ that respects safety($B$), where $B \subseteq A^*$, $B \neq \emptyset$ and $\epsilon \notin B$. Let $\sigma \in A^*$ and $a \in A$ be such that $\sigma a \in B$, and no prefix $\rho \le \sigma$ of $\sigma$ is in $B$. Let safety($a$) be the canonical safety property, but with $a$ playing the role of $b$. Naturally, Theorem 1 holds for this renamed canonical safety property as well. Hence it suffices to show that $\sqsubseteq$ respects the property safety($a$). Let $I := A \setminus \{a\}$. Then $\tau_I$ is an operator that renames all actions other than $a$ into $\tau$; thus if a process of the form $\tau_I(s)$ ever performs a visible action, it must be $a$. Let $r_\sigma$ be a process with $CT(r) = \{\sigma\}$ and $r_{\sigma a}$ be a process with $CT(r) = \{\sigma a\}$. Then, for any choice of $s \in \mathbb{P}$, $(\tau_I(s)\|_0 r_\sigma)\|_A r_{\sigma a}$ is a process all of whose traces are prefixes of $\sigma a$, with $\sigma a \in \text{ptraces}((\tau_I(s)\|_0 r_\sigma)\|_A r_{\sigma a})$ iff $a \in \text{ptraces}(\tau_I(s))$, which is the case iff $s \not\models$ safety($a$). Suppose $p \sqsubseteq q$. Then $(\tau_I(p)\|_0 r_\sigma)\|_A r_{\sigma a} \sqsubseteq (\tau_I(q)\|_0 r_\sigma)\|_A r_{\sigma a}$ and

$$ \begin{array}{l} p \models \text{safety}(a) \Leftrightarrow (\tau_I(p)\|_0 r_\sigma)\|_A r_{\sigma a} \models \text{safety}(B) \Rightarrow \\ (\tau_I(q)\|_0 r_\sigma)\|_A r_{\sigma a} \models \text{safety}(B) \Leftrightarrow q \models \text{safety}(a). \quad \square \end{array} $$

Let $\sqsubseteq_{\text{safety}}$ denote the preorder that is fully abstract w.r.t. the class of safety properties and $\mathcal{O}$. The following, well-known, theorem characterises this preorder as reverse partial trace inclusion.

**Theorem 4** $p \sqsubseteq_{\text{safety}} q \Leftrightarrow \text{ptraces}(p) \supseteq \text{ptraces}(q)$.

**Proof:** Define reverse partial trace inclusion, $\sqsubseteq_T^{-1}$, by $p \sqsubseteq_T^{-1} q$ iff $\text{ptraces}(p) \supseteq \text{ptraces}(q)$.

“$\Leftarrow$”: It suffices to establish that $\sqsubseteq_T^{-1}$ is a precongruence for $\mathcal{O}$ that respects all safety properties.

That $\sqsubseteq_T^{-1}$ is a precongruence for $\mathcal{O}$ follows immediately from the following observations:

$$ \begin{align*} \text{ptraces}(p\|_S q) &= \{\sigma \in \nu\|_S \xi \mid \nu \in \text{ptraces}(p) \wedge \xi \in \text{ptraces}(q)\} \\ \text{ptraces}(\tau_I(p)) &= \{\tau_I(\sigma) \mid \sigma \in \text{ptraces}(p)\} \\ \text{ptraces}(\lambda_s^m(p)) &= \{\lambda_s^m(\sigma) \mid \sigma \in \text{ptraces}(p)\}. \end{align*} $$

Here $\nu\|_S \xi$ denotes the set of sequences of actions for which it is possible to mark each action occurrence as left, right or both, obeying the restriction that an occurrence of action $a$ is marked both left and right iff $a \in S$, such that the subsequence of all left-labelled action occurrences is $\nu$ and the subsequence of all right-labelled action occurrences is $\xi$. Furthermore, the operators $\tau_I$ and $\lambda_s^m$ on $A^*$ are uniquely determined by

$$ \begin{align*} \tau_I(\epsilon) &= \epsilon & \tau_I(a\sigma) &= \begin{cases} \tau_I(\sigma) & \text{if } a \in I \\ a\tau_I(\sigma) & \text{otherwise} \end{cases} \\ \lambda_s^m(\epsilon) &= \epsilon & \lambda_s^m(a\sigma) &= a(m, s)\lambda_{s(m, a)}^m(\sigma). \end{align*} $$

To show that $\sqsubseteq_T^{-1}$ respects all safety properties, let $B \subseteq A^*$, $p \sqsubseteq_T^{-1} q$, and suppose $p \models \text{safety}(B)$. Then $\text{ptraces}(q) \subseteq \text{ptraces}(p)$ and $\text{ptraces}(p) \cap B = \emptyset$. Thus $\text{ptraces}(q) \cap B = \emptyset$, i.e. $q \models \text{safety}(B)$, which had to be shown.
“⇒”: Let $\sqsubseteq$ be any precongruence for $\mathcal{O}$ that respects all safety properties, and suppose $p \sqsubseteq q$. I have to establish that $p \sqsubseteq_T^{-1} q$. Let $B := A^* \setminus \text{ptraces}(p)$. Then $p \models \text{safety}(B)$. Thus $q \models \text{safety}(B)$, i.e. $\text{ptraces}(q) \cap (A^* \setminus \text{ptraces}(p)) = \emptyset$. This yields $\text{ptraces}(q) \subseteq \text{ptraces}(p). \quad \square$

The above characterisation as reverse partial trace inclusion of the coarsest con-
gruence for $\mathcal{O}$ that respects all safety properties, is rather robust under the choice
of $\mathcal{O}$. It holds already for the empty class of operators, and it remains true when
adding in all operators of CSP [4], CCS [12] or ACP$_\tau$ [3], as $\sqsubseteq_T^{-1}$ is known to be
a precongruence for all of them.

By Theorem 3, the characterisation also remains valid when requiring respect
for one arbitrary safety property only, instead of all of them, but to this end
all three operators of $\mathcal{O}$ are needed. If we just retain the state operator, by
Theorem 1 it suffices to require respect for the canonical safety property only.

4 Liveness Properties

A *liveness property* [9] is a property that says that

something good will eventually happen.

To formulate a canonical liveness property, assume that the alphabet $A$ contains one specific action $g$, whose occurrence is *good*. The canonical liveness property now says that $g$ will **eventually** happen.

**Definition 6** A process *p* satisfies the *canonical liveness property*, notation *p* *|= liveness*(*g*), if every complete trace of *p* contains the action *g*.

To arrive at a general concept of liveness property for labelled transition systems, assume that some notion of *good* is defined. Now, to judge whether a process *p* satisfies this liveness property, one should judge whether *p* can reach a state in which one would say that something good had happened. But all observable behaviour of *p* that is recorded in a labelled transition system until one comes to such a verdict, is the sequence of visible actions performed until that point. Thus the liveness property is completely determined by the set sequences of visible actions that, when performed by *p*, lead to such a judgement. Therefore one can just as well define the concept of a liveness property in terms of such a set.

**Definition 7** A *liveness property* of processes in an LTS is given by a set $G \subseteq A^*$. A process *p* satisfies this liveness property, notation $p \models liveness(G)$, when each complete trace of *p* has a prefix in *G*.

This formalisation of liveness properties is essentially different from the one in
[9] and most subsequent work on liveness properties; this point is discussed in
Section 6.

Just as for safety properties, the sets $G := \emptyset$ and $G := \{\epsilon\}$ specify trivial liveness properties.
**Theorem 5** A precongruence for the state operator respects every liveness property iff it respects the canonical liveness property.

**Proof:** Just like the proof of Theorem 1. □

A process $p$ has the *initial progress* property if it cannot immediately diverge or deadlock, i.e. if $\epsilon \notin \text{diverg}(p) \cup \text{deadlocks}(p)$. This is a liveness property, namely with $G$ the set of all sequences over $A^*$ of length 1. It can be understood this way by regarding any occurrence of an action as good.

**Theorem 6** A precongruence for abstraction that respects the initial progress property, respects the canonical liveness property.

**Proof:** Just like the proof of Theorem 2. □

By combining Theorems 5 and 6 one obtains:

**Corollary 2** A precongruence for abstraction and for the state operator that respects the initial progress property, respects all liveness properties.

**Conjecture 1** Any precongruence for $\mathcal{O}$ that respects a single nontrivial liveness property, respects every liveness property.

Let $\sqsubseteq_{liveness}$ denote the preorder that is fully abstract w.r.t. the class of liveness properties and $\mathcal{O}$. I will proceed to characterise $\sqsubseteq_{liveness}$ as the preorder $\sqsubseteq_{FDI}$ based on failures, divergences and infinite traces that is also used in the work on CSP [15]. *Failures* of a process $p$ are defined below; they are pairs $\langle\sigma, X\rangle$ such that $p$ can perform the sequence of visible actions $\sigma$ and then reach a state in which no further progress can be made in case the environment allows only those visible actions to occur that are listed in $X$. The preorder $\sqsubseteq_{FDI}$ does not take into account any information about the behaviour of processes that can be thought of taking place after a divergence. One of the ways to erase this information from the set of failures, divergences and infinite traces of a process is by means of *flooding*. Flooded sets of failures, divergences and infinite traces are indicated by the subscript $\perp$.

**Definition 8** Let $p \in \mathbb{P}$.

* $\text{initials}(p) := \{\alpha \in A_{\tau} \mid \exists q. p \xrightarrow{\alpha} q\}$.

* $\text{failures}(p) := \{\langle\sigma, X\rangle \in A^* \times \mathcal{P}(A) \mid \exists q. p \stackrel{\sigma}{\implies} q \land \text{initials}(q) \cap (X \cup \{\tau\}) = \emptyset\}$.

* $\text{diverg}_{\perp}(p) := \{\sigma\rho \mid \sigma \in \text{diverg}(p) \land \rho \in A^*\}$.

* $\text{inf}_{\perp}(p) := \{\sigma\rho \mid \sigma \in \text{diverg}(p) \land \rho \in A^{\infty}\}$.

* $\text{failures}_{\perp}(p) := \{\langle\sigma\rho, X\rangle \mid \sigma \in \text{diverg}(p) \land \rho \in A^* \land X \subseteq A\}$.

So $\text{deadlocks}(p) = \{\sigma \mid \langle\sigma, A\rangle \in \text{failures}(p)\}$
and $\text{ptraces}(p) = \text{diverg}(p) \cup \{\sigma \mid \langle\sigma, \emptyset\rangle \in \text{failures}(p)\}$.

**Theorem 7** $p \sqsubseteq_{liveness} q \Leftrightarrow \begin{array}{l} \text{diverg}_{\perp}(p) \supseteq \text{diverg}_{\perp}(q) \land \\ \text{inf}_{\perp}(p) \supseteq \text{inf}_{\perp}(q) \land \\ \text{failures}_{\perp}(p) \supseteq \text{failures}_{\perp}(q). \end{array}$
**Proof:** Let $\sqsubseteq_{\sqsubseteq_{FDI}}^{\perp}$ be the preorder defined by: $p \sqsubseteq_{\sqsubseteq_{FDI}}^{\perp} q$ iff the right-hand side of Theorem 7 holds.

“$\Leftarrow$”: It suffices to establish that $\sqsubseteq_{\sqsubseteq_{FDI}}^{\perp}$ is a liveness respecting precongruence.

To show that $\sqsubseteq_{\sqsubseteq_{FDI}}^{\perp}$ respects liveness, let $G \subseteq A^*$, $p \sqsubseteq_{\sqsubseteq_{FDI}}^{\perp} q$, and suppose $p \models liveness(G)$. I need to show that $q \models liveness(G)$. So suppose $\sigma \in CT(q)$. Then either $\sigma \in diverg(g) \subseteq diverg_{\perp}(g) \subseteq diverg_{\perp}(p)$ or $\sigma \in inf(p) \subseteq inf_{\perp}(p) \subseteq inf_{\perp}(q)$ or $\langle\sigma, A\rangle \in failures(q) \subseteq failures_{\perp}(q) \subseteq failures_{\perp}(q)$. In the first case $\rho \in diverg(p) \subseteq CT(p)$ for some $\rho \le \sigma$; in the second case either $\sigma \in inf(p) \subseteq CT(p)$ or $\rho \in diverg(p) \subseteq CT(p)$ for some $\rho < \sigma$; and in the third case either $\langle\sigma, A\rangle \in failures(p)$ or $\rho \in diverg(p) \subseteq CT(p)$ for some $\rho \le \sigma$. In all three cases $\rho \in CT(p)$ for some $\rho \le \sigma$. Since $p \models liveness(G)$, there must be a $\nu \le \rho$ with $\nu \in G$. As $\nu \le \sigma$ it follows that $q \models liveness(G)$.

That $\sqsubseteq_{\sqsubseteq_{FDI}}^{\perp}$ is a precongruence for $\|S\|$ and $\tau_I$ has been established in [15] by means of the following observations:

$$ \begin{align*} \operatorname{diverg}_{\perp}(p\|_S q) &= \{\sigma\rho \mid \exists\langle\nu, X\rangle \in \operatorname{failures}_{\perp}(p), \xi \in \operatorname{diverg}_{\perp}(q) \cdot \\ & \phantom{=} \sigma \in \nu\|_S \xi \wedge \rho \in A^*\} \\ & \phantom{=} \cup \{\sigma\rho \mid \exists\nu \in \operatorname{diverg}_{\perp}(p), \langle\xi, X\rangle \in \operatorname{failures}_{\perp}(q) \cdot \\ & \phantom{=} \sigma \in \nu\|_S \xi \wedge \rho \in A^*\} \end{align*} $$

$$ \begin{align*} \inf_{\perp}(p\|_S q) &= \{\sigma \mid \exists\nu \in \inf_{\perp}(p), \xi \in \inf_{\perp}(q). \sigma \in \nu\|_S \xi\} \cup \\ & \phantom{=} \{\sigma \mid \exists\langle\nu, X\rangle \in \operatorname{failures}_{\perp}(p), \xi \in \inf_{\perp}(q). \sigma \in \nu\|_S \xi\} \cup \\ & \phantom{=} \{\sigma \mid \exists\nu \in \inf_{\perp}(p), \langle\xi, X\rangle \in \operatorname{failures}_{\perp}(q). \sigma \in \nu\|_S \xi\} \cup \\ & \phantom{=} \{\sigma\rho \mid \sigma \in \operatorname{diverg}_{\perp}(p\|_S q) \wedge \rho \in A^{\infty}\} \end{align*} $$

$$ \begin{align*} \operatorname{failures}_{\perp}(p\|_S q) &= \{\langle\sigma, X \cup Y\rangle \mid \exists\langle\nu, X\rangle \in \operatorname{failures}_{\perp}(p), \langle\xi, Y\rangle \in \operatorname{failures}_{\perp}(q) \cdot \\ & \phantom{=} X \setminus S = Y \setminus S \wedge \sigma \in \nu\|_S \xi\} \\ & \phantom{=} \cup \{\langle\sigma, X\rangle \mid \sigma \in \operatorname{diverg}_{\perp}(p\|_S q) \wedge X \subseteq A\}. \end{align*} $$

$$ \operatorname{diverg}_{\perp}(\tau_I(p)) = \{\tau_I(\sigma)\rho \mid \tau_I(\sigma), \rho \in A^* \wedge \sigma \in \inf_{\perp}(p) \cup \operatorname{diverg}_{\perp}(p)\} $$

$$ \begin{align*} \inf_{\perp}(\tau_I(p)) &= \{\tau_I(\sigma) \mid \tau_I(\sigma) \in A^{\infty} \wedge \sigma \in \inf_{\perp}(p)\} \\ & \phantom{=} \cup \{\sigma\rho \mid \sigma \in \operatorname{diverg}_{\perp}(\tau_I(p)) \wedge \rho \in A^{\infty}\} \end{align*} $$

$$ \begin{align*} \operatorname{failures}_{\perp}(\tau_I(p)) &= \{\langle\tau_I(\sigma), X\rangle \mid \langle\sigma, X \cup I\rangle \in \operatorname{failures}_{\perp}(p)\} \\ & \phantom{=} \cup \{\langle\sigma, X\rangle \mid \sigma \in \operatorname{diverg}_{\perp}(\tau_I(p)) \wedge X \subseteq A\}. \end{align*} $$

Here $\tau_I(\sigma)$ for $\sigma \in A^{\infty}$ is the supremum, w.r.t. the prefix order $\le$ on $A^{\omega}$, of the set $\{\tau_I(\rho) \mid \rho < \sigma\}$.

Likewise, $\sqsubseteq_{\sqsubseteq_{FDI}}^{\perp}$ is a congruence for $\lambda_s^m$:

$$ \begin{align*} \operatorname{diverg}_{\perp}(\lambda_s^m(p)) &= \{\lambda_s^m(\sigma)\rho \mid \sigma \in \operatorname{diverg}_{\perp}(p) \wedge \rho \in A^*\} \\ \inf_{\perp}(\lambda_s^m(p)) &= \{\lambda_s^m(\sigma) \mid \sigma \in \inf_{\perp}(p)\} \\ & \phantom{=} \cup \{\sigma\rho \mid \sigma \in \operatorname{diverg}_{\perp}(\lambda_s^m(p)) \wedge \rho \in A^{\infty}\} \\ \operatorname{failures}_{\perp}(\lambda_s^m(p)) &= \{\langle\lambda_s^m(\sigma), X\rangle \mid \langle\sigma, \lambda_s^{-m}(X)\rangle \in \operatorname{failures}_{\perp}(p)\} \\ & \phantom{=} \cup \{\langle\sigma, X\rangle \mid \sigma \in \operatorname{diverg}_{\perp}(\lambda_s^m(p)) \wedge X \subseteq A\}. \end{align*} $$

Here $\lambda_s^{-m}(X) := \{a \in A \mid a(m, s) \in X\}$.

“$\Rightarrow$”: Let $\sqsubseteq$ be any liveness respecting precongruence, and suppose $p \sqsubseteq q$. I have to establish that $p \sqsubseteq_{\sqsubseteq_{FDI}}^{\perp} q$. W.l.o.g. I may assume that neither $p$ nor $q$ has any trace containing the action $g$. For let $\lambda^m$ be an injective renaming operator such that $g$ is not in the image of $\lambda^m$. Then $\lambda^m(p) \sqsubseteq \lambda^m(q)$. Suppose one can
establish $\lambda^m(p) \sqsubseteq_{\bar{F}_{DI}} \lambda^m(q)$. Since $\sqsubseteq_{\bar{F}_{DI}}$ is a precongruence for renaming, this yields $p \equiv_{\bar{F}_{DI}} \lambda^{-m}(\lambda^m(p)) \sqsubseteq_{\bar{F}_{DI}} \lambda^{-m}(\lambda^m(p)) \equiv_{\bar{F}_{DI}} q$.

Suppose $\operatorname{diverg}_{\perp}(p) \not\supseteq \operatorname{diverg}_{\perp}(q)$; say $\sigma \in \operatorname{diverg}_{\perp}(q) \setminus \operatorname{diverg}_{\perp}(p)$. So there is no $\rho \le \sigma$ with $\rho \in \operatorname{diverg}(p)$. Let $r$ be a deterministic process such that $CT(r) = \{\rho g \mid \rho < \sigma\} \cup \{\sigma\}$. Then each complete trace of $p\|^{gr}$ contains $g$. Here I write $\|^g$ for $\|_{A\setminus\{g\}}$, the interleaving operator that synchronises on all visible actions except $g$. As $\sqsubseteq$ is a precongruence, $p \sqsubseteq q$ implies $p\|^{gr} \sqsubseteq q\|^{gr}$, and since $\sqsubseteq$ respects the canonical liveness property, I obtain that each complete trace of $q\|^{gr}$ must contain $g$. However, $\rho \in \operatorname{diverg}(q)$ for some $\rho \le \sigma$. So $\rho \in CT(q\|^{gr})$, although $\rho$ does not contain $g$.

Suppose $\inf_{\perp}(p) \not\supseteq \inf_{\perp}(q)$; say $\sigma \in \inf_{\perp}(q) \setminus \inf_{\perp}(p)$. So $\sigma \notin \inf(p)$ and there is no $\rho < \sigma$ with $\rho \in \operatorname{diverg}(p)$. Let $r$ be a deterministic process such that $CT(r) = \{\rho g \mid \rho < \sigma\} \cup \{\sigma\}$. Then each complete trace of $p\|^{gr}$ contains $g$. As $\sqsubseteq$ is a precongruence, $p \sqsubseteq q$ implies $p\|^{gr} \sqsubseteq q\|^{gr}$, and since $\sqsubseteq$ respects the canonical liveness property, I obtain that each complete trace of $q\|^{gr}$ must contain $g$. However, either $\sigma \in \inf(q)$ or $\rho \in \operatorname{diverg}(q)$ for some $\rho < \sigma$. So either $\sigma \in CT(q\|^{gr})$ or $\rho \in CT(q\|^{gr})$, and neither $\sigma$ nor $\rho$ contains $g$.

Suppose $\operatorname{failures}_{\perp}(p) \not\supseteq \operatorname{failures}_{\perp}(q)$; say $\langle\sigma, X\rangle \in \operatorname{failures}_{\perp}(q) \setminus \operatorname{failures}_{\perp}(p)$. So $\langle\sigma, X\rangle \notin \operatorname{failures}(p)$ and there is no $\rho \le \sigma$ with $\rho \in \operatorname{diverg}(p)$. Let $r$ be a deterministic process with $CT(r) = \{\rho g \mid \rho < \sigma\} \cup \{\sigma a \mid a \in X\}$, and consider the liveness property given by $G := \{\rho g \mid \rho < \sigma\} \cup \{\sigma a \mid a \in X\}$. Then $p\|^{gr} \models \operatorname{liveness}(G)$. As $\sqsubseteq$ is a precongruence, $p \sqsubseteq q$ implies $p\|^{gr} \sqsubseteq q\|^{gr}$, and since $\sqsubseteq$ respects liveness properties, also $q\|^{gr} \models \operatorname{liveness}(G)$. However, either $\langle\sigma, X\rangle \in \operatorname{failures}(q)$ or there is an $\rho \le \sigma$ with $\rho \in \operatorname{diverg}(q)$. So either $\sigma \in CT(q\|^{gr})$ or $\rho \in CT(q\|^{gr})$ for some $\rho \le \sigma$, contradicting that $q\|^{gr} \models \operatorname{liveness}(G)$. $\square$

The standard refinement preorder used in CSP is in fact the *failures-divergences* preorder $\sqsubseteq_{FD}$, defined exactly like $\sqsubseteq_{\bar{F}_{DI}}$, but abstracting from the infinite traces. As remarked in [15], this can be done because in CSP one normally restricts attention to processes $p$ with the property that for any $\sigma \in A^*$ either $\sigma \in \operatorname{diverg}_{\perp}(p)$ or there are only finitely many processes $q$ with $p \stackrel{\sigma}{\Rightarrow} q$. For such processes the set $\inf_{\perp}(p)$ is, with Königs Lemma, completely determined by $\operatorname{failures}_{\perp}(p)$ and $\operatorname{diverg}_{\perp}(p)$, and thus need not be explicitly recorded. When extending CSP to processes not having this property, the component $\inf_{\perp}$ should be added to the semantics of processes [15]. In fact, $\sqsubseteq_{\bar{F}_{DI}}$ is the coarsest precongruence for $\mathcal{O}$ contained in $\sqsubseteq_{FD}$: if $p, q$ and $r$ are the processes used in the $\inf_{\perp}$-case of the above proof, and $I := A \setminus \{g\}$, then $\epsilon \in \operatorname{diverg}_{\perp}(\tau_I(q\|^{gr})) \setminus \operatorname{diverg}_{\perp}(\tau_I(p\|^{gr}))$.

The above characterisation as $\sqsubseteq_{\bar{F}_{DI}}$ of the coarsest congruence for $\mathcal{O}$ that respects all liveness properties, is somewhat robust under the choice of $\mathcal{O}$. It holds already for with just $\|^g$ and injective renaming (for these are the only two operators that are just in the proof), and it remains true when adding in all operators of CSP [4], as $\sqsubseteq_{\bar{F}_{DI}}$ is known to be a precongruence for all of them [15].

By Corollary 2, the above characterisation also remains valid when requiring respect for the initial progress property only, but to this end all three operators of $\mathcal{O}$ are needed. This result has in essence been obtained already by Bill Roscoe
in [15]. The state operator does not feature in [15]; its rôle in this full abstraction
result is taken over by a renaming operator that allows renaming an action *a* into
a choice between two actions *b* and *c*. When ignoring this difference in syntax,
Theorem 7 can be obtained as an immediate corollary of Corollary 2 and that
result. The main reason for using the above proof instead is to show that the
concealment or abstraction operator is not needed here.

By Theorem 5, $\sqsubseteq_{FDI}^{\perp}$ is even fully abstract w.r.t. the partially synchronous interleaving and state operators, and the canonical liveness property. This result, like the full abstraction result of [15], does not hold without the state operator, or something equally powerful, even if renaming and abstraction is allowed to be used. Namely, as pointed out by Antti Puhakka [13], one would fail to distinguish the following two processes:

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

# 5 Conditional Liveness Properties

Figure 1 presents two processes that have the same liveness properties in any

<figure><img src="image_3.png" /><figcaption>**Fig. 1.** *Two processes with the same liveness properties but different conditional liveness properties*</figcaption></figure>

CSP-context. The fact that only the left-hand process *can* do something good doesn't matter here, as neither of the two processes is *guaranteed* to do something good: they may never proceed beyond their initial $\tau$-loops. Nevertheless, from a practical point of view, the difference between these two processes may be enormous. It could be that the action *c* comes with a huge cost, that is only worth making when something good happens afterwards. Only the right-hand side process is able to incur the cost without any benefits, and for this reason it lacks an important property that the left-hand process has. I call such properties *conditional liveness properties* [6,11]. A *conditional liveness property* is a property that says that

*under certain conditions something good will eventually happen.*

To formulate a canonical conditional liveness property, assume that the alphabet
*A* contains two specific action *c* and *g*, where the occurrence of *c* is the condition,
and the occurrence of *g* is good. The canonical conditional liveness property now
says that **if c occurs then g will eventually happen.**
**Definition 9** A process $p$ satisfies the *canonical conditional liveness property*, notation $p \models liveness_c(g)$, if every complete trace of $p$ that contains the action $c$ also contains the action $g$.

To arrive at a general concept of conditional liveness property for labelled transition systems, assume that some condition, and some notion of *good* is defined. Now, to judge whether a process $p$ satisfies this conditional liveness property, one should judge first of all in which states the condition is fulfilled. All observable behaviour of $p$ that is recorded in a labelled transition system until one comes to such a verdict, is the sequence of visible actions performed until that point. Thus the condition is completely determined by the set sequences of visible actions that, when performed by $p$, lead to such a judgement. Next one should judge whether $p$ can reach a state in which one would say that something good had happened. Again, this judgement can be expressed in terms of the sequences of visible actions that lead to such a state.

**Definition 10** A *conditional liveness property* of processes in an LTS is given by two sets $C, G \subseteq A^*$. A process $p$ satisfies this conditional liveness property, notation $p \models liveness_C(G)$, when each complete trace of $p$ that has a prefix in $C$, also has prefix in $G$.

For the sake of added generality, one could make the notion of success dependent on the particular sequence of actions that fulfilled the condition. This would make $G$ a function from $C$ to $\mathcal{P}(A^*)$ and the requirement would be that each complete trace of $p$ that has a prefix $\sigma \in C$, also has prefix in $G(\sigma)$. However, such a generalised conditional liveness property can be expressed as a conjunction of standard ones, and a preorder that respects a given collection of properties also respects their conjunction.

**Theorem 8** A precongruence for the state operator respects every conditional liveness property iff it respects the canonical conditional liveness property.

**Proof:** "Only if" follows because the canonical conditional liveness property is in fact a conditional liveness property, namely the one with $C$ being the set of those sequences that contain the action $c$, and $G$ the set of those sequences that contain the action $g$.

"If": Again I use a state operator that remembers exactly what sequence of actions has occurred so far. Thus the set of internal states of its interface specification $m$ is $A^*$, and $\sigma(m, a) := \sigma a$ for all $\sigma \in A^*$ and $a \in A$. Note that the properties $liveness_C(G)$ and $liveness_{C\setminus G}(G)$ are satisfied by the same processes, so w.l.o.g. I may restrict attention to properties $liveness_C(G)$ with $C \cap G = \emptyset$. Given such a property, define

$$ a(m, \sigma) := \begin{cases} c & \text{if } \sigma a \in C \\ g & \text{if } \sigma a \in G \\ d & \text{otherwise.} \end{cases} $$
Then $\lambda_{\epsilon}^{m}(p) \models liveness_{c}(g)$ iff $p \models liveness_{C}(G)$. Thus, if $p \sqsubseteq q$ and $p \models liveness_{C}(G)$, then $\lambda_{\epsilon}^{m}(p) \sqsubseteq \lambda_{\epsilon}^{m}(q)$ and $\lambda_{\epsilon}^{m}(p) \models liveness_{c}(g)$. Hence $\lambda_{\epsilon}^{m}(q) \models liveness_{c}(g)$, so $q \models liveness_{C}(G)$. $\square$

An element $\sigma \notin \text{diverg}(p) \cup \text{deadlocks}(p)$ is called a deadlock/divergence trace of a process $p$. For any $\sigma \in A^*$, not having a deadlock/divergence trace $\sigma$ is a conditional liveness property, namely with $C := \{\sigma\}$ and $G := \{\sigma a \mid a \in A\}$. Using similar techniques as for Corollary 1, one can establish:

**Corollary 3** A precongruence for abstraction and for the state operator that respects the property of having no deadlock/divergence trace $c$, respects all liveness properties.

Let $\sqsubseteq_{\text{cond. liveness}}$ denote the preorder that is fully abstract w.r.t. the class of conditional liveness properties and $\mathcal{O}$. Furthermore, write $\sqsubseteq_{d/d}$ for the coarsest precongruence for $\mathcal{O}$ such that $q \sqsubseteq_{d/d} p$ implies $\text{deadlocks}(q) \cup \text{diverg}(q) \sqsubseteq \text{deadlocks}(p) \cup \text{diverg}(p)$.

**Corollary 4** $p \sqsubseteq_{\text{cond. liveness}} q$ iff $q \sqsubseteq_{d/d} p$.

**Proof:** "If" follows immediately from Corollary 3. "Only if" follows from the observation that the absence of any deadlock/divergence trace $\sigma$ is a conditional liveness property. $\square$

Antti Puhakka [13] has given a characterisation of the coarsest congruence that preserves deadlock/divergence traces, $\equiv_{d/d}$. His arguments easily extend to a characterisation of $\sqsubseteq_{d/d}$ and hence, using Corollary 4, of $\sqsubseteq_{\text{cond. liveness}}$. Below I will give a direct proof of the same result. It shows that this characterisation is already valid when merely requiring the precongruence property for $\|_{S}$ and injective renaming.

As for $\sqsubseteq_{\text{liveness}}$, the characterisation of $\sqsubseteq_{\text{cond. liveness}}$ is in terms of failures, divergences and infinite traces, and again some information needs to be erased, but less than in the case of $\sqsubseteq_{\text{liveness}}$. This time we need to forget about failures $\langle\sigma, X\rangle \in \text{failures}(p)$ such that $\sigma \in \text{diverg}(p)$, and about infinite traces of $p$ that have arbitrary long prefixes in $\text{diverg}(p)$. In [13] this is achieved by removal of such failures and infinite traces; here, in order to stress the similarity with the refinement preorder of CSP, I equivalently apply the method of flooding.

**Definition 11** Let $p \in \mathbb{P}$.

* $\text{inf}_d(p) := \text{inf}(p) \cup \{\sigma \in A^\infty \mid \forall \rho < \sigma \exists \nu \in \text{diverg}(p), \rho \le \nu < \sigma\}$.

* $\text{failures}_d(p) := \text{failures}(p) \cup \{\langle\sigma, X\rangle \mid \sigma \in \text{diverg}(p) \wedge X \subseteq A\}$.

**Theorem 9** $p \sqsubseteq_{\text{cond. liveness}} q \iff \begin{array}{l} \text{diverg}(p) \supseteq \text{diverg}(q) \wedge \\ \text{inf}_d(p) \supseteq \text{inf}_d(q) \wedge \\ \text{failures}_d(p) \supseteq \text{failures}_d(q). \end{array}$
**Proof:** Let $\sqsubseteq_{FDI}^d$ be the preorder defined by: $p \sqsubseteq_{FDI}^d q$ iff the right-hand side of Theorem 7 holds.

“$\Leftarrow$”: It suffices to establish that $\sqsubseteq_{FDI}^d$ is a precongruence for $\mathcal{O}$ that respects all conditional liveness properties.

To show that $\sqsubseteq_{FDI}^d$ respects conditional liveness properties, let $C, G \subseteq A^*$, $p \sqsubseteq_{FDI}^d q$, and suppose $p \models liveness_C(G)$. I need to show that $q \models liveness_C(G)$. So suppose $\sigma \in CT(q)$ and $\rho \in C$ for some prefix $\rho \le \sigma$. Then one out of three possibilities must apply: either $\sigma \in \text{diverg}(g) \subseteq \text{diverg}(p)$ or $\sigma \in \text{inf}(q) \subseteq \text{inf}_d(q) \subseteq \text{inf}_d(p)$ or $\langle\sigma, A\rangle \in \text{failures}(q) \subseteq \text{failures}_d(q) \subseteq \text{failures}_d(p)$. In the first and last case, one has $\sigma \in CT(p)$. Since $p \models liveness_C(G)$, there must be a $\xi \le \sigma$ with $\xi \in G$, which had to be shown. In the second case either $\sigma \in \text{inf}(p) \subseteq CT(p)$, in which case the argument proceeds as above, or $\exists \nu \in \text{diverg}(p) \subseteq CT(p)$ with $\rho \le \nu < \sigma$. In the latter case, there must be a $\xi \le \nu$ with $\xi \in G$, and as $\nu < \sigma$ it follows that $q \models liveness_C(G)$.

That $\sqsubseteq_{FDI}^d$ is a precongruence for $\|_S$, $\tau_I$ and $\lambda_s^m$ follows from the following observations:

$$
\begin{align*}
\text{diverg}(p\|_S q) &= \{\sigma \mid \exists\langle\nu, X\rangle \in \text{failures}_d(p), \xi \in \text{diverg}(q). \sigma \in \nu\|_S \xi\} \cup \\
&\phantom{=} \{\sigma \mid \exists\nu \in \text{diverg}(p), \langle\xi, X\rangle \in \text{failures}_d(q). \sigma \in \nu\|_S \xi\} \\
\text{inf}_d(p\|_S q) &= \{\sigma \mid \exists\nu \in \text{inf}_d(p), \xi \in \text{inf}_d(q). \sigma \in \nu\|_S \xi\} \cup \\
&\phantom{=} \{\sigma \mid \exists\langle\nu, X\rangle \in \text{failures}_d(p), \xi \in \text{inf}_d(q). \sigma \in \nu\|_S \xi\} \cup \\
&\phantom{=} \{\sigma \mid \exists\nu \in \text{inf}_d(p), \langle\xi, X\rangle \in \text{failures}_d(q). \sigma \in \nu\|_S \xi\} \cup \\
&\phantom{=} \{\sigma \in A^\infty \mid \forall\rho < \sigma \exists\nu \in \text{diverg}(p\|_S q). \rho \le \nu < \sigma\} \\
\text{failures}_d(p\|_S q) &= \{\langle\sigma, X \cup Y\rangle \mid \exists\langle\nu, X\rangle \in \text{failures}_d(p), \langle\xi, Y\rangle \in \text{failures}_d(q). \\
&\phantom{=} X \setminus S = Y \setminus S \land \sigma \in \nu\|_S \xi\} \\
&\phantom{=} \cup \{\langle\sigma, X\rangle \mid \sigma \in \text{diverg}(p\|_S q) \land X \subseteq A\}. \\
\text{diverg}(\tau_I(p)) &= \{\tau_I(\sigma) \mid \tau_I(\sigma) \in A^* \land \sigma \in \text{inf}_d(p) \cup \text{diverg}(p)\} \\
\text{inf}_d(\tau_I(p)) &= \{\tau_I(\sigma) \mid \tau_I(\sigma) \in A^\infty \land \sigma \in \text{inf}_d(p)\} \\
&\phantom{=} \cup \{\sigma \in A^\infty \mid \forall\rho < \sigma \exists\nu \in \text{diverg}(\tau_I(p)). \rho \le \nu < \sigma\} \\
\text{failures}_d(\tau_I(p)) &= \{\langle\tau_I(\sigma), X\rangle \mid \langle\sigma, X \cup I\rangle \in \text{failures}_d(p)\} \\
&\phantom{=} \cup \{\langle\sigma, X\rangle \mid \sigma \in \text{diverg}(\tau_I(p)) \land X \subseteq A\} \\
\text{diverg}(\lambda_s^m(p)) &= \{\lambda_s^m(\sigma) \mid \sigma \in \text{diverg}(p)\} \\
\text{inf}_d(\lambda_s^m(p)) &= \{\lambda_s^m(\sigma) \mid \sigma \in \text{inf}_d(p)\} \\
&\phantom{=} \cup \{\sigma \in A^\infty \mid \forall\rho < \sigma \exists\nu \in \text{diverg}(\lambda_s^m(p)). \rho \le \nu < \sigma\} \\
\text{failures}_d(\lambda_s^m(p)) &= \{\langle\lambda_s^m(\sigma), X\rangle \mid \langle\sigma, \lambda_s^{-m}(X)\rangle \in \text{failures}_d(p)\} \\
&\phantom{=} \cup \{\langle\sigma, X\rangle \mid \sigma \in \text{diverg}(\lambda_s^m(p)) \land X \subseteq A\}.
\end{align*}
$$

“⇒”: Let $\sqsubseteq$ be any precongruence for $\mathcal{O}$ that respects conditional liveness properties, and suppose $p \sqsubseteq q$. I have to establish that $p \sqsubseteq_{FDI}^d q$. W.l.o.g. I may assume that neither $p$ nor $q$ has any trace containing the actions $c$ or $g$. The argument for this is as in the proof of Theorem 7.

Suppose $\text{diverg}(p) \not\subseteq \text{diverg}(q)$; say $\sigma \in \text{diverg}(q) \setminus \text{diverg}(p)$. Let $r$ be a deterministic process such that $CT(r) = \{\sigma cg\}$. Then each complete trace of $p\|^{c,g}r$ that contains $c$ also contains $g$. Here I write $\|^{c,g}$ for $\|_{A\setminus\{c,g\}}$, the interleaving operator that synchronises on all visible actions except $c$ and $g$. As $\sqsubseteq$ is a precongruence, $p \sqsubseteq q$ implies $p\|^{c,g}r \sqsubseteq q\|^{c,g}r$, and since $\sqsubseteq$ respects the canonical conditional liveness property, I obtain that each complete
trace of $q^{\|c,g\}r$ that contains $c$ must also contain $g$. However, as $\sigma \in \text{diverg}(q)$, $\sigma c \in \text{diverg}(q^{\|c,g\}r) \subseteq CT(q^{\|c,g\}r)$, although $\sigma c$ does not contain $g$.

Suppose $\text{inf}_{\text{d}}(p) \supsetneq \text{inf}_{\text{d}}(q)$; say $\sigma \in \text{inf}_{\text{d}}(q) \setminus \text{inf}_{\text{d}}(p)$. So $\sigma \notin \text{inf}(p)$ and there is a $\rho < \sigma$ such that $\rho \le \rho\nu < \sigma$ for no sequence $\rho\nu \in \text{diverg}(p)$. Let $r$ be a deterministic process such that $CT(r) = \{\rho c\text{vg} \mid \rho\nu < \sigma\} \cup \{\sigma\}$. Then each complete trace of $p^{\|g\}r$ that contains $c$, must also contain $g$. As $\sqsubseteq$ is a precongruence, $p \sqsubseteq q$ implies $p^{\|c,g\}r \sqsubseteq q^{\|g,c\}r$, and since $\sqsubseteq$ respects the canonical conditional liveness property, I obtain that each complete trace of $q^{\|c,g\}r$ that contains $c$ must also contain $g$. However, either $\sigma \in \text{inf}(q)$ or $\rho\nu \in \text{diverg}(q)$ for some $\rho \le \rho\nu < \sigma$. In each case $q^{\|c,g\}r$ has a complete trace that contains $c$ but not $g$.

Suppose $\text{failures}_d(p) \supsetneq \text{failures}_d(q)$; say $\langle\sigma, X\rangle \in \text{failures}_d(q) \setminus \text{failures}_d(p)$. So $\langle\sigma, X\rangle \notin \text{failures}(p)$ and $\sigma \notin \text{diverg}(p)$. Let $r$ be a deterministic process with $CT(r) = \{\sigma ca \mid a \in X\}$, let $C$ be the set of sequences containing $c$, and consider the conditional liveness property given by $C$ and $G := \{\sigma ca \mid a \in X\}$. Then $p^{\|c}r \models \text{liveness}_C(G)$. As $\sqsubseteq$ is a precongruence, $p \sqsubseteq q$ implies $p^{\|c}r \sqsubseteq q^{\|c}r$, and since $\sqsubseteq$ respects conditional liveness properties, also $q^{\|g}r \models \text{liveness}_C(G)$. However, either $\langle\sigma, X\rangle \in \text{failures}(q)$ or $\sigma \in \text{diverg}(q)$. So $\sigma c \in CT(q^{\|g}r)$, contradicting that $q^{\|c}r \models \text{liveness}_C(G)$. $\square$

In [14], Bill Roscoe has shown that $\underline{\sqsubseteq}_{\text{FDI}}^d$ is a precongruence for all operators of CSP; he also developed a new fixed point theory that shows that it is a congruence for recursion as well.

# 6 Linear Time Properties

Safety, liveness, and conditional liveness properties, as studied in the previous sections, are special cases of linear time properties. A linear time property can be thought of as any requirement on the observable content of the runs of a process. The property is satisfied by a process when the observable content of all its maximal runs satisfy this requirement. Hence a linear time property can be formalised by the set of sequences over $A^\omega$ that, when performed in a maximal run of a process, meet the requirement.

**Definition 12** A linear time property of processes in an LTS is given by a set $P \subseteq A^\omega$. A process $p$ satisfies this property, notation $p \models P$, when $CT(p) \subseteq P$.

A safety property is a special kind of linear time property, namely $\text{safety}(B) = \{\sigma \in A^\omega \mid \neg\exists\rho \in B. \rho \le \sigma\}$. Likewise, $\text{liveness}(G) = \{\sigma \in A^\omega \mid \exists\rho \in G. \rho \le \sigma\}$, and $\text{liveness}_C(G) = \{\sigma \in A^\omega \mid (\exists\rho \in C. \rho \le \sigma) \Rightarrow (\exists\nu \in G. \nu \le \sigma)\}$.

In [9] and most subsequent work, liveness properties are formalised in a different way than in this paper. For the canonical liveness property it is fundamentally impossible to ever tell that it is not going to be satisfied when one has only observed a finite prefix of a maximal run of a process. For if “something good” is promised to happen, it is always possible to assume it will be further in the future. In [9], this is taken to be the defining characteristic of liveness properties, and a property $P$ is called a liveness property iff $\forall\rho \in A^*. \exists\sigma \in P. \rho \le \sigma$.
The property *liveness*($G$) with $G = \{a\}$ for instance says that the first visible action of a process should be an $a$. It is a liveness property in my sense, since the first action being an $a$ can be thought of as a good thing that happened eventually; here the requirement that it has to happen as first action could be part of one's concept of *good*. However, it is not a liveness property as formalised in [9] and subsequent work, since the occurrence of a $b \neq a$ as first action proves that the property will never be satisfied.

The property that from some point onwards all visible actions a process performs should be $g$'s, is an example of a liveness property in the sense of [9] that is not a liveness property in my sense. Namely, at no point can one ever tell that something good has happened.

A well known theorem [9] says that any linear time property $P$ can be written as the conjunction $safety(B) \cap P_{liveness}$ of a safety property and a liveness property in the sense of [9]. Namely,

$$ B := \{ \rho \in A^* | \neg \exists \sigma \in P. \rho \leq \sigma \} \quad \text{and} \quad P_{liveness} := P \cup (A^\omega \setminus safety(B)). $$

Such a theorem does not hold for my liveness properties.

My characterisation of $\sqsubseteq_{liveness}$ would still be valid if I would have taken as class of liveness properties the intersection of mine and the ones from [9]. This follows immediately from Theorem 5, as the canonical liveness property is in this intersection. So the extra generality in my definition is harmless. However, the extra restriction makes a difference, as the canonical conditional liveness property, for instance, is a liveness property in the sense of [9].

Liveness properties in the sense of [9] are studied because proving them requires a different tool set than proving safety properties. However, as far as practical applications are concerned, one is mostly interested in conjunctions of safety and liveness properties, i.e. general linear time properties. I will therefore not try to characterise coarsest congruences that respect just the liveness properties in the sense of [9].

The coarsest congruence respecting all linear time properties has been characterised as NDFD-equivalence by Roope Kaivola and Antti Valmari in [8]; this results extends to preorders in a straightforward way. The NDFD preorder can be defined just like $\sqsubseteq_{FDI}^d$, except that $inf(\_)$ is used instead of $inf(\_\_)$). In fact, this result can also be obtained as corollary of what we have seen so far.

$$ \textbf{Theorem 10} \quad p \sqsubseteq_{lt\text{-}properties} q \Leftrightarrow \begin{array}{l} \text{diverg}(p) \supseteq \text{diverg}(q) \wedge \\ \text{inf}(p) \supseteq \text{inf}(q) \wedge \\ \text{failures}_d(p) \supseteq \text{failures}_d(q). \end{array} $$

**Proof:** Let $\sqsubseteq_{NDFD}$ be the preorder defined by: $p \sqsubseteq_{NDFD} q$ iff the right-hand side of Theorem 10 holds.

“$\Leftarrow$”: It suffices to establish that $\sqsubseteq_{NDFD}$ is a precongruence for $\mathcal{O}$ that respects all linear time properties.

To show that $\sqsubseteq_{NDFD}$ respects linear time properties, let $P \subseteq A^\omega$, $p \sqsubseteq_{NDFD} q$, and suppose $p \models P$. I need to show that $q \models P$. So suppose $\sigma \in CT(q)$. Then either $\sigma \in \text{diverg}(g) \subseteq \text{diverg}(p)$ or $\sigma \in \text{inf}(q) \subseteq \text{inf}(q)$ or $\langle \sigma, A \rangle \in \text{failures}(q) \subseteq$
$failures_d(q) \subseteq failures_d(p)$. In the last case, one has either $\langle\sigma, A\rangle \in failures(p)$ or $\sigma \in diverg(p)$. So in all cases $\sigma \in CT(p)$. Since $p \models P$, it must be that $\sigma \in P$. It follows that $CT(q) \subseteq P$, i.e. $q \models P$.

That $\sqsubseteq_{FDI}^d$ is a precongruence for $\|_S$, $\tau_I$ and $\lambda_s^m$ follows from similar, but simpler, observations as in the proof of Theorem 9.

“⇒”: Let $\sqsubseteq$ be any precongruence for $\mathcal{O}$ that respects linear time properties, and suppose $p \sqsubseteq q$. I have to establish that $p \sqsubseteq_{NDFD} q$. That $diverg(p) \supset diverg(q)$ and $failures_d(p) \supset failures_d(q)$ follows immediately from Theorem 9, using that conditional liveness properties are linear time properties. That $inf(p) \supset inf(q)$ follows immediately by considering the linear time property $CT(p)$. $\square$

To obtain this result it suffices to define $\sqsubseteq_{lt\text{-}properties}$ as the coarsest precongruence w.r.t. $\|_S$ and injective renaming that respects all linear time properties. However, it happens to also be a precongruence for all operators of CSP.

Linear time properties do not capture the entire observable behaviour or processes in the neutral environment. Orthogonal to them are *possibility properties*, such as: a process *may* do an action *g*. As argued by Leslie Lamport, “verifying possibility properties tells you nothing interesting about a system” [10]. Nevertheless, it is not hard to characterise the coarsest precongruence for $\mathcal{O}$ that respects linear time properties as well as all possibility properties, and thereby arguably the entire observable behaviour of a process in a neutral environment. It is $\equiv_{NDFD}$, the symmetric closure of $\sqsubseteq_{NDFD}$.

# 7 Concluding remark

The methodology of the paper is close in spirit to the work on testing equiva-
lences by Rocco De Nicola and Matthew Hennessy [5], and the results in Sec-
tions 3 and 4 are comparable as well. The notion of *must testing* of [5] could be
reinterpreted as a way to test liveness properties, and hence, unsurprisingly, my
preorder $\sqsubseteq_{liveness}$ is exactly the must-testing preorder of [5]. However, my safety
preorder is exactly the *inverse* of the *may testing* preorder of [5]. This can be
explained by thinking, in the context of may testing, of the “success”-action $\omega$
as marking a state of *failure*, rather than one of *success*. Now the property of
whether a process may reach $\omega$ is exactly the negation of whether it will always
avoid $\omega$. This turns may-testing around, from testing certain possibility proper-
ties, to testing safety properties. It remains to elaborate a theory of testing that
captures the concept of conditional liveness.

# References

1. M. Alexander & W. Gardner, editors (2008): *Process Algebra for Parallel and Distributed Processing*. Chapman & Hall.

2. J.C.M. Baeten & J.A. Bergstra (1988): *Global renaming operators in concrete process algebra*. *Information and Computation* 78(3), pp. 205–245.

3. J.A. Bergstra & J.W. Klop (1985): *Algebra of communicating processes with abstraction*. *Theoretical Computer Science* 37(1), pp. 77–121.
4. S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): *A theory of communicating sequential processes*. Journal of the ACM 31(3), pp. 560-599.

5. R. De Nicola & M. Hennessy (1984): *Testing equivalences for processes*. Theoretical Computer Science 34, pp. 83-133.

6. R.J. van Glabbeek & M. Voorhoeve (2006): *Liveness, Fairness and Impossible Futures*. In: Christel Baier & Holger Hermanns, editors: CONCUR, LNCS 4137, Springer, pp. 126-141. Available at http://dx.doi.org/10.1007/11817949_9.

7. R.J. van Glabbeek (2001): *The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes*. In: J.A. Bergstra, A. Ponse & S.A. Smolka, editors: Handbook of Process Algebra, chapter 1, Elsevier, pp. 3-99. Available at http://Boole.stanford.edu/pub/spectrum1.ps.gz.

8. R. Kaivola & A. Valmari (1992): *The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic*. In: Rance Cleaveland, editor: CONCUR'92, LNCS 630, Springer, pp. 207-221. Available at http://dx.doi.org/10.1007/BFb0084793.

9. L. Lamport (1977): *Proving the correctness of multiprocess programs*. IEEE Transactions on Software Engineering 3(2), pp. 125-143.

10. Leslie Lamport (1998): *Proving Possibility Properties*. Theoretical Computer Science 206(1-2), pp. 341-352. See especially http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-possibility.

11. P.B. Levy (2008): *Infinite trace equivalence*. Annals of Pure and Applied Logic 151(2-3), pp. 170-198. Available at http://dx.doi.org/10.1016/j.apal.2007.10.007.

12. R. Milner (1990): *Operational and algebraic semantics of concurrent processes*. In: J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201-1242. Alternatively see *Communication and Concurrency*, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as *A Calculus of Communicating Systems*, LNCS 92, Springer-Verlag, 1980.

13. A. Puhakka (2001): *Weakest Congruence Results Concerning "Any-Lock"*. In: N. Kobayashi & B.C. Pierce, editors: Proceedings TACS'01, LNCS 2215, Springer, pp. 400-419.

14. A.W. Roscoe (2004): *Seeing Beyond Divergence*. In: Ali E. Abdallah, Cliff B. Jones & Jeff W. Sanders, editors: 25 Years Communicating Sequential Processes, Lecture Notes in Computer Science 3525, Springer, pp. 15-35. Available at http://dx.doi.org/10.1007/11423348_2.

15. A.W. Roscoe (1997): *The Theory and Practice of Concurrency*. Prentice-Hall. Available at http://www.comlab.ox.ac.uk/bill.roscoe/publications/68b.pdf.