theoremTheorem[section] lemma[theorem]Lemma definition[theorem]Definition
proposition[theorem]Proposition corollary[theorem]Corollary
example[theorem]Example University of Sheffield, United Kingdom Universität
Duisburg-Essen, Germany Universität Duisburg-Essen, Germany Universität
Duisburg-Essen, Germany Harsh Beohar and Sebastian Gurke and Barbara König and
Karla Messing [500]Theory of computation Concurrency [500]Theory of
computation Modal and temporal logics

###### Acknowledgements.

We want to thank Jonas Forster, Lutz Schröder and Paul Wild for several
interesting discussions on the topics of this paper. XX Map—->

# Hennessy-Milner Theorems via Galois Connections

Harsh Beohar  Sebastian Gurke  Barbara König  Karla Messing

###### Abstract

We introduce a general and compositional, yet simple, framework that allows us
to derive soundness and expressiveness results for modal logics characterizing
behavioural equivalences or metrics (also known as Hennessy-Milner theorems).
It is based on Galois connections between sets of (real-valued) predicates on
the one hand and equivalence relations/metrics on the other hand and covers a
part of the linear-time-branching-time spectrum, both for the qualitative case
(behavioural equivalences) and the quantitative case (behavioural metrics). We
derive behaviour functions from a given logic and give a condition, called
compatibility, that characterizes under which conditions a logically induced
equivalence/metric is induced by a fixpoint equation. In particular this
framework allows us to derive a new fixpoint characterization of directed
trace metrics.

###### keywords:

behavioural equivalences and metrics, modal logics, Galois connections

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]these are the CONCUR
review comments

inline]B: British English vs. American English?

##  1 Introduction

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]The results in the
general framework are already known (as mentioned by the authors), making it
unclear what the “main theorem” of this paper is
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]The generality of the
framework and that of the examples are not matching

In the verification of state-based transition systems, modal logics play a
central role: they can be used to specify the properties that a system must
satisfy and model-checking techniques allow us to verify whether this is in
fact the case. Modal logics also play a fundamental role in characterizing
behavioural equivalences: van Glabbeek in his seminal paper [g:linear-
branching-time] showed how a whole spectrum of behavioural equivalences and
preorders can be characterized via modal logics. This characterization is also
known as the Hennessy-Milner theorem [hm:hm-logic], which says that two states
$x,y$ are equivalent (wrt. to some notion of behavioural equivalence) iff they
satisfy the same formulas $\phi$ (of a given modal logic). Formally, $x\sim
y\iff\forall\phi\colon(x\models\phi\iff y\models\phi)$.

For quantitative systems, the notion of behavioural equivalence is often too
strict and small deviations in quantitative information, such as
probabilities, can cause two states that intuitively behave very much alike to
be inequivalent in a formal sense. Hence it is natural to consider various
metrics for determining at what behavioural distance two states lie
[dgjp:metrics-labelled-markov, bw:behavioural-pseudometric]. This yields an
extension of classical notions of behavioural equivalence which knows only
distance $0$ (two states behave the same) and distance $1$ (two states behave
differently). Such metrics have often been studied in probabilistic settings
[dgjp:metrics-labelled-markov], but they can be extended to measuring other
forms of distances, for instance for metric transition systems [afs:linear-
branching-metrics, fl:quantitative-spectrum-journal].

In the quantitative case, equivalences are replaced by pseudo-metrics and
evaluation of a formula $\phi$ results in a real-valued (as opposed to a
boolean-valued) function $\llbracket\phi\rrbracket$, intuitively indicating to
which degree a state satisfies a formula. Stated in this context the Hennessy-
Milner property says that
$d(x,y)=\bigvee_{\phi}|\llbracket\phi\rrbracket(x)-\llbracket\phi\rrbracket(y)|$,
where $d$ is the behavioural metric.

We present a general framework that allows to easily deduce the Hennessy-
Milner property for a variety of equivalences, preorders and (directed)
metrics in the qualitative and quantitative setting. We rely on a well-known
property [cc:systematic-analysis, cc:temporal-abstract-interpretation,
bkp:abstraction-up-to-games-fixpoint] for Galois connections that says under
which conditions left adjoints preserve least fixpoints. Such Galois
connections relate the logical with the behavioural universe and translate
sets of (real-valued) predicates to equivalences (metrics) and vice versa. Our
_first_ contribution is the identification of adjunctions both in
quantitative/qualitative settings, which are crucial in capturing bisimilarity
and (decorated) trace versions of equivalences/preorders/metrics.

While most contributions to this area start with a behavioural equivalence
(resp. metric) and define a corresponding characteristic logic, our approach
goes in the other direction, with the slogan: _“Derive behaviour functions
from a modal logic”_. The recipe, which is our _second_ contribution, is as
follows: we define a logic function living in the logical universe and check
that it is compatible with the closure induced by the Galois connection.
Compatibility ensures that the Hennessy-Milner property is satisfied when we
transfer the logic function into a behaviour function living in the
behavioural universe. More concretely, we can guarantee that the least
fixpoint of the logic function (the set of all formulas) induces an
equivalence (resp. metric) which is the least fixpoint of the behaviour
function. Note that in the qualitative case, the Galois connection is
contravariant, resulting in behavioural equivalence being the greatest
fixpoint, as usual.

Related ideas have been considered in more categorical settings [kr:logics-
coinductive-predicates, k:coalg-process-equivalence], here we demonstrate that
this can be done in a purely lattice-theoretical setup and in particular for
behavioural metrics. To our knowledge, the adjunctions that we are considering
here, have not yet been used to derive Hennessy-Milner theorems and behaviour
functions. Our _third_ contribution is the novel connection to up-to functions
and compatibility and we show how closure properties for up-to functions can
be employed to combine logics, leading to a modular framework. Furthermore,
the behaviour function that we obtain for the trace metric case is, as far as
we know, not yet known in the literature. Our _final_ contribution is the
characterisation of these behaviour functions in more concrete terms both in
the qualitative (Thm. 4.3 and Cor. 4.3) and quantitative (Thm. 5.3 and Cor.
5.3) cases. In turn, these general results effortlessly instantiate into many
of the equivalences in the van Glabbeek spectrum and immediately yield:
logical characterizations, the hierarchy between them and also recursive
characterizations, which are often hard to obtain (at least in the metric
case).

##  2 Preliminaries

Functions and Relations. Given a function $f\colon X\to Y$ and $Z\subseteq X$
we write $f[Z]$ for $\\{f(z)\mid z\in Z\\}$. Similarly, for a relation
$R\subseteq X\times X$ and $X^{\prime}\subseteq X$, we define
$R[X^{\prime}]=\\{y\in X\mid\exists x\in X^{\prime}\colon(x,y)\in R\\}$.
Furthermore, $Y^{X}$ denotes the set of all functions from $X$ to $Y$ and, for
a given set $\mathcal{F}\subseteq Y^{X}$ of functions, by
$\langle\mathcal{F}\rangle$ we denote a function of type $X\to
Y^{\mathcal{F}}$ defined as $\langle\mathcal{F}\rangle(x)(f)=f(x)$. For
$S\subseteq X$, $\chi_{S}\colon X\to\\{0,1\\}$ stands for the characteristic
function of $S$.

A _congruence_ is an equivalence relation
$R\subseteq\mathcal{P}(X)\times\mathcal{P}(X)$ satisfying the condition:
$\bigcup_{i\in I}X_{i}\,R\,\bigcup_{i\in I}Y_{i}$ whenever $X_{i}\,R\,Y_{i}$
for all $i\in I$. Given any relation
$R\subseteq\mathcal{P}(X)\times\mathcal{P}(X)$, by $\mathit{cong}(R)$ we
denote its _congruence closure_ , i.e., the smallest congruence such that
$R\subseteq\mathit{cong}(R)$.

The directed relation lifting
$R_{\overrightarrow{H}}\subseteq\mathcal{P}(X)\times\mathcal{P}(X)$ for a
relation $R\subseteq X\times X$ is defined as
$X_{1}\mathrel{R_{H}}X_{2}\iff\forall x_{1}\in X_{1}\exists x_{2}\in
X_{2}\colon x_{1}\mathrel{R}x_{2}$. Furthermore, we write
$R_{H}=R_{\overrightarrow{H}}\cap(R_{\overrightarrow{H}})^{-1}$, which can be
seen as a special case of the Hausdorff distance (see below).color=green!20]B:
reformulated this
remark.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]the name
Hausdorff should appear already here to understand rH — done

Pseudo-metrics. We use truncated subtraction and addition on the interval
$[0,1]$, i.e., for $r,s\in[0,1]$ we have $r\oplus s=\min\\{r+s,1\\}$,
$r\ominus s=\max\\{0,r-s\\}$.

A _directed pseudo-metric_ or _hemimetric_ on a set $X$ is a function
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]directed pseudo-
metrics are traditionally called hemimetrics — done? $d\colon X\times
X\to[0,1]$ such that for all $x,y,z\in X$ (i) $d(x,x)=0$, (ii) $d(x,z)\leq
d(x,y)\oplus d(y,z)$. It is called a _pseudo-metric_ if in addition (iii)
$d(x,y)=d(x,y)$ for all $x,y\in X$. Whenever $d(x,y)=0$ implies $x=y$ we drop
the prefix “pseudo-” and call $d$ a _metric_. Given a directed pseudo-metric
$d$ on $X$, $\overline{d}$ refers to the _symmetrization_ of $d$, i.e.,
$\overline{d}(x,y)=\max\\{d(x,y),d(y,x)\\}$color=green!20]B: replaced
$\max(a,b)$ by $\max\\{a,b\\}$, for every $x,y\in X$. Some examples of metrics
used in this paper are the following:

  * •

The discrete metric $d_{\text{disc}}$ on a set $A$ is $d_{\text{disc}}(a,b)=1$
if $a\neq b$ and $0$ otherwise.

  * •

The _Euclidean_ distance $d$ on the interval $[0,1]$ given by
$d(r,r^{\prime})=|r-r^{\prime}|$.

  * •

The _sup-metric_ $d$ on $[0,1]^{I}$ is given by $d(p,p^{\prime})=\sup_{i\in
I}|p(i)-p^{\prime}(i)|$.

  * •

The product of two (pseudo)metric spaces $(X,d_{X})$ and $(Y,d_{Y})$ is a
(pseudo)metric space $(X\times Y,d_{X}\otimes d_{Y})$, where $(d_{X}\otimes
d_{Y})((x,y),(x^{\prime},y^{\prime}))=\max\\{d_{X}(x,x^{\prime}),d_{Y}(y,y^{\prime})\\}$.

  * •

The directed Hausdorff lifting $d_{\overrightarrow{H}}$ of a directed space
$(X,d)$ is a directed pseudo-metric on $\mathcal{P}X$ given by
$d_{\overrightarrow{H}}(U,V)=\sup_{x\in U}\inf_{y\in V}d(x,y)$. Alternatively,
$d_{\overrightarrow{H}}(U,V)=\bigwedge_{U\subseteq V_{\epsilon}}\epsilon$,
where $V_{\epsilon}=\\{x\mid\bigwedge_{v\in V}d(x,v)\leq\epsilon\\}$.
Moreover, the Hausdorff lifting $d_{H}$ of a pseudo-metric $d$ is the
symmetrization of $d_{\overrightarrow{H}}$. Intuitively, the Hausdorff
distance between two sets is the farthest that any element of one set has to
“travel” to reach the other set.

Given a directed pseudo-metric $d\colon X\times X\to[0,1]$, a function
$f\colon X\to[0,1]$ is called _non-expansive wrt. $d$_ whenever for all
$x,y\in X$: $f(x)\ominus f(y)\leq d(x,y)$.

######  Lemma 2.1.

Let $I$ be an index set and let $a,b,a_{i},b_{i}\in[0,1]$, where $i\in I$.
Then the following (in)equalities hold. They are all equalities if
$I\neq\emptyset$.

$\displaystyle\Big{(}\bigvee_{i\in I}a_{i}\Big{)}\ominus b=\bigvee_{i\in
I}\Big{(}a_{i}\ominus b\Big{)}\qquad\Big{(}\bigwedge_{i\in
I}a_{i}\Big{)}\ominus b\leq\bigwedge_{i\in I}\Big{(}a_{i}\ominus b\Big{)}$
$\displaystyle a\ominus\Big{(}\bigvee_{i\in I}b_{i}\Big{)}\leq\bigwedge_{i\in
I}\Big{(}a\ominus b_{i}\Big{)}\qquad a\ominus\Big{(}\bigwedge_{i\in
I}b_{i}\Big{)}=\bigvee_{i\in I}\Big{(}a\ominus b_{i}\Big{)}$

Furthermore

$\displaystyle\Big{(}\bigvee_{i\in I}a_{i}\Big{)}\ominus\Big{(}\bigvee_{i\in
I}b_{i}\Big{)}\leq\bigvee_{i\in I}\Big{(}a_{i}\ominus
b_{i}\Big{)}\qquad\Big{(}\bigwedge_{i\in
I}a_{i}\Big{)}\ominus\Big{(}\bigwedge_{i\in I}b_{i}\Big{)}\leq\bigvee_{i\in
I}\Big{(}a_{i}\ominus b_{i}\Big{)}$

######  Proof 2.2.

The first four (in)qualities are straightforward.

For the fifth inequality observe that

$\displaystyle\bigvee_{i\in I}\Big{(}a_{i}\ominus
b_{i}\Big{)}\oplus\Big{(}\bigvee_{i\in I}b_{i}\Big{)}$
$\displaystyle\geq\bigvee_{i\in I}\Big{(}(a_{i}\ominus b_{i})\oplus
b_{i}\Big{)}\geq\bigvee_{i\in I}a_{i}$

Since $x\leq y\oplus z\iff x\ominus z\leq y$, the statement follows.

For the sixth inequality we use the fifth inequality and compute

$\displaystyle\Big{(}\bigwedge_{i\in
I}a_{i}\Big{)}\ominus\Big{(}\bigwedge_{i\in I}b_{i}\Big{)}$
$\displaystyle=\Big{(}1-\bigvee_{i\in
I}(1-a_{i})\Big{)}\ominus\Big{(}1-\bigvee_{i\in I}(1-b_{i})\Big{)}$
$\displaystyle=\Big{(}\bigvee_{i\in
I}(1-b_{i})\Big{)}\ominus\Big{(}\bigvee_{i\in I}(1-a_{i})\Big{)}$
$\displaystyle\leq\bigvee_{i\in
I}\big{(}(1-b_{i})\ominus\big{(}(1-a_{i})\big{)}=\bigvee_{i\in
I}\Big{(}a_{i}\ominus b_{i}\Big{)}$

Lattices, Fixpoints and Galois Connections. A _complete lattice_
$(\mathbb{L},\sqsubseteq)$ consists of a set $\mathbb{L}$ with a partial order
$\sqsubseteq$ such that each $Y\subseteq\mathbb{L}$ has a least upper bound
$\bigsqcup Y$ (also called supremum, join) and a greatest lower bound
$\bigsqcap Y$ (also called infimum, meet). In particular, $\mathbb{L}$ has a
bottom element $\bot=\bigsqcap\mathbb{L}$ and a top element
$\top=\bigsqcup\mathbb{L}$. Whenever the order is clear from the context, we
simply write $\mathbb{L}$ for a complete lattice. For example:

  * •

$([0,1],\leq)$ has a lattice structure with infimum $\bigwedge$ and supremum
$\bigvee$.

  * •

The set $\mathit{Eq}(X)$ ($\mathit{Pre}(X)$) of equivalences (preorders) on
$X$ is a lattice with $\bigsqcup=\bigcap$ and the join $\bigsqcup\mathcal{R}$
is the least equivalence (resp. preorder) generated by $\bigcup\mathcal{R}$.

  * •

The set $\mathit{PMet}(X)$ ($\mathit{DPMet}(X)$) of (directed) pseudo-metrics
is lattice-ordered by $\leq$.

Via the Knaster-Tarski theorem it is well-known that any monotone function
$f\colon\mathbb{L}\to\mathbb{L}$ on a complete lattice $\mathbb{L}$ has a
_least fixpoint_ $\mu f$ and a _greatest fixpoint_ $\nu f$.

Let $\mathbb{L}$, $\mathbb{B}$ be two lattices. A _Galois connection_ from
$\mathbb{L}$ to $\mathbb{B}$ is a pair $\alpha\dashv\gamma$ of monotone
functions $\alpha\colon\mathbb{L}\to\mathbb{B}$,
$\gamma\colon\mathbb{B}\to\mathbb{L}$ such that for all $\ell\in L$:
$\ell\sqsubseteq\gamma(\alpha(\ell))$ and for all $m\in\mathbb{B}$:
$\alpha(\gamma(m))\sqsubseteq m$. Equivalently, $\alpha(\ell)\sqsubseteq
m\iff\ell\sqsubseteq\gamma(m)$, for all $\ell\in\mathbb{L},m\in\mathbb{B}$.
The function $\alpha$ (resp. $\gamma$) is also called the _left_ (resp.
_right_) _adjoint_ and it preserves arbitrary joins (meets).

For an arbitrary function $f$, we define $f^{\omega}$ as
$f^{\omega}(x)=\bigsqcup_{i\in\mathbb{N}_{0}}f^{i}(x)$.
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]$log^{\omega}$ is
defined later — done Given a function $f\colon X\to[0,1]$, the function
$\tilde{f}\colon\mathcal{P}(X)\to[0,1]$ denotes the join-preserving function
generated by $f$ and is defined as $\tilde{f}(X^{\prime})=\bigvee_{x\in
X^{\prime}}f(x)$ (for $X^{\prime}\subseteq X$).

Closures. A _closure_ $c$ is a monotone, idempotent and extensive (i.e.
$x\sqsubseteq c(x)$) function on a lattice. Given a Galois connection
$\alpha\dashv\gamma$, the map $\gamma\circ\alpha$ is always a closure.
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]By extensive, you mean
$x\leq c(x)$? — done

Among other closure operators, we will often close under a given set of
operators. More concretely, let $Z$ be a set with an operation $\mathrm{op}$
and $Z^{\prime}\subseteq Z$, then
$\operatorname{\mathrm{cl}}^{\mathrm{op}}(Z^{\prime})$ is the least superset
of $Z^{\prime}$ that is closed under applying $\mathrm{op}$. For instance,
given a set $\mathcal{S}\subseteq\mathcal{P}(X)$,
$\operatorname{\mathrm{cl}}^{\cup}(\mathcal{S})$ closes $\mathcal{S}$ under
arbitrary unions and $\operatorname{\mathrm{cl}}^{\cup,\cap}(\mathcal{S})$
under arbitrary unions and intersections. On the other hand
$\operatorname{\mathrm{cl}}_{f}^{\mathrm{op}}$ closes only under finite
application of $\mathrm{op}$ (such as finite unions or intersections).

A special case is the shift, where, given a set
$\mathcal{F}\subseteq[0,1]^{X}$,
$\operatorname{\mathrm{cl}}^{\mathrm{sh}}(\mathcal{F})$ is the closure under
constant shifts, i.e., operations $f\mapsto f\ominus c$, $f\mapsto f\oplus c$
for $c\in[0,1]$.

Transition Systems. We will restrict to systems of the following kind in this
paper.

######  Definition 2.3 ((Metric) Transition Systems).

A _transition system_ over an alphabet $A$ is a pair $(X,\to)$ consisting of a
state space $X$ and a transition relation $\to\ \subseteq\,X\times A\times X$.
We write $x\xrightarrow{a}x^{\prime}$ for $(x,a,x^{\prime})\in\to$. For $x\in
X$, $\delta(x)=\\{(a,x^{\prime})\mid x\stackrel{{\scriptstyle
a}}{{\to}}x^{\prime}\\}$ and $\delta_{a}(x)$ denotes the $a$-successors of
$x$. A transition system is _finitely branching_ if $\delta(x)$ is finite for
every $x$. linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]About
finitely branching: this is not the usual notion for the classical Hennessy-
Milner theorem, but what is used in [7]. For the usual one, you need that for
all x, a $\delta_{a}(x)$ is finite. Actually, everything done in Section 4 can
be done with the usual definition. Of course, this is not a reasonable
definition for metrics, and what is done in Section 5 really relies on your
definition. But I do believe that your definition is also not reasonable as it
does not hold very often (especially in cases where it makes sense to consider
metrics on the alphabet). [7] says that most of what they do can be done in
the more general framework of compact branching. It seems hard in your case,
as you use it to restrict arbitrary conjunctions to finite ones (basically
Lemma 5.2).

