15312 LABEL:LastPageJul. 02, 2018Aug. 07, 2019

* This is an extended version of the paper with the same title, published in the proceedings of CONCUR 2017 [DHS17].

# Divergence and unique solution of equations

Adrien Durier  Univ. Lyon, ENS de Lyon, CNRS, UCB Lyon 1, LIP
<EMAIL_ADDRESS><EMAIL_ADDRESS>,  Daniel Hirschkoff
and  Davide Sangiorgi  INRIA and Università di Bologna
<EMAIL_ADDRESS>
###### Abstract.

We study proof techniques for bisimilarity based on _unique solution of
equations_.

We draw inspiration from a result by Roscoe in the denotational setting of CSP
and for failure semantics, essentially stating that an equation (or a system
of equations) whose infinite unfolding never produces a divergence has the
unique-solution property. We transport this result onto the operational
setting of CCS and for bisimilarity. We then exploit the operational approach
to: refine the theorem, distinguishing between different forms of divergence;
derive an abstract formulation of the theorems, on generic LTSs; adapt the
theorems to other equivalences such as trace equivalence, and to preorders
such as trace inclusion. We compare the resulting techniques to enhancements
of the bisimulation proof method (the ‘up-to techniques’). Finally, we study
the theorems in name-passing calculi such as the asynchronous $\pi$-calculus,
and use them to revisit the completeness part of the proof of full abstraction
of Milner’s encoding of the $\lambda$-calculus into the $\pi$-calculus for
Lévy-Longo Trees.

###### Key words and phrases:

Bisimilarity, unique solution of equations, termination, process calculi

##  1\. Introduction

In this paper we study the technique of _unique solution of equations_ for
(weak) behavioural relations. We mainly focus on bisimilarity but we also
consider other equivalences, such as trace equivalence, as well as preorders
such as trace inclusion. Roughly, the technique consists in proving that two
tuples of processes are componentwise in a given behavioural relation by
establishing that they are solutions of the same system of equations.

In this work, behavioural relations, hence also bisimilarity, are meant to be
_weak_ because they abstract from internal moves of terms, as opposed to the
_strong_ relations, which make no distinctions between the internal moves and
the external ones (i.e., the interactions with the environment). Weak
equivalences are, practically, the most relevant ones: e.g., two equal
programs may produce the same result with different numbers of evaluation
steps. Further, the problems tackled in this paper only arise in the weak
case.

The technique of unique solution has been proposed by Milner in the setting of
CCS, and plays a prominent role in proofs of examples in his book [Mil89]. The
method is important in verification techniques and tools based on algebraic
reasoning [Ros10, BBR10, GM14]. Not all equations have a unique solution: for
instance any process trivially satisfies $X=X$. To ensure unique solution, it
is often required that equations satisfy some kind of _guardedness_ condition;
see, e.g., [BW90, GM14]. In CCS, the notion of guardedness is syntactic:
variables of the equations can only appear underneath a visible prefix. This
is not sufficient to guarantee uniqueness. Hence, in Milner’s theorem [Mil89],
uniqueness of solutions relies on an additional limitation: the equations must
be ‘sequential’, that is, the variables of the equations may not be preceded,
in the syntax tree, by the parallel composition operator. This limits the
expressiveness of the technique (since occurrences of other operators above
the variables, such as parallel composition and restriction, in general cannot
be removed), and its transport onto other languages (e.g., languages for
distributed systems or higher-order languages usually do not include the sum
operator, which makes the theorem essentially useless). A comparable
technique, involving similar limitations, has been proposed by Hoare in his
book about CSP [Hoa85], and plays an equally essential role in the theory of
CSP.

In order to overcome such limitations, a variant of the technique, called
_unique solution of contractions_ , has been proposed [San15]. The technique
is for behavioural equivalences; however the meaning of ‘solution’ is defined
in terms of the contraction of the chosen equivalence. Contraction is,
intuitively, a preorder that conveys an idea of efficiency on processes, where
efficiency is measured on the number of internal actions needed to perform a
certain activity. The condition for applicability of the technique is, as for
Milner’s, purely syntactic: each variable in the body of an equation should be
underneath a prefix. The technique has two main disadvantages: 1\. the
equational theory of the contraction preorder associated to an equivalence is
not the same as the equational theory of the equivalence itself, which thus
needs to be studied as well; 2\. the contraction preorder is strictly finer
than the equivalence, hence there are equivalent processes, one of which might
be solution of a given contraction, while the other is not, and the technique
might not be applicable in this case.

In this paper we explore a different approach, inspired by results by Roscoe
in CSP [Ros97, Ros92], essentially stating that a guarded equation (or system
of equations) whose infinite unfolding never produces a divergence has the
unique-solution property. Roscoe’s result is presented, as usual in CSP, with
respect to denotational semantics and failure based equivalence [BHR84, BR84].
In such a setting, where divergence is catastrophic (e.g., it is the bottom
element of the domain), the theorem has an elegant and natural formulation.
(Indeed, Roscoe develops a denotational model [Ros92] in which the proof of
the theorem is just a few lines.)

We draw inspiration from Roscoe’s work to formulate the counterpart of these
results in the operational setting of CCS and bisimilarity. In comparison with
the denotational CSP proof, the operational CCS proof is more complex. The
operational setting offers however a few advantages. First, we can formulate
more refined versions of the theorem, in which we distinguish between
different forms of divergence. Notably, we can ignore divergences that appear
after finite unfoldings of the equations, called _innocuous_ divergences in
this paper. (These refinements would look less natural in the denotational and
trace-based setting of CSP, where any divergence causes a process to be
considered undefined.) A second and more important advantage comes as a
consequence of the flexibility of the operational approach: the unique-
solution theorems can be tuned to other behavioural relations (both
equivalences and preorders), and to other languages.

To highlight the latter aspect, we present abstract formulations of the
theorems, on a generic LTS (i.e., without reference to CCS). In this abstract
formulation, the body of an equation becomes a function on the states of the
LTS. The theorems for CCS are instances of the abstract formulations.
Similarly we can derive analogous theorems for other languages. Indeed we can
do so for all languages whose constructs have an operational semantics with
rules in the GSOS format [BIM88] (assuming appropriate hypotheses, among which
congruence properties). In contrast, the analogous theorems fail for languages
whose constructs follow the _tyft/tyxt_ [GV92] format, due to the possibility
of rules with a _lookahead_. We also consider extensions of the theorems to
name-passing calculi such as the $\pi$-calculus.

The abstract version of our main unique-solution theorem has been formalised
using the Coq proof assistant [Dur17].

The bisimulation proof method is a well-established and extensively studied
technique for deriving bisimilarity results. An advantage of this method are
its enhancements, provided by the so called ‘up-to techniques’ [PS11].
Powerful such enhancements are ‘up to context’, whereby in the derivatives of
two terms a common context can be erased, ‘up to expansion’, whereby two
derivatives can be rewritten using the expansion preorder, and ‘up to
transitivity’, whereby the matching between two derivatives is made with
respect to the transitive closure of the candidate relation (rather than the
relation alone). Different enhancements can sometimes be combined, though care
is needed to preserve soundness. One of the most powerful combinations is an
_‘up to transitivity and context’_ technique due to Pous, which relies on a
termination hypothesis [Pou08]. This technique generalises ‘up to expansion’
and combines it with ‘up to context’ and ‘up to transitivity’. We show that,
modulo an additional hypothesis, our techniques are at least as powerful as
this up-to technique: any up-to relation can be turned into a system of
equations of the same size (where the size of a relation is the number of its
pairs, and the size of a system of equations is the number of its equations)
for which uniqueness of solutions holds.

An important difference between unique solution of equations and up-to
techniques arises in the (asynchronous) $\pi$-calculus. In this setting, forms
of bisimulation enhancements that involve ‘up to context’, such as ‘up to
expansion and context’, require closure of the candidate relation under
substitutions (or instantiation of the formal parameters of an abstraction
with arbitrary actual parameters). It is an open problem whether this closure
is necessary in the asynchronous $\pi$-calculus, where bisimilarity is closed
under substitutions. Our unique-solution techniques are strongly reminiscent
of up to context techniques (the body of an equation acts like a context that
is erased in a proof using ‘up to context’); yet, surprisingly, no closure
under substitutions is required.

As an example of application of our techniques in the $\pi$-calculus, we
revisit the completeness part of the proof of full abstraction for the
encoding of the call-by-name $\lambda$-calculus into the $\pi$-calculus
[San00, SX18] with respect to Levy-Longo Trees (LTs). The proof in [San00,
SX18] uses ‘up to expansion and context’. Such up-to techniques seem to be
essential: without them, it would be hard even to define the bisimulation
candidate. For our proof using unique-solution, there is one equation for each
node of a given LT, describing the shape of such node. (By the time the
revision of this paper has been completed, we have used to the technique to
establish full abstraction for the encoding of the call-by-value
$\lambda$-calculus [DHS18].)

_Outline of the paper:_ Section 2 provides background about CCS and
behavioural relations. We formulate our main results for CCS in Section 3, and
generalise them in an abstract setting in Section 4. Section 5 shows how our
results can be applied to the $\pi$-calculus.

_Comparison with the results published in[DHS17]:_ this paper is an extended
version of [DHS17]. We provide here detailed proofs which were either absent
or only sketched in [DHS17], notably for: our two main unique-solution
theorems (Theorems 3.1 and 3.2); the comparison with up-to techniques in
Section 3.4.2; the analysis of call-by-name $\lambda$-calculus in the
asynchronous $\pi$-calculus (Theorem 5.2). We also include more detailed
discussions along the paper, notably about the applicability of our techniques
(in particular, Lemma 5.1, Propositions 4.3 and Proposition 4.2, and Remark
3.2).

##  2\. Background

#### CCS

We assume an infinite set of _names_ $a,b,\ldots$ and a set of _constant
identifiers_ (or simply _constants_) to write recursively defined processes.
The special symbol $\tau$ does not occur in the names and in the constants.
The class of the CCS processes is built from the operators of parallel
composition, guarded sum, restriction, and constants, and the guard of a sum
can be an input, an output, or a silent prefix:

$\begin{array}[]{ccl}P&:=&\;P_{1}|P_{2}\;\;\;\mbox{\Large{$\mid$}}\;\;\;\Sigma_{i\in
I}\mu_{i}.P_{i}\;\;\;\mbox{\Large{$\mid$}}\;\;{\boldsymbol{\nu}}a\>P\;\;\;\mbox{\Large{$\mid$}}\;\;\;K\end{array}\qquad\qquad\begin{array}[]{ccl}\mu&:=&a\;\;\;\mbox{\Large{$\mid$}}\;\;\;\overline{a}\;\;\;\mbox{\Large{$\mid$}}\;\;\;\tau\end{array}$

where $I$ is a countable indexing set. Sums are guarded to ensure that
behavioural equivalences and preorders are substitutive. We write
${\boldsymbol{0}}$ when $I$ is empty, and $P+Q$ for binary sums, with the
understanding that, to fit the above grammar, $P$ and $Q$ should be sums of
prefixed terms. Each constant $K$ has a definition
$K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}P$. We sometimes
omit trailing ${\boldsymbol{0}}$, e.g., writing $a|b$ for
$a.{\boldsymbol{0}}|b.{\boldsymbol{0}}$ . We write $\mu^{n}.P$ for $P$
preceded by $n$ $\mu$-prefixes. In a few examples we write $!\mu.P$ as
abbreviation for the constant
$K_{\mu.P}\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\mu.(P|K_{\mu.P})$.
The operational semantics is given by means of a Labelled Transition System
(LTS), and is given in Figure 1 (the symmetric versions of the rules
$\mathtt{parL}$ and $\mathtt{comL}$ have been omitted). The _immediate
derivatives_ of a process $P$ are the elements of the set
$\\{P^{\prime}\;\mid\;P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}\mbox{
for some $\mu$ }\\}$. We use $\ell$ to range over visible actions (i.e.,
inputs or outputs, excluding $\tau$).