For a set $\Delta\subseteq A\times X$ we denote by
$\operatorname{lab}(\Delta)$ the set of labels of $\Delta$, in other words the
projection to the first argument, i.e.
$\operatorname{lab}(\Delta)=\\{a\mid\exists x\in X\colon(a,x)\in\Delta\\}$.
Similarly $\operatorname{tgt}(\Delta)$ is the set of targets and projects to
the second argument.

A _metric transition system_ over $A$ is a triple $(X,\to,d_{A})$ with a
metric $d_{A}\colon A\times A\to[0,1]$.

######  Definition 2.4 (Traces).

For $x\in X,\sigma=a_{1}\cdots a_{n}\in A^{*}$, we write
$x\xrightarrow{\sigma}x^{\prime}$ if $x\stackrel{{\scriptstyle
a_{1}}}{{\to}}\cdots\stackrel{{\scriptstyle a_{n}}}{{\to}}x^{\prime}$ and
define $\operatorname{Tr}(x)=\\{\sigma\mid\exists x^{\prime}\colon
x\xrightarrow{\sigma}x^{\prime}\\}$. We extend $\delta,\delta_{a}$ to
sequences $\hat{\delta},\hat{\delta}_{\sigma}$ in the obvious way.

Given a metric transition system, the distance of two traces is defined as
$d_{\mathrm{Tr}}\colon A^{*}\times A^{*}\to[0,1]$ where
$d_{\mathrm{Tr}}(\sigma_{1},\sigma_{2})=1$ if $|\sigma_{1}|\neq|\sigma_{2}|$,
$d_{\mathrm{Tr}}(\varepsilon,\varepsilon)=0$ and
$d_{\mathrm{Tr}}(a_{1}\sigma^{\prime}_{1},a_{2}\sigma^{\prime}_{2})=\max\\{d_{A}(a_{1},a_{2}),d_{\mathrm{Tr}}(\sigma^{\prime}_{1},\sigma^{\prime}_{2})\\}$
(sup-metric).

##  3 General Framework

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]About your framework:
you state most of the results on complete lattices, but I believe you only
need chain-completeness: 1) you do not use the special adjoint functor, you
are already given the Galois connection, 2) I think all the instances of
Knaster-Tarski theorem could be of Markowsky’s. Our results are based on the
following theorem that shows how fixpoints are preserved by Galois
connections, a well-known property, see for instance [cc:systematic-analysis,
cc:temporal-abstract-interpretation, bkp:abstraction-up-to-games-fixpoint].

We first introduce the notion of compatibility that has been studied in
connection with up-to techniques, enhancing coinductive proofs [p:complete-
lattices-up-to].

######  Definition 3.1.

Let $\operatorname{log},c\colon\mathbb{L}\to\mathbb{L}$ be two monotone endo-
functions on a lattice $\mathbb{L}$. We call $\operatorname{log}$
$c$-compatible whenever $\operatorname{log}\circ c\sqsubseteq
c\circ\operatorname{log}$.

Let $\mathbb{L},\mathbb{B}$ be two complete lattices with a Galois connection
$\alpha\colon\mathbb{L}\to\mathbb{B}$, $\gamma\colon\mathbb{B}\to\mathbb{L}$
and two monotone endo-functions
$\operatorname{log}\colon\mathbb{L}\to\mathbb{L}$,
$\operatorname{beh}\colon\mathbb{B}\to\mathbb{B}$.

  1. 1.

Then $\alpha\circ\operatorname{log}=\operatorname{beh}\circ\alpha$ implies
$\alpha(\mu\,\operatorname{log})=\mu\,\operatorname{beh}$.

  2. 2.

Let $c=\gamma\circ\alpha$ be the closure operator corresponding to the Galois
connection and assume that
$\operatorname{beh}=\alpha\circ\operatorname{log}\circ\gamma$. Then
$c$-compatibility of $\operatorname{log}$ implies
$\alpha(\mu\,\operatorname{log})=\mu\,\operatorname{beh}$.

  3. 3.

Whenever $\alpha\circ\operatorname{log}=\operatorname{beh}\circ\alpha$ and
$\operatorname{log}$ reaches its fixpoint in $\omega$ steps, i.e.,
$\mu\operatorname{log}=\operatorname{log}^{\omega}(\bot)$, so does
$\operatorname{beh}$. Here,
$\operatorname{log}^{\omega}=\bigsqcup_{i<\omega}\operatorname{log}^{i}$,
$\operatorname{log}^{0}=\bot$, and
$\operatorname{log}^{i+1}=\operatorname{log}\circ\operatorname{log}^{i}$ (for
$i\in\mathbb{N}$).
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]$log^{\omega}$ is
defined later

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]by additive you mean
preserves join?

######  Proof 3.2.

  1. 1.

We use the fact that $\mu\,\operatorname{beh}=\operatorname{beh}^{i}(\bot)$
for a suitable ordinal $i$. We show by transfinite induction that
$\alpha(\operatorname{log}^{i}(\bot))=\operatorname{beh}^{i}(\bot)$ for all
ordinals $i$.

For successor ordinals we have
$\alpha(\operatorname{log}^{i+1}(\bot))=\alpha(\operatorname{log}(\operatorname{log}^{i}(\bot)))=\operatorname{beh}(\alpha(\operatorname{log}^{i}(\bot)))=\operatorname{beh}(\operatorname{beh}^{i}(\bot))=\operatorname{beh}^{i+1}(\bot)$.

In addition $\alpha$ is join preserving since it is part of a Galois
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]by additive you mean
preserves join? HB: Fixed. connection. Hence for limit ordinals (including
$i=0$):
$\alpha(\operatorname{log}^{i}(\bot))=\alpha(\bigsqcup_{j<i}\operatorname{log}^{j}(\bot))=\bigsqcup_{j<i}\alpha(\operatorname{log}^{j}(\bot))=\bigsqcup_{j<i}\operatorname{beh}^{j}(\bot)=\operatorname{beh}^{i}(\bot)$.

  2. 2.

Easy corollary:
$\alpha\circ\operatorname{log}\sqsubseteq\alpha\circ\operatorname{log}\circ\gamma\circ\alpha=\operatorname{beh}\circ\alpha$.
Furthermore
$\operatorname{log}\circ\gamma\circ\alpha\sqsubseteq\gamma\circ\alpha\circ\operatorname{log}$
implies
$\operatorname{beh}\circ\alpha=\alpha\circ\operatorname{log}\circ\gamma\circ\alpha\sqsubseteq\alpha\circ\operatorname{log}$
by transpose. Hence
$\alpha\circ\operatorname{log}=\operatorname{beh}\circ\alpha$ and the first
result applies.

  3. 3.

Straightforward. linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]need
same assumption as for 3.2.1

Here $\mathbb{L}$ is the universe in which the logic lives and $\mathbb{B}$ is
the universe in which equivalences respectively metrics live. Furthermore
$\operatorname{log}$ is the “logic function”, constructing modal logic
formulas, and $\mu\,\operatorname{log}$ will be the set of all formulas. On
the other hand $\operatorname{beh}$ is the “behaviour function” whose least
(respectively greatest) fixpoint is the behavioural equivalence/metric.

######  Remark 3.3.

Note that the above theorem is true even in more general situations, for
example if $\mathbb{L}$ and $\mathbb{B}$ are only assumed to be CPOs. We stick
to complete lattices however since they are more widely known. Also, on a
complete lattice many notions of continuity, such as Scott-continuity or
chain-continuity, coincide [MR398913]. In the following we will therefore
simply say that a monotone function on $\mathbb{L}$ or $\mathbb{B}$ is
continuous if it preserves suprema of all (well-ordered) chains.

The recipe used in this paper is the following: first, define a logical
universe $\mathbb{L}$ and a logic function
$\operatorname{log}\colon\mathbb{L}\to\mathbb{L}$. Then choose a suitable
Galois connection $\alpha\dashv\gamma$ to a behaviour universe $\mathbb{B}$
and show that $\operatorname{log}$ is $c$-compatible, where
$c=\gamma\circ\alpha$ is the closure associated to the Galois connection. Then
define the behaviour function
$\operatorname{beh}=\alpha\circ\operatorname{log}\circ\gamma\colon\mathbb{B}\to\mathbb{B}$
and from the results above, we automatically obtain the equality
$\alpha(\mu\,\operatorname{log})=\mu\,\operatorname{beh}$, which tells us that
logical and behavioural equivalence respectively distance coincide (Hennessy-
Milner theorem). This will be worked out in the following examples.

Combining logic functions results in the combination of the corresponding
behaviour functions, which is essential in establishing Hennessy-Milner
theorems compositionally.

Let $i\in\\{1,2\\}$ and
$\operatorname{log}_{i},c\colon\mathbb{L}\to\mathbb{L}$ be monotone functions
on a complete lattice $\mathbb{L}$ such that $\operatorname{log}_{i}$ are
$c$-compatible. Then $\operatorname{log}_{1}\sqcup\operatorname{log}_{2}$ and
$\operatorname{log}_{1}\circ\operatorname{log}_{2}$ are also $c$-compatible.

Let $\operatorname{beh}_{i}=\alpha\circ\operatorname{log}_{i}\circ\gamma$ be
the behaviour functions corresponding to $\operatorname{log}_{i}$. Then the
behaviour functions of $\operatorname{log}_{1}\sqcup\operatorname{log}_{2}$
and $\operatorname{log}_{1}\circ\operatorname{log}_{2}$ are, respectively,
$\operatorname{beh}_{1}\sqcup\operatorname{beh}_{2}$ and
$\operatorname{beh}_{1}\circ\operatorname{beh}_{2}$.

######  Proof 3.4.

The $c$-compatibility of
$\operatorname{log}_{1}\sqcup\operatorname{log}_{2},\operatorname{log}_{1}\circ\operatorname{log}_{2},\operatorname{log}^{\omega}$
follows from [p:complete-lattices-up-to].

The behaviour function of $\operatorname{log}_{1}\sqcup\operatorname{log}_{2}$
is

$\alpha\circ(\operatorname{log}_{1}\sqcup\operatorname{log}_{2})\circ\gamma=\alpha\circ(\operatorname{log}_{1}\circ\gamma\sqcup\operatorname{log}_{2}\circ\gamma)=\alpha\circ\operatorname{log}_{1}\circ\gamma\sqcup\alpha\circ\operatorname{log}_{2}\circ\gamma=\operatorname{beh}_{1}\sqcup\operatorname{beh}_{2}$

since $\alpha$, as left adjoint, preserves joins.

The behaviour function of $\operatorname{log}_{1}\circ\operatorname{log}_{2}$
is

$\displaystyle\alpha\circ\operatorname{log}_{1}\circ\operatorname{log}_{2}\circ\gamma$
$\displaystyle\sqsubseteq$
$\displaystyle\alpha\circ\operatorname{log}_{1}\circ\gamma\circ\alpha\circ\operatorname{log}_{2}\circ\gamma=\operatorname{beh}_{1}\circ\operatorname{beh}_{2}$
$\displaystyle\operatorname{beh}_{1}\circ\operatorname{beh}_{2}$
$\displaystyle=$
$\displaystyle\alpha\circ\operatorname{log}_{1}\circ\gamma\circ\alpha\circ\operatorname{log}_{2}\circ\gamma=\alpha\circ\operatorname{log}_{1}\circ
c\circ\operatorname{log}_{2}\circ\gamma$ $\displaystyle\sqsubseteq$
$\displaystyle\alpha\circ
c\circ\operatorname{log}_{1}\circ\operatorname{log}_{2}\circ\gamma=\alpha\circ\operatorname{log}_{1}\circ\operatorname{log}_{2}\circ\gamma$

since $\alpha\circ c=\alpha\circ\gamma\circ\alpha=\alpha$.

Furthermore every constant function $k$ and the identity are $c$-compatible.
Their corresponding behaviour functions are the constant function
$b\mapsto\alpha(\ell)$color=green!20]B: replaced $R$ by $b$ since we are still
in the general case (where $\ell$ is the constant value of $k$) respectively
the co-closure $\alpha\circ\gamma$.

We are using techniques for the construction of up-to functions studied in
[p:complete-lattices-up-to], but we are using them in a non-standard way. The
point is subtle since the closure is usually supposed to be the up-to
function, while in our notion of compatibility the logic function plays this
role. Furthermore we are interested in least fixpoints, while the results of
[p:complete-lattices-up-to] study post-fixpoints up-to in order to show that a
lattice element is below the greatest fixpoint.

##  4 Qualitative Case

We will start with the classical, qualitative case with behavioural
equivalences on the one side and boolean-valued modal logics on the other
side. In this way we will recreate parts of the theory of [g:linear-branching-
time], incorporating it into the setting of adjunctions as described earlier.
Throughout this section we fix a transition system $(X,\to)$ over $A$.

###  4.1 Bisimilarity

For standard bisimilarity we work with the lattices
$\mathbb{L}=(\mathcal{P}(\mathcal{P}(X)),\subseteq)$ and
$\mathbb{B}=(\mathit{Eq}(X),\supseteq)$. The Galois connection is given as
follows, where $[x]_{R}$ is the equivalence class of $x$ wrt. $R$:

$\displaystyle\operatorname{\alpha_{b}}(\mathcal{S})$ $\displaystyle=$
$\displaystyle\\{(x,x^{\prime})\in X\times X\mid\forall
S\in\mathcal{S}\colon(x\in S\iff x^{\prime}\in S)\\}$
$\displaystyle\operatorname{\gamma_{b}}(R)$ $\displaystyle=$
$\displaystyle\\{S\subseteq X\mid\forall(x,x^{\prime})\in R\colon(x\in S\iff
x^{\prime}\in S)\\}=\left\\{\bigcup\\{[x]_{R}\mid x\in S\\}\mid S\subseteq
X\right\\}.$

Intuitively $\operatorname{\alpha_{b}}$ generates an equivalence on $X$ from a
set of subsets of $X$ and $\operatorname{\gamma_{b}}$ maps an equivalence to
all subsets of $X$ that are closed under this equivalence. Both functions are
monotone and it is easy to see from the definition that it is indeed a Galois
connection (see also Prop. 4.1 below). As logic function we consider
$\operatorname{\log_{b}}\colon\mathcal{P}(\mathcal{P}(X))\to\mathcal{P}(\mathcal{P}(X))$
with $\operatorname{\log_{b}}(\mathcal{S})=\bigcup_{a\in
A}\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\mathcal{S})]$,
where $\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}$ closes $\mathcal{S}$ under
finite unions and complement (hence also finite intersections). Moreover,
$\Diamond_{a}(S)=\\{x\in X\mid\exists x^{\prime}\in S:\
x\xrightarrow{a}x^{\prime}\\}$ for $a\in A$.

The function $\operatorname{\log_{b}}$ is easily seen to be continuous and
$\mu\,\operatorname{\log_{b}}$ is the set of subsets of $X$ obtained by
evaluating modal logic formulas consisting of constants
$\mathit{true},\mathit{false}$ (empty conjunction/disjunction), binary
conjunctions/disjunctions, negation and diamond modality, where the outermost
operator is always the modality. Note that $\mu\operatorname{\log_{b}}$ is a
strict subset of the usual modal logic formulas, but sufficient for
expressivity.

We first study the closure associated to the Galois connection, which is
important for showing compatibility later on, and the corresponding co-
closure.

The closure
$\operatorname{c_{b}}=\operatorname{\gamma_{b}}\circ\operatorname{\alpha_{b}}$
closes a set $\mathcal{S}\subseteq\mathcal{P}(X)$ under arbitrary boolean
operations (union, intersection, complement), while the co-closure
$\operatorname{\alpha_{b}}\circ\operatorname{\gamma_{b}}$ is the identity.

######  Proof 4.1.

  * •

First, it is easy to see from the definition that, given $\mathcal{S}$,
$\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}))$ contains
$\mathcal{S}$ and is closed under arbitrary unions, intersections and
complement. In particular, if $S_{i}\in\operatorname{\gamma_{b}}(R)$ for $i\in
I$, then $\bigcup_{i\in I}S_{i}\in\operatorname{\gamma_{b}}(R)$ and
$\bigcap_{i\in I}S_{i}\in\operatorname{\gamma_{b}}(R)$. Furthermore
$S\in\operatorname{\gamma_{b}}(R)$ implies $\bar{S}=X\backslash
S\in\operatorname{\gamma_{b}}(R)$.

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]your argument that you
can restrict to S such that b(S) = S seems off. — We show that
$\gamma_{b}(\alpha_{b}(S))=S$ if $S=b(S)$. (*) Based on this we can prove that
$\gamma_{b}(\alpha_{b}(S^{\prime}))=b(S^{\prime})$ for arbitrary S’.
$b(S^{\prime})\leq\gamma_{b}(\alpha_{b}(S^{\prime}))$ follows from the first
paragraph of the proof. The other inequality holds since
$\gamma_{b}(\alpha_{b}(S^{\prime}))\leq\gamma_{b}(\alpha_{b}(b(S^{\prime})))=b(S^{\prime})$
(using (*)). We want to show that
$\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}))=\operatorname{\mathrm{cl}}^{\lor,\lnot}(\mathcal{S})$.
In fact, it is sufficient to show
$\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}))=\mathcal{S}$
for every set $\mathcal{S}$ with
$\operatorname{\mathrm{cl}}^{\lor,\lnot}(\mathcal{S})=\mathcal{S}$, since then
$\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}^{\prime}))=\operatorname{\mathrm{cl}}^{\lor,\lnot}(\mathcal{S}^{\prime})$
for arbitrary $\mathcal{S}^{\prime}$. In more detail:
$\operatorname{\mathrm{cl}}^{\lor,\lnot}(\mathcal{S}^{\prime})\subseteq\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}^{\prime}))$
follows from the first paragraph of the proof. The other inequality holds
since
$\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}^{\prime}))\subseteq\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\operatorname{\mathrm{cl}}^{\lor,\lnot}(\mathcal{S}^{\prime})))=\operatorname{\mathrm{cl}}^{\lor,\lnot}(\mathcal{S}^{\prime})$.
Here we use that the closure is idempotent.

Let hence $\mathcal{S}=\operatorname{\mathrm{cl}}^{\lor,\lnot}(\mathcal{S})$
and we assume that $\mathcal{S}=\\{S_{i}\subseteq X\mid i\in\mathcal{I}\\}$.
Now let
$T\in\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}))$.
Define the family of indices corresponding to sets of $\mathcal{S}$ contained
in $T$:

$\mathcal{I}^{\prime}=\\{j\in\mathcal{I}\mid S_{j}\subseteq T\\}.$

Then $T=\bigcup_{j\in\mathcal{I}^{\prime}}S_{j}$: The inclusion
$T\supseteq\bigcup_{j\in\mathcal{I}^{\prime}}S_{j}$ holds trivially. To show
$T\subseteq\bigcup_{j\in\mathcal{I}^{\prime}}S_{j}$, consider an element $t\in
T$ and assume that $t\not\in\bigcup_{j\in\mathcal{I}^{\prime}}S_{j}$. For this
$t$, define

$\mathcal{I}^{t}=\\{i\in\mathcal{I}\mid t\in S_{i}\\}.$

It cannot be empty, since $\mathcal{S}$, which is closed under arbitrary
boolean operators, including the empty intersection, always contains $X$
itself. Furthermore, $\mathcal{I}^{\prime}\cap\mathcal{I}^{t}=\emptyset$.
Define the set $\bigcap_{j\in\mathcal{I}^{t}}S_{j}$, which is contained in
$\mathcal{S}$, since $\mathcal{S}$ is closed under intersection, and hence is
of the form $S_{k}$ for some index $k\in\mathcal{I}$. Then we have $t\in
S_{k}\in\mathcal{S}$. This means that $k\not\in\mathcal{I}^{\prime}$ and hence
$S_{k}\not\subseteq T$, which in turn implies the existence of $x\in
S_{k}\setminus T$.

We now show that $(t,x)\in\operatorname{\alpha_{b}}(\mathcal{S})$: consider an
arbitrary $S_{j}\in\mathcal{S}$. If $t\in S_{j}$, then $j\in\mathcal{I}^{t}$
and so $x\in S_{k}\subseteq S_{j}$. On the other hand, if there is $x\in
S_{j}$ but $t\not\in S_{j}$, then $t$ must be in the complement of $S_{j}$,
which is also in $\mathcal{S}$, and will be called $S_{\overline{\jmath}}$ for
an index $\overline{\jmath}\in\mathcal{I}$. It follows that
$\overline{\jmath}\in\mathcal{J}^{t}$ which again implies $x\in S_{k}\subseteq
S_{\overline{\jmath}}$, which is a contradiction to the assumption that $x\in
S_{j}$. This means that for a $t\in T$ and $x\not\in T$,
$(t,x)\in\operatorname{\alpha_{b}}(\mathcal{S})$ and hence
$T\not\in\operatorname{\gamma_{b}}(\operatorname{\alpha_{b}}(\mathcal{S}))$,
which contradicts the assumption.

  * •

Regarding the co-closure,
$R\subseteq\operatorname{\alpha_{b}}(\operatorname{\gamma_{b}}(R))$ follows
directly from the definition. In particular if $(x_{1},x_{2})\in R$, then also
$(x_{1},x_{2})\in\operatorname{\alpha_{b}}(\operatorname{\gamma_{b}}(R))$,
since each set in $\operatorname{\gamma_{b}}(R)$ contains $x_{1}$ iff it
contains $x_{2}$.

For the other inclusion, we prove the contraposition and let
$(x_{1},x_{2})\not\in R$ and let $S=[x_{1}]_{R}$ be the equivalence class of
$x_{1}$, which does not contain $x_{2}$. Clearly
$S\in\operatorname{\gamma_{b}}(R)$ and hence $S$ separates $x_{1},x_{2}$,
which means that
$(x_{1},x_{2})\not\in\operatorname{\alpha_{b}}(\operatorname{\gamma_{b}}(R))$,
as required.

The next step is to show that the logic function is indeed
$\operatorname{c_{b}}$-compatible, so that we can invoke Thm. 3. Not being
compatible basically means that the closure $\operatorname{c_{b}}$ introduces
operators that clash with logical equivalence. For the proof of Prop. 4.1 we
require the fact that the transition system is finitely branching. We first
need the following lemma:

Let $(X,\to)$ be a finitely branching transition system and $(X_{i}\subseteq
X)_{i\in\mathcal{I}}$ be a sequence of sets of states. Then, for $a\in A$, we
have
$\Diamond_{a}\Big{(}\bigcap_{i\in\mathcal{I}}X_{i}\Big{)}=\bigcap_{\begin{subarray}{c}\mathcal{I}_{0}\subseteq\mathcal{I}\\\
\mathcal{I}_{0}\text{
finite}\end{subarray}}\Diamond_{a}\Big{(}\bigcap_{i\in\mathcal{I}_{0}}X_{i}\Big{)}.$

######  Proof 4.2.

We are going to argue that if the transition system is $\kappa$-branching,
then

$\Diamond_{a}\Big{(}\bigcap_{i\in\mathcal{I}}X_{i}\Big{)}=\bigcap_{\begin{subarray}{c}\mathcal{I}_{0}\subseteq\mathcal{I}\\\
|\mathcal{I}_{0}|<\kappa\end{subarray}}\Diamond_{a}\Big{(}\bigcap_{i\in\mathcal{I}_{0}}X_{i}\Big{)}.$

The left-hand side is clearly contained in the right-hand side. For the other
direction assume that $x\in X$ is not an element of the left-hand side. Let
$\\{x_{i}\mid i<\lambda\\}$ with $\lambda<\kappa$ be the set of $a$-successors
of $x$. By assumption for every $j<\lambda$ there is an index
$i_{j}\in\mathcal{I}$ with $x_{j}\notin X_{i_{j}}$. Put
$\mathcal{I}_{0}=\\{i_{j}\mid j<\lambda\\}$, then
$|\mathcal{I}_{0}|\leq\lambda<\kappa$ and
$x\notin\Diamond_{a}\bigcap_{i\in\mathcal{I}_{0}}X_{i}$.

For finitely branching transition systems, $\operatorname{\log_{b}}$ is
$\operatorname{c_{b}}$-compatible.

######  Proof 4.3.

We first show that, given $\mathcal{S}\subseteq\mathcal{P}(X)$ and $a\in A$,
$\Diamond_{a}[\operatorname{c_{b}}(\mathcal{S})]\subseteq\operatorname{c_{b}}(\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\mathcal{S})])$:
let $S\in\Diamond_{a}[\operatorname{c_{b}}(\mathcal{S})]$, i.e.,
$S=\Diamond_{a}T$ where $T\in\operatorname{c_{b}}(\mathcal{S})$, i.e., $T$ can
be written in disjunctive normal form as
$T=\bigcup_{i\in\mathcal{I}}\bigcap_{j\in\mathcal{J}}S_{ij}$, where either
$S_{ij}\in\mathcal{S}$ or $\overline{S_{ij}}\in\mathcal{S}$, i.e., $S_{ij}$
itself or its complement is contained in $\mathcal{S}$.

Then, according to Lem. 4.1, we have that

$S=\Diamond_{a}T=\bigcup_{i\in\mathcal{I}}\Diamond_{a}\bigcap_{j\in\mathcal{J}}S_{ij}=\bigcup_{i\in\mathcal{I}}\bigcap_{\begin{subarray}{c}\mathcal{J}_{0}\subseteq\mathcal{J}\\\
\mathcal{J}_{0}\text{
finite}\end{subarray}}\Diamond_{a}\bigcap_{j\in\mathcal{J}_{0}}S_{ij}$

and hence
$S\in\operatorname{c_{b}}(\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\mathcal{S})])$.

Furthermore, since
$\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}\circ\operatorname{c_{b}}=\operatorname{c_{b}}$:

$\displaystyle\operatorname{\log_{b}}(\operatorname{c_{b}}(\mathcal{S}))$
$\displaystyle=\bigcup_{a\in
A}\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\operatorname{c_{b}}(\mathcal{S}))]=\bigcup_{a\in
A}\Diamond_{a}[\operatorname{c_{b}}(\mathcal{S})]\subseteq\bigcup_{a\in
A}\operatorname{c_{b}}(\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\mathcal{S})])$
$\displaystyle\subseteq\operatorname{c_{b}}(\bigcup_{a\in
A}\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\mathcal{S})])=\operatorname{c_{b}}(\operatorname{\log_{b}}(\mathcal{S}))$

This theorem would straightforwardly generalize to the case where the set of
$a$-successors is finite for each $a$ in the qualitative case, but not
directly in the qualitative case which we treat later. Hence in this paper we
require the transition system to be finitely branching for branching
equivalences/metrics, a requirement that is unnecessary in the trace
case.color=green!20]B: Added this remark, I think it’s safe.

As a result we can derive the behaviour function from the logic function via
the Galois connection. Not surprisingly, this behaviour function is in fact
the well-known function whose greatest fixpoint (remember the contravariance)
is bisimilarity.

The behaviour function $\operatorname{beh_{b}}$ can be characterized as:
$x_{1}\mathrel{\operatorname{beh_{b}}(R)}x_{2}$ iff

$\forall a\in
A,y_{1}\in\delta_{a}(x_{1})\,\exists{y_{2}\in\delta_{a}(x_{2})}\colon
y_{1}\mathrel{R}y_{2}\land\forall a\in
A,y_{2}\in\delta_{a}(x_{2})\,\exists{y_{1}\in\delta_{a}(x_{1})}\colon
y_{1}\mathrel{R}y_{2}.$

In particular this means that
$(x_{1},x_{2})\in\operatorname{\alpha_{b}}(\mu\operatorname{\log_{b}})=\mu\,\operatorname{beh_{b}}$
iff $x_{1},x_{2}$ are bisimilar.

######  Proof 4.4.

Let $R$ be an equivalence on $X$ and observe that

$\displaystyle\operatorname{\alpha_{b}}(\Diamond_{a}[\operatorname{\gamma_{b}}(R)])$
$\displaystyle=\\{(x_{1},x_{2})\mid\forall
S\in\operatorname{\gamma_{b}}(R)\colon(x_{1}\in\Diamond_{a}S\iff
x_{2}\in\Diamond_{a}S)\\}$
$\displaystyle=\\{(x_{1},x_{2})\mid\delta_{a}(x_{1})\cap
S\neq\emptyset\iff\delta_{a}(x_{2})\cap S\neq\emptyset\text{ if $S$ is closed
under $R$}\\}$ $\displaystyle=\\{(x_{1},x_{2})\mid\delta_{a}(x_{1})\cap
E\neq\emptyset\iff\delta_{a}(x_{2})\cap E\neq\emptyset$
$\displaystyle\qquad\qquad\qquad\text{ if $E$ is an equivalence class of
$R$}\\}$ $\displaystyle=\\{(x_{1},x_{2})\mid\forall
y_{1}\in\delta_{a}(x_{1})\leavevmode\nobreak\ \exists
y_{2}\in\delta_{a}(x_{2})\colon(y_{1},y_{2})\in R\mathop{\land}$
$\displaystyle\qquad\qquad\qquad\forall
y_{2}\in\delta_{a}(x_{2})\leavevmode\nobreak\ \exists
y_{1}\in\delta_{a}(x_{1})\colon(y_{1},y_{2})\in R\\}$

The second equality stems from the fact that $x\in\Diamond_{a}(S)$ iff
$\delta_{a}(x)\cap S\neq\emptyset$ and the fact that $\gamma_{b}(R)$ contains
all subsets of $X$ that are closed under $R$, i.e., $x\in S$ and $x\,R\,y$
implies $y\in S$.

Since
$\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}\circ\operatorname{\gamma_{b}}=\operatorname{\gamma_{b}}$,
we have:

$\displaystyle\operatorname{\alpha_{b}}(\operatorname{\log_{b}}(\operatorname{\gamma_{b}}(R)))$
$\displaystyle=\operatorname{\alpha_{b}}(\bigcup_{a\in
A}\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\operatorname{\gamma_{b}}(R))])=\bigcap_{a\in
A}\operatorname{\alpha_{b}}(\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cup,\lnot}_{f}(\operatorname{\gamma_{b}}(R))])$
$\displaystyle=\bigcap_{a\in
A}\operatorname{\alpha_{b}}(\Diamond_{a}[\operatorname{\gamma_{b}}(R)]),$

as defined above.

It is well known that the behaviour function $\operatorname{beh_{b}}$ for
bisimilarity is continuous if the underlying transition system is finitely
branching.

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]About continuity: you
should give more care about what you mean about continuity. What you call
continuity in L221, is Scott-cocontinuity, and later on, you mostly prove
omega-cocontinuity.

###  4.2 Simulation Preorders

In this section we show that not only equivalences, but also behavioural
preorders can be integrated into our framework. Our logical and behavioural
universes are given by the lattices
$\mathbb{L}=(\mathcal{P}(\mathcal{P}(X)),\subseteq)$ and
$\mathbb{B}=(\mathit{Pre}(X),\supseteq)$. The Galois connection is given as
follows:

$\displaystyle\operatorname{\alpha_{s}}(\mathcal{S})$ $\displaystyle=$
$\displaystyle\\{(x_{1},x_{2})\mid\forall S\in\mathcal{S}\colon(x_{1}\in
S\Rightarrow x_{2}\in S)\\}$ $\displaystyle\operatorname{\gamma_{s}}(R)$
$\displaystyle=$ $\displaystyle\\{S\subseteq X\mid\forall s\in S\colon
R[\\{s\\}]\subseteq S\\}.$

In other words,
$\operatorname{\alpha_{s}}(\mathcal{S})[x]=\bigcap\\{S\in\mathcal{S}\mid x\in
S\\}$. As logic function we consider
$\operatorname{\log_{s}}\colon\mathcal{P}(\mathcal{P}(X))\to\mathcal{P}(\mathcal{P}(X))$
with $\operatorname{\log_{s}}(\mathcal{S})=\bigcup_{a\in
A}\Diamond_{a}[\operatorname{\mathrm{cl}}^{\cap}_{f}(\mathcal{S})]$, where
$\operatorname{\mathrm{cl}}^{\cap}_{f}$ closes a family of sets $\mathcal{S}$
under finite intersections. Hence the corresponding logic may use
$\Diamond_{a}$ ($a\in A$), conjunction and true (the empty intersection),
where we again consider only formulas where the outermost operator is a
modality. The logic function $\operatorname{\log_{s}}$ is continuous and
$\mu\,\operatorname{\log_{s}}$ contains all sets that are obtained from
evaluating such formulas.

As desired, the closure induced by the Galois connection closes under union
and intersection, but _not_ under negation, an operation that should be
disallowed in a logic characterizing simulation. The co-closure is instead the
identity on preorders, as in Sct. 4.1.

The closure
$\operatorname{c_{s}}=\operatorname{\gamma_{s}}\circ\operatorname{\alpha_{s}}$
closes a family of subsets of $X$ under arbitrary unions and intersections.
Moreover, the co-closure
$\operatorname{\alpha_{s}}\circ\operatorname{\gamma_{s}}$ is the identity on
$\mathit{Pre}(X)$.

######  Proof 4.5.

It is easy to see that $\mathcal{S}\subseteq\operatorname{c_{s}}(\mathcal{S})$
and that $\operatorname{c_{s}}(\mathcal{S})$ is closed under arbitrary unions
and intersections.

Since $\operatorname{c_{s}}$ is a closure operation, it thus suffices to show
the claim under the assumption that $\mathcal{S}$ is already closed under
unions (see the proof of Prop. 4.1). Assume that
$\mathcal{S}=\\{S_{i}\subseteq X\mid i\in\mathcal{I}\\}$ for some index set
$\mathcal{I}$. Now let
$T\in\operatorname{\gamma_{s}}(\operatorname{\alpha_{s}}(\mathcal{S}))$ and
define

$\mathcal{I}^{\prime}=\\{i\in\mathcal{I}\mid S_{i}\subseteq T\\}.$

Clearly $\bigcup_{i\in\mathcal{I}^{\prime}}S_{i}\subseteq T$. We want to show
that $\bigcup_{i\in\mathcal{I}^{\prime}}S_{i}=T$ and assume by contradiction
that there exists $t\in T$ with
$t\not\in\bigcup_{i\in\mathcal{I}^{\prime}}S_{i}$. We let

$\mathcal{I}^{t}=\\{i\in\mathcal{I}\mid t\in S_{i}\\}.$

Since $\mathcal{S}$ is closed under arbitrary intersections, it always
contains $X$ and hence $\mathcal{I}^{t}$ is non-empty.

Since $\mathcal{S}$ is closed under intersection,
$\bigcap_{j\in\mathcal{I}^{t}}S_{j}$ is also in $\mathcal{S}$ and is of the
form $S_{k}$ for some index $k$. Clearly $t\in S_{k}$. This means that
$k\not\in\mathcal{I}^{\prime}$ and hence $S_{k}\not\subseteq T$, which implies
the existence of $x\in S_{k}\backslash T$.

We can show that $(t,x)\in\operatorname{\alpha_{t}}(\mathcal{S})$: consider an
arbitrary $S_{j}\in\mathcal{S}$. If $t\in S_{j}$, then $j\in\mathcal{I}^{t}$
and so $S_{k}\subseteq S_{j}$, which implies $x\in S_{j}$.

This means that for a $t\in T$ and $x\not\in T$,
$(t,x)\in\operatorname{\alpha_{t}}(\mathcal{S})$ and hence
$T\not\in\operatorname{\gamma_{t}}(\operatorname{\alpha_{t}}(\mathcal{S}))$,
which is a contradiction.

For co-closure let $R\in\mathit{Pre}(X)$. It is clear that
$\operatorname{\alpha_{s}}\circ\operatorname{\gamma_{s}}(R)$ is a preorder
with $R\subseteq\operatorname{\alpha_{s}}\circ\operatorname{\gamma_{s}}(R)$.
Let $Q$ be any other preorder with $R\subseteq Q$, we show that
$\operatorname{\alpha_{s}}\circ\operatorname{\gamma_{s}}(R)\subseteq Q$.
Assume that
$(x,y)\in\operatorname{\alpha_{s}}\circ\operatorname{\gamma_{s}}(R)$, that
means $y\in\bigcap\\{S\in\operatorname{\gamma_{s}}(R)\mid x\in S\\}$. Consider
the set $S:=\\{z\in X\mid(x,z)\in Q\\}$. Then $x\in S$, since $Q$ is reflexive
and we claim that also $S\in\operatorname{\gamma_{s}}(R)$. To this end let
$s\in S$ and $(s,t)\in R$, then also $(s,t)\in Q$ and since $Q$ is transitive
$t\in S$. This shows that $R[\\{s\\}]\subseteq S$, so indeed
$S\in\operatorname{\gamma_{s}}(R)$. It follows that $y\in S$ and therefore
$(x,y)\in Q$.

We show that $\operatorname{\log_{s}}$ is $\operatorname{c_{s}}$-compatible
and subsequently state the main result of this section.

For finitely branching transition systems, $\operatorname{\log_{s}}$ is
$\operatorname{c_{s}}$-compatible.

######  Proof 4.6.

Let $S\in\operatorname{\log_{s}}\circ\operatorname{c_{s}}(\mathcal{S})$, then
$S=\Diamond_{a}(\bigcap_{i\in\mathcal{I}}T_{i})$ with
$T_{i}\in\operatorname{c_{s}}(\mathcal{S})$ for all $i\in\mathcal{I}$. Since
$\operatorname{c_{s}}(\mathcal{S})$ is closed under intersections, we have
$T:=\bigcap_{i\in\mathcal{I}}T_{i}\in\operatorname{c_{s}}(\mathcal{S})$. By
our characterization of the closure, the set $T$ can be written as a union of
intersections of sets from $\mathcal{S}$, say
$T=\bigcup_{j\in\mathcal{J}}\bigcap_{i\in\mathcal{I}_{j}}S_{j,i}$ with
$S_{j,i}\in\mathcal{S}$ for all $j,i$. Then

$S=\Diamond_{a}(T)=\bigcup_{j\in\mathcal{J}}\Diamond_{a}(\bigcap_{i\in\mathcal{I}_{j}}S_{j,i})=\bigcup_{j\in\mathcal{J}}\bigcap_{\begin{subarray}{c}\mathcal{I}_{*}\subseteq\mathcal{I}_{j}\\\
\text{finite}\end{subarray}}\Diamond_{a}(\bigcap_{i\in\mathcal{I}_{*}}S_{j,i})\in\operatorname{c_{s}}\circ\operatorname{\log_{s}}(\mathcal{S})$

The behaviour function $\operatorname{beh_{s}}$ can be characterized as
follows: $x_{1}\mathrel{\operatorname{beh_{s}}(R)}x_{2}$ iff $\forall a\in
A,y_{1}\in\delta_{a}(x_{1})\ \exists{y_{2}\in\delta_{a}(x_{2})}\colon
y_{1}\mathrel{R}y_{2}$, i.e.,
$(x_{1},x_{2})\in\operatorname{\alpha_{s}}(\mu\,\operatorname{\log_{s}})=\mu\,\operatorname{beh_{s}}$
iff $x_{2}$ simulates $x_{1}$. Moreover, for finitely branching transition
systems, $\operatorname{beh_{s}}$ is continuous.