$\mathtt{sum}$ $\displaystyle{\over\Sigma_{i\in
I}\mu_{i}.P_{i}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P_{i}}$
$\mathtt{parL}$
$\displaystyle{P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}\over
P|Q\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}|Q}$
$\mathtt{comL}$
$\displaystyle{P\mathrel{\stackrel{{\scriptstyle{\;\;a\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}\hskip
5.69046pt\hskip
5.69046ptQ\mathrel{\stackrel{{\scriptstyle{\;\;\overline{a}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}Q^{\prime}\over
P|Q\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}|Q^{\prime}}$

$\mathtt{res}$
$\displaystyle{P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}\over{\boldsymbol{\nu}}a\>P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}{\boldsymbol{\nu}}a\>P^{\prime}}$
$\mu\neq a,\overline{a}$ $\mathtt{const}$
$\displaystyle{P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}\over
K\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}}$
if $K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}P$

Figure 1. The LTS for CCS

Some standard notations for transitions: $\Longrightarrow$ is the reflexive
and transitive closure of
$\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}$,
and
$\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
is
$\Longrightarrow\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\Longrightarrow$
(the composition of the three relations). Moreover,
$P\mathrel{\stackrel{{\scriptstyle{\;\;\hat{\mu}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}$
holds if
$P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}$
or ($\mu=\tau$ and $P=P^{\prime}$); similarly
$P\mathrel{\stackrel{{\scriptstyle{\;\;{\hat{\mu}}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}P^{\prime}$
holds if
$P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}P^{\prime}$
or ($\mu=\tau$ and $P=P^{\prime}$). We write
$P(\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}})^{n}P^{\prime}$
if $P$ can become $P^{\prime}$ after performing $n$ $\mu$-transitions.
Finally,
$P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}$
holds if there is $P^{\prime}$ with
$P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}$,
and similarly for other forms of transitions.

#### Further notations.

Letters ${\mathcal{R}},{\mathcal{S}}$ range over relations. We use the infix
notation for relations, e.g., $P\mathrel{\mathcal{R}}Q$ means that
$(P,Q)\in{\mathcal{R}}$, and we write ${\mathcal{R}}{\mathcal{S}}$ for the
composition of ${\mathcal{R}}$ and ${\mathcal{S}}$. A relation _terminates_ if
there is no infinite sequence $P_{1}{\mathcal{R}}P_{2}{\mathcal{R}}\dots$. We
use a tilde to denote a tuple, with countably many elements; thus the tuple
may also be infinite. All notations are extended to tuples componentwise;
e.g., $\widetilde{P}\mathrel{\mathcal{R}}\widetilde{Q}$ means that
$P_{i}\mathrel{\mathcal{R}}Q_{i}$, for each component $i$ of the tuples
$\widetilde{P}$ and $\widetilde{Q}$. We use symbol
$\stackrel{{\scriptstyle\mbox{\scriptsize def}}}{{=}}$ for abbreviations; for
instance, $P\stackrel{{\scriptstyle\mbox{\scriptsize def}}}{{=}}G$, where $G$
is some expression, means that $P$ stands for the expression $G$. In contrast,
symbol $\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}$ is used
for the definition of constants, and $=$ for syntactic equality and for
equations. If $\leq$ is a preorder, then $\geq$ is its inverse (and
conversely).

We focus on _weak_ behavioural relations, which abstract from the number of
internal steps performed by equivalent processes, because they are, in
practice, the important relations.

######  Definition  (Bisimilarity).

A relation ${{\mathcal{R}}}$ is a _bisimulation_ if, whenever
$P\mathrel{\mathcal{R}}Q$, we have:

  1. (1)

$P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}$
implies that there is $Q^{\prime}$ such that
$Q\mathrel{\stackrel{{\scriptstyle{\;\;\hat{\mu}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}Q^{\prime}$
and $P^{\prime}\mathrel{\mathcal{R}}Q^{\prime}$;

  2. (2)

the converse, on the actions from $Q$.

$P$ and $Q$ are _bisimilar_ , written $P\approx Q$, if
$P\mathrel{\mathcal{R}}Q$ for some bisimulation ${\mathcal{R}}$.

#### Systems of equations.

We need variables to write equations. We use capital letters $X,Y,Z$ for these
variables and call them _equation variables_. The body of an equation is a CCS
expression possibly containing equation variables. We use $E,E^{\prime},\dots$
to range over _equation expressions_ ; these are process expressions that may
contain occurrences of variables; that is, the grammar for processes is
extended with a production for variables.

######  Definition .

Assume that, for each $i$ of a countable indexing set $I$, we have a variable
$X_{i}$, and an expression $E_{i}$, possibly containing some variables. Then
$\\{X_{i}=E_{i}\\}_{i\in I}$ (sometimes written $\widetilde{X}=\widetilde{E}$)
is a _system of equations_. (There is one equation for each variable $X_{i}$.)

In the equation $X=E[X]$, we sometimes call body of the equation the equation
expression $E$ (we use the same terminology for systems of equations).

$E[\widetilde{P}]$ is the process resulting from $E$ by replacing each
variable $X_{i}$ with the process $P_{i}$, assuming $\widetilde{P}$ and
$\widetilde{X}$ have the same length. (This is syntactic replacement.) The
components of $\widetilde{P}$ need not be different from each other, while
this must hold for the variables $\widetilde{X}$.

######  Definition .

Suppose $\\{X_{i}=E_{i}\\}_{i\in I}$ is a system of equations. We say that:

  * •

$\widetilde{P}$ is a _solution of the system of equations for $\approx$_ if
for each $i$ it holds that $P_{i}\approx E_{i}[\widetilde{P}]$.

  * •

The system has _a unique solution for $\approx$_ if whenever $\widetilde{P}$
and $\widetilde{Q}$ are both solutions for $\approx$, then
$\widetilde{P}\approx\widetilde{Q}$.

Examples of systems with a unique solution for $\approx$ are:

  1. (1)

$X=a.X$

  2. (2)

$X_{1}=a.X_{2}$, $X_{2}=b.X_{1}$

The unique solution of the system (1), modulo $\approx$, is the constant
$K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}a.K$: for any
other solution $P$ we have $P\approx K$. The unique solution of (2), modulo
$\approx$, is given by the constants $K_{1},K_{2}$ with
$K_{1}\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}a.K_{2}$ and
$K_{2}\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}b.K_{1}$;
again, for any other pair of solutions $P_{1},P_{2}$ we have $K_{1}\approx
P_{1}$ and $K_{2}\approx P_{2}$.

Examples of systems that do not have unique solution are:

  1. (1)

$X=X$

  2. (2)

$X=\tau.X$

  3. (3)

$X=a|X$

All processes are solutions of (1) and (2); examples of solutions for (3) are
$K$ and $K|b$, for
$K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}a.K$

######  Remark .

To prove that two processes $P$ and $Q$ are equivalent using the unique
solution proof technique, one has first to find an equation $X=E[X]$ of which
both $P$ and $Q$ are solutions. Then, a sufficient condition for uniqueness of
solutions makes it possible to deduce $P\approx Q$.

The unique-solution method is currently particularly used in combination with
algebraic laws [Ros10, BBR10, GM14].

######  Definition .

An equation expression $E$ is

  * •

_strongly guarded_ if each occurrence of a variable in $E$ is underneath a
visible prefix;

  * •

_(weakly) guarded_ if each occurrence of a variable in $E$ is underneath a
prefix, visible or not;

  * •

_sequential_ if each occurrence of a variable in $E$ is only appears
underneath prefixes and sums .

We say that an equation satisfies one of the above properties when its body
does. These notions are extended to systems of equations in a natural way: for
instance, $\\{X_{i}=E_{i}\\}_{i\in I}$ is guarded if each expression $E_{i}$
is (w.r.t. every variable that occurs in $E_{i}$).

In other words, if the system is sequential, then for every expression
$E_{i}$, any sub-expression of $E_{i}$ in which $X_{j}$ appears, apart from
$X_{j}$ itself, is a sum (of prefixed terms). For instance,

  * •

$X=\tau.X+\mu.{\boldsymbol{0}}$ is sequential but not strongly guarded,
because the guarding prefix for the variable is not visible.

  * •

$X=\ell.X|P$ is guarded but not sequential.

  * •

$X=\ell.X+\tau.{\boldsymbol{\nu}}a\>(a.\overline{b}|a.{\boldsymbol{0}})$, as
well as $X=\tau.(a.X+\tau.b.X+\tau)$ are both guarded and sequential.

######  Remark  (Recursive specifications in ACP).

Systems of equations are called _recursive specifications_ in the literature
related to ACP [BW90]. In that context, other notions of guardedness have been
studied. A sufficient condition, more powerful than Milner’s, was originally
given by Baeten, Bergstra and Klop [BW90], where synchronisation is
transformed into a visible action, which is then deleted through an explicit
operator. An equation is then guarded if no such deletion operator appears in
its body.

In some process calculi, such as ACP [BW90] and mCRL2 [GM14], guardedness is
synonymous, for an equation, to having a unique solution: this follows the
_Recursive specification principle_ (RSP), which states that guarded recursive
specifications are unique (while the _Recursive definition principle_ states
that recursive specifications do have solutions). Increasingly general
definitions of guardedness that make this principle sound are then studied. In
this framework, our contribution can be seen as a new notion of guardedness,
stronger that what is found in the literature, under which the recursive
definition principle is sound for weak bisimilarity.

######  Theorem  (unique solution of equations, [Mil89]).

A system of strongly guarded and sequential equations has a unique solution
for $\approx$.

The proof exploits an invariance property on immediate transitions for
strongly guarded and sequential expressions, and then extracts a bisimulation
(up to bisimilarity) out of the solutions of the system.

To see the need of the sequentiality condition, consider the equation (from
[Mil89])

$X={\boldsymbol{\nu}}a\>(a.X|\overline{a})\enspace,$

where the occurrence of $X$ in the equation expression is strongly guarded but
not sequential. Any process that does not use $a$ is a solution.

#### Note.

In CCS, $\nu$ is not a binder; this allows us to write equations where local
names are used outside their scopes (for instance,
$X=a.{\boldsymbol{\nu}}a\>(\overline{a}|X)$), as there is no alpha-renaming.
It would still be possible, when $\nu$ has to be considered a binder (in a
higher-order setting, for example), to write similar equations in a parametric
fashion: $X=(a)~{}a.{\boldsymbol{\nu}}a\>(\overline{a}|X\langle a\rangle)$.
Such an approach is adopted in Section 5, to handle name passing.

######  Definition  (Divergence).

A process $P$ _diverges_ if it can perform an infinite sequence of internal
moves, possibly after some visible ones; i.e., there are processes $P_{i}$,
$i\geq 0$, and some $n$, such that
$P=P_{0}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{0}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P_{2}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\dots$
and for all $i>n$, $\mu_{i}=\tau$. We call a _divergence of $P$_ the sequence
of transitions
$\big{(}P_{i}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P_{i+1}\big{)}_{i}$
.

######  Example .