######  Proof 4.7.

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]continuity: 1) precise
which order you consider 2) you do not need to assume $R_{0}=XxX$ and … 3)
"$y_{n}\in\delta(**y**)$ 4) "single" –> "at least one" — Only need that Rn is
descending chain (don’t need $R_{n+1}=beh(R_{n})$

HB: fixed 1 is clarified; for 2,3,4, there is no need to look at the suggested
sequence, since the arguments given holds for any descending sequence. Let
$R\in\mathit{Pre}(X)$ and define $U(R)=\\{(x_{1},x_{2})\mid\forall a\in
A,y_{1}\in\delta_{a}(x_{1})\ \exists{y_{2}\in\delta_{a}(x_{2})}\colon
y_{1}\mathrel{R}y_{2}\\}$.

We want to show that
$U(R)=\operatorname{\alpha_{s}}\circ\operatorname{\log_{s}}\circ\operatorname{\gamma_{s}}(R)$.
First assume that

$(x,y)\in\operatorname{\alpha_{s}}\circ\operatorname{\log_{s}}\circ\operatorname{\gamma_{s}}(R)=\\{(x,y)\in
X\mid\forall T\in(\operatorname{\log_{s}}\circ\operatorname{\gamma_{s}})(R)\
(x\in T\Rightarrow y\in T)\\}$

We show that $(x,y)\in U(R)$. Let $x^{\prime}\in\delta_{a}(x)$ and note that
$S:=R[\\{x^{\prime}\\}]\in\operatorname{\gamma_{s}}(R)$ by the transitivity of
$R$. Now define

$T:=\Diamond_{a}S=\\{z\in X\mid\exists
z^{\prime}\in\delta_{a}(z)\colon(x^{\prime},z^{\prime})\in
R\\}\in\operatorname{\log_{s}}\circ\operatorname{\gamma_{s}}(R)$

Clearly $x\in T$ by the reflexivity of $R$ and therefore $y\in T$. That means,
there is some $y^{\prime}\in\delta_{a}(y)$ with $(x^{\prime},y^{\prime})\in
R$. Hence $(x,y)\in U(R)$.

Conversely assume that we have $(x,y)\in U(R)$. Let
$T\in\operatorname{\log_{s}}\circ\operatorname{\gamma_{s}}(R)$ be arbitrary
and assume that $x\in T$. Choose $S\in\operatorname{\gamma_{s}}(R)$ with
$T=\Diamond_{a}S$ and take $x^{\prime}\in S$ such that
$x^{\prime}\in\delta_{a}(x)$. Then there is some $y^{\prime}\in\delta_{a}(y)$
with $(x^{\prime},y^{\prime})\in R$. Also from $x^{\prime}\in
S\in\operatorname{\gamma_{s}}(R)$ and the definition of
$\operatorname{\gamma_{s}}$, we obtain $R[\\{x^{\prime}\\}]\subseteq S$. It
follows that $y^{\prime}\in R[\\{x^{\prime}\\}]\subseteq S$. Thus $y\in T$.

Lastly, to argue $\operatorname{beh_{s}}$ is continuous, assume the given
transition system is finitely branching. Note that
$\mathbb{B}=(\mathit{Pre}(X),\supseteq)$, so we need to show that for a
descending sequence $(R_{\beta})_{\beta<\kappa}$ in $\mathit{Pre}(X)$ indexed
by ordinals, equality holds between the following sets. By monotonicity we
have

$\operatorname{beh_{s}}(\bigcap_{\beta<\kappa}R_{\beta})\leq\bigcap_{\beta<\kappa}\operatorname{beh_{s}}(R_{\beta})$

For the other direction fix $x\in X$ and let
$y\in\bigcap_{\beta<\kappa}\operatorname{beh_{s}}(R_{\beta})[x]$. Assume that
$x^{\prime}\in\delta_{a}(x)$, then for all $\beta<\kappa$ there is some
$y_{\beta}$, such that $y_{\beta}\in\delta_{a}(y)$ and $y_{\beta}\in
R_{n}[x^{\prime}]$. If the transition system is finitely branching there is a
single $y^{\prime}$ such that $y_{\beta}=y^{\prime}$ for unboundedly many
$\beta<\kappa$ (due to the given descending sequence of preorders). It follows
that $y^{\prime}\in\bigcap_{\beta<\kappa}R_{\beta}[x^{\prime}]$. And therefore
$y\in\operatorname{beh_{s}}(\bigcap_{\beta<\kappa}R_{\beta})[x]$.

###  4.3 Trace Equivalence

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]why you do not stick
to the lattice of congruences instead of the one of the equivalence relation
on P(X)? We now follow the same storyline to set up a Galois connection and
framework for trace equivalence, which will later be enriched to decorated
traces like complete/failure/ready traces [g:linear-branching-time]. Note that
we cannot use the Galois connections from the previous sections, since in
particular $c$-compatibility would fail, due to the fact that negation and
conjunction have to be disallowed in a logic using the diamond modality to
characterize trace equivalence, while instead disjunction is permitted. On the
logic side we use the same lattice
$\mathbb{L}=(\mathcal{P}(\mathcal{P}(X)),\subseteq)$, however, the behaviour
lattice $\mathbb{B}=(\mathit{Eq}(\mathcal{P}(X)),\supseteq)$ is the set of all
equivalences over $\mathcal{P}(X)$ (instead of equivalences over $X$).
Choosing powerset as a semantic domain seems natural due to determinization.
The corresponding Galois connection is given as follows:

$\displaystyle\operatorname{\alpha_{t}}(\mathcal{S})$ $\displaystyle=$
$\displaystyle\\{(X_{1},X_{2})\in\mathcal{P}(X)\times\mathcal{P}(X)\mid\forall
S\in\mathcal{S}\colon(X_{1}\cap S\neq\emptyset\iff X_{2}\cap
S\neq\emptyset)\\}$ $\displaystyle\operatorname{\gamma_{t}}(R)$
$\displaystyle=$ $\displaystyle\\{S\subseteq X\mid\forall(X_{1},X_{2})\in
R\colon(X_{1}\cap S\neq\emptyset\iff X_{2}\cap S\neq\emptyset)\\}.$

Now we consider
$\operatorname{\log_{t}}\colon\mathcal{P}(\mathcal{P}(X))\to\mathcal{P}(\mathcal{P}(X))$
with $\operatorname{\log_{t}}(\mathcal{S})=\bigcup_{a\in
A}\Diamond_{a}[\mathcal{S}]\cup\\{X\\}$, which is again continuous. Then
$\mu\operatorname{\log_{t}}$ represents a set of subsets of $X$ obtained by
evaluating modal logic formulas consisting of the constant $\mathit{true}$
(which evaluates to $\\{X\\}$) and iterated application of the diamond
modalities.

In order to study the Galois connection
$\operatorname{\alpha_{t}}\dashv\operatorname{\gamma_{t}}$ and study its
associated closures, we need the notion of the top element of an equivalence
class.

######  Definition 4.8 (Top element).

Let $R\subseteq\mathcal{P}(X)\times\mathcal{P}(X)$ be a congruence. Given an
equivalence class $E$ of $R$, the top element of this class is the union of
all sets in the equivalence class, i.e., it equals $\bigcup_{S\in E}S$.

We now show that in a congruence each equivalence class $E$ is closed under
union and hence the name top element is well chosen in the sense that it is
contained in $E$.

######  Lemma 4.9.

Consider a congruence relation $R\subseteq\mathcal{P}(X)\times\mathcal{P}(X)$
and a set $\\{X_{i}\subseteq X\mid i\in\mathcal{I}\\}$ where $X_{i}\,RX_{j}$
for all $i,j\in\mathcal{I}$. Then whenever $\mathcal{J}\subseteq\mathcal{I}$,
$\bigcup_{i\in\mathcal{J}}X_{i}$ is in the same equivalence class as the
$X_{i}$, $i\in\mathcal{I}$. In particular this means that the top element of
an equivalence class is also an element of this equivalence class.

######  Proof 4.10.

Let $\mathcal{J}\subseteq\mathcal{I}$ and fix an arbitrary $k\in\mathcal{I}$.
For every $i\in\mathcal{J}$, $X_{k}\,RX_{i}$ and so, since $R$ is a congruence
relation, the union of the left hand sides must be in relation to the union of
the right hand sides:
$\bigcup_{i\in\mathcal{J}}X_{k}\,R\bigcup_{i\in\mathcal{J}}X_{i}$. This is
equivalent to $X_{k}\,R\bigcup_{i\in\mathcal{J}}X_{i}$. Since $X_{k}$ was an
arbitrary element of the equivalence class that is in relation to all other
elements of the class, $\bigcup_{i\in\mathcal{J}}X_{i}$ is also contained in
this class. And since the above holds for $\mathcal{J}=\mathcal{I}$, the top
element of an equivalence class, $\bigcup_{i\in\mathcal{I}}X_{i}$, is also in
the class.

######  Lemma 4.11.

Let $R$ be a congruence relation over a set $X$ and $X_{1},X_{2}\subseteq X$.
Then $X_{1}\,R\,X_{2}$ if and only if for every top element $S$ of an
equivalence class, $X_{1}\subseteq S\Leftrightarrow X_{2}\subseteq S$.

######  Proof 4.12.

First we show that from $X_{1}RX_{2}$, $X_{1}\subseteq S\Leftrightarrow
X_{2}\subseteq S$ follows. Let $X_{1},X_{2}\subseteq X$ be in relation wrt.
$R$, i.e., $X_{1}\,R\,X_{2}$, and let $S$ be any top element. If $S$ and
$X_{1}$ and $X_{2}$ are in the same equivalence class in with regard to $R$,
then $X_{1}\subseteq S$ and $X_{2}\subseteq S$ must both hold.

Now let $S$ be the top element of an equivalence class that $X_{1}$ and thus
also $X_{2}$ do not belong to, and let $T$ be the top element of $X_{1}$ and
$X_{2}$’s equivalence class. Without loss of generality assume that
$X_{1}\subseteq S$ and $X_{2}\not\subseteq S$. This implies $S\cup X_{1}=S$
and thus

$\displaystyle S\leavevmode\nobreak\ $ $\displaystyle R\leavevmode\nobreak\
S\cup X_{1}$ ($S=S\cup S_{1}$) $\displaystyle S\cup X_{1}\leavevmode\nobreak\
$ $\displaystyle R\leavevmode\nobreak\ S\cup T$ ($X_{1}\leavevmode\nobreak\
R\leavevmode\nobreak\ T$) $\displaystyle S\cup T\leavevmode\nobreak\ $
$\displaystyle R\leavevmode\nobreak\ S\cup X_{2}$ ($T\leavevmode\nobreak\
R\leavevmode\nobreak\ X_{2}$)

which means $S\leavevmode\nobreak\ R\leavevmode\nobreak\ S\cup X_{2}$ by
transitivity. Since $X_{2}\not\subseteq S$ and therefore $S\subset S\cup
X_{2}$, this is a contradiction to the assumption that $S$ is the top element
of this equivalence class.

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]direction missing —
fixed Furthermore we want to show that from $X_{1}\subseteq S\Leftrightarrow
X_{2}\subseteq S$ for each top element $S$, we can conclude that
$X_{1}\,R\,X_{2}$. To this end, let $S_{1},S_{2}$ be the top elements of the
equivalence classes of $X_{1},X_{2}$, respectively and assume that
$X_{1}\subseteq S\Leftrightarrow X_{2}\subseteq S$ holds for each top element
$S$. Due to the definition of top elements, we have $X_{i}\subseteq S_{i}$,
and from the assumption it follows $X_{j}\subseteq S_{i}$, for
$\\{i,j\\}=\\{1,2\\}$. Then $X_{1}\,R\,S_{1}=(S_{1}\cup X_{2})\,R\,(S_{1}\cup
S_{2})\,R\,(X_{1}\cup S_{2})=S_{2}\,R\,X_{2}$.

The closure
$\operatorname{c_{t}}=\operatorname{\gamma_{t}}\circ\operatorname{\alpha_{t}}$
closes a set of subsets of $X$ under arbitrary unions, while the co-closure
$\operatorname{\alpha_{t}}\circ\operatorname{\gamma_{t}}$ maps an equivalence
on $\mathcal{P}(X)$ to its congruence closure.

######  Proof 4.13.

  * •

First, we show that the closure of $\mathcal{S}$ under union is a subset of
$\operatorname{\gamma_{t}}(\operatorname{\alpha_{t}}(\mathcal{S}))$. Let
$\mathcal{S}=\\{S_{i}\subseteq X\mid i\in\mathcal{I}\\}$ for some index set
$\mathcal{I}$, and consider $\bigcup_{i\in\mathcal{J}}S_{i}$ for
$\mathcal{J}\subseteq\mathcal{I}$. For
$(X_{1},X_{2})\in\operatorname{\alpha_{t}}(\mathcal{S})$, for all
$S\in\mathcal{S}$, it holds $X_{1}\cap S\not=\emptyset\Leftrightarrow
X_{2}\cap S\not=\emptyset$. Let $\\{k,l\\}=\\{1,2\\}$, then

$\displaystyle
X_{k}\cap\bigcup_{i\in\mathcal{J}}S_{i}=\bigcup_{i\in\mathcal{J}}(X_{k}\cap
S_{i})\not=\emptyset\Leftrightarrow\exists i^{*}\in\mathcal{J}:X_{k}\cap
S_{i^{*}}\not=\emptyset$ $\displaystyle\Rightarrow X_{l}\cap
S_{i^{*}}\not=\emptyset\Rightarrow\bigcup_{i\in\mathcal{J}}(X_{l}\cap
S_{i})\not=\emptyset\Leftrightarrow
X_{l}\cap\bigcup_{i\in\mathcal{J}}S_{i}\not=\emptyset$

This means that
$X_{1}\cap\bigcup_{i\in\mathcal{J}}S_{i}\not=\emptyset\Leftrightarrow
X_{2}\cap\bigcup_{i\in\mathcal{J}}S_{i}\not=\emptyset$. So for all
$\mathcal{J}\subseteq\mathcal{I}$, for all elements
$\bigcup_{i\in\mathcal{J}}S_{i}$ of the closure under union of $\mathcal{S}$,
$\bigcup_{i\in\mathcal{J}}S_{i}\in\operatorname{\gamma_{t}}(\operatorname{\alpha_{t}}(\mathcal{S}))$.

It is now sufficient to show that given $\mathcal{S}=\\{S_{i}\subseteq X\mid
i\in\mathcal{I}\\}$ as above,
$\operatorname{\gamma_{t}}(\operatorname{\alpha_{t}}(\mathcal{S}))=\mathcal{S}$,
whenever $\mathcal{S}$ is already closed under union (see proof of Prop. 4.1).
Let $T\in\operatorname{\gamma_{t}}(\operatorname{\alpha_{t}}(\mathcal{S}))$
and define $\mathcal{I}^{\prime}=\\{i\in\mathcal{I}\mid S_{i}\subseteq T\\}$
and show that $\bigcup_{j\in\mathcal{I}^{\prime}}S_{j}=T$, which implies
$T\in\mathcal{S}$.

The inclusion $\bigcup_{j\in\mathcal{I}^{\prime}}S_{j}\subseteq T$ holds by
definition. For the reverse, take an element $t\in T$ and assume by
contradiction that $t\not\in\bigcup_{j\in\mathcal{I}^{\prime}}S_{j}$. Define
the index set $\mathcal{I}^{t}=\\{i\in\mathcal{I}\mid t\in S_{i}\\}$. If this
set were empty, there would be no index $i\in\mathcal{I}$ such that $t\in
S_{i}$, which means $\\{t\\}$ would equivalent to $\emptyset$ wrt. the
relation $\operatorname{\alpha_{t}}(\mathcal{S})$. Because
$T\cap\\{t\\}\neq\emptyset$ but $T\cap\emptyset=\emptyset$ it would follow
that
$T\not\in\operatorname{\gamma_{t}}(\operatorname{\alpha_{t}}(\mathcal{S}))$, a
contradiction. Hence $\mathcal{I}^{t}\not=\emptyset$.

Since there is no index $j\in\mathcal{I}^{t}$ such that $S_{j}\subseteq T$,
define a mapping $p:\mathcal{I}^{t}\rightarrow X$ where $p(j)\in S_{j}$ and
$p(j)\not\in T$. Then take $X_{1}:=\\{p(j)\mid j\in\mathcal{I}^{t}\\}$ and
$X_{2}:=X_{1}\cup\\{t\\}$. Note that $X_{1}\subseteq X_{2}$, and so for every
$i\in\mathcal{I}$, $S_{i}\cap X_{1}\not=\emptyset$ implies $S_{i}\cap
X_{2}\not=\emptyset$ and $S_{i}\cap X_{2}\not=\emptyset$ implies $(S_{i}\cap
X_{1})\cup(S_{i}\cap\\{t\\})\not=\emptyset$. The latter could either be the
case due to $S_{i}\cap X_{1}\not=\emptyset$, or else it holds that
$S_{i}\cap\\{t\\}\not=\emptyset$, which implies that $t\in S_{i}$ for some
$i\in\mathcal{I}^{t}$. This in turn means that $p(i)\in S_{i}$ and by
definition $p(i)\in X_{1}$, so again we get $S_{i}\cap X_{1}\not=\emptyset$.
In either case it holds $S_{i}\cap X_{1}\not=\emptyset\Leftrightarrow
S_{i}\cap X_{2}\not=\emptyset$. But $T\cap X_{1}=\emptyset$ and $T\cap
X_{2}=\\{t\\}$, which is a contradiction to
$T\in\operatorname{\gamma_{t}}(\operatorname{\alpha_{t}}(\mathcal{S}))$.

  * •

We show that the co-closure of a relation is a congruence relation. For a
relation $R$, $\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$ is a
congruence. Reflexivity, symmetry and transitivity are easily verifiable. For
$\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$ to be a congruence
relation, for any
$(Y_{1,1},Y_{1,2}),\dots,(Y_{n,1},Y_{n,2})\in\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$
the componentwise union must also be contained in the co-closure: it must hold
$(\bigcup_{i\in\\{1,\dots,n\\}}Y_{i,1},\bigcup_{i\in\\{1,\dots,n\\}}Y_{i,2})\in\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$.
So let
$(Y_{1,1},Y_{1,2}),\dots,(Y_{n,1},Y_{n,2})\in\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$.
Then according to the definition it must hold that $(Y_{i,1}\cap
S\not=\emptyset)\Leftrightarrow(Y_{i,2}\cap S\not=\emptyset)$ for all
$i=1,\dots,n$. Thus

$\displaystyle\left(\bigcup_{i\in\\{1,\dots,n\\}}Y_{i,1}\right)\cap
S=\bigcup_{i\in\\{1,\dots,n\\}}(Y_{i,1}\cap S)\not=\emptyset$
$\displaystyle\Leftrightarrow\exists i^{*}\in\\{1,\dots,n\\}\colon
Y_{i^{*},1}\cap S\not=\emptyset\ \Leftrightarrow\exists
i^{*}\in\\{1,\dots,n\\}\colon Y_{i^{*},2}\cap S\not=\emptyset$
$\displaystyle\Leftrightarrow\bigcup_{i\in\\{1,\dots,n\\}}(Y_{i,2}\cap
S)=\left(\bigcup_{i\in\\{1,\dots,n\\}}Y_{i,2}\right)\cap S\not=\emptyset$

and so
$(\bigcup_{i\in\\{1,\dots,n\\}}Y_{i,1},\bigcup_{i\in\\{1,\dots,n\\}}Y_{i,2})\in\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$.

If $R$ is a congruence relation, we show that
$\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))=R$. For some
$(X_{1},X_{2})\in R$, applying $\operatorname{\gamma_{t}}$ to $R$ yields the
set $\mathcal{S}$ where all elements $S$ satisfy $X_{1}\cap
S\not=\emptyset\Leftrightarrow X_{2}\,\cap\not=\emptyset$. This in turn means
that $(X_{1},X_{2})$ will be an element of
$\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$. As $(X_{1},X_{2})$
was chosen arbitrarily, it follows
$R\subseteq\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$.

For the other inclusion, let
$(X_{1},X_{2})\in\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$ and
let $S_{i}$ be the top element of the $R$-equivalence class containing
$X_{i}$, for $i\in\\{1,2\\}$. The set $\operatorname{\gamma_{t}}(R)$ can be
rewritten to

$\\{S\subseteq X\mid\forall(X_{1},X_{2})\in R\mid X_{1}\cap
S=\emptyset\Leftrightarrow X_{2}\cap S=\emptyset\\},$

which in turn is equivalent to the set

$\\{S\subseteq X\mid\forall(X_{1},X_{2})\in R\mid
X_{1}\subseteq\overline{S}\Leftrightarrow X_{2}\subseteq\overline{S}\\}.$

This condition can only hold if $\overline{S}$ is a top element of an
equivalence class of $R$, and so the set $\operatorname{\gamma_{t}}(R)$
contains exactly those sets $S$ where $\overline{S}$ is a top element of $R$.
Hence, $\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$ is the set

$\displaystyle\\{(Y_{1},Y_{2})\mid\forall\text{ top elements }T\text{ of
}R\mid Y_{1}\cap\overline{T}=\emptyset\Leftrightarrow
Y_{2}\cap\overline{T}=\emptyset\\}$
$\displaystyle=\\{(Y_{1},Y_{2})\mid\forall\text{ top elements }T\text{ of
}R\mid Y_{1}\subseteq T\Leftrightarrow Y_{2}\subseteq T\\}$

By Lem. 4.11, $X_{1}\,R\,X_{2}$ and thus follows
$\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))\subseteq R$.

Let $R$ be an equivalence on $\mathcal{P}(X)$ and remember that
$\mathit{cong}(R)$ is the congruence closure of $R$. As shown above,
$R\subseteq\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$. This (1)
together with $\operatorname{\alpha_{t}}$ and $\operatorname{\gamma_{t}}$
being monotone functions (2) where
$\operatorname{\alpha_{t}}\circ\operatorname{\gamma_{t}}$ preserves
congruences (3) implies

$R\overset{(1)}{\subseteq}\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))\overset{(2)}{\subseteq}\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(\mathit{cong}(R)))\overset{(3)}{=}\mathit{cong}(R).$

Since $\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$ is a
congruence and contains $R$, and $\mathit{cong}(R)$ is the smallest such
congruence, it follows that
$\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))=\mathit{cong}(R)$.

As indicated in the general “recipe”, the next step is to show that the logic
function is compatible with the closure. Intuitively this is true since
diamond distributes over union.

The logic function $\operatorname{\log_{t}}$ is
$\operatorname{c_{t}}$-compatible.

######  Proof 4.14.

Let $\mathcal{S}=\\{S_{i}\subseteq X\mid i\in\mathcal{I}\\}$. Using the fact
that $\operatorname{c_{t}}$ closes a set of sets under arbitrary unions and
diamond commutes with union, we obtain:

$\displaystyle\operatorname{\log_{t}}(\operatorname{c_{t}}(\mathcal{S}))$
$\displaystyle=\bigcup_{a\in
A}\Diamond_{a}[\operatorname{c_{t}}(\mathcal{S})]\cup\\{X\\}$
$\displaystyle=\bigcup_{a\in
A}\Diamond_{a}[\\{\bigcup_{i\in\mathcal{J}}S_{i}\mid\mathcal{J}\subseteq\mathcal{I}\\}]\cup\\{X\\}$
$\displaystyle=\\{\Diamond_{a}(\bigcup_{i\in\mathcal{J}}S_{i})\mid\mathcal{J}\subseteq\mathcal{I},a\in
A\\}\cup\\{X\\}$
$\displaystyle=\\{\bigcup_{i\in\mathcal{J}}\Diamond_{a}(S_{i})\mid\mathcal{J}\subseteq\mathcal{I},a\in
A\\}\cup\\{X\\}$
$\displaystyle\subseteq\operatorname{c_{t}}(\\{\Diamond_{a}(S_{i})\mid
S_{i}\in\mathcal{S},a\in A\\}\cup\\{X\\})$
$\displaystyle=\operatorname{c_{t}}(\operatorname{\log_{t}}(\mathcal{S})).$

Finally the induced behaviour function is the one expected for trace
equivalence: the bisimilarity function on the determinized transition system.
This is true only for congruences, since $\operatorname{beh_{t}}$
automatically returns a congruence. However, since in the Kleene iteration we
obtain only congruences, it is easy to see that $\mu\operatorname{beh_{t}}$ is
indeed trace equivalence (cf. Thm. 4.3).

On a congruence relation $R\subseteq\mathcal{P}(X)\times\mathcal{P}(X)$, we
have $X_{1}\mathrel{\operatorname{beh_{t}}(R)}X_{2}$ iff $(X_{1}=\emptyset\iff
X_{2}=\emptyset)\land\forall a\in
A\colon\delta_{a}[X_{1}]\mathrel{R}\delta_{a}[X_{2}]$. The restriction of
$\operatorname{beh_{t}}$ to congruences is continuous, independent of the
branching type of the transition system.

######  Proof 4.15.

Let $R$ be a congruence relation and define

$T(R)=\\{(X_{1},X_{2})\in\mathcal{P}(X)\times\mathcal{P}(X)\mid(X_{1}=\emptyset\Leftrightarrow
X_{2}=\emptyset)\land\forall a\in
Y(\delta_{a}[X_{1}]\,R\,\delta_{a}[X_{2}])\\}.$

We will show that $\operatorname{beh_{t}}$ coincides with $T$ on each
congruence $R$. Combining the definitions of the functions
$\operatorname{\alpha_{t}}$, $\operatorname{\log_{t}}$ and
$\operatorname{\gamma_{t}}$, their concatenation can be characterized as

$\displaystyle\operatorname{\alpha_{t}}\circ\operatorname{\log_{t}}\circ\,\operatorname{\gamma_{t}}(R)$
$\displaystyle=\\{(X_{1},X_{2})\mid\forall a\in
A,S\in\operatorname{\gamma_{t}}(R):X_{1}\cap\Diamond_{a}S\not=\emptyset\Leftrightarrow
X_{2}\cap\Diamond_{a}S\not=\emptyset\mathop{\land}$
$\displaystyle\qquad\qquad\qquad X_{1}=\emptyset\iff X_{2}=\emptyset\\}.$

The condition $X_{1}=\emptyset\iff X_{2}=\emptyset$ holds since
$X\in\operatorname{\log_{t}}(\operatorname{\gamma_{t}}(R))$.

We now show
$T(R)\subseteq\operatorname{\alpha_{t}}\circ\operatorname{\log_{t}}\circ\,\operatorname{\gamma_{t}}(R)$
for a congruence $R$. Let $(X_{1},X_{2})\in T(R)$ (hence $X_{1}=\emptyset\iff
X_{2}=\emptyset$) and thus $(\delta_{a}[X_{1}],\delta_{a}[X_{2}])\in R$. For
an

$S\in\operatorname{\gamma_{t}}(R)=\\{S\mid\forall(Y_{1},Y_{2})\in R:S\cap
Y_{1}\not=\emptyset\Leftrightarrow S\cap Y_{2}\not=\emptyset\\},$

we have $S\cap\delta_{a}[X_{1}]\not=\emptyset$ iff
$S\cap\delta_{a}[X_{2}]\not=\emptyset$, which means
$X_{1}\cap\Diamond_{a}S\not=\emptyset$ iff
$X_{2}\cap\Diamond_{a}S\not=\emptyset$, implying
$(X_{1},X_{2})\in\operatorname{\alpha_{t}}\circ\operatorname{\log_{t}}\circ\,\operatorname{\gamma_{t}}$.

It remains to be shown, that
$\operatorname{\alpha_{t}}\circ\operatorname{\log_{t}}\circ\,\operatorname{\gamma_{t}}(R)\subseteq
T(R)$. To this end, assume
$(X_{1},X_{2})\in\operatorname{\alpha_{t}}\circ\operatorname{\log_{t}}\circ\,\operatorname{\gamma_{t}}(R)$.
According to the definition, for all $S\in\operatorname{\gamma_{t}}(R)$,
$X_{1}\cap\Diamond_{a}S\not=\emptyset\Leftrightarrow
X_{2}\cap\Diamond_{a}S\not=\emptyset$ and considering the $a$-successors of
$X_{1}$ and $X_{2}$ instead of the $a$-predecessors of the $S$, this yields
$\delta_{a}[X_{1}]\cap S\not=\emptyset\Leftrightarrow\delta_{a}[X_{2}]\cap
S\not=\emptyset$. This in turn implies
$(\delta_{a}[X_{1}],\delta_{a}[X_{2}])\in\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))$
for all $a\in A$. We know from Proposition 4.3 that
$\operatorname{\alpha_{t}}(\operatorname{\gamma_{t}}(R))=R$, since $R$ is a
congruence and the co-closure
$\operatorname{\alpha_{t}}\circ\operatorname{\gamma_{t}}$ preserves congruence
relations. In particular, this means that
$(\delta_{a}[X_{1}],\delta_{a}[X_{2}])\in R$ for all $a\in A$. In addition
$X_{1}=\emptyset\iff X_{2}\in\emptyset$ and hence $(X_{1},X_{2})\in T(R)$,
which concludes the proof.

The continuity is obvious from this characterization.

Since on congruences $\operatorname{beh_{t}}$ agrees with the usual fixpoint
function for trace equivalence and $\operatorname{beh_{t}}$ preserves
congruences, the corresponding iteration algorithm agrees with the usual one,
where one compute bisimilarity on the determinized transition system.

#### Decorated Trace Equivalence

We now consider completed trace/ready/failure/possible futures equivalence
from the van Glabbeek spectrum [g:linear-branching-time] and explain how these
equivalences can be obtained by adding fixed predicates. We parameterize over
a family $\mathcal{S}$ of predicates over the state space (see Fig. 1). We
first characterize the fixpoint of the behaviour function, modified with an
extra preorder as follows. The advantage of this characterisation is that it
allows to state various decorated trace equivalences in terms of transfer
properties attributed to bisimulation relations.

Let $R_{0}\in\operatorname{Pre}(X)$ and consider the map
$\operatorname{beh}_{R_{0}}=\operatorname{beh_{t}}\cap({R}_{0})_{H}$. Then
$\mu\,\operatorname{beh}_{R_{0}}$ is equal to the set $\Omega(R_{0})$ of those
pairs $(X_{1},X_{2})$, such that if $x\in X_{1}$ admits a trace
$x_{1}\xrightarrow{\sigma}x^{\prime}_{1}$, then there exists $x_{2}\in X_{2}$,
such that $x_{2}\xrightarrow{\sigma}x^{\prime}_{2}$ and
$x^{\prime}_{1}\mathrel{R_{0}}x^{\prime}_{2}$ (and vice versa).

######  Proof 4.16.

We set $\Omega=\Omega(R_{0})$ and first show that
$\Omega\subseteq\mu\,\operatorname{beh}$. By the Knaster-Tarski Theorem it
suffices to show that $\Omega\subseteq\operatorname{beh}_{R_{0}}(\Omega)$,
since every post-fixpoint is below the greatest fixpoint. Let
$(X_{1},X_{2})\in\Omega$, then the following properties hold:

  1. 1.

Clearly $X_{1}=\emptyset\iff X_{2}=\emptyset$.

  2. 2.

We have $(\delta_{a}[X_{1}],\delta_{a}[X_{2}])\in\Omega$. For if $\sigma$ is a
trace of some state $x^{\prime}_{1}\in\delta_{a}[X_{1}]$ and
$x^{\prime}_{1}\xrightarrow{\sigma}x^{\prime\prime}_{2}$, then
$x\xrightarrow{a}x^{\prime}_{1}\xrightarrow{\sigma}x^{\prime\prime}_{1}$ for
some state in $x_{1}\in X_{1}$ and consequently there is $x_{2}\in X_{2}$,
such that
$x_{2}\xrightarrow{a}x_{2}^{\prime}\xrightarrow{\sigma}x_{2}^{\prime\prime}$
with $x^{\prime\prime}_{1}\mathrel{R_{0}}x_{2}^{\prime\prime}$. In particular
$x^{\prime}_{2}\in\delta_{a}[X_{2}]$. The same holds vice versa.

  3. 3.

By considering the empty trace in the definition of $\Omega$, we obtain
$(X_{1},X_{2})\in(R_{0})_{H}$.

Since $\Omega$ is clearly a congruence, these three properties imply that
$(X_{1},X_{2})\in\operatorname{beh}_{R_{0}}(\Omega)$.

For the other direction we assume that $\Theta$ is a fixpoint of
$\operatorname{beh}_{R_{0}}$ and a congruence, and show that
$\Theta\subseteq\Omega$. Fix a pair $(X_{1},X_{2})\in\Theta$ and assume that
$x_{0}\in X_{1}$ admits a trace
$x_{0}\xrightarrow{a_{0}}x_{1}\xrightarrow{a_{1}}\dots\xrightarrow{a_{\ell-1}}x_{\ell}$.
Since $\Theta$ is a fixpoint and a congruence, we get

$(\hat{\delta}_{a_{0}\dots a_{\ell-1}}[X_{1}],\hat{\delta}_{a_{0}\dots
a_{\ell-1}}[X_{2}])\in(\operatorname{beh}_{R_{0}})^{\ell}(\Theta)=\Theta$

Using the fixpoint property one more time, we get

$\hat{\delta}_{a_{0}\dots
a_{\ell-1}}[X_{1}]\mathrel{(R_{0})_{H}}\hat{\delta}_{a_{0}\dots
a_{\ell-1}}[X_{2}]$

In particular, there is some $y_{\ell}\in\hat{\delta}_{a_{0}\dots
a_{\ell-1}}[X_{2}]$ with $x_{\ell}\mathrel{R_{0}}y_{\ell}$. The other
direction is analogous. We therefore can conclude that
$(X_{1},X_{2})\in\Omega$. Since congruences are preserved under
$\operatorname{beh}_{R_{0}}$ and under intersections, we know that
$\mu\,\operatorname{beh}_{R_{0}}$ is a congruence, hence
$\mu\,\operatorname{beh}_{R_{0}}\subseteq\Omega$.

In order to infer that $\mu\operatorname{beh_{t}}$ characterizes trace
equivalence simply set $R_{0}=X\times X$.

The idea is to fix a set $\mathcal{S}$ of predicates and add these to our
trace logic, using $R_{0}=\operatorname{\alpha_{s}}(\mathcal{S})$ as the
preorder required in the above theorem. In order to ensure that logical and
behavioural equivalence coincide, we require that $\mathcal{S}$ has certain
“good” properties.

Let $\mathcal{S}\subseteq\mathcal{P}(X)$ such that $\forall x\exists
S\in\mathcal{S}\colon(x\in S\land\forall y\colon
x\,\operatorname{\alpha_{s}}(\mathcal{S})\,y\iff y\in S)$. Then,
$\operatorname{\alpha_{t}}(\mathcal{S})$ coincides with the relation lifting
$(\operatorname{\alpha_{s}}(\mathcal{S}))_{H}$.

######  Proof 4.17.

$\subseteq$ Let $X_{1}\mathrel{\operatorname{\alpha_{t}}(\mathcal{S})}X_{2}$
and let $x_{1}\in X_{1}$. By the assumption we find some $S\in\mathcal{S}$
such that $x_{1}\in S$ and $\forall y\colon
x_{1}\,\operatorname{\alpha_{s}}(\mathcal{S})\,y\iff y\in S$. Clearly,
$x_{1}\in X_{1}\cap S$ and we find that $X_{2}\cap S\neq\emptyset$. I.e.,
there is some $x_{2}\in X_{2}\cap S$ and by the assumption we have
$x_{1}\operatorname{\alpha_{s}}(\mathcal{S})\,x_{2}$ since $x_{2}\in S$.

$\supseteq$ Let
$X_{1}\mathrel{(\operatorname{\alpha_{s}}(\mathcal{S}))_{H}}X_{2}$ and let
$S\in\mathcal{S}$. Suppose $x_{1}\in X_{1}\cap S\neq\emptyset$. Then there is
some $x_{2}\in X_{2}$ such that
$x_{1}\mathrel{\operatorname{\alpha_{s}}(\mathcal{S})}x_{2}$. Clearly, by the
assumption we get $x_{2}\in S$.

The condition of Lem. 4.3 is for instance satisfied if $\mathcal{S}$ is closed
under intersections. We obtain the following characterization of decorated
trace logics.

Assume that $\mathcal{S}$ satisfies the requirements of Lem. 4.3 and let
$R_{0}=\operatorname{\alpha_{s}}(\mathcal{S})$. Consider the logic function
$\operatorname{log}_{\mathcal{S}}=\operatorname{log}_{t}\cup\mathcal{S}$. Then
$\operatorname{\alpha_{t}}(\mu\,\operatorname{log}_{\mathcal{S}})=\Omega(R_{0})=\mu\,\operatorname{beh}_{R_{0}}$.

Hence if we instantiate $\mathcal{S}$ as in Figure 1, where

$T_{X}=\delta^{-1}(\emptyset)\qquad\operatorname{\mathrm{Ref}}(B)=\\{x\mid\operatorname{lab}(\delta(x))\cap
B=\emptyset\\}\quad\operatorname{\mathrm{Ready}}(B)=\\{x\mid\operatorname{lab}(\delta(x))=B\\},$

we obtain complete trace/failure/readiness equivalences as the least fixpoint
of $\operatorname{beh}_{R_{0}}$. In all these cases $\mathcal{S}\cup\\{X\\}$
satisfies the requirements of Lem. 4.3.

######  Proof 4.18.

Let
$\operatorname{beh}_{\mathcal{S}}=\operatorname{\alpha_{t}}\circ\operatorname{log}_{\mathcal{S}}\circ\operatorname{\gamma_{t}}$
be the corresponding behaviour function, then

$\operatorname{beh}_{\mathcal{S}}=\operatorname{beh}_{t}\cap\alpha_{t}(\mathcal{S})=\operatorname{beh}_{t}\cap(R_{0})_{H}$

and the from the above theorem we get that
$\alpha(\mu\,\operatorname{log}_{\mathcal{S}})=\mu\,\operatorname{beh}_{\mathcal{S}}=\Omega(R_{0})$.

The fact that the various instantiations results in complete
trace/failure/readiness equivalences is a direct consequence of Thm. 4.3.

We can check that all sets $\mathcal{S}\cup\\{X\\}$ satisfy the requirements
of Lem. 4.3. (Note that $X$ is already provided by the logic function
$\operatorname{\log_{t}}$.)

  * •

completed trace: given $x\in X$ choose $X$ if
$\operatorname{lab}(\delta(x))\neq\emptyset$, $T_{X}$ otherwise.

  * •

failure: given $x\in X$ choose
$\operatorname{\mathrm{Ref}}(A\backslash\operatorname{lab}(\delta(x)))$.

  * •

ready: given $x\in X$ choose
$\operatorname{\mathrm{Ready}}(\operatorname{lab}(\delta(x)))$.

  * •

possible future: we enforce the condition by closing under arbitrary
intersections.

$\mathcal{S}$ | $x\mathrel{R_{0}}y$ | Behavioural equivalence
---|---|---
$\\{T_{X}\\}$ | $\operatorname{lab}(\delta(x))=\emptyset\implies\operatorname{lab}(\delta(y))=\emptyset$ | completed trace
$\\{\operatorname{\mathrm{Ref}}(B)\mid B\subseteq A\\}$ | $\operatorname{lab}(\delta(y))\subseteq\operatorname{lab}(\delta(x))$ | failure
$\\{\operatorname{\mathrm{Ready}}(B)\mid B\subseteq A\\}$ | $\operatorname{lab}(\delta(x))=\operatorname{lab}(\delta(y))$ | ready
$\operatorname{\mathrm{cl}}^{\cap}(\mu\,\operatorname{log}_{t}\cup\neg(\mu\,\operatorname{\log_{t}}))$ | $\operatorname{Tr}(x)=\operatorname{Tr}(y)$ | possible futures
Figure 1: Behavioural equivalences obtained from a logic of the form
$\operatorname{log}_{0}(\mathcal{F})=\operatorname{\log_{t}}(\mathcal{F})\cup\mathcal{S}$,
respectively a behaviour function of the form
$\operatorname{beh}_{0}=\operatorname{beh}_{t}\cap(R_{0})_{H}$.

Note that $\\{X\\}$ is already generated by
$\operatorname{\log_{t}}$.color=green!20]B: added this remark, since otherwise
$\\{X\\}$ comes a bit out of nowhere. The predicate $T_{X}$ semantically
corresponds to the predicate called $0$ in [g:linear-branching-time], which is
satisfied by each state which has no out-going transitions. Similarly, the
predicates $\operatorname{\mathrm{Ref}}(B)$ (resp.
$\operatorname{\mathrm{Ready}}(B)$) corresponds to the predicates $\tilde{B}$
(resp. $B$) in [g:linear-branching-time], which is satisfied by those states
that refuse (resp. enable) all the actions from $B$.

##  5 Quantitative Case

After discussing the classical case of behavioural equivalences, we will now
follow an analogous path to obtain behavioural distances in a quantitative
setting. We will begin by first considering the bisimulation pseudo-metric,
then directed simulation pseudo-metric, and lastly conclude with the directed
(decorated) trace pseudo-metric, from which one can obtain the undirected
version by symmetrization. In each case, we will again start out by defining
the logics and derive the fixpoint equations for the corresponding behaviour
function.

In addition, our decorated trace distance can be seen as the quantitative
generalization of a decorated trace preorder, which when instantiated
corresponds to (complete) trace/failure/ready inclusions. So, in this sense,
our decorated trace distance is going to be parametric. Lastly, though the
concrete trace distance is studied elsewhere (cf. [afs:linear-branching-
metrics, fl:quantitative-spectrum-journal]), we are not aware of this fixpoint
characterization of (decorated) trace distance in the literature. There is a
recursive characterization in [fl:quantitative-spectrum-journal], but based on
an auxiliary lattice that serves as memory.color=green!20]B: Modified the
claim that we are the first to do fixpoint equations for trace metrics.