The process
$L\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}a.{\boldsymbol{\nu}}a\>(L|\overline{a})$
diverges, since
$L\mathrel{\stackrel{{\scriptstyle{\;\;a\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}{\boldsymbol{\nu}}a\>(L|\overline{a})$,
and (leaving aside ${\boldsymbol{0}}$ and useless restrictions)
${\boldsymbol{\nu}}a\>(L|\overline{a})$ has a $\tau$ transition onto itself.

##  3\. Main Results

###  3.1. Divergences and Unique Solution

This section is devoted to our main results for bisimilarity, in the case of
CCS. We need to reason with the unfoldings of the given equation $X=E$: we
define the $n$-th unfolding of $E$ to be $E^{n}$; thus $E^{1}$ is defined as
$E$, $E^{2}$ as $E[E]$, and $E^{n+1}$ as $E^{n}[E]$. The _infinite_ unfolding
represents the simplest and most intuitive solution to the equation. In the
CCS grammar, such a solution is obtained by turning the equation into a
constant definition, namely the constant $K_{E}$ with
$K_{E}\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}E[K_{E}]$. We
call $K_{E}$ the _syntactic solution of the equation_.

For a system of equations $\widetilde{X}=\widetilde{E}[\widetilde{X}]$, the
unfoldings are defined accordingly (where $E_{i}$ replaces $X_{i}$ in the
unfolding): we write $\widetilde{E}^{2}$ for the system
$\\{X_{i}=E_{i}[\widetilde{E}]\\}_{i\in I}$, and similarly for
$\widetilde{E}^{n}$. The syntactic solutions are defined to be the set of
mutually recursive constants
$\\{K_{\widetilde{E},i}\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}E_{i}[\widetilde{K}_{\widetilde{E}}]\\}_{i}$.

As equation expressions are terms of an extended CCS grammar, that includes
variables, we can apply the SOS rules of CCS to them (assuming that variables
have no transitions). We extend accordingly to expressions notations and
terminology for LTS and transitions.

We have the following properties for transitions of processes of the form
$E[\widetilde{P}]$, where the transition emanates from the $E$ component only:

######  Lemma  (Expression transitions).

  1. (1)

Given $E$ and $E^{\prime}$ two equation expressions, if
$E\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E^{\prime}$,
then
$E[\widetilde{P}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E^{\prime}[\widetilde{P}]$,
for all processes $\widetilde{P}$, and
$E[\widetilde{F}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E^{\prime}[\widetilde{F}]$
for all equation expressions $\widetilde{F}$.

  2. (2)

If $E$ is a guarded expression and
$E[\widetilde{P}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}T$,
then there is an expression $E^{\prime}$ such that
$E\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E^{\prime}$
and $T=E^{\prime}[\widetilde{P}]$. Similarly for a transition
$E[\widetilde{F}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E^{\prime}$.

###### Proof.

  1. (1)

By a simple induction on the derivation of the transition.

  2. (2)

By a simple induction on the equation expression $E$.

∎

In the hypothesis of case 1 above, we sometimes call a transition
$E[\widetilde{P}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E^{\prime}[\widetilde{P}]$
_an instance_ of the expression transition
$E\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E^{\prime}$.

######  Definition  (Reducts).

  1. (1)

The _set of reducts_ of an expression $E$, written $\mathtt{red}(E)$, is given
by:

$\mathtt{red}(E)\quad\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\quad\bigcup_{n}\>\\{E_{n}\;\mid\;E\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E_{1}\dots\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{n}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}E_{n}\mbox{
for some $\mu_{i},E_{i}$ ($1\leq i\leq n$) }\\}.$

  2. (2)

The set of _reducts of the unfoldings_ of a system of equations
$\\{X_{i}=E_{i}[\widetilde{X}]\\}_{i\in I}$, also written
$\mathtt{red}_{\omega}(\widetilde{E})$, is defined as

$\mathtt{red}_{\omega}(\widetilde{E})\quad\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\quad\bigcup_{n\in\mathbb{N},i\in
I}\mathtt{red}(E_{i}^{n})$

######  Definition .

A system of equations $\widetilde{E}$ _protects its solutions_ if, for all
solution $\widetilde{P}$ of the equation
$\widetilde{X}=\widetilde{E}[\widetilde{X}]$, the following holds: for all
$E^{\prime}\in\mathtt{red}_{\omega}(\widetilde{E})$, if
$E^{\prime}[\widetilde{P}]\xRightarrow{\mu}Q$ for some $\mu$ and $Q$, then
there exists $E^{\prime\prime}$ and $n$ such that
$E^{\prime}[\widetilde{E}^{n}]\xRightarrow{\hat{\mu}}E^{\prime\prime}$, and
$E^{\prime\prime}[\widetilde{P}]\approx Q$.

Consider a single equation $X=E[X]$: it protects its solutions when all
sequences of transitions emanating from $E^{\prime}[P]$, where $P$ is a
solution of $E$ and $E^{\prime}$ is a reduct of the unfoldings of $E$, can be
mimicked by transitions involving unfoldings of $E$ and reducts of $E$ only
(without $P$ performing a transition). This is a technical condition, which is
useful in the proofs. In this paper, all examples of equations having a unique
solution satisfy this property.

######  Proposition .

A system of equations that protects its solutions has a unique solution for
$\approx$.

###### Proof.

Given two solutions $\widetilde{P}$, $\widetilde{Q}$ of the system of
equations $\widetilde{X}=\widetilde{E}[\widetilde{X}]$ we prove that the
relation

${\mathcal{R}}\quad\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\quad\\{(S,T)~{}|~{}\exists
E^{\prime},\text{ s.t. }S\approx E^{\prime}[\widetilde{P}],\,T\approx
E^{\prime}[\widetilde{Q}]\text{ and
}E^{\prime}\in\mathtt{red}_{\omega}(\widetilde{E})\\}$

is a bisimulation relation such that
$\widetilde{P}{\mathcal{R}}\widetilde{Q}$.

We consider $(S,T)\in{\mathcal{R}}$, that is, $S\approx
E^{\prime}[\widetilde{P}]$ and $T\approx E^{\prime}[\widetilde{Q}]$, for some
$E^{\prime}\in\mathtt{red}_{\omega}(\widetilde{E})$. If
$S\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}S^{\prime}$,
then by bisimilarity
$E^{\prime}[\widetilde{P}]\xRightarrow{\hat{\mu}}S^{\prime\prime}\approx
S^{\prime}$. Since $\widetilde{E}$ protects its solutions, there are
$n,~{}{E^{\prime\prime}}$ such that
$E^{\prime}[\widetilde{E}^{n}]\xRightarrow{\hat{\mu}}E^{\prime\prime}$ and
$E^{\prime\prime}[\widetilde{P}]\approx S^{\prime\prime}$. We can deduce by
Lemma 3.1(1) that
$E^{\prime}[\widetilde{E}^{n}[\widetilde{Q}]]\xRightarrow{\hat{\mu}}{E^{\prime\prime}}[\widetilde{Q}]$.
Since $\widetilde{Q}$ is a solution of $\widetilde{E}$, we have
$\widetilde{Q}\approx\widetilde{E}^{n}[\widetilde{Q}]$. This entails, as we
know by hypothesis $T\approx E^{\prime}[\widetilde{Q}]$, that $T\approx
E^{\prime}[\widetilde{Q}]\approx
E^{\prime}[\widetilde{E}^{n}[\widetilde{Q}]]$. By bisimilarity, we deduce from
$E^{\prime}[\widetilde{E}^{n}[\widetilde{Q}]]\xRightarrow{\hat{\mu}}{E^{\prime\prime}}[\widetilde{Q}]$
that $T\xRightarrow{\hat{\mu}}T^{\prime}\approx
E^{\prime\prime}[\widetilde{Q}]$.

The situation can be depicted on the following diagram:

$\textstyle{S\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu}$$\textstyle{\approx}$$\textstyle{E^{\prime}[\widetilde{P}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{\approx}$$\textstyle{E^{\prime}[\widetilde{E}^{n}[\widetilde{P}]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\scriptstyle{=}$$\textstyle{E^{\prime}[\widetilde{E}^{n}[\widetilde{Q}]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{\approx}$$\textstyle{E^{\prime}[\widetilde{Q}]}$$\textstyle{\approx}$$\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{S^{\prime}}$$\textstyle{\approx}$$\textstyle{S^{\prime\prime}}$$\textstyle{\approx}$$\textstyle{E^{\prime\prime}[\widetilde{P}]}$$\textstyle{E^{\prime\prime}[\widetilde{Q}]}$$\textstyle{\approx}$$\textstyle{T^{\prime}}$

Then, from $E^{\prime}\in\mathtt{red}_{\omega}(\widetilde{E})$ and
$E^{\prime}[\widetilde{E}^{n}]\mathrel{\stackrel{{\scriptstyle{\;\;\hat{\mu}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E^{\prime\prime}$,
we deduce that $E^{\prime\prime}\in\mathtt{red}_{\omega}(\widetilde{E})$.
Finally, $T^{\prime}\approx E^{\prime\prime}[\widetilde{Q}]$ and
$S^{\prime}\approx E^{\prime\prime}[\widetilde{P}]$ give that
$(S,T)\in{\mathcal{R}}$.

We reason symmetrically for $T\xrightarrow{\mu}T^{\prime}$. ∎

We say that the syntactic solutions of the system $\widetilde{E}$ do not
diverge if, for all $i\in I$, $K_{\widetilde{E},i}$ does not diverge.

######  Theorem  (Unique solution).

A guarded system of equations whose syntactic solutions do not diverge has a
unique solution for $\approx$.

###### Proof.

To enhance readability, we first give the proof for a single equation
$X=E[X]$. We discuss the generalisation to a system of equations at the end of
the proof.

Given a guarded equation expression $E$, we prove that $E$ protects the
solutions of its equations. To prove that, we need to consider a transition
$E_{0}[P]\xRightarrow{\mu}P^{\prime}$, for some
$E_{0}\in\mathtt{red}_{\omega}(E)$ and some solution $P$ of $E$.

We build a sequence of expressions $E_{n}$, and an increasing sequence of
transitions $E_{0}[E^{n}]\xRightarrow{\mu?}E_{n}$ (where
$\xRightarrow{\mu?}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\Rightarrow\cup\xRightarrow{\hat{\mu}}$) such that: either this
construction stops, yielding a transition
$E_{0}[E^{n}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{n}$,
or the construction is infinite, therefore giving a divergence of $K_{E}$.

We build this sequence so that it additionally satisfies:

  * •

Either we have $E_{0}[E^{n}]\xRightarrow{\hat{\mu}}E_{n}$ and
$E_{n}[P]\Rightarrow\approx P^{\prime}$, or $E_{0}[E^{n}]\Rightarrow E_{n}$
and $E_{n}[P]\xRightarrow{\hat{\mu}}\approx P^{\prime}$.

  * •

The sequence is strictly increasing: the sequence of transitions
$E_{0}[E^{n+1}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{n}[E]$
is a strict prefix of the sequence of transitions
$E_{0}[E^{n+1}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{n+1}$

This construction is illustrated by Figure 3. We start with the empty sequence
from $E_{0}$.

Suppose therefore that at step $n$, we have for example
$E_{0}[E^{n}[P]]\xRightarrow{\mu}E_{n}[P]\Rightarrow T_{n}$, with
$P^{\prime}\approx T_{n}$.

$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E_{0}[E^{n}[P]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{=}$$\scriptstyle{\mu?}$$\textstyle{E_{0}[E^{n+1}[P]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu?}$$\textstyle{=}$$\textstyle{E_{0}[E^{n+1}[P]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu?}$$\textstyle{E_{n}[P]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu?}$$\textstyle{\approx}$$\textstyle{E_{n}[E[P]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu?}$$\textstyle{=}$$\textstyle{E_{n}[E[P]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu?}$$\scriptstyle{\mu?}$$\textstyle{E_{n+1}[P]}$$\textstyle{\ignorespaces{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}A}}$$\textstyle{P^{\prime}~{}~{}\approx~{}~{}T_{n}}$$\textstyle{\approx}$$\textstyle{T_{n+1}}$$\textstyle{=}$$\textstyle{T_{n+1}}$

Figure 2. Recursion: construction of the sequence of transitions
$E_{0}[E^{n}[P]]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{n}$

---
$\textstyle{E_{0}[P]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{\approx}$$\textstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}E_{0}[E}[P]{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{\approx}$$\textstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}E_{0}[E^{2}}[P]{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}]}{\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}$$\scriptstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}\mu?}}$$\textstyle{\approx}$$\textstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}E_{0}[E^{3}}[P]{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}\mu?}}$$\textstyle{\approx}$$\textstyle{\dots}$$\textstyle{\approx}$$\textstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}E_{0}[E^{n}}[P]{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}\mu?}}$$\scriptstyle{\mu?}$$\scriptstyle{\mu?}$$\textstyle{P^{\prime}}$$\textstyle{\approx}$$\textstyle{T_{1}}$$\textstyle{\approx}$$\textstyle{T_{2}}$$\textstyle{\approx}$$\textstyle{T_{3}}$$\textstyle{\approx}$$\textstyle{\dots}$$\textstyle{\approx}$$\textstyle{{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}{E_{n}}}[P]}${{{

Figure 3. Construction of the expression transition

  * •

If $E_{n}[P]\Rightarrow T_{n}$ is the empty sequence, we stop. We have in this
case $E_{0}[E]^{n}\xRightarrow{\mu}E_{n}$ and $P^{\prime}\approx E_{n}[P]$.

  * •

Otherwise (as depicted on Figure 2), we unfold further equation $E$: we have
$E_{0}[E^{n+1}]\xRightarrow{\mu}E_{n}[E]$ by Lemma 3.1. By congruence and
bisimilarity we have $E_{n}[E[P]]\Rightarrow T_{n+1}\approx P^{\prime}$ for
some $T_{n+1}$. If $E_{n}[E[P]]\Rightarrow T_{n+1}$ is the empty sequence, we
stop as previously. Otherwise, we take
$E_{n}[E]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{n+1}$
to be the longest prefix sequence of transitions in $E_{n}[E[P]]\Rightarrow
T_{n+1}$ that are instances of expression transitions from $E_{n}[E]$ (we
remark that as $E_{n}[E]$ is guarded, this sequence is not empty).

Suppose now that the construction given above never stops. We know that
$E_{n}[E]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{n+1}$,
therefore
$E_{n}[K_{E}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{n+1}[K_{E}]$.
This gives an infinite sequence of transitions starting from $E_{0}[K_{E}]$:
$E_{0}[K_{E}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}E_{1}[K_{E}]\mathrel{\stackrel{{\scriptstyle{\;\;\mu?\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}\dots$.
We observe that in the latter sequence, every step involves at least one
transition, and moreover, there is at most one visible action ($\mu$)
occurring in this infinite sequence. Therefore $E_{0}[K_{E}]$ is divergent,
which contradicts the hypothesis of the theorem. Hence, the construction does
stop, and this concludes the proof.

#### Systems of equations.

To extend the previous proof to systems of equations, we consider solutions
$\widetilde{P}$ to the system $\widetilde{E}$, and use unfoldings of the
system of equations (instead of unfoldings of a single equation). We also
reason about an initial transition from $E_{0}[\widetilde{P}]$, where $E_{0}$
is a reduct of the unfoldings of one of the equations (i.e.,
$E_{0}\in\mathtt{red}_{\omega}(\widetilde{E})$). ∎

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu}$$\textstyle{\approx}$$\textstyle{E[P]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{\approx}$$\textstyle{E[E[P]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{\approx}$$\textstyle{\dots}$$\textstyle{\approx}$$\textstyle{E^{n}[P]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{E^{n}[\cdot]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{E^{n}[Q]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$$\textstyle{\approx}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}}$

Figure 4. Proof of Theorem 3.1, building a a transition of $E^{n}[Q]$ where
$Q$ does not move

###  3.2. Innocuous Divergences

In the remainder of the section we refine Theorem 3.1 by taking into account
only certain forms of divergence. To introduce the idea, consider the equation
$X=a.X|K$, for
$K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\tau.K$: the
divergences induced by $K$ do not prevent uniqueness of the solution, as any
solution $P$ necessarily satisfies $P\approx a.P$. Indeed the variable of the
equation is strongly guarded and a visible action has to be produced before
accessing the variable. These divergences are not dangerous because they do
not percolate through the infinite unfolding of the equation; in other words,
a finite unfolding may produce the same divergence, therefore it is not
necessary to go to the infinite unfolding to diverge. We call such divergences
_innocuous_. Formally, these divergences are derived by applying only a finite
number of times rule $\mathtt{const}$ of the LTS (see Figure 1) to the
constant that represents the syntactic solution of the equation. Those
divergences can be understood as instances, in the syntactic solution, of
divergences of some finite unfolding of the equation: Consider a (single)
equation $X=E[X]$; this way, any divergence of $E^{n}$ can be transformed into
an innocuous divergence of $K_{E}$. This idea is also behind Lemma 4.1 below.

This refinement fits well the operational approach we adopt to formalise the
results; it looks less natural in a denotational or trace-based setting for
CSP like in [Ros92, Ros97], where any divergence causes a process to be
considered undefined.

######  Definition  (Innocuous divergence).

Consider a guarded system of equations $\widetilde{X}=\widetilde{E}$ and its
syntactic solutions $\widetilde{K}_{\widetilde{E}}$. A divergence of
$K_{\widetilde{E},i}$ (for some $i$) is called _innocuous_ when, summing up
all usages of rule $\mathtt{const}$ with one of the $K_{\widetilde{E},j}$s
(including $j=i$) _in all derivation proofs of the transitions belonging to
the divergence_ , we obtain a finite number.

######  Theorem  (Unique solution with innocuous divergences).

Let $\widetilde{X}=\widetilde{E}$ be a system of guarded equations, and
$\widetilde{K}_{\widetilde{E}}$ be its syntactic solutions. If all divergences
of any $K_{\widetilde{E},i}$ are innocuous, then $\widetilde{E}$ has a unique
solution for $\approx$.

###### Proof.

We reason like in the proof of Theorem 3.1. We explain the difference, in the
case where we have a single equation (bearing in mind that the generalisation
discussed at the end of the proof of Theorem 3.1 can be carried over
accordingly).

Along the construction in that proof, if at some point the transition
$E_{0}[E^{n}[P]]\xRightarrow{\hat{\mu}}T_{n}$ is an instance of an expression
transition $E_{0}[E^{n}]\xRightarrow{\hat{\mu}}E_{n}$, then the construction
can stop.

Consequently, if the construction never stops, we build a non innocuous
divergence: we can assume that for any $n$,
$E_{0}[E^{n}[P]]\xRightarrow{\hat{\mu}}T_{n}$ is not an instance of an
expression transition from $E_{0}[E^{n}]$. This means that in this sequence of
transitions, the LTS rule $\mathtt{const}$ is used at least $n$ times applied
to the constant $K_{E}$. Hence, the divergence we build uses at least $n$
times the rule $\mathtt{const}$ applied to the constant $K_{E}$, for all $n$.
Therefore, the divergence is not innocuous, which is a contradiction. ∎

######  Remark .

The conditions for unique solution in Theorems 3.1 and 3.2 combine syntactic
(guardedness) and semantic (divergence-free) conditions. A purely semantic
condition can be used if rule $\mathtt{const}$ of Figure 1 is modified so that
the unfolding of a constant yields a $\tau$-transition:

$\overline{K\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P}^{\mbox{
if }K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}P}$

Thus in the theorems the condition imposing guardedness of the equations could
be dropped. The resulting theorems would actually be more powerful because
they would accept equations which are not syntactically guarded: it is
sufficient that each equation has a finite unfolding which is guarded. For
instance the system of equations $X=b|Y$, $Y=a.X$ would be accepted, although
the first equation is not guarded.

######  Remark .

Even taking innocuous divergences into account, our criterion for equations to
have a unique solution is not complete. Indeed, the following equation

$X=a.X+\overline{a}.X+d.(X|X)$

has a non-innocuous divergence: its syntactic solution, $K$, has the
transition
$K\mathrel{\stackrel{{\scriptstyle{\;\;d\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}K|K$;
then, $K|K$ diverges by unfolding on both sides at every step. However, the
equation has a unique solution, intuitively because the prefix $d$ acts as a
strong guard, that does not take part in the divergence. This could hint at
further developments of our theory.

Note moreover that this equation is non-linear, in the sense that there are
occurrences of the same variable $X$ in parallel. In practice, such examples
are not very useful; for linear equations, we were not able to find counter-
examples.

###  3.3. Conditions for unique solution

The following lemma states a condition to ensure that all divergences produced
by a system of equations are innocuous. This condition is decidable, but weak.
However, in practice, it is often satisfied; it is in particular sufficient in
all examples in the paper.

######  Lemma .

Consider a system of equations $\widetilde{X}=\widetilde{E}$, and suppose that
for each $i$ there is $n_{i}$ such that in $E_{i}^{n_{i}}$, each variable is
underneath a visible prefix (say, $a$ or $\overline{a}$) whose complementary
prefix ($\overline{a}$ or $a$) does not appear in any equation. Then the
system has only innocuous divergences.

###### Proof.

The condition ensures that at least one of the prefix occurring above the
equation variables may never take part in a $\tau$ action. This entails that
this prefix cannot be triggered along an infinite sequence of $\tau$ steps.
Hence a divergence of the unique solution of such a system of equations may
not require the rule const to be used an infinite number of times. ∎

###  3.4. Comparison with other techniques

We now compare our technique with two alternative approaches: unique solution
of contractions, and enhancements of bisimulation.

####  3.4.1. An example (lazy and eager servers), and comparison with
contractions

We now show an example of application of our technique, taken from [San15].
The example also illustrates the relative strengths of the two unique solution
theorems (Theorems 3.1 and 3.2), and a few aspects of the comparison with
other bisimulation techniques.

For the sake of readability, we use a version of CCS with value passing; this
could be translated into pure CCS [Mil89]. In a value-passing calculus,
$a(x).P$ is an input at $a$ in which $x$ is the placeholder for the value
received, whereas $\overline{a}\langle{n}\rangle.P$ is an output at $a$ of the
value $n$; and $A\langle n\rangle$ is a parametrised constant. This example
consists of two implementations of a server; this server, when interrogated by
clients at a channel $c$, should start a certain interaction protocol with the
client, after consulting an auxiliary server $A$ at $a$.

We consider the two following implementations of this server: the first one,
$L$, is ‘lazy’, and consults $A$ only _after_ a request from a client has been
received. In contrast, the other one, $E$, is ‘eager’, and consults $A$
_beforehand_ , so then to be ready in answering a client:

$\begin{array}[]{crcl}\begin{array}[]{rcl}L&\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}&c(z).a(x).(L|R\langle
x,z\rangle)\\\
E&\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}&a(x).c(z).(E|R\langle
x,z\rangle)\end{array}&~{}\qquad A\langle
n\rangle&\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}&\overline{a}\langle{n}\rangle.A\langle
n+1\rangle\end{array}$

Here $R\langle x,z\rangle$ represents the interaction protocol that is started
with a client, and can be any process. It may use the values $x$ and $z$
(obtained from the client and the auxiliary server $A$); the interactions
produced may indeed depend on the values $x$ and $z$. We assume for now that
$R\langle x,z\rangle$ may not use channel $c$ and $a$; that is, the
interaction protocol that has been spawned need not come back to the main
server or to the auxiliary server. Moreover we assume $R$ may not diverge. We
want to prove that the two servers, when composed with $A$, yield bisimilar
processes. We thus define ${L\\!S}\langle
n\rangle\,\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\,{\boldsymbol{\nu}}a\>(A\langle
n\rangle|L)$ and ${E\\!S}\langle
n\rangle\,\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\,{\boldsymbol{\nu}}a\>(A\langle
n\rangle|E)$. A proof that ${L\\!S}\langle n\rangle\approx{E\\!S}\langle
n\rangle$ using the plain bisimulation proof method would be long and tedious,
due to the differences between the lazy and the eager server, and to the fact
that $R$ is nearly an arbitrary process.

The paper [San15] presents two proofs of this equivalence. One proof makes use
of the ‘bisimulation up-to expansion and context’ technique; this makes it
possible to carry out a proof using a single pair of processes for each
integer $n$. A proof of similar size uses the technique of ‘unique solution of
contractions’, by establishing, with the help of a few simple algebraic laws,
that $\\{{L\\!S}\langle n\rangle\\}_{n}$ and $\\{{E\\!S}\langle
n\rangle\\}_{n}$ are solutions of the same system of contractions.

We can also build a proof using the technique of ‘unique solution of
equations’. Milner’s original version of this technique cannot be used,
because the equations make use of operators other than just prefix and sum. In
contrast, Theorem 3.1 can be applied. The equations are:
$\\{X_{n}=c(z).(X_{n+1}|R\langle n,z\rangle)\\}_{n}$. The proofs that the two
servers are solutions can be carried out using a few algebraic laws: expansion
law, structural laws for parallel composition and restriction, one $\tau$-law.
It is essentially the same proof as that for unique solution of contractions.

To apply Theorem 3.1, we also need to check that the equations do not produce
divergences. This check is straightforward, as no silent move may be produced
by interactions along $c$, and any two internal communications at $a$ are
separated by a visible input at $c$. Moreover, by assumption, the protocol $R$
does not produce internal divergences.

If on the other hand the hypothesis that $R$ may not diverge is lifted, then
Theorem 3.1 is not applicable anymore, and divergences are possible. However,
such divergences are innocuous: the equation need not be unfolded an infinite
number of times for the divergence to occur. We can therefore still prove the
result, by appealing to the more powerful Theorem 3.2.

We can relax the definition of $R$ even further and allow calls back to the
main server from $R$ itself. In this case, interactions between $R$ and the
main server (eager or lazy) may yield divergences (for instance setting
$R\stackrel{{\scriptstyle\mbox{\scriptsize def}}}{{=}}\overline{c}$). Such
divergences need not be innocuous, as intuitively they require infinitely many
unfolding of the body of an equation. Thus now even Theorem 3.2 is not
applicable. (More precisely, for Theorem 3.2 to fail $R\langle n,z\rangle$,
for each $n$ and $z$, should have the possibility of performing an output at
$c$ as first visible transition.)

This becomes therefore an example in which the ‘unique solution of
contraction’ technique is more powerful, as such technique does not rely on
conditions about divergence and is therefore applicable.

####  3.4.2. Comparison with up-to techniques

Milner’s syntactic condition for unique solution of equations essentially
allows only equations in which variables are underneath prefixes and sums. The
technique is not complete [San15]; for instance it cannot handle the server
example of Section 3.4.1.

The technique of ‘unique solution of contractions’ [San15] relies on the
theory of an auxiliary preorder (contraction), needed to establish the meaning
of ‘solution’; and the soundness theorems in [San15] use a purely syntactic
condition (guarded variables). In contrast, our techniques with equations do
not rely on auxiliary relations and their theory, but the soundness theorems
use a semantic condition (divergence) , see also Remark 3.2).

The two techniques are incomparable. Considering the server example of Section
3.4.1, the contraction technique is capable of handling also the case in which
the protocol $R$ is freely allowed to make calls back to the main server,
including the possibility that, in doing this, infinitely many copies of $R$
are spawned. This possibility is disallowed for us, as it would correspond to
a non-innocuous divergence. On the other hand, when using contraction, a
solution is evaluated with respect to the contraction preorder, that conveys
an idea of efficiency (measured against the number of silent transitions
performed). Thus, while two bisimilar processes are solutions of exactly the
same set of equations, they need not be solutions of the same contractions.
For instance, we can use our techniques to prove that processes
$K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\tau.a.a.K$ and
$H\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}a.H$ are
bisimilar because solutions of the equation $X=a.X$; in contrast, only $H$ is
a solution of the corresponding contraction.

#### Up-to techniques.

We compare our unique-solution techniques with one of the most powerful forms
of enhancement of the bisimulation proof method, namely Pous ‘up to
transitivity and context’ technique [Pou08]. This technique allows one to use
‘up to weak bisimilarity’, ‘up to transitivity’, and ‘up to context’
techniques together. While ‘up to weak bisimilarity’ and ‘up to transitivity’
are known to be unsound techniques [PS11], here they are combined safely
thanks to a ‘control relation’, written below $\succ$, which satisfies a
termination hypothesis. This control relation is used to make sure there is no
cyclic or infinite sequence of $\tau$ transitions used to hide other potential
visible transitions. In that regard, this condition is very similar to the
non-divergence hypothesis of Theorem 3.2, as can be seen in the proofs below.

Formally, contexts are processes that can contain holes, indexed by some
finite set of integers. Therefore, contexts are like equation expressions,
except that numbered holes are used instead of variable names. In this
section, we will switch freely between equation expressions and contexts,
keeping in mind that contexts are needed to study up-to techniques while
equation expressions are needed for unique solution of equations.

We write $\mathcal{C}({\mathcal{R}})$ for the context closure of a relation
${\mathcal{R}}$, defined as the set of all pairs
$(C[\widetilde{P}],C[\widetilde{Q}])$ with
$\widetilde{P}\mathrel{\mathcal{R}}\widetilde{Q}$. Moreover,
$\overline{\mathcal{R}}$ stands for
$(\approx\cup\,\mathcal{C}({\mathcal{R}}))$, and ${\mathcal{R}}^{+}$ for the
transitive closure of ${\mathcal{R}}$.

######  Definition .

Let $\succ$ be a relation that is transitive, closed under contexts, and such
that
$\succ(\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{+})$
terminates. A relation ${\mathcal{R}}$ is a _bisimulation up to $\succ$ and
context_ if, whenever $P\mathrel{\mathcal{R}}Q$:

  1. (1)

if
$P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}$
then
$Q\mathrel{\stackrel{{\scriptstyle{\;\;\hat{\mu}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}Q^{\prime}$
for some $Q^{\prime}$ with
$P^{\prime}\>\mathrel{(\succ{\cap}\,\overline{\mathcal{R}})^{+}\;\>\mathcal{C}({\mathcal{R}})\;\approx}\>Q^{\prime}$;

  2. (2)

the converse on the transitions from $Q$.

We refer to [Pou08] for more details on this up-to technique, and for the the
proof of its soundness.

We remark that in [Pou08], instead of the transitive closure
$(\succ\cap~{}\overline{{\mathcal{R}}})^{+}$ in Definition 3.4, we have a
_reflexive_ and transitive closure. We do not know if relaxing this technical
condition breaks Theorem 3.4 below.

We introduce some notations in order to state the correspondence between the
technique introduced in Definition 3.4 and systems of equations.

If ${\mathcal{R}}$ is a relation, then we can also view ${\mathcal{R}}$ as an
ordered sequence of pairs (e.g., assuming some lexicographical ordering). Then
${\mathcal{R}}_{i}$ indicates the tuple obtained by projecting the pairs in
${\mathcal{R}}$ on the $i$-th component ($i=1,2$).

In the following statement, the _size_ of a relation is the number of pairs it
contains, and the size of a system of equations is the number of equations it
consists of.

######  Theorem  (Completeness with respect to up-to techniques).

Suppose ${\mathcal{R}}$ is a bisimulation up to $\succ$ and context. Then
there exists a guarded system of equations, with only innocuous divergences,
that admits ${\mathcal{R}}_{1}$ and ${\mathcal{R}}_{2}$ as solutions.
Moreover, this system has the same size as ${\mathcal{R}}$.

###### Proof.

Suppose ${\mathcal{R}}=\\{(P_{i},Q_{i})\\}_{i\in I}$ is a bisimulation up to
$\succ$ and context.

We index the transitions of $P_{i}$ from $1$ to $n_{i}$, and write
$P_{i}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i,j}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}_{i,j}$
for $1\leq j\leq n_{i}$.

Then, by Definition 3.4, for $1\leq j\leq n_{i}$, there exist $C_{i,j}$ and
$Q^{\prime}_{i,j}$ such that we have the following diagram:

$\textstyle{P_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu_{i,j}}$$\textstyle{\mathcal{R}}$$\textstyle{Q_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\hat{\mu}_{i,j}}$$\textstyle{P^{\prime}_{i,j}}$$\textstyle{(\succ\cap(\approx\cup{\mathcal{C}({\mathcal{R}})}))^{+}}$$\textstyle{C_{i,j}[\widetilde{P}]}$$\textstyle{\mathcal{C}({\mathcal{R}})}$$\textstyle{C_{i,j}[\widetilde{Q}]}$$\textstyle{\approx}$$\textstyle{Q^{\prime}_{i,j}}$

We define the system of equations $\widetilde{X}=\widetilde{E}$ by setting
$\forall i\in I,~{}E_{i}=\sum_{j=1}^{n_{i}}\mu_{i,j}.C_{i,j}[\widetilde{X}]$.
By construction, this system and ${\mathcal{R}}$ have the same size.

We prove that $\widetilde{P}$ is a solution of $\widetilde{X}=\widetilde{E}$.
We have that $P_{i}\sim\sum_{j=1}^{n_{i}}\mu_{i,j}.P^{\prime}_{i,j}$.
Moreover, by the results in [Pou08], since
$\succ(\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{+})$
terminates, ${\mathcal{R}}\subseteq\approx$, which implies
$(\succ\cap(\approx\cup\mathcal{C}({\mathcal{R}})))^{+}\subseteq{\approx}$.
Therefore, $P^{\prime}_{i,j}\approx C_{i,j}[\widetilde{P}]$, and
$P_{i}\approx\sum_{j=1}^{n_{i}}\mu_{i,j}.C_{i,j}[\widetilde{P}]$. This shows
that $\widetilde{P}$ is a solution of $\widetilde{X}=\widetilde{E}$.

Since ${\mathcal{R}}\subseteq\approx$, we have
$\widetilde{P}\approx\widetilde{Q}$, hence $\widetilde{Q}$ is also a solution
of the system of equations.

It is left to prove that if for some $i$, $K_{\widetilde{E},i}$ has a non-
innocuous divergence, then
$\succ(\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{+})$
does not terminate. As this would be contradictory, we will be able to apply
Theorem 3.2 to finish the proof.

Assume that
$K_{\widetilde{E},k}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\dots\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{n}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F_{0}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\dots$,
and that this divergence is not innocuous. Based on this divergence, we build
a sequence of equation expressions $F_{n}$ and $F_{n}^{\prime}$ such that:

$F_{0}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{*}F^{\prime}_{0}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F_{1}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{*}F_{1}^{\prime}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F_{2}[\widetilde{K}_{\widetilde{E}}]\dots$

In the above divergence, we have that for all $n$,
$F_{n}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{*}F_{n}^{\prime}$
(these are expression transitions) and
$F_{n}^{\prime}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F_{n+1}[\widetilde{K}_{\widetilde{E}}]$;
moreover, the latter transition is not an instance of an expression transition
from $F_{n}^{\prime}$ (meaning that $\widetilde{K}_{\widetilde{E}}$
contributes to the transition). We will then show that
$F_{n}^{\prime}[\widetilde{P}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\succ
F_{n+1}[\widetilde{P}]$. Therefore
$\succ(\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{+})$
does not terminate.

$F_{0}$ is already given. Assume then that we have $F_{n}$ such that there is
a non innocuous divergence from $F_{n}[\widetilde{K}_{\widetilde{E}}]$. This
entails that there exists $F_{n}^{\prime}$ such that
$F_{n}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{*}F_{n}^{\prime}[\widetilde{K}_{\widetilde{E}}]$,
$F_{n}^{\prime}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}$,
and the latter transition is not an instance of an expression transition from
$F_{n}^{\prime}$. Without loss of generality, we can assume that the
transitions in
$F_{n}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{*}F_{n}^{\prime}[\widetilde{K}_{\widetilde{E}}]$
are instances of expression transitions.

The fact that transition
$F_{n}^{\prime}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}$
is not an instance of an expression transition means that at least one
equation expression $E_{i}$ is involved in it. For readability, we assume that
this transition is of the form
$F_{n}^{\prime}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F_{n}^{\prime}[(K_{\widetilde{E},k})_{k<i},Q,(K_{\widetilde{E},k})_{k>i}]$
for some $k$ and some $Q$, with
$K_{\widetilde{E},i}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}Q$
(i.e., in $F_{n}^{\prime}$ there is only one copy of $K_{\widetilde{E},i}$,
and the transition involves only $K_{\widetilde{E},i}$). The reasoning below
can be adapted to cases where the $\tau$-transition involves a more complex
synchronisation, and/or several copies of $K_{\widetilde{E},i}$.

Since $E_{i}=\sum_{j}\mu_{i,j}.C_{i,j}[\widetilde{X}]$, there is $j$ such that
$\tau=\mu_{i,j}$ and $Q=C_{i,j}[\widetilde{K}_{\widetilde{E}}]$. We then fix
$F_{n+1}$ to be $F_{n}^{\prime}\\{C_{i,j}[\widetilde{X}]/X_{i}\\}$. Indeed we
have
$F_{n}^{\prime}[\widetilde{K}_{\widetilde{E}}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F_{n+1}[\widetilde{K}_{\widetilde{E}}]$.

We have observed that $P_{i}\sim\sum_{j}\mu_{i,j}.P^{\prime}_{i,j}$, and
$E_{i}=\sum_{j}\mu_{i,j}.C_{i,j}[\widetilde{X}]$, hence any transition from
$E_{i}$ can be mimicked by a transition of $P_{i}$. Therefore we have that
$P_{i}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}_{i,j}$
and
$F_{n}^{\prime}[\widetilde{P}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F_{n}^{\prime}[(P_{k})_{k<i},P^{\prime}_{i,j},(P_{k})_{k>i}]$.
We have that $P^{\prime}_{i,j}\succ^{+}C_{i,j}[\widetilde{P}]$ by
construction, hence, since $\succ$ is transitive, $P^{\prime}_{i,j}\succ
C_{i,j}[\widetilde{P}]$; finally, $\succ$ is closed by contexts, hence

$F_{n}^{\prime}[(P_{k})_{k<i},P^{\prime}_{i,j},(P_{k})_{k>i}]\succ
F_{n}^{\prime}[(P_{k})_{k<i},C_{i,j}[\widetilde{P}],(P_{k})_{k>i}]=F_{n+1}[\widetilde{P}]\enspace.$

The sequence of equation expressions $F_{n}$ and $F_{n}^{\prime}$ has thus
been defined in such a way that
$F_{n}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{*}F_{n}^{\prime}$,
hence
$F_{n}[\widetilde{P}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{*}F_{n}^{\prime}[\widetilde{P}]$.
We also have
$F_{n}^{\prime}[\widetilde{P}]\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\succ
F_{n+1}[\widetilde{P}]$, thus
$F_{n}[\widetilde{P}](\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{+})\succ
F_{n+1}[\widetilde{P}]$. This is an infinite sequence for
$(\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{+})\succ$,
hence we also have non-termination for
$\succ(\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}^{+})$.
This yields a contradiction. ∎

Theorem 3.2 is essential to establish Theorem 3.4; Theorem 3.1 would be
insufficient.

##  4\. Abstract Formulation

###  4.1. Abstract LTS and Operators

In this section we propose generalisations of the unique-solution theorems.
For this we introduce abstract formulations of them, which are meant to
highlight their essential ingredients. When instantiated to the specific case
of CCS, such abstract formulations yield the theorems in Section 3. The proofs
are adapted from those of the corresponding theorems in Section 3. The results
of this section, up to Theorem 4.1, have been formalised in Coq theorem prover
[Dur17].

The abstract formulation is stated on a generic LTS, that is, a triple
$\mathcal{T}~{}=~{}(S,\Lambda,\rightarrow)$ where: $S$ is the set of states;
$\Lambda$ the set of action labels, containing the special label $\tau$
accounting for silent actions; $\rightarrow$ is the transition relation. As
usual, we write
$s_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}s_{2}$
when ${(s_{1},\mu,s_{2})}\in{\rightarrow}$. The definition of weak
bisimilarity $\approx$ is as in Section 2. We omit explicit reference to
$\mathcal{T}$ when there is no ambiguity.

We reason about _state functions_ , i.e., functions from $S$ to $S$, and use
$f,f^{\prime},g$ to range over them. As usual, $f\circ g$ denotes the
composition of $f$ and $g$. The CCS processes of Section 2 correspond here to
the states of an LTS. In turn, a CCS context $C$ corresponds to a state
function, mapping a process $P$ to the process $C[P]$.

######  Definition .

A state function $f$ _respects a relation $R$_ whenever $xRy$ implies
$f(x)Rf(y)$, for all states $x,y$.

######  Definition  (Autonomy).

For state functions $f,f^{\prime}$ we say that there is an _autonomous
$\mu$-transition from $f$ to $f^{\prime}$_, written
$f\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f^{\prime}$,
if for all states $x$ it holds that
$f(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f^{\prime}(x)$.

Likewise, given a set $\mathcal{F}$ of state functions and $f\in\mathcal{F}$,
we say that a transition
$f(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}y$
is _autonomous on $\mathcal{F}$_ if, for some $f^{\prime}\in\mathcal{F}$ we
have
$f\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f^{\prime}$
and $y=f^{\prime}(x)$. Moreover, we say that _function $f$ is autonomous on
$\mathcal{F}$_ if all the transitions emanating from $f$ (that is, all
transitions of the form
$f(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}y$,
for some $x,\mu,y$) are autonomous on $\mathcal{F}$.

When $\mathcal{F}$ is clear, we omit it, and we simply say that a function _is
autonomous_.

Thus, $f$ is autonomous on $\mathcal{F}$ if, for some indexing set $I$, there
are $\mu_{i}$ and functions $f_{i}\in\mathcal{F}$ such that for all $x$ it
holds that:
$f(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{i}(x)$,
for each $i$; the set of all transitions emanating from $f(x)$ is precisely
$\cup_{i}\\{f(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{i}(x)\\}$.
Autonomous transitions correspond to expression transitions in CCS, and
autonomous functions correspond to guarded contexts, which do not need the
contribution of their process argument to perform the first transition.

We now formulate conditions under which, intuitively, a state function behaves
like a CCS context. Functions satisfying these conditions are called
_operators_. Such operators are defined relative to a behavioural equivalence
or preorder; in this section we are interested in bisimilarity, hence the
relation $R$ in the definition below should be understood to be $\approx$.

######  Definition  (Set of operators).

Consider an LTS $\mathcal{T}$, a binary relation $R$ on $\mathcal{T}$, and a
set $\mathcal{O}$ of functions from $S$ to $S$. We say that $\mathcal{O}$ is a
_set of $R$-operators on $\mathcal{T}$_ if the following conditions hold:

  1. (1)

$\mathcal{O}$ contains the identity function;

  2. (2)

$\mathcal{O}$ is closed by composition (that is, $f\circ g\in\mathcal{O}$
whenever $f,g\in\mathcal{O}$);

  3. (3)

composition preserves autonomy (i.e., if $g$ is autonomous on $\mathcal{O}$,
then so is $f\circ g$);

  4. (4)

$R$ is preserved, that is, all functions in $\mathcal{O}$ respect $R$

A ‘symmetric variant’ of clause 3 always holds: if $f$ is autonomous, then so
is $f\circ g$: indeed, transitions of $f(x)$ do not depend on $x$, hence
transitions of $f(g(x))$ do not depend on either $x$ or $g$. Clause 4
expresses congruence of the equivalence w.r.t. the set of contexts: here, the
state functions in $\mathcal{O}$. The autonomous transitions of a set of
$R$-operators yield an LTS whose states are the operators themselves. Such
transitions are of the form
$f\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g$.

In the remainder of this section, we assume $R$ to be equal to bisimilarity,
and call _set of operators_ any set of $\approx$-operators, without specifying
the relation. Where the underlying set $\mathcal{O}$ of operators is clear, we
simply call a function belonging to $\mathcal{O}$ an _operator_.

We define weak transitions as follows:
$f\mathrel{\stackrel{{\scriptstyle{\;\;\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g$
if there is a sequence of autonomous transitions
$f\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\dots\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{n}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g$.
$\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
is then simply
$\mathrel{\stackrel{{\scriptstyle{\;\;\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\mathrel{\stackrel{{\scriptstyle{\;\;\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.

We use state functions to express equations, such as $X=f(X)$. We thus look at
conditions under which such an equation has a unique solution (again, the
generalisation to a system of equations is easy, using $n$-ary functions).

Thinking of functions as equation expressions, to formulate our abstract
theory about unique solution of equations, we have to define the divergences
of finite and infinite unfoldings of state functions. The $n$th unfolding of
$f$ (for $n\geq 1$), $f^{n}$, is the function obtained by $n$ applications of
$f$. An operator is _well-behaved_ if there is $n$ with $f^{n}$ autonomous
(the well-behaved operators correspond, in CCS, to equations some finite
unfolding of which yields a guarded expression). We also have to reason about
the infinite unfolding of an equation $X=f(X)$. For this, given a set
$\mathcal{O}$ of operators, we consider the infinite terms obtained by
infinite compositions of operators in $\mathcal{O}$, that is, the set
coinductively defined by the grammar:

$F:=f\circ F\hskip 28.45274pt\mbox{ for $f\in\mathcal{O}$ }$

(Note that this syntax only deals with infinite compositions. Since
$\mathcal{O}$ is closed under finite compositions, we do not need to handle
such compositions in the above definition.) In particular, we write
$f^{\infty}$ for the infinite term $f\circ f\circ f\circ\ldots$.

We define the autonomous transitions for such infinite terms using the
following rules:

$\displaystyle{g\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g^{\prime}\over
g\circ
F\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g^{\prime}\circ
F}\mbox{ $g$ autonomous}\hskip 56.9055pt\displaystyle{(g\circ f)\circ
F\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F^{\prime}\over
g\circ(f\circ
F)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F^{\prime}}\mbox{
$g$ not autonomous}$

Intuitively a term is ‘unfolded’, with the second rule, until an autonomous
function is uncovered, and then transitions are computed using the first rule
(we disallow unnecessary unfoldings; these would complicate our abstract
theorems, by adding duplicate transitions, since the transitions of $g\circ f$
duplicate those of $g$ when $g$ is autonomous). An infinite term has no
transitions if none of its finite unfoldings ever yields an autonomous
function. This situation does not arise for terms of the form $f^{\infty}$ or
$g\circ f^{\infty}$, where $f$ is well-behaved, which are the terms we are
interested in. Note that no infinite term belongs to a set of operators.

These rules are consistent for finite compositions of functions in
$\mathcal{O}$, in the sense that they allow one to infer the correct
transitions for finite compositions of functions.

The following lemmas show that infinite terms have the same transitions
$\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}$
and weak transitions
$\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
as their counterpart finite unfoldings. To build a transition
$f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F$
from a transition of an unfolding
$f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g$,
we need to reason up to (finite) unfoldings of $f$: thus we set $=_{f}$ to be
the symmetric reflexive transitive closure of the relation that relates $g$
and $g^{\prime}$ whenever $g=g^{\prime}\circ f$.

######  Lemma .

Let $f$ be a well-behaved operator and $g$ an operator in some set
$\mathcal{O}$. Then $g\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F$
for some $F$ if and only if there is $n$ such that $g\circ
f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h$
for some $h$; in which case, there is $h^{\prime}=_{f}h$ such that
$F=h^{\prime}\circ f^{\infty}$.

###### Proof.

  1. $(\Rightarrow)$

Assume $g\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}F$.
By a simple induction over the derivation of this transition, we get that
there is $n$ such that $f^{n}$ is autonomous,
$f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h$,
and $F=h\circ f^{\infty}$

  2. $(\Leftarrow)$

Assume $g\circ
f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h$.
Since $f$ is well-behaved and composition respects autonomy, there is $m$ such
that $g\circ f^{m}$ is autonomous; we take that $m$ to be the minimum among
the exponents that make $g\circ f^{m}$ autonomous. If $n\leq m$, there is an
autonomous transition $g\circ
f^{m}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h\circ(f^{m-n})$.
If $m\leq n$, given that $g\circ f^{m}$ is autonomous, there is a transition
$g\circ
f^{m}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h^{\prime}$,
where $h^{\prime}\circ f^{n-m}=h$. Either way, $g\circ
f^{m}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h_{0}$,
where $h_{0}=_{f}h$.

Since $m$ is the smallest exponent that makes $g\circ f^{m}$ autonomous, we
can derive $(g\circ f^{m})\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g_{0}\circ
f^{\infty}$. This concludes the proof. ∎

We now adapt Lemma 4.1 to weak transitions.

######  Lemma .

Let $f$ be a well-behaved operator and $g$ an operator in some set
$\mathcal{O}$. Then $g\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}F$
for some $F$ if and only if there is $n$ such that $g\circ
f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}h$
for some $h$; in which case, there is $h^{\prime}=_{f}h$ such that
$F=h^{\prime}\circ f^{\infty}$.

###### Proof.

For each implication, proceed by induction over the length of
$\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
and use Lemma 4.1. ∎

######  Definition  (Operators and divergences).

Let $f,f^{\prime},f_{i}$ be operators in a set $\mathcal{O}$ of operators, and
consider the LTS induced by the autonomous transitions of operators in
$\mathcal{O}$. A sequence of transitions
$f_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{2}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{3}\dots$is
a _divergence_ if for some $n\geq 1$ we have $\mu_{i}=\tau$ whenever $i\geq
n$. We also say that $f_{1}$ _diverges_. We apply these notations and
terminology also to infinite terms, as expected.

In the remainder of the section we fix a set $\mathcal{O}$ of operators and we
only consider autonomous transitions on $\mathcal{O}$. We now state the
“abstract version” of Theorem 3.1.

######  Theorem  (Unique solution, abstract formulation).

Let $f$ be a well-behaved operator on $\mathcal{O}$ on some LTS $\mathcal{T}$.
If $f^{\infty}$ does not diverge, then the equation $X=f(X)$ either has no
solution or has a unique solution for $\approx$.

###### Proof.

The proof is essentially the same as that of Theorem 3.1, replacing equations
expressions with operators, from a fixed set of operators $\mathcal{O}$ (one
still has to consider reducts from an operator), and replacing instantiation
of equation expression transitions with instantiation of autonomous
transitions. A guarded equation expression becomes an autonomous operator. ∎

The equation in the statement of the theorem might have no solution at all.
For example, consider the LTS $(\mathbb{N},\\{a\\},\rightarrow)$ where for
each $n$ we have
$n+1\mathrel{\stackrel{{\scriptstyle{\;\;a\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}n$.
The function $f$ with $f(n)=n+1$ is an operator of the set
$\mathcal{O}=\\{f^{n}\\}_{n\in\mathbb{N}}$ (with $f^{0}=\mathtt{Id}$, the
identity function). The function $f$ is autonomous because, for all $n$, the
only transition of $f(n)$ is
$f(n)\mathrel{\stackrel{{\scriptstyle{\;\;a\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}n$
(this transition is autonomous because
$f\mathrel{\stackrel{{\scriptstyle{\;\;a\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\mathtt{Id}$).
A fixpoint of $f$ would be an element $x$ with
$x\mathrel{\stackrel{{\scriptstyle{\;\;a\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}x$,
and there is no such $x$ in the LTS.

Theorem 4.1 can be refined along the lines of Theorem 3.2. For this, we have
to relate the divergences of any $f^{n}$ (for $n\geq 1$) to divergences of
$f^{\infty}$, in order to distinguish between innocuous and non-innocuous
divergences.

######  Lemma .

Consider an autonomous operator $f$ on $\mathcal{O}$ and a divergence of
$f^{n}$

$f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\ldots\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{i}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}f_{i+1}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\ldots$

This yields a divergence of $f^{\infty}$:
$f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g_{1}\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\ldots\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g_{i}\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}g_{i+1}\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;\tau\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\ldots$

such that for all $i\geq 1$, $g_{i}$ is an operator and $g_{i}=_{f}f_{i}$.

###### Proof.

The proof is a simple induction on the sequence of transitions defining the
divergence. At each step, we unfold $f^{\infty}$ as many times as needed. ∎

Given a divergence $\Delta$ of $f^{n}$, we write $\Delta^{\infty}$ to indicate
the divergence of $f^{\infty}$ obtained from $\Delta$ as in Lemma 4.1. We call
a divergence of $f^{\infty}$ _innocuous_ when it can be described in this way,
that is, as a divergence $\Delta^{\infty}$ obtained from a divergence $\Delta$
of $f^{n}$, for some $n$.

######  Theorem  (Unique solution with innocuous divergences, abstract
formulation).

Let $f\in\mathcal{O}$ be a well-behaved operator. If all divergences of
$f^{\infty}$ are innocuous, then the equation $X=f(X)$ either has no solution
or has a unique solution for $\approx$.

###### Proof.

Just as in CCS, where the proof of Theorem 3.1 has to be modified for Theorem
3.2, here the proof of Theorem 4.1 is to be modified. The modification is
essentially the same as in CCS, again substituting equation expressions for
operators. ∎

###  4.2. Reasoning with other Behavioural Relations

#### Trace-based Equivalences.

We can adapt the results of the previous section about bisimilarity to other
settings, including both preorders and non-coinductive relations. As an
example, we consider trace-based relations.

We call a finite sequence of actions $s=\mu_{1},\ldots,\mu_{n}$, where each
$\mu_{i}$ is a visible action, a _trace_. Accordingly, an infinite sequence of
such actions $s=(\mu_{i})_{i\in\mathbb{N}}$ is called an _infinite trace_.
Given $s=\mu_{1},\dots,\mu_{n}$ a trace, we write
$x\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
if
$x\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}x_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}x_{2}\ldots
x_{n-1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}x_{n}$,
for some states $x_{1},\ldots,x_{n}$. Likewise, given
$s=(\mu_{i})_{i\in\mathbb{N}}$ an infinite trace, we write
$x\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
if there are states $(x_{i})_{i\in\mathbb{N}}$ such that $x=x_{0}$ and for all
$i\in\mathbb{N}$,
$x_{i}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}x_{i+1}$.

######  Definition  (Trace-based relations).

Two states $x,y$ are in the _trace inclusion_ , written $x\subseteq_{tr}y$, if
$x\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
implies
$y\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
for each trace $s$. They are _trace equivalent_ , written $x\approx_{tr}y$, if
both $x\subseteq_{tr}y$ and $y\subseteq_{tr}x$ hold.

Two states $x,y$ are in the _infinite trace inclusion_ , written
$x\subseteq_{tr^{\infty}}y$, if
$x\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
implies
$y\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
for each finite or infinite trace $s$. They are _infinite trace equivalent_ ,
written $x\approx_{tr}^{\infty}y$, if both $x\subseteq_{tr^{\infty}}y$ and
$y\subseteq_{tr^{\infty}}x$ hold.

The definitions from Section 4.1 are the same as for $\approx$; however we now
consider sets of $\subseteq_{tr}$-operators, i.e., we are interested in
operators that respect $\subseteq_{tr}$. Indeed the preorder $\subseteq_{tr}$
is used in the proof of unique solution for $\approx_{tr}$, hence operators
must respect $\subseteq_{tr}$ rather than $\approx_{tr}$.

The notion of trace is extended to operators like we do for weak transitions:
we write
$f\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
if there is a sequence of autonomous transitions
$f\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}f_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}\dots\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}f_{n}$
($s=\mu_{1},\dots,\mu_{n}$), and likewise for infinite traces.

######  Lemma .

Given a well-behaved $\subseteq_{tr}$-operator $f$, a
$\subseteq_{tr}$-operator $g$, and a (finite) trace $s$, we have $g\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
if and only if there is $n$ such that $g\circ
f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.

###### Proof.

We proceed by induction over the length of $s$, and apply Lemma 4.1 in each
case. ∎

All theorems obtained for $\approx$ can be adapted to $\approx_{tr}$, with
similar proofs. As an example, Theorem 4.1 becomes:

######  Theorem .

Let $f\in\mathcal{O}$ be a well-behaved $\subseteq_{tr}$-operator. If all
divergences of $f^{\infty}$ are innocuous, then the equation $X=f(X)$ either
has no solution or has a unique solution for $\approx_{tr}$.

###### Proof.

We proceed by showing that $x\subseteq_{tr}f(x)$ implies
$x\subseteq_{tr}f^{\infty}$, and then that $f(x)\subseteq_{tr}x$ implies
$f^{\infty}\subseteq_{tr}x$. This indeed gives that $x\approx_{tr}f(x)$
implies $x\approx_{tr}f^{\infty}$; hence the equation has at most one solution
($f^{\infty}$ does not belong to the LTS, hence it is not a solution).

  1. (1)

$f(x)\subseteq_{tr}x$ implies $f^{\infty}\subseteq_{tr}x$. For this part, the
absence of divergence hypothesis is not needed.

Let $s$ be a trace, and assume
$f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.
By Lemma 4.2, there is $n$ such that
$f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.
Hence,
$f^{n}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.
Since $f(x)\subseteq_{tr}x$ and $f$ is an $\subseteq_{tr}$-operator, we have
that $f^{n}(x)\subseteq_{tr}f^{n-1}(x)\subseteq_{tr}\dots\subseteq_{tr}x$.
Hence,
$x\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
and $f^{\infty}\subseteq_{tr}x$.

  2. (2)

$x\subseteq_{tr}f(x)$ implies $x\subseteq_{tr}f^{\infty}$. This part of the
proof is very similar to the proofs of Theorems 3.2 and 4.1.

Assume $x\subseteq_{tr}f(x)$, and
$x\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.
We want to show that there exists some $n$ such that
$f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
then apply Lemma 4.2; this would show
$f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.
To that end, we build a strictly increasing sequence of (autonomous)
transitions $f^{n\times
p}\mathrel{\stackrel{{\scriptstyle{\;\;s_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n}$,
such that
$g_{n}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime}n\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
and such that $s=s_{n}s^{\prime}_{n}$ for all $n$ ($s_{n}$ and
$s^{\prime}_{n}$ are traces whose concatenation is $s$). Here $p$ is such that
$f^{p}$ is autonomous (we always unfold $p$ times at once). Strictly
increasing means that the transition $f^{(n+1)\times
p}\mathrel{\stackrel{{\scriptstyle{\;\;s_{n+1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n+1}$
can be decomposed as $f^{(n+1)\times
p}\mathrel{\stackrel{{\scriptstyle{\;\;s_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n}\circ
f^{p}\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n+1}$
for some $s^{\prime\prime}_{n}$ ($s_{n+1}=s_{n}s^{\prime\prime}_{n}$). This
construction will have to stop, otherwise we build a non-innocuous divergence.

#### Construction of the sequence.

Assume $p$ is such that $f^{p}$ is autonomous; such a $p$ exists, since $f$ is
well-behaved.

We initialise with the empty trace from $f^{0}=\mathtt{id}$. Indeed, we have
$\mathtt{id}(x)\mathrel{\stackrel{{\scriptstyle{\;\;\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}\mathtt{id}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
and $s$ is indeed the concatenation of itself with the empty trace.

Then, at step $n$, suppose we have, for instance, $f^{n\times
p}\mathrel{\stackrel{{\scriptstyle{\;\;s_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n}$,
and
$g_{n}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime}_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.

     * •

If $s^{\prime}_{n}$ is the empty trace, we stop. We have in this case
$f^{n}\mathrel{\stackrel{{\scriptstyle{\;\;s\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
which concludes.

     * •

Otherwise, we have $f^{(n+1)\times
p}\mathrel{\stackrel{{\scriptstyle{\;\;s_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n}\circ
f$ (by autonomy). The operators are $\subseteq_{tr}$-operators, and by
hypothesis $x\subseteq_{tr}f(x)$, therefore $g_{n}(x)\subseteq_{tr}g_{n}\circ
f^{p}(x)$. From there, $g_{n}\circ
f^{p}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime}_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$.

$s^{\prime}_{n}$ is not the empty sequence, so there is $y_{1},\dots,y_{n}$
for $n\geq 1$ such that $g_{n}\circ
f^{p}(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}y_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\dots\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{n}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}y_{n}$,
where $s^{\prime}_{n}=\mu_{1}\dots\mu_{k}$. Take $\mu_{1}\dots\mu_{i}$ the
longest prefix of $s^{\prime}_{n}$ such that there is operators
$h_{1},\dots,h_{i}$ such that $g_{n}\circ
f^{p}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h_{1}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{2}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}\dots\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}h_{i}$.
It cannot be empty: indeed, $f^{p}$ is autonomous and composition respects
autonomy, hence so is $g_{n}\circ f^{p}$, so $g_{n}\circ
f^{p}(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{1}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}y_{1}$
is always autonomous. We take $g_{n+1}$ to be $h_{i}$, $s^{\prime}_{n+1}$ to
be the trace corresponding to $\mu_{i+1}\dots\mu_{k}$ (i.e., removing all
$\tau$s) and $s_{n+1}$ to be $s_{n}s^{\prime\prime}_{n}$, where
$s^{\prime\prime}_{n}$ is the trace corresponding to $\mu_{1}\dots\mu_{i}$
(again, removing all $\tau$s).

Then, we indeed have $f^{n\times p}\circ f^{p}=f^{(n+1)\times
p}\mathrel{\stackrel{{\scriptstyle{\;\;s_{n+1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n+1}$,
and
$g_{n+1}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime}_{n+1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
where $s=s_{n+1}s^{\prime}_{n+1}$.

Suppose now that the construction given above never stops. To make the
argument clearer, we reason up to $=_{f}$ (we identify all operators that are
$=_{f}$). We know that
$g_{n}\circ{f^{p}}\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n+1}$,
therefore, by applying Lemma 4.1 as many times as needed (just as in Lemma
4.2), we get that $g_{n}\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{n}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{n+1}\circ
f^{\infty}$.

This gives an infinite sequence of transitions starting from $f^{\infty}$:
$f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{0}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}g_{1}\circ
f^{\infty}\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}\dots$.
We observe that in the latter sequence, every step involves at least one
transition (the $s^{\prime\prime}_{i}$ are supposed non-empty, otherwise we
would have stopped). Moreover, the sequence
$s^{\prime\prime}_{1}s^{\prime\prime}_{2}\dots$, when removing all $\tau$s, is
a prefix of $s$. Therefore there is a finite number of visible actions
occurring in this infinite sequence. Therefore $f^{\infty}$ is divergent.

Furthermore, this divergence is not innocuous: at every step, we know that the
transition
$g_{n+1}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{n+1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
is not autonomous, otherwise $s^{\prime\prime}_{n+1}$ would be part of
$s_{n}$. Hence, there cannot be such a divergence
$f^{m}\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{0}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}\dots$,
as this would imply
$g_{n+1}(x)\mathrel{\stackrel{{\scriptstyle{\;\;s^{\prime\prime}_{n+1}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$
is autonomous for $n$ such that $n\times p\geq m$. ∎

In contrast, the theorems fail for _infinitary trace equivalence_ ,
$\approx_{tr}^{\infty}$ (whereby two processes are equated if they have the
same traces, including the infinite ones), for the same reason why the ‘unique
solution of contraction’ technique fails in this case [San15]. As a
counterexample, we consider equation $X=a+a.X$, whose syntactic solution has
no divergences. The process
$P\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}\sum_{n>0}a^{n}$
is a solution, yet it is not $\approx_{tr}^{\infty}$-equivalent to the
syntactic solution of the equation, because the syntactic solution has an
infinite trace involving $a$ transitions. This phenomenon is due to the
presence of infinitary observables.

#### Preorders.

We show how the theory for equivalences can be transported onto _preorders_.
This means moving to _systems of pre-equations_ , $\\{X_{i}\leq E_{i}\\}_{i\in
I}$. With preorders, our theorems have a different shape: we do not use pre-
equations to reason about unique solution – we expect interesting pre-
equations to have many solutions, some of which may be incomparable with each
other. We rather derive theorems to prove that, in a given preorder, any
solution of a pre-equation is below its syntactic solution.

In the LTS we consider, an equation does not always have a solution. We thus
extend the original LTS with the transitions corresponding to the autonomous
transitions of the syntactic solution $f^{\infty}$.

We write $\subseteq_{tr}$ for trace inclusion, $\subseteq_{tr^{\infty}}$ for
infinitary trace inclusion, and $\leq_{s}$ for weak simulation. These
preorders are standard from the literature [vG90].

In the abstract setting, the body of the pre-equations are functions. Then the
theorems give us conditions under which, given a pre-equation $X\leq f(X)$ and
a behavioural preorder $\preceq$, a solution $r$, i.e., a state for which
$r\preceq f(r)$ holds, is below the syntactic solution $f^{\infty}$. We
present the counterpart of Theorem 4.1; other theorems are transported in a
similar manner, both the statements and the proofs.

######  Theorem .

Let $f\in\mathcal{O}$ be a well-behaved operator. If all divergences of
$f^{\infty}$ are innocuous, then, given a preorder
${\leq}\in{\\{\subseteq_{tr},\subseteq_{tr^{\infty}},\leq_{s}\\}}$, whenever
$x\leq f(x)$ we also have $x\leq f^{\infty}$, for any state $x$.

###### Proof.

  1. (1)

For $\subseteq_{tr}$, the proof is given as the item 2 of the proof of Theorem
4.2.

  2. (2)

For $\subseteq_{tr^{\infty}}$, the proof is very similar to the previous
proof: simply consider infinite traces, and rather that disjunct over whether
or not the construction stops (the construction cannot stop), disjunct over
whether the full trace is captured, or only $\tau$ actions occur from a moment
in the construction.

  3. (3)

For $\leq_{s}$ The proof is strictly included in the proofs of Theorems 3.2 or
4.1. ∎

Theorem 4.2 intuitively says that the syntactic solution of a pre-equation is
_maximal_ among all solutions. Note that, in contrast with equations, Theorem
4.2 and the theory of pre-equations also work for _infinitary trace
inclusion_.

The opposite direction for pre-equations, namely $\\{X_{i}\geq E_{i}\\}_{i\in
I}$ is less interesting; it means that the syntactic solution is _minimal_
among the solutions. This property is usually easy to obtain for a behavioural
preorder, and we do not need hypotheses such as autonomy, well-behavedness, or
non divergence, as stated in the following proposition:

######  Proposition .

Let $f\in\mathcal{O}$ be an operator, $\leq\in\\{\subseteq_{tr},\leq_{s}\\}$,
and $x$ such that $f(x)\leq x$. Then, $f^{\infty}\leq x$.

###### Proof.

  1. (1)

For $\subseteq_{tr}$, the proof is given as item 1 of the proof of Theorem
4.2.

  2. (2)

For $\leq_{s}$, the proof is very similar to the above proof for
$\subseteq_{tr}$. ∎

However, Proposition 4.2 may fail for preorders with infinitary observables,
such as infinitary trace inclusion. This is why the theory of equations fails
for infinitary trace equivalence. Indeed, if $P$ is a solution for the
equation $E\subseteq_{tr^{\infty}}X$ (whether or not $E$ is divergence-free),
then $K_{E}\subseteq_{tr^{\infty}}P$ does not necessarily hold. The equation
$X=a+a.X$, which is discussed after Theorem 4.2, provides a counter-example to
illustrate this observation.

######  Remark .

Suppose that $x$ and $y$ are such that $x\leq f(x)$ and $y\leq x$. Then we do
not necessarily have $y\leq f(y)$. Take for instance, in CCS, $P=a.b$, $Q=a|b$
and $E=a.X+b.X$. Then $Q\leq_{s}E[Q]$, and $P\leq_{s}Q$, however
$P\not\leq_{s}E[P]$.

###  4.3. Rule formats

A way to instantiate the results in Sections 4.1 and 4.2 is to consider _rule
formats_ [AFV01, MRG07]. These provide a specification for the form of the SOS
rules used to describe the constructs of a language. To fit a rule format into
the abstract formulation of the theory from Section 4.1, we view the
constructs of a language as functions on the states of the LTS (the terms or
processes of the language).

One of the most common formats is GSOS [BIM95, BIM88, vG05, FvG16]. The format
guarantees that the constructs of the language preserve autonomy. This allows
to show that the set of unary contexts (meaning, contexts that can be filled
with one term) in a GSOS language constitute a set of operators (Definition
4.1 (when seen as functions from terms to terms), and allows us to apply
Theorem 4.1 to any GSOS language.

We now use $x,y$ for _state variables_ , and $t,u$ for terms that are part of
the considered GSOS language (i.e., for elements of the set of states). We use
$c,d$ for contexts, seen as functions from the set of states to itself. We
write $\mathtt{op}$ for a construct of the language (a function symbol).

For a complete overview of rule formats and for the relevant definitions, we
refer the reader to [BIM88]. We recall the format of GSOS rules below,
slightly modified in order to use contexts:
{x_i$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μi,jy_i,j
∣ i∈I,
1≤j≤m_i}∪{x_j$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ’j,k
∣ j∈J, 1≤k≤n_j}
op(~x)$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ
c(~x,~y) $I,J$ are fixed subsets of $[1,n]$, where $n$ is the length of
$\widetilde{x}$. For $i\in I$ (resp. $j\in J$), $m_{i}$ (resp. $n_{j}$) is a
fixed integer. $\widetilde{y}$ is the list consisting of all $y_{i,j}$ for
$i\in I$ and $1\leq j\leq m_{j}$, as well as all $y_{j,k}$ for $j\in J$ and
$1\leq k\leq n_{j}$. $c$ is a context belonging to the language.

######  Lemma .

The set of unary contexts $\mathcal{O}$ of a language defined within the GSOS
format is such that composition in $\mathcal{O}$ preserves autonomy on
$\mathcal{O}$.

###### Proof.

Let $\mathcal{L}$ be such a language. We reason by induction over the contexts
(which are defined inductively using the constructs of $\mathcal{L}$).

  * •

The empty context (i.e., the ‘hole’, corresponding to the identity function
$\mathtt{id}$) preserves autonomy: if $c\in\mathcal{O}$ is autonomous, then so
is $\mathtt{id}\circ c=c$.

  * •

Consider a $n$-ary construct of the language (a function symbol),
$\mathtt{op}$, and a context $c=\mathtt{op}(c_{1},\dots,c_{n})$, where the
$c_{i}$’s are unary contexts.

We have to show that so is $c\circ c^{\prime}$, for $c^{\prime}$ autonomous.
Consider for this a transition $c\circ
c^{\prime}(t)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}u$
($t,u\in\mathcal{L}$), we prove that this transition is autonomous. The last
rule of the derivation tree of this transition is an instance of a GSOS rule
as seen above:
{x_i$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μi,jy_i,j
∣ i∈I,
1≤j≤m_i}∪{x_j$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ’j,k
∣ j∈J, 1≤k≤n_j}
op(~x)$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ
c_0(~x,~y) ($I,J$ and the $m_{i}$s and $n_{j}$s being fixed, as well as
$c_{0}$).

By definition $c\circ c^{\prime}(t)=\mathtt{op}(c_{1}\circ