In the rest of this section we fix a metric transition system $(X,\to,d_{A})$
over $A$.

###  5.1 Bisimulation Pseudo-metrics

Recall the adjunction from Sct. 4.1, which we will enrich by replacing a
predicate $S\subseteq X$ with a function $f\colon X\to[0,1]$, while pseudo-
metrics now play the role of equivalences. In particular, our logical and
behavioural universes are given by the lattices
$\mathbb{L}=(\mathcal{P}([0,1]^{X}),\subseteq)$ and
$\mathbb{B}=(\mathit{PMet}(X),\leq)$, respectively. Moreover, the Galois
connection is given as follows:

$\displaystyle\operatorname{\alpha_{B}}(\mathcal{F})(x_{1},x_{2})=\bigvee_{f\in\mathcal{F}}|f(x_{1})-f(x_{2})|$
(for $\mathcal{F}\subseteq[0,1]^{X}$)
$\displaystyle\operatorname{\gamma_{B}}(d)=\
\\{f\in[0,1]^{X}\mid\forall{x_{1},x_{2}\in X}:|f(x_{1})-f(x_{2})|\leq
d(x_{1},x_{2})\\}$ $\displaystyle\text{(for $d\in\mathit{PMet}(X)$)}.$

I.e., $\operatorname{\alpha_{B}}(\mathcal{F})$ is the least metric on $X$ such
that all functions in $\mathcal{F}$ are non-expansive wrt. the Euclidean
metric on $[0,1]$, while $\operatorname{\gamma_{B}}$ returns all the non-
expansive functions wrt. $d\in\mathit{PMet}(X)$.

Next we introduce a family of modalities $(\operatorname{\bigcirc}_{a}f)_{a\in
A}$ in the style of [afs:linear-branching-metrics] is:

$\operatorname{\bigcirc}_{a}f(x)=\bigvee\\{\overline{D_{a}}(b)\land
f(x^{\prime})\mid x\xrightarrow{b}x^{\prime}\\},\quad\text{where
$D_{a}(b)=d_{A}(b,a)$ and $\overline{D_{a}}(b)=1-D_{a}(b)$}.$

So we consider the (continuous) logic function
$\operatorname{\log_{B}}\colon\mathcal{P}([0,1]^{X})\to\mathcal{P}([0,1]^{X})$
that maps a set $\mathcal{F}\subseteq[0,1]^{X}$ of functions to the set
$\bigcup_{a\in
A}\operatorname{\bigcirc}_{a}[\operatorname{\mathrm{cl}}^{\land,\lnot,\mathrm{sh}}_{f}(\mathcal{F})]$,
where $\operatorname{\mathrm{cl}}^{\land,\lnot,\mathrm{sh}}_{f}$ closes
$\mathcal{F}$ under finite meets, complements ($f\mapsto 1-f$), and constant
shifts (and hence also under finite joins), which are all non-expansive
operators (cf. Prop. 5.3). It should be noted that
$\operatorname{\bigcirc}_{a}$ is a quantitative generalization of the
qualitative diamond modality in the following sense.

If $d_{A}$ is a discrete metric then $\operatorname{\bigcirc}_{a}f(x)=1\iff
x\in\Diamond_{a}f^{-1}(\\{1\\})$.

######  Proof 5.1.

Let $f\in[0,1]^{X}$. Then we find

$\displaystyle\operatorname{\bigcirc}_{a}f(x)=1\iff$ $\displaystyle\
\exists{b,x^{\prime}}\ x\xrightarrow{b}x^{\prime}\land(1-d_{A}(b,a))=1\land
f(x^{\prime})=1$ $\displaystyle\iff$ $\displaystyle\
\exists{b,x^{\prime}}\colon x\xrightarrow{b}x^{\prime}\land d_{A}(b,a)=0\land
f(x^{\prime})=1$ $\displaystyle\iff$ $\displaystyle\
\exists{b,x^{\prime}}\colon x\xrightarrow{b}x^{\prime}\land b=a\land
f(x^{\prime})=1$ $\displaystyle\iff$ $\displaystyle\
x\in\Diamond_{a}f^{-1}(\\{1\\}).$

Following the development of Sct. 4.1, we establish the metric version of Lem.
4.1: Let $(X,\to,d_{A})$ be a finitely branching metric transition system and
$\mathcal{F}\subseteq[0,1]^{X}$ be a family of functions. Then for $c\in A$ we
have
$\operatorname{\bigcirc}_{c}\Big{(}\bigwedge_{f\in\mathcal{F}}f\Big{)}=\bigwedge_{\begin{subarray}{c}\mathcal{F}_{0}\subseteq\mathcal{F}\\\
\mathcal{F}_{0}\text{
finite}\end{subarray}}\operatorname{\bigcirc}_{c}\Big{(}\bigwedge_{f\in\mathcal{F}_{0}}f\Big{)}.$

######  Proof 5.2.

One inequality holds independently of the properties of the transition system,
namely for all $x\in X$ and an arbitrary subset
$\mathcal{F}_{0}\subseteq\mathcal{F}$ we have

$\displaystyle\operatorname{\bigcirc}_{c}\bigwedge_{f\in\mathcal{F}}f$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\big{(}\overline{D_{c}}(a)\land\bigwedge_{f\in\mathcal{F}}f(x^{\prime})\big{)}$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{f\in\mathcal{F}}\big{(}\overline{D_{c}}(a)\land
f(x^{\prime})\big{)}$
$\displaystyle\leq\bigwedge_{f\in\mathcal{F}}\bigvee_{(a,x^{\prime})\in\delta(x)}\big{(}\overline{D_{c}}(a)\land
f(x^{\prime})\big{)}$
$\displaystyle\leq\bigwedge_{f\in\mathcal{F}_{0}}\bigvee_{(a,x^{\prime})\in\delta(x)}\big{(}\overline{D_{c}}(a)\land
f(x^{\prime})\big{)}=\bigwedge_{f\in\mathcal{F}_{0}}\operatorname{\bigcirc}_{c}f$

For the other inequality first observe that it holds whenever
$\mathcal{F}=\emptyset$, hence in the following we assume
$\mathcal{F}\neq\emptyset$. Fix $x\in X$ and let $\varepsilon>0$. Let
$\delta(x)=\\{(a_{1},x_{1}),\dots,(a_{n},x_{n})\\}$ be the finitely many
outgoing transitions from $x$. Choose functions
$f_{1},\dots,f_{n}\in\mathcal{F}$ such that

$f_{j}(x_{j})\leq\bigwedge_{f\in\mathcal{F}}f(x_{j})+\varepsilon$

for all $j=1,\dots,n$. Then

$\displaystyle\bigwedge_{\begin{subarray}{c}\mathcal{F}_{0}\subseteq\mathcal{F}\\\
\text{finite}\end{subarray}}\operatorname{\bigcirc}_{c}\bigwedge_{f\in\mathcal{F}_{0}}f(x)$
$\displaystyle\leq\operatorname{\bigcirc}_{c}\bigwedge_{j=1}^{n}f_{j}(x)$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\big{(}\overline{D_{c}}(a)\land\big{(}f_{1}(x^{\prime})\land\dots\land
f_{n}(x^{\prime})\big{)}\big{)}$
$\displaystyle\leq\bigvee_{(a,x^{\prime})\in\delta(x)}\big{(}\overline{D_{c}}(a)\land\bigwedge_{f\in\mathcal{F}}(f(x^{\prime})+\varepsilon)\big{)}$
$\displaystyle=\operatorname{\bigcirc}_{c}\bigwedge_{f\in\mathcal{F}}(f(x)+\varepsilon)$
$\displaystyle=\big{(}\operatorname{\bigcirc}_{c}\bigwedge_{f\in\mathcal{F}}f\big{)}(x)+\varepsilon.$

Since $\varepsilon>0$ and $x$ are arbitrary, we get

$\bigwedge_{\begin{subarray}{c}\mathcal{F}_{0}\subseteq\mathcal{F}\\\
\text{finite}\end{subarray}}\operatorname{\bigcirc}_{c}\bigwedge_{f\in\mathcal{F}_{0}}f\leq\operatorname{\bigcirc}_{c}\bigwedge_{f\in\mathcal{F}}f.$

In the quantitative case, the closures induced by the Galois connections had
appealing characterizations via boolean operators. Here the closure
$\operatorname{c_{B}}$ is obtained by post-composing the functions in
$\mathcal{F}$ with _all_ non-expansive operators. This is in fact a corollary
of the McShane-Whitney extension theorem [McS:ExtensionOfFunctions,
W:ExtensionOfFunctions].

######  Proposition 5.3.

The closure
$\operatorname{c_{B}}=\operatorname{\gamma_{B}}\circ\operatorname{\alpha_{B}}$
on $\mathcal{F}\subseteq[0,1]^{X}$ can be characterized as follows:

$\operatorname{c_{B}}(\mathcal{F})=\\{\operatorname{op}\circ\langle\mathcal{F}\rangle\mid\operatorname{op}\colon[0,1]^{\mathcal{F}}\to[0,1]\text{
is non-expansive wrt.\thinspace the sup-metric}\\}.$

Moreover, the co-closure
$\operatorname{\alpha_{B}}\circ\operatorname{\gamma_{B}}$ is the identity.

The proof of the above proposition and the next two results are analogous to
the corresponding results in the next section on simulationcolor=green!20]B:
we were talking about “one-sided simulation”, also in a corollary. I removed
this since it is not formally defined..

######  Proposition 5.4.

For finitely branching transition systems, $\operatorname{\log_{B}}$ is
$\operatorname{c_{B}}$-compatible.

######  Theorem 5.5.

The behaviour function $\operatorname{beh_{B}}$ on any $d\in\mathit{PMet}(X)$
is $\operatorname{beh_{B}}(d)=(d_{A}\otimes d)_{H}\circ(\delta\times\delta)$,
which results exactly in bisimulation metrics as considered in [afs:linear-
branching-metrics]. Moreover, $\operatorname{beh_{B}}$ is continuous for
finitely branching transition systems.

It is well-known that the kernel of the bisimulation metric, i.e., the pairs
of states with distance $0$, is exactly bisimilarity [fl:quantitative-
spectrum-journal].

###  5.2 Directed Simulation Metrics

In this section, we will treat simulation distance. Our logical and
behavioural universes are $\mathbb{L}=(\mathcal{P}([0,1]^{X}),\subseteq)$ and
$\mathbb{B}=(\mathit{DPMet}(X),\leq)$ with

$\displaystyle\operatorname{\alpha_{S}}(\mathcal{F})(x_{1},x_{2})=\bigvee_{f\in\mathcal{F}}(f(x_{1})\ominus
f(x_{2}))$ (for $\mathcal{F}\subseteq[0,1]^{X}$)
$\displaystyle\operatorname{\gamma_{S}}(d)=\\{f\in[0,1]^{X}\mid\forall{x_{1},x_{2}\in
X}:f(x_{1})\ominus f(x_{2})\leq d(x_{1},x_{2})\\}$ $\displaystyle\text{(for
$d\in\mathit{DPMet}(X)$)}.$

Now our (continuous) logic function
$\operatorname{\log_{S}}\colon\mathcal{P}([0,1]^{X})\to\mathcal{P}([0,1]^{X})$
is the mapping $\mathcal{F}\mapsto\bigcup_{c\in
A}\bigcirc_{c}[\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}_{f}(\mathcal{F})]$,
where $\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}_{f}$ closes
$\mathcal{F}$ under finite meets and constant shifts (whose necessity is
argued in Ex. 5.9). To characterize the closure $\operatorname{c_{S}}$ we use
a directed version of the McShane-Whitney extension theorem
[McS:ExtensionOfFunctions, W:ExtensionOfFunctions] (a special case of enriched
Kan extensions).

The closure
$\operatorname{c_{S}}=\operatorname{\gamma_{S}}\circ\operatorname{\alpha_{S}}$
on $\mathcal{F}$ is the set given in Prop. 5.3 except that $\operatorname{op}$
is non-expansive wrt. the directed sup-metric. The co-closure
$\operatorname{\alpha_{S}}\circ\operatorname{\gamma_{S}}$ is the identity.

######  Proof 5.6.

Let $g\in\operatorname{c_{S}}(\mathcal{F})$. We show that $g$ is of the form
$\operatorname{op}\circ\langle\mathcal{F}\rangle$ for a suitable
$\operatorname{op}$. For this define
$\operatorname{op}\colon[0,1]^{\mathcal{F}}\to[0,1]$ by

$\operatorname{op}(v)=\bigwedge_{x\in
X}\big{(}g(x)\oplus\bigvee_{f\in\mathcal{F}}(v(f)\ominus f(x))\big{)}$

Let now $u,v\in[0,1]^{\mathcal{F}}$ and assume without loss of generality that
$\operatorname{op}(u)\geq\operatorname{op}(v)$, since otherwise
$\operatorname{op}(u)\ominus\operatorname{op}(v)=0$. Then

$\displaystyle\operatorname{op}(u)\ominus\operatorname{op}(v)$
$\displaystyle=\bigwedge_{x\in
X}\big{(}g(x)\oplus\bigvee_{f\in\mathcal{F}}(u(f)\ominus
f(x))\big{)}-\bigwedge_{x\in
X}\big{(}g(x)\oplus\bigvee_{f\in\mathcal{F}}(v(f)\ominus f(x))\big{)}$
$\displaystyle\leq\bigvee_{x\in X}\bigvee_{f\in\mathcal{F}}(u(f)\ominus
f(x))-\bigvee_{f\in\mathcal{F}}(v(f)\ominus f(x))$
$\displaystyle\leq\bigvee_{x\in X}\bigvee_{f\in\mathcal{F}}(u(f)\ominus v(f))$
$\displaystyle=\bigvee_{f\in\mathcal{F}}(u(f)\ominus v(f))$

It remains to show that $g=\operatorname{op}\circ\langle\mathcal{F}\rangle$.
Fix $y\in X$, then

$\displaystyle\operatorname{op}\circ\langle\mathcal{F}\rangle(y)$
$\displaystyle=\bigwedge_{x\in
X}\big{(}g(x)\oplus\bigvee_{f\in\mathcal{F}}(\langle\mathcal{F}\rangle(y)(f)\ominus
f(x))\big{)}$ $\displaystyle=\bigwedge_{x\in
X}\big{(}g(x)\oplus\bigvee_{f\in\mathcal{F}}(f(y)\ominus f(x))\big{)}$
$\displaystyle\leq g(y)\oplus\bigvee_{f\in\mathcal{F}}(f(y)\ominus f(y))$
$\displaystyle=g(y)$

On the other hand, for all $x\in X$ we have

$g(x)\oplus\bigvee_{f\in\mathcal{F}}(f(y)\ominus f(x))\geq
g(x)\oplus(g(y)\ominus g(x))\geq g(y)$

since $g\in\operatorname{c_{S}}(\mathcal{F})$. And this implies that

$\operatorname{op}\circ\langle\mathcal{F}\rangle(y)=\bigwedge_{x\in
X}\big{(}g(x)\oplus\bigvee_{f\in\mathcal{F}}(f(y)\ominus f(x))\big{)}\geq
g(y)$

Conversely, let $g=\operatorname{op}\circ\langle\mathcal{F}\rangle$, then

$\displaystyle g(x)\ominus
g(y)=\operatorname{op}(\langle\mathcal{F}\rangle(x))\ominus\operatorname{op}(\langle\mathcal{F}\rangle(y))\leq\bigvee_{f\in\mathcal{F}}f(x)\ominus
f(y)=\operatorname{\alpha_{S}}(\mathcal{F})(x,y)$

and therefore $g\in\operatorname{c_{S}}(\mathcal{F})$.

For the co-closure consider some $d\in\mathit{DPMet}(X)$. Clearly
$\operatorname{\alpha_{S}}\circ\operatorname{\gamma_{S}}(d)\leq d$ and it
suffices to prove the other inequality. Fix a point $y\in X$ and define a map
$f\colon X\to[0,1]$ by $f(x)=d(x,y)$. Then $f\in\operatorname{\gamma_{S}}(d)$
and therefore

$\operatorname{\alpha_{S}}\circ\operatorname{\gamma_{S}}(d)(x,y)\geq
f(x)\ominus f(y)=d(x,y).$

In order to show $\operatorname{c_{S}}$-compatibility of
$\operatorname{\log_{S}}$, we first derive an alternative characterization of
the closure in terms of certain normal form given below. Note that a similar
statement holds in the context of bisimulation pseudo-metric when we replace
the closure $\operatorname{c_{S}}$ by $\operatorname{c_{B}}$. [Normal Form]
Let $\mathcal{F}\subseteq[0,1]^{X}$ with $1\in\mathcal{F}$ and
$f\in\operatorname{c_{S}}(\mathcal{F})$. Then there is a family of functions
$\\{f^{\varepsilon}_{(x,y)}\mid\varepsilon>0\text{ and }x,y\in X\\}$, where
each function $f^{\varepsilon}_{(x,y)}$ is a constant shift of a function in
$\mathcal{F}$, such that $f=\bigvee_{\varepsilon>0}\bigwedge_{x\in
X}\bigvee_{y\in X}f^{\varepsilon}_{(x,y)}$.

######  Proof 5.7.

By our characterization of the closure (Prop. 5.2),
$f=\operatorname{op}\circ\langle\mathcal{F}\rangle$ for some
$\operatorname{op}\colon[0,1]^{\mathcal{F}}\to[0,1]$ with

$\operatorname{op}(u)\ominus\operatorname{op}(v)\leq\bigvee_{f\in\mathcal{F}}u(f)\ominus
v(f)$

for all $u,v\in[0,1]^{\mathcal{F}}$. Given $\varepsilon>0$ and a fixed pair of
states $(x,y)$, let us construct a function $f^{\varepsilon}_{(x,y)}\colon
X\to[0,1]$ with
$f^{\varepsilon}_{(x,y)}(x)=\operatorname{op}\circ\langle\mathcal{F}\rangle(x)$
and
$f^{\varepsilon}_{(x,y)}(y)\geq\operatorname{op}\circ\langle\mathcal{F}\rangle(y)-\varepsilon$
as follows. We distinguish two cases:

  1. 1.

First assume that
$\operatorname{op}\circ\langle\mathcal{F}\rangle(y)>\operatorname{op}\circ\langle\mathcal{F}\rangle(x)$.

By our assumption on the operator $\operatorname{op}$ we have

$\operatorname{op}\circ\langle\mathcal{F}\rangle(y)\ominus\operatorname{op}\circ\langle\mathcal{F}\rangle(x)\leq\bigvee_{f\in\mathcal{F}}f(y)\ominus
f(x)$

In particular there is a function $f^{\varepsilon}_{(x,y)}\in\mathcal{F}$ with

$f^{\varepsilon}_{(x,y)}(y)-f^{\varepsilon}_{(x,y)}(x)\geq\operatorname{op}\circ\langle\mathcal{F}\rangle(y)-\operatorname{op}\circ\langle\mathcal{F}\rangle(x)-\varepsilon$

Applying a constant shift, we can arrange that
$f^{\varepsilon}_{(x,y)}(x)=\operatorname{op}\circ\langle\mathcal{F}\rangle(x)$
and

$f^{\varepsilon}_{(x,y)}(y)\geq\operatorname{op}\circ\langle\mathcal{F}\rangle(y)-\varepsilon$

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]last argument of 1. is
not clear — For clarity one could restrict case 1. to those x, y, epsilon
where op ° <F>(y) - op ° <F>(x) >= epsilon. We dont need that 1 is in F for
this step, this should be removed to avoid confusion.

  1. 2.

Next assume that
$\operatorname{op}\circ\langle\mathcal{F}\rangle(y)\leq\operatorname{op}\circ\langle\mathcal{F}\rangle(x)$.

In this case let $f^{\varepsilon}_{(x,y)}$ be the constant function with value
$\operatorname{op}\circ\langle\mathcal{F}\rangle(x)$.

This completes the construction of the family
$\\{f^{\varepsilon}_{(x,y)}\mid\varepsilon>0\text{ and }x,y\in X\\}$. Note
that for each $\varepsilon>0$ and each $z\in X$ we have

$\bigwedge_{x\in X}\bigvee_{y\in X}f^{\varepsilon}_{(x,y)}(z)\leq\bigvee_{y\in
X}f^{\varepsilon}_{(z,y)}(z)=\operatorname{op}\circ\langle\mathcal{F}\rangle(z)$

And thus, taking the supremum over all $\varepsilon>0$, we get

$\bigvee_{\varepsilon>0}\bigwedge_{x\in X}\bigvee_{y\in
X}f^{\varepsilon}_{(x,y)}(z)\leq\operatorname{op}\circ\langle\mathcal{F}\rangle(z)$

It suffices to prove the other inequality. Let $z\in X$ and $\delta>0$, then

$\bigvee_{\varepsilon>0}\bigwedge_{x\in X}\bigvee_{y\in
X}f^{\varepsilon}_{(x,y)}(z)\geq\bigwedge_{x\in X}\bigvee_{y\in
X}f^{\delta}_{(x,y)}(z)\geq\bigwedge_{x\in X}f^{\delta}_{(x,z)}(z)$

By construction

$f^{\delta}_{(x,z)}(z)\geq\operatorname{op}\circ\langle\mathcal{F}\rangle(z)-\delta.$

Hence

$\bigvee_{\varepsilon>0}\bigwedge_{x\in X}\bigvee_{y\in
X}f^{\varepsilon}_{(x,y)}(z)\geq\operatorname{op}\circ\langle\mathcal{F}\rangle(z)-\delta$

and since $\delta>0$ is arbitrary, we can conclude, as desired, that

$\bigvee_{\varepsilon>0}\bigwedge_{x\in X}\bigvee_{y\in
X}f^{\varepsilon}_{(x,y)}(z)\geq\operatorname{op}\circ\langle\mathcal{F}\rangle(z).$

These results enable us to show that the logic function is indeed compatible
with closure, a prerequisite for being able to derive the corresponding
behaviour function. For finitely branching transition systems,
$\operatorname{\log_{S}}$ is $\operatorname{c_{S}}$-compatible.

######  Proof 5.8.

Let $g\in\operatorname{\log_{S}}\circ\operatorname{c_{S}}(\mathcal{F})$, then
$g=\operatorname{\bigcirc}_{a}f$ for some function
$f\in\operatorname{c_{S}}(\mathcal{F})$. Moreover, by Prop. 5.6 there is a
familiy of functions $\\{f^{\varepsilon}_{(x,y)}\mid\varepsilon>0\text{ and
}x,y\in X\\}$, where each function $f^{\varepsilon}_{(x,y)}$ is a constant
shift of a function in $\mathcal{F}\cup\\{1\\}$, such that

$\operatorname{op}\circ\langle\mathcal{F}\rangle=\bigvee_{\varepsilon>0}\bigwedge_{x\in
X}\bigvee_{y\in X}f^{\varepsilon}_{(x,y)}$

Using the complete distributivity of $[0,1]^{X}$, the fact that
$\operatorname{\bigcirc}_{c}$ distributes over suprema and Lem. 5.1, it now
follows that

$\displaystyle g$
$\displaystyle=\operatorname{\bigcirc}_{a}f=\operatorname{\bigcirc}_{a}(\operatorname{op}\circ\langle\mathcal{F}\rangle)=\operatorname{\bigcirc}_{a}\Big{(}\bigvee_{\varepsilon>0}\bigwedge_{x\in
X}\bigvee_{y\in X}f^{\varepsilon}_{(x,y)}\Big{)}$
$\displaystyle=\operatorname{\bigcirc}_{a}\Big{(}\bigvee_{\varepsilon>0}\bigvee_{h:X\to
Y}\bigwedge_{x\in X}f^{\varepsilon}_{(x,h(x))}\Big{)}$
$\displaystyle=\bigvee_{\varepsilon>0}\bigvee_{h:X\to
Y}\operatorname{\bigcirc}_{a}\Big{(}\bigwedge_{x\in
X}f^{\varepsilon}_{(x,h(x))}\Big{)}$
$\displaystyle=\bigvee_{\varepsilon>0}\bigvee_{h:X\to
Y}\bigwedge_{\begin{subarray}{c}X_{0}\subseteq X\\\
\text{finite}\end{subarray}}\operatorname{\bigcirc}_{a}\Big{(}\bigwedge_{x\in
X_{0}}f^{\varepsilon}_{(x,h(x))}\Big{)}$

Since $\operatorname{\bigcirc}_{a}\Big{(}\bigwedge_{x\in
X_{0}}f^{\varepsilon}_{(x,h(x))}\Big{)}\in\operatorname{\bigcirc}_{a}[\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}_{f}(\mathcal{F}\cup\\{1\\})]=\operatorname{\bigcirc}_{a}[\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}_{f}(\mathcal{F})]\subseteq\operatorname{\log_{S}}(\mathcal{F})$,
we conclude that this function is contained in
$\operatorname{c_{S}}\circ\operatorname{\log_{S}}(\mathcal{F})$.
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]is it obvious that
$c_{s}(F)$ is closed under joins and meets. — Yes, more generally
$gamma_{S}(d)$ is always closed under joins and meets.

######  Example 5.9.

We show that adding shifts to the logic function is necessary to obtain
compatibility. Consider the metric transition system
$(\\{x,y,x_{1},y_{1}\\},\\{x\xrightarrow{1}x_{1},y\xrightarrow{0}y_{1}\\},d_{A})$
with $d_{A}$ is an Euclidean metric over the alphabet $A=[0,1]$.

Assume that $\mathcal{F}=\\{f\\}$ with
$f(x)=f(y)=f(x_{1})=\nicefrac{{1}}{{2}}$color=green!20]B: changed from xfrac
to nicefrac package, since the fractions looked strange., $f(y_{1})=0$, where
the pseudo-metric $d=\operatorname{\alpha_{S}}(\mathcal{F})$ has distance $0$
for the states $x,y,x_{1}$ and it yields distance $\nicefrac{{1}}{{2}}$
between $y_{1}$ and all other states. Then it is easy to see that $g$ with
$g(x)=g(y)=g(x_{1})=1$, $g(y_{1})=\nicefrac{{1}}{{2}}$ is contained in
$\operatorname{c_{S}}(\mathcal{F})$, since it is non-expansive wrt. $d$. Then
$\operatorname{\bigcirc}_{1}g\in\operatorname{\log_{S}}(\operatorname{c_{S}}(\mathcal{F}))$
and

$\operatorname{\bigcirc}_{1}g(x)\ominus\operatorname{\bigcirc}_{1}g(y)=(\overline{D_{1}}(1)\land
g(x_{1}))\ominus(\overline{D_{1}}(0)\land g(y_{1}))=(1\land
1)\ominus(0\land\nicefrac{{1}}{{2}})=1.$

In order for compatibility to hold, $\operatorname{\bigcirc}_{1}g$ must be
contained in $\operatorname{c_{S}}(\operatorname{\log_{S}}(\mathcal{F}))$,
i.e., it has to be non-expansive wrt.
$\operatorname{\alpha_{S}}(\operatorname{\log_{S}}(\mathcal{F}))$. If the
logic function does not use shifts, it only closes $\mathcal{F}$ under finite
meets and joins, which results in $f$, $0$ (empty join), $1$ (empty meet). For
all $r\in[0,1],\bar{f}\in\operatorname{c_{S}}(\mathcal{F})$, we have
$\operatorname{\bigcirc}_{r}\bar{f}(x)\ominus\operatorname{\bigcirc}_{r}\bar{f}(y)<\operatorname{\bigcirc}_{1}g(x)\ominus\operatorname{\bigcirc}_{1}g(y)$,
which means
$\operatorname{\bigcirc}_{1}g\not\in\operatorname{c_{S}}(\operatorname{\log_{S}}(\mathcal{F}))$.
In particular,

$\operatorname{\bigcirc}_{r}f(x)\ominus\operatorname{\bigcirc}_{r}f(y)=(\overline{D_{r}}(1)\land
f(x_{1}))\ominus(\overline{D_{r}}(0)\land
f(y_{1}))=(\overline{D_{r}}(1)\land\nicefrac{{1}}{{2}})\ominus(\overline{D_{r}}(0)\land
0)\leq\nicefrac{{1}}{{2}}.$

The behaviour function $\operatorname{beh_{S}}$ can be characterized as
$\operatorname{beh_{S}}(d)=(d_{A}\otimes
d)_{\overrightarrow{H}}\circ(\delta\times\delta)$ for any
$d\in\mathit{DPMet}(X)$. In particular,
$\operatorname{\alpha_{S}}(\mu\,\operatorname{\log_{S}})=\mu\,\operatorname{beh_{S}}$
is the directed similarity metric of [afs:linear-branching-metrics]. Moreover,
$\operatorname{beh_{S}}$ is continuous for finitely branching transition
systems.

######  Proof 5.10.

Fix a metric $d\in\mathit{DPMet}(X)$. We need to show that for all states
$x,y$ we have

$\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(y)}d_{A}(a,b)\lor
d(x^{\prime},y^{\prime})=(\operatorname{\alpha_{S}}\circ\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}})(d)(x,y)$

First note that
$\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}_{f}\circ\operatorname{\gamma_{S}}=\operatorname{\gamma_{S}}$.
Hence one direction follows from
linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]$c\in[0,1]$ should be
$c\in A$. B: fixed

$\displaystyle(\operatorname{\alpha_{S}}\circ\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}})(d)(x,y)$
$\displaystyle=\bigvee_{f\in\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}}(d)}(f(x)\ominus
f(y))\leq\bigvee_{c\in
A}\bigvee_{f\in\operatorname{\gamma_{S}}(d)}\big{(}\operatorname{\bigcirc}_{c}f(x)\ominus\operatorname{\bigcirc}_{c}f(y)\big{)}$
$\displaystyle\leq\bigvee_{c\in
A}\bigvee_{f\in\operatorname{\gamma_{S}}(d)}\big{(}\bigvee_{(a,x^{\prime})\in\delta(x)}(\overline{D_{c}}(a)\land
f(x^{\prime}))\ominus\bigvee_{(b,y^{\prime})\in\delta(x)}(\overline{D_{c}}(a)\land
f(y^{\prime}))\big{)}$ $\displaystyle\leq\bigvee_{c\in
A}\bigvee_{f\in\operatorname{\gamma_{S}}(d)}\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(x)}\big{(}(1-d_{A}(c,a))\land
f(x^{\prime})\ominus(1-d_{A}(c,b))\land f(y^{\prime})\big{)}$
$\displaystyle\leq\bigvee_{c\in
A}\bigvee_{f\in\operatorname{\gamma_{S}}(d)}\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(x)}\big{(}d_{A}(a,b)\lor(f(x^{\prime})\ominus
f(y^{\prime}))\big{)}$
$\displaystyle\leq\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(x)}(d_{A}(a,b)\lor
d(x^{\prime},y^{\prime})),$

where we used the triangle inequality in the second-last step.

For the other direction, consider

$r:=\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(y)}(d_{A}(a,b)\lor
d(x^{\prime},y^{\prime}))$

We can assume that $r>0$, otherwise there is nothing to prove. Let
$\varepsilon>0$ with $\varepsilon<r$ and take $(\hat{a},\hat{x})\in\delta(x)$
such that

$d_{A}(\hat{a},b)\lor d(\hat{x},y^{\prime})\geq r-\varepsilon,\quad\text{for
all $(b,y^{\prime})\in\delta(y)$}.$

Let $Y:=\\{y^{\prime}\in\operatorname{tgt}(\delta(y))\mid
d(\hat{x},y^{\prime})\geq r-\varepsilon\\}$ and define $g_{0}\colon
Y\cup\\{\hat{x}\\}\to[0,1]$ by

$g_{0}(z)=\begin{cases}1&\text{if }z=\hat{x}\\\ 1-(r-\varepsilon)&\text{if
}z\in Y\end{cases}$

Then $g_{0}$ is non-expansive wrt. $d$ and can be extended to a non-expansive
function $g\colon X\to[0,1]$ by $g(z)=\bigwedge_{y\in Y}(g_{0}(y)\oplus
d(z,y))$. By definition
$\operatorname{\bigcirc}_{\hat{a}}g\in\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}}(d)$
and therefore

$(\operatorname{\alpha_{S}}\circ\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}})(d)(x,y)=\bigvee_{f\in\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}}(d)}(f(x)\ominus
f(y))\geq\operatorname{\bigcirc}_{\hat{a}}g(x)\ominus\operatorname{\bigcirc}_{\hat{a}}g(y).$

Furthermore, it holds that

$\displaystyle\operatorname{\bigcirc}_{\hat{a}}g(x)$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\big{(}(1-d_{A}(\hat{a},a))\land
g(x^{\prime})\big{)}\geq(1-d_{A}(\hat{a},\hat{a}))\land g(\hat{x})=1$
$\displaystyle\operatorname{\bigcirc}_{\hat{a}}g(y)$
$\displaystyle=\bigvee_{(b,y^{\prime})\in\delta(y)}\big{(}(1-d_{A}(\hat{a},b))\land
g(y^{\prime})\big{)}\leq 1-(r-\varepsilon),$

For this have to show that $(1-d_{A}(\hat{a},b))\land g(y^{\prime})\leq
1-(r-\varepsilon)$ for all $(b,y^{\prime})\in\delta(y)$. We distinguish the
following cases: if $y^{\prime}\in Y$, then $g(y^{\prime})=1-(r-\varepsilon)$
and the inequality follows. If however $y^{\prime}\not\in Y$, then by
definition $d(\hat{x},y^{\prime})<r-\varepsilon$ and hence – since
$d_{A}(\hat{a},b)\lor d(\hat{x},y^{\prime})\geq r-\varepsilon$, we must have
$d_{A}(\hat{a},b)\geq r-\varepsilon$, which implies that
$1-d_{A}(\hat{a},b)\leq 1-(r-\varepsilon)$ and again the inequality follows.
Combined we have that
$(\operatorname{\alpha_{S}}\circ\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}})(d)(x,y)\geq
r-\varepsilon$ and since $\varepsilon>0$ is arbitrary, this implies that
$(\operatorname{\alpha_{S}}\circ\operatorname{\log_{S}}\circ\operatorname{\gamma_{S}})(d)(x,y)\geq
r$.

To show that $\operatorname{beh_{S}}$ is continuous, assume that
$(X,\to,d_{A})$ is finitely branching. Let $(d_{\beta})_{\beta<\kappa}$ be an
ascending sequence in $\mathit{DPMet}(X)$, by the monotonicity of the function
$\operatorname{beh_{S}}$ it is clear that
$\operatorname{beh_{S}}(\bigvee_{\beta<\kappa}d_{\beta})\geq\bigvee_{\beta<\kappa}\operatorname{beh_{S}}(d_{\beta})$.
For the other direction, fix $x,y\in X$ and use the above characterization of
$\operatorname{beh_{S}}$ to derive

$\operatorname{beh_{S}}(\bigvee_{\beta<\kappa}d_{\beta})(x,y)=\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(y)}\Big{(}d_{A}(a,b)\lor(\bigvee_{\beta<\kappa}d_{\beta})(x^{\prime},y^{\prime})\Big{)}.$

Then finitely branching ensures that the supremum is achieved at some
$(\hat{a},\hat{x})\in\delta(x)$, i.e.,

$\operatorname{beh_{S}}(\bigvee_{\beta<\kappa}d_{\beta})(x,y)=\bigwedge_{(b,y^{\prime})\in\delta(y)}\Big{(}d_{A}(\hat{a},b)\lor(\bigvee_{\beta<\kappa}d_{\beta})(\hat{x},y^{\prime})\Big{)}.$

For every $\beta<\kappa$ choose some $(b_{\beta},y_{\beta})\in\delta(y)$, such
that $d_{A}(\hat{a},b_{\beta})\lor d_{\beta}(\hat{x},y_{\beta})$ is minimal.
Again, since the transition system is finitely branching, there is a single
$(\hat{b},\hat{y})\in\delta(y)$, such that $b_{\beta}=\hat{b}$ and
$y_{\beta}=\hat{y}$ for unboundedly many $\beta<\kappa$. From the definition
of $\operatorname{beh_{S}}$ we get

$\displaystyle\operatorname{beh_{S}}(d_{\beta})(x,y)$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(y)}\big{(}d_{A}(a,b)\lor
d_{\beta}(x^{\prime},y^{\prime})\big{)}$
$\displaystyle\geq\bigwedge_{(b,y^{\prime})\in\delta(y)}\big{(}d_{A}(\hat{a},b)\lor
d_{\beta}(\hat{x},y^{\prime})\big{)}$
$\displaystyle=d_{A}(\hat{a},b_{\beta})\lor d_{\beta}(\hat{x},y_{\beta}).$

Thus it suffices to show that

$\bigvee_{\beta<\kappa}\big{(}d_{A}(\hat{a},b_{\beta})\lor
d_{\beta}(\hat{x},y_{n})\big{)}\geq
d_{A}(\hat{a},\hat{b})\lor(\bigvee_{\beta<\kappa}d_{\beta})(\hat{x},\hat{y}).$

Fix $\beta<\kappa$ and choose $\eta\geq\beta$ with $b_{\eta}=\hat{b}$ and
$y_{\eta}=\hat{y}$, then

$d_{A}(\hat{a},\hat{b})\lor d_{\beta}(\hat{x},\hat{y})\leq
d_{A}(\hat{a},\hat{b})\lor
d_{\eta}(\hat{x},\hat{y})=d_{A}(\hat{a},b_{\eta})\lor
d_{\eta}(\hat{x},y_{\eta}).$

Every metric transition system can be viewed as a classical one by forgetting
the metric on the labels. In addition, we can first compute the simulation
metric of the quantitative system and then discretize the values to obtain
qualitative simulation equivalence.

Consider the Galois connection $\alpha\dashv\gamma$ with
$\alpha\colon\mathit{DPMet}(X)\to\operatorname{Pre}(X)$ and
$\gamma\colon\operatorname{Pre}(X)\to\mathit{DPMet}(X)$ given by the maps
$\alpha(d)=\\{(x,y)\mid d(x,y)=0\\}$, $\gamma(R)=1-\chi_{R}$. If the
transition system is finitely branching, then
$\alpha\circ\operatorname{beh_{S}}(d)=\operatorname{beh_{s}}\circ\alpha(d)$
for every $d\in\mathit{DPMet}(X)$. In particular
$\mu\,\operatorname{beh_{s}}=\alpha(\mu\,\operatorname{beh_{S}})$ due to Thm.
3.

######  Proof 5.11.

Fix $d\in\mathit{DPMet}(X)$, it is easy to see that
$\operatorname{beh_{s}}\circ\alpha(d)\subseteq\alpha\circ\operatorname{beh_{S}}(d)$.
For the other direction fix a pair
$(x,y)\in\alpha\circ\operatorname{beh_{S}}(d)$, then

$0=\operatorname{beh_{S}}(d)(x,y)=\bigvee_{(a,x^{\prime})\in\delta(x)}\bigwedge_{(b,y^{\prime})\in\delta(y)}d_{A}(a,b)\lor
d(x^{\prime},y^{\prime})$

We want to show that

$(x,y)\in\operatorname{beh_{s}}\circ\alpha(d)=\\{(x,y)\mid\forall
x^{\prime}\in\delta_{a}(x)\,\exists y^{\prime}\in\delta_{a}(y)\colon
d(x^{\prime},y^{\prime})=0\\}$

Fix $a\in A$ and consider $x^{\prime}\in\delta_{a}(x)$. Since the transition
system is finitely branching, there is $(b,y^{\prime})\in\delta(y)$ with
$d_{A}(a,b)\lor d(x^{\prime},y^{\prime})=0$, that means
$d_{A}(a,b)=0=d(x^{\prime},y^{\prime})$. But $d_{A}$ is a proper metric, thus
$a=b$ and we are done.

We conclude this section by the observation that the characterization in Thm.
5.2 allows us to eliminate constant shifts from the simulation logic.

Let
$\operatorname{log}^{\prime}\colon\mathcal{P}([0,1]^{X})\to\mathcal{P}([0,1]^{X})$
be the variant of $\operatorname{\log_{S}}$, where we do not close under
constant shifts. If the transition system is finitely branching, then
$\operatorname{log}^{\prime}$ is still sound and expressive for simulation,
that means
$\operatorname{\alpha_{S}}(\mu\,\operatorname{log}^{\prime})=\mu\,\operatorname{beh_{S}}$.

######  Proof 5.12.

It is clear that $\operatorname{log}^{\prime}$ is sound, it suffices to show
that it is still expressive. To this end let $x,y\in X$ and define
$r:=\alpha(\mu\,\operatorname{log}^{\prime})(x,y)$. Also let $\varepsilon>r$
and define
$R=\\{(p,q)\mid\alpha(\mu\,\operatorname{log}^{\prime})<\varepsilon\\}$, then
$(x,y)\in R$ and we show that $R$ is an $\varepsilon$-simulation.

Let $(p,q)\in R$ and assume that $p\xrightarrow{a}p^{\prime}$, we need to show
that there is some $q^{\prime}$ with $q\xrightarrow{b}q^{\prime}$, such that
$d_{A}(a,b)\leq\varepsilon$ and $(p^{\prime},q^{\prime})\in R$. Assume for a
contradiction that there is no such $q^{\prime}$ and let
$(b_{1},q_{1}),\dots,(b_{n},q_{n})$ be the finitely many outgoing transitions
from $q$. For each index $i$, we ether have
$\alpha(\mu\,\operatorname{log}^{\prime})(p^{\prime},q_{i})\geq\varepsilon$ or
$d_{A}(a,b_{i})\geq\varepsilon$. In the first case, we choose, without loss of
generality, a function $f_{i}\in\mu\,\operatorname{log}^{\prime}$ with
$f_{i}(p^{\prime})-f_{i}(q_{i})\geq\varepsilon$, in the other case we let
$f_{i}=1$. Now consider

$f:=\operatorname{\bigcirc}_{a}(f_{1}\land\dots\land
f_{n})\in\mu\,\operatorname{log}^{\prime}$

Let $j$ be the index, for which $f_{j}(p^{\prime})$ is minimal, and note that

$\displaystyle f(p)-f(q)$ $\displaystyle\geq(f_{1}\land\dots\land
f_{n})(p^{\prime})-\bigvee_{(b,q^{\prime})\in\delta(q)}\big{(}\overline{D_{c}}(a)\land(f_{1}\land\dots\land
f_{n})(q^{\prime})\big{)}$
$\displaystyle=\bigwedge_{(b,q^{\prime})\in\delta(q)}f_{j}(p^{\prime})-\big{(}\overline{D_{c}}(a)\land(f_{1}\land\dots\land
f_{n})(q^{\prime})\big{)}\geq\varepsilon$

a contradiction. So $R$ is indeed an $\varepsilon$-simulation and therefore

$\mu\,\operatorname{beh_{S}}(x,y)=\bigwedge\\{\delta\in[0,1]\mid\ \text{there
is a $\delta$-simulation $R$ with $(x,y)\in R$}\\}\leq\varepsilon$

Since $\varepsilon>r$ is arbitrary, it follows that
$\mu\,\operatorname{beh_{S}}(x,y)\leq r$.

###  5.3 Directed Trace Metrics

In this section, we treat the directed version of the (decorated) trace
distance whose fixpoint characterization is novel and, at the same time, the
most complex scenario considered in this paper. We will sometimes omit the
adjective ‘directed’.

Based on the qualitative case of trace equivalence (Sct. 4.3), we fix the
logical and behavioural universes to be the lattices
$\mathbb{L}=(\mathcal{P}([0,1]^{X}),\subseteq)$ and
$\mathbb{B}=(\mathit{DPMet}(\mathcal{P}(X)),\leq)$ with

$\displaystyle\operatorname{\alpha_{T}}(\mathcal{F})(X_{1},X_{2})=\
\bigvee_{f\in\mathcal{F}}(\tilde{f}(X_{1})\ominus\tilde{f}(X_{2}))$ (for
$\mathcal{F}\subseteq[0,1]^{X}$) $\displaystyle\operatorname{\gamma_{T}}(d)=\
\\{f\in[0,1]^{X}\mid\tilde{f}\text{ is non-expansive wrt.\thinspace}d\\}$
$\displaystyle\text{(for $d\in\mathit{DPMet}(\mathcal{P}X)$)}.$

It is easy to see that $\operatorname{\alpha_{T}}(\mathcal{F})$ is always
join-preserving in its first argument. Notice that we could have defined
$\mathbb{L}$ as those functions in $[0,1]^{\mathcal{P}(X)}$ that are join-
preserving. As a result, one expects that the closure $\operatorname{c_{T}}$
may close a set $\mathcal{F}$ under all non-expansive and join-preserving
operators. However, this is unfortunately not true as witnessed by the
following counterexample. This points to a more fundamental problem that there
is no McShane-Whitney type result for join-preserving operators: a join-
preserving operator defined on some subset does not necessarily have a join-
preserving extension to the whole space.color=green!20]B: We were referring
twice to the example. Fixed.

######  Example 5.13.

Let $X=\\{x,y,z\\}$ and $\mathcal{F}=\\{f_{1},f_{2}\\}\subseteq[0,1]^{X}$,
where $f_{1}$ and $f_{2}$ are the mappings $x,y\mapsto 1,z\mapsto 0$ and
$x,z\mapsto 0,y\mapsto\nicefrac{{1}}{{2}}$, respectively. Now consider a map
$g\colon X\to[0,1]$ with $g(x)=\nicefrac{{1}}{{2}}$, $g(y)=1$ and $g(z)=0$.
Then it is easily seen that $g\in\operatorname{c_{T}}(\mathcal{F})$. However,
we claim that there is no join-preserving and non-expansive operator
$\operatorname{op}\colon[0,1]^{2}\to[0,1]$ such that
$g=\operatorname{op}\circ\langle f_{1},f_{2}\rangle$. Assume otherwise that
$\operatorname{op}(f_{1}(u),f_{2}(u))=g(x)$ (for $u\in X$), which implies
$\operatorname{op}(1,0)=\nicefrac{{1}}{{2}}$,
$\operatorname{op}(1,\nicefrac{{1}}{{2}})=1$, and $\operatorname{op}(0,0)=0$.
Due to non-expansivity of $\operatorname{op}$ we conclude that
$\operatorname{op}(0,\nicefrac{{1}}{{2}})\leq\nicefrac{{1}}{{2}}$, which leads
to the following contradiction:

$1=\operatorname{op}(1,\nicefrac{{1}}{{2}})=\operatorname{op}((1,0)\lor(0,\nicefrac{{1}}{{2}}))=\operatorname{op}(1,0)\lor\operatorname{op}(0,\nicefrac{{1}}{{2}})=\nicefrac{{1}}{{2}}.$

As (continuous) logic function
$\operatorname{\log_{T}}\colon\mathcal{P}([0,1]^{X})\to\mathcal{P}([0,1]^{X})$
we define $\operatorname{\log_{T}}(\mathcal{F})=\bigcup_{a\in
A}\bigcirc_{a}[\operatorname{\mathrm{cl}}^{\mathrm{sh}}(\mathcal{F})]\cup\\{1\\}$,
where $\operatorname{\mathrm{cl}}^{\mathrm{sh}}$ closes a set of functions
under constant shifts, as in Sct. 5.2, and $1$ is the constant $1$-function.
Typically, operators of a ‘metric’ logic ought to preserve non-expansiveness,
which is not the case for the shift $f\mapsto f\oplus r$; since it might
increase the distance of a non-empty set to the empty set. This is not
problematic in our case, since the distance of $\emptyset$ to any other set is
$1$ anyway, induced by the constant operator $1$. (Note that the empty join is
$0$.) Nevertheless, we will show in Thm. 5.3 that our logic characterizes
trace distance, i.e.,
$\operatorname{\alpha_{T}}(\mu\operatorname{\log_{T}})=d_{T}$, where
$d_{T}:=(d_{\mathrm{Tr}})_{\overrightarrow{H}}\circ(\operatorname{Tr}\times\operatorname{Tr})$.

The co-closure, on the other hand, is straightforward to characterize. The co-
closure $\operatorname{\alpha_{T}}\circ\operatorname{\gamma_{T}}$ maps a
directed pseudo-metric $d$ to the greatest directed pseudo-metric $d^{\prime}$
such that $d^{\prime}\leq d$ and $d^{\prime}$ is join-preserving in its first
argument.

######  Proof 5.14.

It suffices to show that
$\operatorname{\alpha_{T}}\circ\operatorname{\gamma_{T}}$ is the identity on
directed pseudo-metrics $d$ that are already join-preserving in the first
argument. For any directed pseudo-metric $d$ we have
$\operatorname{\alpha_{T}}\circ\operatorname{\gamma_{T}}(d)\leq d$, we show
the other inequality in case $d$ is join-preserving in the first argument. Let
$Y_{1},Y_{2}\subseteq X$, we will construct a function $f\colon X\to[0,1]$
with $f\in\operatorname{\gamma_{T}}(d)$ that witnesses the distance between
$Y_{1}$ and $Y_{2}$. Define

$f(x)=d(\\{x\\},Y_{2})$

Given any two sets $X_{1},X_{2}\subseteq X$, the preservation of joins and the
triangle inequality yield

$\tilde{f}(X_{1})\ominus\tilde{f}(X_{2})=d(X_{1},Y_{2})\ominus
d(X_{2},Y_{2})\leq d(X_{1},X_{2})$

So indeed $f\in\operatorname{\gamma_{T}}(d)$ and therefore

$\operatorname{\alpha_{T}}\circ\operatorname{\gamma_{T}}(d)(Y_{1},Y_{2})\geq\tilde{f}(Y_{1})\ominus\tilde{f}(Y_{2})=d(X_{1},Y_{2}).$

Next we turn our attention to the compatibility of our logic function. Here we
have to work around the fact that the closure can not be easily characterized,
neither in terms of operators nor in terms of a suitable normal form (cf.
Prop. 5.6). Still, compatibility holds, even for transition systems of
arbitrary branching type.

######  Lemma 5.15.

Let $h\colon X\to[0,1]$, $c\in A$ and $Y\subseteq X$. Then it holds that

$\widetilde{\operatorname{\bigcirc}_{c}h}(Y)=\bigwedge_{\Delta\subseteq\delta[Y]}\big{(}\widetilde{\overline{D_{c}}}(\operatorname{lab}(\delta[Y]\setminus\Delta))\lor\tilde{h}(\operatorname{tgt}(\Delta))\big{)}$

######  Proof 5.16.

Using distributivity we obtain:

$\displaystyle\widetilde{\operatorname{\bigcirc}_{c}h}(Y)$
$\displaystyle=\bigvee_{x\in
Y}\bigvee_{(a,x^{\prime})\in\delta(x)}(\overline{D_{c}}(a)\land
h(x^{\prime}))=\bigvee_{(a,x^{\prime})\in\delta[Y]}(\overline{D_{c}}(a)\land
h(x^{\prime}))$
$\displaystyle=\bigwedge_{\Delta\subseteq\delta[Y]}\Big{(}\bigvee_{(a,x^{\prime})\in\delta[Y]\backslash\Delta}\overline{D_{c}}(a)\lor\bigvee_{(a,x^{\prime})\in\Delta}h(x^{\prime})\Big{)}$
$\displaystyle=\bigwedge_{\Delta\subseteq\delta[Y]}\Big{(}\bigvee_{a\in\operatorname{lab}(\delta[Y]\backslash\Delta)}\overline{D_{c}}(a)\lor\bigvee_{x^{\prime}\in\operatorname{tgt}(\Delta)}h(x^{\prime})\Big{)}$
$\displaystyle=\bigwedge_{\Delta\subseteq\delta[Y]}\Big{(}\widetilde{\overline{D_{c}}}(\operatorname{lab}(\delta[Y]\backslash\Delta))\lor\tilde{h}(\operatorname{tgt}(\Delta))\Big{)}.$

The logic function $\operatorname{\log_{T}}$ is
$\operatorname{c_{T}}$-compatible.

######  Proof 5.17.

Let $g\in\operatorname{\log_{T}}\circ\operatorname{c_{T}}(\mathcal{F})$, then
$g=\operatorname{\bigcirc}_{c}h$ for some function
$h\in\operatorname{\mathrm{cl}}^{\mathrm{sh}}(\operatorname{c_{T}}(\mathcal{F}))$.
Let $X_{1},X_{2}\subseteq X$, we need to show that the distance witnessed by
$g$ between $X_{1}$ and $X_{2}$ satisfies

$\tilde{g}(X_{1})\ominus\tilde{g}(X_{2})\leq\bigvee_{f\in\operatorname{\log_{T}}(\mathcal{F})}\big{(}\tilde{f}(X_{1})\ominus\tilde{f}(X_{2})\big{)}$

First, using Lem. 5.15, compute

$\displaystyle\tilde{g}(X_{1})\ominus\tilde{g}(X_{2})=\widetilde{\operatorname{\bigcirc}_{c}h}(X_{1})\ominus\widetilde{\operatorname{\bigcirc}_{c}h}(X_{2})$
$\displaystyle=\Bigg{(}\bigvee_{x_{1}\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x_{1})}\big{(}\overline{D_{c}}(a)\land
h(x^{\prime})\big{)}\Bigg{)}\ominus\Bigg{(}\bigwedge_{\Delta\subseteq\delta[X_{2}]}\big{(}\widetilde{\overline{D_{c}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\lor\tilde{h}(\operatorname{tgt}(\Delta))\big{)}\Bigg{)}$
$\displaystyle=\bigvee_{x_{1}\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x_{1})}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\big{(}\overline{D_{c}}(a)\land
h(x^{\prime})\big{)}\ominus\big{(}\widetilde{\overline{D_{c}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\lor\tilde{h}(\operatorname{tgt}(\Delta))\big{)}\Big{)}$
$\displaystyle\leq\bigvee_{x_{1}\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x_{1})}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\Big{)}\land\Big{(}h(x^{\prime})\ominus\tilde{h}(\operatorname{tgt}(\Delta))\Big{)}.$
(1)

In the penultimate step, we use the following inequality (for
$r_{1},r_{2},r_{3},r_{4}\in[0,1]$) which is due to $r\ominus\\_\dashv\\_\oplus
r$ and the fact that both $\\_\ominus r$ and $\lor$ are monotonic.

$(r_{1}\land r_{2})\ominus(r_{3}\lor r_{4})=((r_{1}\land r_{2})\ominus
r_{3})\lor((r_{1}\land r_{2})\ominus r_{4})\leq(r_{1}\ominus
r_{3})\lor(r_{2}\ominus r_{4})$

Now fix a state $x_{1}\in X_{1}$, a transition
$(a,x^{\prime})\in\delta(x_{1})$, and $\Delta\subseteq\delta[X_{2}]$. We claim
that

$h(x^{\prime})\ominus\tilde{h}(\operatorname{tgt}(\Delta))\leq\bigvee_{\begin{subarray}{c}f\in
s(\mathcal{F})\\\
f(x^{\prime})=1\end{subarray}}(f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\Delta))).$
(2)

To see this, without loss of generality, let $\Delta\neq\emptyset$. Moreover,
let $h=h^{\prime}\circledast r$, for some
$h^{\prime}\in\operatorname{c_{T}}(\mathcal{F})$ and
$\circledast\in\\{\oplus,\ominus\\}$. Then we derive and use
$h^{\prime}\in\operatorname{c_{T}}(\mathcal{F})$ in the fourth step.

$\displaystyle h(x^{\prime})\ominus\tilde{h}(\operatorname{tgt}(\Delta))=$
$\displaystyle\bigwedge_{x^{\prime\prime}\in\operatorname{tgt}(\Delta)}h(x^{\prime})\ominus
h(x^{\prime\prime})$ $\displaystyle=$
$\displaystyle\bigwedge_{x^{\prime\prime}\in\operatorname{tgt}(\Delta)}(h^{\prime}(x^{\prime})\circledast
r)\ominus(h^{\prime}(x^{\prime\prime})\circledast r)$ $\displaystyle=$
$\displaystyle\bigwedge_{x^{\prime\prime}\in\operatorname{tgt}(\Delta)}h^{\prime}(x^{\prime})\ominus
h^{\prime}(x^{\prime\prime})$ $\displaystyle=$ $\displaystyle\
h^{\prime}(x^{\prime})\ominus\tilde{h^{\prime}}(\operatorname{tgt}(\Delta))$
$\displaystyle\leq$ $\displaystyle\
\bigvee_{f\in\mathcal{F}}(f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\Delta)))$
$\displaystyle\leq$ $\displaystyle\
\bigvee_{\begin{subarray}{c}f\in\operatorname{\mathrm{cl}}^{\mathrm{sh}}(\mathcal{F})\\\
f(x^{\prime})=1\end{subarray}}(f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\Delta))).$

Furthermore, $\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(B)$ (for
any $B\subseteq A$) is maximal when $c=a$:

$\displaystyle\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(B)$
$\displaystyle=(1-d_{A}(c,a))\ominus\bigvee_{b\in B}(1-d_{A}(c,b))$
$\displaystyle\leq\bigwedge_{b\in
B}\big{(}(1-d_{A}(c,a))\ominus(1-d_{A}(c,b))\big{)}$
$\displaystyle\leq\bigwedge_{b\in B}d_{A}(a,b)=\bigwedge_{b\in
B}(1-(1-d_{A}(a,b)))$ $\displaystyle=1\ominus\bigvee_{b\in
B}(1-d_{A}(a,b))=\overline{D_{a}}(a)\ominus\widetilde{\overline{D_{a}}}(B).$

Now using the above observation and (2) in (1) we get:

$\displaystyle\Big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\Big{)}\land\Big{(}h(x^{\prime})\ominus\tilde{h}(\operatorname{tgt}(\Delta))\Big{)}$
$\displaystyle\leq\Big{(}\overline{D_{a}}(a)\ominus\widetilde{\overline{D_{a}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\Big{)}\land\Big{(}h(x^{\prime})\ominus\tilde{h}(\operatorname{tgt}(\Delta))\Big{)}$
$\displaystyle\leq\bigvee_{\begin{subarray}{c}f\in s(\mathcal{F})\\\
f(x^{\prime})=1\end{subarray}}\Big{(}\big{(}\overline{D_{a}}(a)\ominus\widetilde{\overline{D_{a}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\big{)}\land\big{(}f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\Delta))\big{)}\Big{)}$
$\displaystyle=\bigvee_{\begin{subarray}{c}f\in s(\mathcal{F})\\\
f(x^{\prime})=1\end{subarray}}\Big{(}1\ominus\big{(}\widetilde{\overline{D_{a}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\lor\tilde{f}(\operatorname{tgt}(\Delta))\big{)}\Big{)}$
$\displaystyle=\bigvee_{\begin{subarray}{c}f\in s(\mathcal{F})\\\
f(x^{\prime})=1\end{subarray}}\Big{(}\big{(}\overline{D_{a}}(a)\land
f(x^{\prime})\big{)}\ominus\big{(}\widetilde{\overline{D_{a}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\lor\tilde{f}(\operatorname{tgt}(\Delta))\big{)}\Big{)}$
$\displaystyle\leq\bigvee_{f\in
s(\mathcal{F})}\Big{(}\big{(}\overline{D_{a}}(a)\land
f(x^{\prime})\big{)}\ominus\big{(}\widetilde{\overline{D_{a}}}(\operatorname{lab}(\delta[X_{2}]\backslash\Delta))\lor\tilde{f}(\operatorname{tgt}(\Delta))\big{)}\Big{)}$
$\displaystyle\leq\bigvee_{f\in
s(\mathcal{F})}\big{(}\widetilde{\operatorname{\bigcirc}_{a}f}(X_{1})\ominus\widetilde{\operatorname{\bigcirc}_{a}f}(X_{2})\big{)}$
$\displaystyle\leq\bigvee_{f\in\operatorname{\log_{T}}(\mathcal{F})}\big{(}\tilde{f}(X_{1})\ominus\tilde{f}(X_{2})\big{)}.$

Since $x_{1}\in X_{1}$, $(a,x^{\prime})\in\delta(x_{1})$ and
$\Delta\subseteq\delta[X_{2}]$ are arbitrary, we get

$\tilde{g}(X_{1})\ominus\tilde{g}(X_{2})\leq\bigvee_{f\in\operatorname{\log_{T}}(\mathcal{F})}\big{(}\tilde{f}(X_{1})\ominus\tilde{f}(X_{2})\big{)}.$

Now we can characterize the behaviour function as follows. To the best of our
knowledge, this is the first time that a fixpoint function for trace metrics