Map—-¿ ExistsMapdashdashdash¿ EmbeddingC-+-¿ MonoC—¿ Epi—-¿¿ Openo—¿¿
Closedtriangle—¿ EMap===== 11institutetext: The University of Sheffield, U.K.
11email<EMAIL_ADDRESS>22institutetext: Universität Duisburg-Essen,
Germany
22email<EMAIL_ADDRESS>33institutetext: FernUniversität Hagen,
Germany
33email<EMAIL_ADDRESS>44institutetext: Hochschule Rhein-
Waal, Germany
44email<EMAIL_ADDRESS>
# Predicate and relation liftings for coalgebras with side effects: an
application in coalgebraic modal logic

Harsh Beohar 11 Barbara König 22 Sebastian Küpper 33 Christina Mika-Michalski
44

###### Abstract

We study coalgebraic modal logic to characterise behavioural equivalence in
the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or
an Eilenberg-Moore category. Our aim is to develop a general framework based
on indexed categories/fibrations that is common to the aforementioned
categories. In particular, we show how the coalgebraic notion of behavioural
equivalence arises from a relation lifting (a special kind of indexed
morphism) and we give a general recipe to construct such liftings in the above
three cases. Lastly, we apply this framework to derive logical
characterisations for (weighted) language equivalence and conditional
bisimilarity.

###### Keywords:

(co)Kleisli categories Indexed morphisms Indexed categories/fibrations.

##  1 Introduction

Coalgebra [34] offers a categorical framework for specifying and reasoning
about state-based transition systems in a generic way. In particular, new
types of transition systems, behavioural equivalences (or distances), modal
logics and games can be obtained by suitably instantiating the theory of
coalgebras. While many types of transition systems can already be studied in
the category $\mathbf{Set}$, systems with side effects – leading to a notion
of trace equivalence or conditional bisimilarity – usually require to move to
a setting beyond $\mathbf{Set}$, using Kleisli, coKleisli or Eilenberg-Moore
categories, where the (co)monad specifies the side-effects.

Behavioural equivalences for such scenarios have already been studied
extensively (see e.g. [1, 13, 17, 20]). Modal logics, on the other hand, have
been considered to a lesser extent with side effects [22, 24, 10]; the
emphasis (see the survey [29] and the recent articles [12, 22, 26, 30]) has
been on logical characterisation of various notions of bisimulation relations
and metrics. The aim of the present paper is to close this gap by applying the
dual adjunction setup for fibrations developed by Kupke and Rot [30] to derive
logical characterisations for coalgebras with side effects. Recently, another
powerful approach [10] based on graded monads has been developed to handle
equivalences from the van Glabbeek spectrum and beyond. There the
characterising notion is not coalgebraic behavioural equivalence, but a
refinement of it, called finite depth behavioural equivalence. In addition,
Kupke and Rot [30] when comparing their work with [10] noted that “trace
equivalences of various kinds covered in [10] cannot be captured directly in
their setup”. Hence we will show how to capture linear notions such as trace,
language, and failure equivalences in their setup.

$\mathbf{E}$$\mathbf{Set}$1$\mathbf{Coalg}_{\mathbf{E}}(F_{\lambda})$$\mathbf{Coalg}_{\mathbf{Set}}(F)$$F$$F_{\lambda}$

Here, in order to treat these linear notions of equivalence uniformly, we
follow the approach of Hermida and Jacobs [15] to capture bisimulation
relations using the language of fibrations [16]; they have increasingly
appeared in the coalgebraic literature [7, 8, 14, 18, 23, 25, 30, 37]. The
general idea is as follows and is illustrated above in (1). First, a system is
modelled as a coalgebra $X\rTo^{\alpha}FX$ for some endofunctor
$\mathbf{Set}\rTo^{F}\mathbf{Set}$. Second a fibration $\mathbf{E}$ of binary
relations on the working category of sets is realised, whose fibres are all
the relations on the underlying state space. Third, a mechanism
$\mathcal{P}(X\times X)\rTo^{\lambda}\mathcal{P}(FX\times FX)$ (aka relation
lifting) is defined, which amounts to the lifting of $F$ to an endofunctor
$F_{\lambda}$ on $\mathbf{E}$. Now one can study the coalgebras induced by
$F_{\lambda}$ and, more importantly, this category
$\mathbf{Coalg}_{\mathbf{E}}(F_{\lambda})$ can be again arranged (see (1)) as
a fibration on $\mathbf{Coalg}_{\mathbf{Set}}(F)$. Lastly, the applicability
is shown by characterising bisimulation relations on $X$ as coalgebras of a
certain endofunctor living in the fibre above $(X,\alpha)$.

One of the objectives of this paper is to extend this ‘categorical’ picture
(1) w.r.t. coalgebraic notion of behavioural equivalence for dynamical systems
having side effects, i.e., those systems that can be modelled as coalgebras
living in a (co)Kleisli or Eilenberg-Moore category for some (co)monad on
$\mathbf{Set}$. Typical examples, in the context of this paper, are the
following: nondeterministic (linear weighted) automata modelled as coalgebras
in the Kleisli category for the powerset (multiset) monad (see Sections 6 and
0.B); conditional transition systems (which facilitate formal modelling of
software product lines) modelled as coalgebas in the coKleisli category for
the writer comonad $\mathbb{K}\times\\_$ (see Section 7). We left out case
studies in Eilenberg-Moore categories in this paper; however, they are shown
to satisfy the assumptions of this paper (Section 0.C).

We explore the general conditions on relation liftings (technically they are
called indexed morphisms in the paper like the ones indicated by $\lambda$ in
(1)) to ensure that behavioural equivalences can be viewed as coalgebras
living in the fibre above a given coalgebra $(X,\alpha)$ with side effects.
Another contribution is a recipe for obtaining relation and predicate liftings
(a special type of indexed morphisms) whose definition and correctness proof
are otherwise (at least in the Kleisli case) quite cumbersome to establish.
Predicate liftings are instrumental in providing interpretation to various
modalities for coalgebras in (co)Kleisli or Eilenberg-Moore categories, just
like in the case of $\mathbf{Set}$ (cf. [18, 32, 35]). Technically, our study
focuses on lifting an indexed morphism for a given endofunctor $F$ on
$\mathbf{Set}$ to an indexed morphism for a (co)Kleisli extension/Eilenberg-
Moore lifting $\bar{F}$ of $F$. And to the best of our knowledge, this
question is open at least for coalgebras with side effects.

Once we have captured behavioural equivalence in a fibration, we can then
apply the Kupke-Rot setup [30] based on dual adjunctions (see the survey [29]
on coalgebraic modal logic) to establish the logical characterisation of
behavioural equivalence. In particular, we first construct the Kupke-Rot setup
for behavioural equivalences and show that the sufficient conditions for
adequacy (i.e., behavioural equivalence is contained in logical equivalence)
and expressivity (i.e., converse of adequacy) given in [30] are satisfied.
This setup is later used to derive the logical characterisation for (weighted)
language equivalence and conditional bisimilarity; note that these notions
were not studied in [30].

While several ingredients (especially encompassing fibrations) used in this
paper are already known, our paper contains the following original
contributions:

  * •

We capture behavioural equivalences on coalgebras beyond $\mathbf{Set}$ as a
fibred notion by characterising them as special types of coalgebras.

  * •

We give concrete recipes for defining predicate and relation liftings (which
is both tedious and error-prone) in (co)Kleisli and Eilenberg-Moore
categories.

  * •

We extend the dual adjunction framework for fibrations by Kupke and Rot to
side effects, in particular to Kleisli categories. Here we need a mechanism to
factor the state space of a coalgebra by behavioural equivalence, which is
difficult if the category has no coequalisers. We provide a technique based on
reflective subcategories to circumvent this issue.

This paper is organised as follows. Section 2 sets the relevant categorical
preliminaries required for this paper. It is assumed that the reader is
already familiar with basic category theory, particularly, how a Kleisli or an
Eilenberg-Moore category is induced by a monad. Section 3 introduces the
assumptions that ensure behavioural equivalence is a fibred notion (in the
sense of (1)). Section 4 is devoted to coalgebraic modal logic where general
adequacy and expressivity results for behavioural equivalence are derived from
[30]. Section 5 gives the recipe to construct relation/predicate liftings for
coalgebras with side effects. In the next sections, the results of this paper
are applied in the context of nondeterministic automata and conditional
transition systems. Section 8 concludes this paper with some discussions on
future research. Note that proofs as well as additional material on linear
weighted and generalised Moore automata in Kleisli and Eilenberg-Moore
categories can be found in the appendix.

##  2 Preliminaries

#### Coalgebraic preliminaries [19, 34]

Let $\mathbf{C}$ be a category and let $\mathbf{C}\rTo^{F}\mathbf{C}$ be an
endofunctor modelling the branching type of the system of interest. Then the
behaviour of a state-based system will be modelled as an $F$-coalgebra (or,
simply coalgebra), i.e., as a morphism $X\rTo^{\alpha}FX$ in the category
$\mathbf{C}$.

###### Definition 1

A _coalgebra homomorphism_ $f$ between $(X,\alpha)$ and $(Y,\beta)$ is a
morphism $X\rTo^{f}Y\in\mathbf{C}$ satisfying $Ff\circ\alpha=\beta\circ f$.
The collection of coalgebras and their homomorphisms forms a category denoted
$\mathbf{Coalg}_{\mathbf{C}}(F)$.

Moreover, one can define behavioural equivalence on the (concrete) states of a
coalgebra under the assumption that there is a functor
$\mathbf{C}\rTo^{|\\_|}\mathbf{Set}$. By the concrete state-space of a
coalgebra $(X,\alpha)$, we mean the set $|X|$. Typically, in our case studies,
the functor $|\\_|$ will be a forgetful functor and will have a left/right
adjoint $\iota$. For instance, $\iota$ is left adjoint to $|\\_|$ when
$\mathbf{C}=\mathbf{Kl}(T)$ or $\mathbf{C}=\mathbf{EM}(T)$ (for some monad
$\mathbf{Set}\rTo^{T}\mathbf{Set}$), while it is right adjoint when
$\mathbf{C}=\mathbf{coKl}(G)$ for some comonad
$\mathbf{Set}\rTo^{G}\mathbf{Set}$.

###### Definition 2

Two states $x,x^{\prime}\in|X|$ of a coalgebra $(X,\alpha)$ are _behaviourally
equivalent_ iff there is a coalgebra homomorphism $f$ such that
$|f|x=|f|x^{\prime}$.

###### Example 1

An interesting example of coalgebras living in Kleisli categories is
nondeterministic automata (NDA). Following [13] an NDA is a coalgebra living
in $\mathbf{C}=\mathbf{Kl}(\mathcal{P})$, which is isomorphic to the category
$\mathbf{Rel}$ of sets as objects and relations as maps. Recall that a Kleisli
extension $\mathbf{Rel}\rTo^{\bar{F}}\mathbf{Rel}$ of
$\mathbf{Set}\rTo^{F}\mathbf{Set}$ (i.e. $\bar{F}\circ\iota=\iota\circ F$) is
in correspondence [31, Theorem 2.2] with a distributive law
$FT\rTo^{\vartheta}TF$ such that the following diagrams commute in
$\mathbf{Set}$.

Consider $F\\_=A\times\\_+1$ (where $1=\\{\bullet\\}$) with the following
distributive law [17]:

$\mathit{Act}\times\mathcal{P}X+1\rTo^{\vartheta_{X}}\mathcal{P}(\mathit{Act}\times
X+1)\qquad\quad(a,U)\mapsto\\{a\\}\times U,\ \bullet\mapsto\\{\bullet\\}.$ (2)

This induces a functor $\mathbf{Rel}\rTo^{\bar{F}}\mathbf{Rel}$ which acts on
a relation $X\rTo^{f}Y$, seen as a Kleisli arrow
$X\rTo^{f^{\prime}}\mathcal{P}{Y}$, as follows: $\bar{F}f=\vartheta_{Y}\circ
Ff^{\prime}$. Notice that $\bar{F}$-coalgebras model implicit nondeterminism
(i.e. this side-effect is hidden to an outside observer) [13], thus
behavioural equivalence typically coincides with _language equivalence_
(instead of bisimilarity) in this case.

#### Predicate liftings as indexed morphisms

Predicates and their liftings are quite common within the literature on
(coalgebraic) modal logic. In particular, a predicate is used as the semantics
of a logical formula [32], or as a relation on the state space of a coalgebra
[15]. In the basic setting, when $\mathbf{C}=\mathbf{Set}$, the predicates on
a set $X$ are given by the subsets of $X$. Now, given a function $X\rTo^{f}Y$,
a predicate $V$ on $Y$ (i.e. $V\subseteq Y$) can be transformed into a
predicate on $X$ by the pullback operation ${f}^{-1}V\subseteq X$ in
$\mathbf{Set}$. Note that this operation is functorial in nature; thus this
‘logical’ structure can be organised as a functor
${\mathbf{Set}}^{\text{op}}\rTo^{\hat{\mathcal{P}}}\mathbf{Cat}$ [18], where
$\hat{\mathcal{P}}X$ is the poset $(\mathcal{P}X,\subseteq)$ viewed as a
category. As noted by Jacobs in [18], _predicate logic on a category is given
by an indexed category_ and _predicate liftings are (endo)morphisms of indexed
categories_.

###### Definition 3

An indexed category is a $\mathbf{Cat}$-valued presheaf, i.e., a contravariant
functor $\Phi$ from $\mathbf{C}$ to $\mathbf{Cat}$. In addition, a morphism
between two indexed categories
${\mathbf{C}}^{\text{op}}\rTo^{\Phi}\mathbf{Cat}$ and
${\mathbf{D}}^{\text{op}}\rTo^{\Psi}\mathbf{Cat}$ is a pair of a functor
$\mathbf{C}\rTo^{G}\mathbf{D}$ and a natural transformation
$\Phi\rTo^{\lambda}\Psi\circ{G}^{\text{op}}$.

###### Note 1

Often the application of $\Phi$ on $f\in\mathbf{C}$ is denoted as $f^{*}$. We
also omit the use of superscript ‘op’ on functors and use the phrases ‘indexed
morphism’ and ‘predicate lifting’ interchangeably.

###### Remark 1

Another, equivalent, way to organise logic is by specifying the fibration of
predicates over a category [16]. The transformation of a fibration over
$\mathbf{C}$ into a contravariant pseudofunctor $\mathbf{C}\rTo\mathbf{Cat}$
is given by taking the fibres at each object in $\mathbf{C}$. Conversely one
has to invoke the so-called _Grothendieck construction_ to get a fibration,
which glues all the fibres $(\Phi X)_{X\in\mathbf{C}}$ to form a total
category of predicates $\mathbb{E}(\Phi)$ defined as follows.

$(X,U)\in\mathbb{E}(\Phi)X\in\mathbf{C}\land U\in\Phi
X\qquad(X,U)\rTo^{f,\bar{f}}(Y,V)\in\mathbb{E}(\Phi)X\rTo^{f}Y\in\mathbf{C}\land
U\rTo^{\bar{f}}f^{*}V\in\Phi X$

Moreover, there is an obvious ‘forgetful’ functor
$\mathbb{E}(\Phi)\rTo^{p}\mathbf{C}$ given by $(X,U)\mapsto X$ that induces a
(split) fibration on $\mathbf{C}$ [16, 18]. In the parlance of concrete
categories, the functor $p$ is topological [2, Definition 21.1] when $\Phi$
has fibred limits. Often, in applications, the fibres $(\Phi X,\preceq)$ (at
each $X\in\mathbf{C}$) form a poset (rather than a full-fledged category); we
label such an indexed category/fibration as _thin_. We restrict ourselves to
thin fibrations in this paper.

###### Example 2

The contravariant powerset functor
$\mathbf{Set}\rTo^{\hat{\mathcal{P}}}\mathbf{Cat}$ is an example of an indexed
category such that $\mathbb{E}(\hat{\mathcal{P}})\rTo\mathbf{Set}$ is a
bifibration [16]. This is because the reindexing functor ${f}^{-1}$ (for any
function $f$) has a left adjoint given by the direct image functor $f_{!}$.
Moreover, as an example of a predicate lifting, consider $F=\mathcal{P}$ over
$\mathbf{C}=\mathbf{Set}$ (which describes the branching type of unlabelled
transition systems) with
$\hat{\mathcal{P}}X\rTo^{\lambda_{X}}\hat{\mathcal{P}}\mathcal{P}X$ given by
$U\mapsto\mathcal{P}U$. It is well known that the above predicate lifting
encodes the box modality $\Box$ from logic [18].

##  3 Behavioural equivalence through indexed morphisms

Indexed morphisms not only induce modalities of interest in Computer Science;
but they can also be used to characterise behavioural equivalence. The
original idea [15] is to work with an indexed category
${\mathbf{Set}}^{\text{op}}\rTo^{\Psi}\mathbf{Cat}$ of binary relations, i.e.,
$\Psi$ is the composition
${\mathbf{Set}}^{\text{op}}\rTo^{\\_\times\\_}{\mathbf{Set}}^{\text{op}}\rTo^{\hat{\mathcal{P}}}\mathbf{Cat}$.
In particular, $\Psi X$ is the set of all relations on $X$. Then, for a
relation lifting $\Psi X\rTo^{\lambda_{X}}\Psi FX$ and a coalgebra
$X\rTo^{\alpha}FX\in\mathbf{Set}$, bisimilarity is the largest fixpoint of the
functional:

$\Psi X\rTo^{\lambda_{X}}\Psi FX\rTo^{\alpha^{*}}\Psi X.$ (3)

Unfortunately, this idea of working with relations on the concrete state space
immediately does not generalise to coalgebras with side effects; e.g., in the
case of conditional transition systems (CTSs) viewed as coalgebras living in
the coKleisli category of the writer comonad $\mathbb{K}\times\\_$ (see
Section 7). The problem essentially lies in associating a fibre to be the set
of all binary relations on the state space. There are situations (as in CTSs)
where the fibres will only be some subset of all the relations on the state
space. As a result, we impose the following restriction:

  1. A1

our working category $\mathbf{C}$ has binary products $\otimes$.

Thus we can define an indexed category $\Psi$ of relations as the composition:

${\mathbf{C}}^{\text{op}}\rTo^{\\_\otimes\\_}{\mathbf{C}}^{\text{op}}\rTo^{|\\_|}{\mathbf{Set}}^{\text{op}}\rTo^{\hat{\mathcal{P}}}\mathbf{Cat}.$
(4)

We view the elements of $\Psi X$ (for some object $X\in C$) as ‘abstract’
relations on $X$. Furthermore, A1 also ensures that for any object
$X\in\mathbf{C}$ there is a function

$|X\otimes X|\rTo^{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle}|X|\times|X|,$

where $X\otimes X\rTo^{\pi_{1}^{X},\pi_{2}^{X}}X$ are the two projection
arrows in $\mathbf{C}$. And thanks to these functions, we can define abstract
equality in the fibre $\Psi X$. In particular,

$\equiv_{X}\ =\
{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle}^{-1}=_{|X|}\enspace.$

Notice that in some cases (like when $\mathbf{C}$ is a Kleisli or Eilenberg-
Moore category) the abstract equality $\equiv_{X}$ coincides with the equality
on the concrete state space $=_{|X|}$ because the forgetful functor is product
preserving. However, in the context of CTSs, we will see that the two notions
of equality differ.

######  Proposition 1 ()

Under Assumption A1 the square drawn in (LABEL:eq:squarepbk) commutes for any
arrow $X\rTo^{f}Y$ in $\mathbf{C}$. As a result, there is a functor
$\mathbf{C}\rTo^{\mathrm{Eq}}\mathbb{E}(\Psi)$ (henceforth called _equality_
functor) that maps an object $X$ to the abstract equality $\equiv_{X}$.

The next proposition (originally from [18]) is a general result on indexed
categories useful in lifting an endofunctor on $\mathbf{C}$ to an endofunctor
on the given fibration $\mathbb{E}(\Phi)$. Moreover the category of coalgebras
of the lifted endofunctor can be structured again as a fibration on the given
category of coalgebras in which our original system of interest is modelled.

###### Proposition 2

Consider the diagram in (LABEL:eq:genresult), then the following statements
hold for a given functor $\mathbf{C}\rTo^{F}\mathbf{C}$ and an indexed
morphism $\Phi\rTo^{\lambda}\Phi F$.

  * •

The map $\lambda$ induces a map
$\mathbb{E}(\Phi)\rTo^{F_{\lambda}}\mathbb{E}(\Phi)$ of fibrations given by
$(X,U)\mapsto(FX,\lambda_{X}U)$.

  * •

The category of coalgebras induced by $F_{\lambda}$ forms a fibration on
$\mathbf{Coalg}_{\mathbf{C}}(F)$, where
${\mathbf{Coalg}_{\mathbf{C}}(F)}^{\text{op}}\rTo^{\Phi_{\lambda}^{F}}\mathbf{Cat}$
is the mapping: $(X,\alpha)\mapsto\mathbf{Coalg}_{\Phi
X}(\alpha^{*}\circ\lambda_{X})$.

Now recall (3) and $\Psi$ as indexed category of relations on $\mathbf{Set}$
(i.e. substitute $\otimes$ by $\times$ and $|\\_|$ by the identity functor in
(4)), an arbitrary bisimulation relation $R$ on a coalgebra
$X\rTo^{\alpha}FX\in\mathbf{Set}$ is the relation $R\in\Psi X$ satisfying
$R\subseteq\alpha^{*}\lambda_{X}R$. In other words, bisimulation relations on
the state space $X$ are again coalgebras of the functor
$\alpha^{*}\circ\lambda_{X}$ living in the fibre $\Psi X$. Next we show that
the same holds for behavioural equivalence in general, however, under the
following assumptions:

  1. A2

the given morphism $\Psi\rTo^{\lambda}\Psi F$ preserves $\mathrm{Eq}$, i.e.,
$F_{\lambda}\circ\mathrm{Eq}=\mathrm{Eq}\circ F_{\lambda}$. Equivalently, this
means that $\lambda_{X}(\equiv_{X})=\ \equiv_{FX}$ for every $X\in\mathbf{C}$.

  2. A3

the functor $\mathrm{Eq}$ has a left adjoint $\mathbb{Q}$.

###### Remark 2

Assumption A3 already appeared in [15] to model quotient types in the context
of type theory. However, our usage is in the unit $\kappa$ of
$\mathbb{Q}\dashv\mathrm{Eq}$ to construct a witnessing coalgebra homomorphism
in Theorem 3.2. This idea is already known in type theory; for instance, see
[11, Theorem 3.7] where a similar result was proven albeit under the stronger
assumption that the final coalgebra for $F$ exists. So when
$\mathbf{C}=\mathbf{Set}$, $\mathbb{Q}$ maps an relation $R$ on $X$ to the
quotient generated by the smallest equivalence containing $R$; the unit
$\kappa_{X}$ (for any set $X$) is the usual quotient function mapping an
element to its equivalence class.

######  Theorem 3.1 ()

Given an indexed morphism $\Psi\rTo^{\lambda}\Psi\circ F$, then under
Assumptions A1 and A2, the behavioural equivalence induced by a coalgebra
homomorphism $f\in\mathbf{Coalg}_{\mathbf{C}}(F)$ on a coalgebra
$(X,\alpha)\in\mathbf{Coalg}_{\mathbf{C}}(F)$ is a
$\alpha^{*}\circ\lambda$-coalgebra living in the fibre $\Psi X$, i.e.,
$f^{*}(\equiv_{Y})\subseteq\alpha^{*}\lambda_{X}(f^{*}\equiv_{Y}).$

######  Theorem 3.2 ()

Under Assumptions A1, A2, and A3 for every $\alpha^{*}\circ\lambda$-coalgebra
$R$ there is a coalgebra homomorphism $f\in\mathbf{Coalg}_{\mathbf{C}}(F)$
such that $R\subseteq f^{*}(\equiv_{\text{cod}(f)})$, where $\text{cod}(f)$
denotes the codomain of $f$. Moreover, $R=f^{*}(\equiv_{\text{cod}(f)})$ when
the unit of $\mathbb{Q}\dashv\mathrm{Eq}$ is Cartesian.

###### Remark 3

An application of Theorem 3.2 could be in establishing the completeness of
coalgebraic games (as in the spirit of [28]). For instance, if the winning
positions of Duplicator viewed as a relation $R$ is a coalgebra in the fibre
of $\Psi$, then Theorem 3.2 can be used to show that winning positions of
Duplicator are behaviourally equivalent. In the future, we would like to test
this application by working out a notion of 2-player games for coalgebra with
side effects.

##  4 Coalgebraic modal logic

The ‘partial’ characterisation of behavioural equivalence as a fibred notion
(cf. Theorems 3.1 and 3.2) enables us to use the dual adjunction framework of
Kupke and Rot [30] in (LABEL:eq:KupkeRot_Setup) to develop a logical
characterisation of behavioural equivalence. It should be noted that, although
this framework can handle behavioural preorders and distances, we prove our
results only for behavioural equivalence, i.e. in the context of Assumptions
A1 and A2. Below we explain the role of various functors drawn in
(LABEL:eq:KupkeRot_Setup) in an incremental manner; subsequently, we will
establish our general adequacy and expressivity results (Theorems 4.1 and 4.3)
for behavioural equivalences.

The fibration $\mathbb{E}(\Psi)\rTo^{p}\mathbf{C}$ will be used to define
(internally) a behavioural equivalence of interest. Often it is defined as a
colimit of a diagram resembling the final sequence in a fibre (cf. [14]). More
abstractly, we assume that the indexed category $\Psi^{F}_{\lambda}$ (recall
this notation from Proposition 2) has indexed final objects, for some indexed
morphism $\Psi\rTo^{\lambda}\Psi F$.

######  Lemma 1 ()

Suppose ${\mathbf{C}}^{\text{op}}\rTo^{\Phi}\mathbf{Cat}$ has indexed final
objects (i.e., the final object exists in each fibre $\Phi X$) and the
reindexing functor $f^{*}$ preserves these final objects. Then there is a
functor $\mathbf{C}\rTo^{\mathbbm{1}}\mathbb{E}(\Phi)$ that is right adjoint
to $p$.

Usually, $\mathbbm{1}$ is used (called the _truth functor_ [16] in the context
of logic) when the underlying fibration $\mathbb{E}(\Phi)\rTo^{p}\mathbf{C}$
has indexed final objects. However when $\Psi^{F}_{\lambda}$ satisfies the
conditions of the previous lemma, it results in a functor
$\mathbf{Coalg}_{\mathbf{C}}(F)\rTo^{\mathbbm{1}^{\lambda}}\mathbf{Coalg}_{\mathbb{E}(\Psi)}(F_{\lambda})$
(which we call _the behavioural conformance_ functor) that maps a coalgebra
$X\rTo^{\alpha}FX$ to the terminal element in $\mathbf{Coalg}_{\Psi
X}(\alpha^{*}\circ\lambda_{X})$ denoted as $1^{\lambda}_{X}$. Note that
$1^{\lambda}_{X}$ in our applications will correspond to the largest
behavioural equivalence on a given system. Moreover, it is not hard to arrive
at the adjoint situation as indicated in (LABEL:eq:largestbehequiv). So, in
other words, the behavioural conformance functor is right adjoint to the
forgetful functor that witnesses the fibration of behavioural conformance on
coalgebras.

###### Example 3

Consider the indexed category $\Psi$ induced by binary relations on sets and a
labelled transition system modelled as a coalgebra
$X\rTo^{\alpha}(\mathcal{P}X)^{\mathit{Act}}$, i.e., our
$\mathbf{C}=\mathbf{Set},F=(\mathcal{P}\\_)^{\mathit{Act}}$. Consider the
function $\Psi X\rTo^{\lambda_{X}}\Psi FX$ that maps a relation $R\in\Psi X$
to a relation $\lambda_{X}R\in\Psi FX$ (below
$q,q^{\prime}\in(\mathcal{P}X)^{\mathit{Act}}$):

$q\mathrel{\lambda_{X}R}q^{\prime}\iff\forall_{a,x}\exists_{x^{\prime}}\ (x\in
qa\implies x^{\prime}\in q^{\prime}a)\land\forall_{a,x^{\prime}}\exists_{x}\
(x^{\prime}\in q^{\prime}a\implies x\in qa).$

It is well known (as first noted in [15]) that a bisimulation relation is a
$\alpha^{*}\circ\lambda$-coalgebra. Moreover, bisimilarity
$\leftrightarroweq_{X}$ (the largest bisimulation relation on $X$) corresponds
to the final object in $\Psi_{\lambda}(X,\alpha)$, i.e.,
$\mathbbm{1}^{\lambda}(X,\alpha)=\ (X,\alpha,\leftrightarroweq_{X})$.

As for the dual adjunction $\mathcal{S}\dashv\mathcal{T}$ in
(LABEL:eq:KupkeRot_Setup), it provides a connection (cf. [33]) between states
and theories (the formulae satisfied by a state). The syntax of the logic is
given by a functor $\mathbf{A}\rTo^{L}\mathbf{A}$ and it is assumed that the
initial algebra $L\mathcal{A}\rTo^{h}\mathcal{A}\in\mathbf{A}$ exists for $L$,
which models the typical Lindenbaum algebra induced by the term algebra.
Lastly, the natural transformation $\delta$ gives the one-step interpretation
to the formulae which can be given its mate $\theta$ as described below (cf.
[21, Proposition 2]).

###### Proposition 3

Given
$\mathbf{C}\rTo^{F}\mathbf{C},\mathbf{A}\rTo^{L}\mathbf{A},\mathbf{C}\pile{\rTo^{\mathcal{S}}\\\
\lTo_{\mathcal{T}}}{\mathbf{A}}^{\text{op}}$ with
$\mathcal{S}\dashv\mathcal{T}$, there is a correspondence between
$F\mathcal{T}\rTo^{\delta}\mathcal{T}L$ and
$\mathcal{S}F\rTo^{\theta}L\mathcal{S}$.

Now given a coalgebra $X\rTo^{\alpha}FX\in\mathbf{C}$, the semantics
$\mathcal{A}\rTo^{\llbracket\\_\rrbracket_{X}}\mathcal{S}X$ of the logic
$(L,\delta)$ is given by the universal property of the initial algebra
$L\mathcal{A}\rTo^{h}\mathcal{A}$. In particular, it is the unique arrow in
$\mathbf{A}$ that makes the following diagram (drawn on the left) commutative.
And the transpose of the semantics map $\llbracket\\_\rrbracket_{X}$ under
$\mathcal{S}\dashv\mathcal{T}$ gives a ‘theory’ map
$X\rTo^{\llparenthesis\\_\rrparenthesis_{X}}Q\mathcal{A}$; it is the unique
arrow in $\mathbf{C}$ that makes the following diagram on the right
commutative. Once these niceties are set up, one can argue when a logic
($L,\delta$) is adequate and expressive. Intuitively, a logic ($L,\delta$) is
adequate if behaviourally equivalent states satisfy the same logical formulae;
while an adequate logic is expressive if logically equivalent states are also
behaviourally equivalent. The formulation below is a straightforward
formulation of adequacy and expressivity given in [30] using the language of
indexed categories.

###### Definition 4

Suppose the behavioural conformance functor $\mathbbm{1}^{\lambda}$ exists
(for some $\lambda$) with
${\mathbf{A}}^{\text{op}}\rTo^{\bar{\mathcal{T}}}\mathbb{E}(\Psi)$ such that
$p\circ\bar{\mathcal{T}}=\mathcal{T}$. Then a logic $(L,\delta)$ is _adequate_
(resp.  _expressive_) w.r.t. $\bar{\mathcal{T}}$ if
$(X,1_{X}^{\lambda})\rTo^{\llparenthesis\\_\rrparenthesis_{X}}\bar{\mathcal{T}}\mathcal{A}$
is a (resp. Cartesian) map in $\mathbb{E}(\Psi)$, for every coalgebra
$X\rTo^{\alpha}FX\in\mathbf{C}$.

The role of $\bar{\mathcal{T}}$ is to encode a relationship between the
theories of any two states (cf. [30]); so we let
$\bar{\mathcal{T}}=\mathrm{Eq}\circ\mathcal{T}$ in the context of behavioural
equivalence. Next we state the main result of this section, which is a
refinement of adequacy and expressivity results given in [30].

######  Theorem 4.1 ()

Under the assumptions of Theorem 3.1, if $\bar{\mathcal{T}}$ has a left
adjoint $\bar{\mathcal{S}}$, the logic $(L,\delta)$ is adequate. Moreover it
is expressive if $|\delta_{\mathcal{A}}|$ is injective.

In short, the Kupke-Rot logical setup for behavioural equivalence can be
summarised as drawn left on the next page. Now if our indexed category $\Psi$
satisfies A3 (like in the case of coKleisli and Eilenberg-Moore categories),
then $\bar{\mathcal{S}}=\mathcal{S}\circ\mathbb{Q}$ as indicated in (5).
However, in the case of Kleisli categories we will construct
$\bar{\mathcal{S}}$ under some restrictions (cf. Theorem 4.3).

$\begin{diagram}$ (5)

### Construction of $\bar{\mathcal{S}}$ for Kleisli categories

Unfortunately, arbitrary (co)limits in general do not exists in a Kleisli
category. For instance, one of our working categories
$\mathbf{Kl}(\mathcal{P})\cong\mathbf{Rel}$ (the category of sets and
relations) does not have all coequalisers, but $\mathbf{Rel}$ has a reflective
subcategory ${\mathbf{Set}}^{\text{op}}$ that does. The presence of these
coequalisers in the reflective subcategory will then be used to construct
$\bar{\mathcal{S}}$.

###### Definition 5

A subcategory $\mathbf{B}\rMono^{\jmath}\mathbf{C}$ is _reflective_ when the
inclusion functor $\jmath$ has a left adjoint $\mathfrak{r}$ (often called as
reflector).

######  Theorem 4.2 ([1])

If $\mathbf{B}\rMono^{\jmath}\mathbf{C}$ is a reflective subcategory of
$\mathbf{C}$ and $\mathbf{C}\rTo^{F}\mathbf{C}$ preserves $\mathbf{B}$, i.e.,
$\forall_{B,f\in\mathbf{B}}\ (FB\in\mathbf{B}\land Ff\in\mathbf{B})$ and
$F\circ\jmath=\jmath\circ F,$ then
$\mathbf{Coalg}_{B}(F)\pile{\lTo~{}{\bar{\mathfrak{r}}}\\\
\rTo~{}{\bar{\jmath}}}\mathbf{Coalg}_{C}(F)$ with
$\bar{\mathfrak{r}}\dashv\bar{\jmath}$. Here, $\bar{\jmath}$ is the obvious
inclusion.

The reflector $\bar{\mathfrak{r}}$ typically results in a form of (on-the-fly)
determinisation (cf. Example 4). Moreover, in our case studies, these
reflective subcategories will also take the place of algebras in (5), and if
these reflective subcategories have coequalisers, then we can construct
$\bar{\mathcal{S}}$ in general.

So let
$\mathbf{B}={\mathbf{A}}^{\text{op}},\mathcal{S}=\mathfrak{r},\mathcal{T}=\jmath$,
and $(X,R)\in\mathbb{E}(\Psi)$. Then the idea is to use the following series
of transformations (depicted below on the left) to construct
$\bar{\mathcal{S}}$ as the equaliser of the parallel arrows
$\mathcal{S}p_{1}^{\prime},\mathcal{S}p_{2}^{\prime}\in\mathbf{A}$. Below
$p_{i}$ (for $i\in\\{1,2\\}$) are the obvious projection functions and each
$p_{i}^{\prime}$ is the transpose of $p_{i}$ under the free-forgetful
adjunction $\iota\dashv|\\_|$.

$\mathcal{S}\iota R\pile{\rTo^{\mathcal{S}p_{1}^{\prime}}\\\
\rTo_{\mathcal{S}p_{2}^{\prime}}}\mathcal{S}X\in{\mathbf{A}}^{\text{op}}\iota
R\pile{\rTo^{p_{1}^{\prime}}\\\
\rTo_{p_{2}^{\prime}}}X\in\mathbf{Kl}(T)R\pile{\rTo^{p_{1}}\\\
\rTo_{p_{2}}}|X|\in\mathbf{Set}$

Let $(\bar{\mathcal{S}}(X,R),e)$ be the equaliser of
$\mathfrak{r}p_{i}^{\prime}$ in $\mathbf{A}$. Now
$(X,R)\rTo^{f}(Y,S)\in\mathbb{E}(\Psi)$ means that
$X\rTo^{f}Y\in\mathbf{Kl}(T)$ and $R\subseteq{(|f|\times|f|)}^{-1}S$. So there
is a function $R\rTo^{g}S$ such that $|f|\circ p_{i}=q_{i}\circ g$ with
$p_{i},q_{i}$ being the obvious projections when the relations $R,S$ are
viewed as spans in $\mathbf{Set}$. Moreover $f\circ
p_{i}^{\prime}=q_{i}^{\prime}\circ\iota g$ due to the naturality of the counit
of $\iota\dashv|\\_|$. So the two squares in (LABEL:eq:coequaliser) commute
and the universal property of equalisers gives the unique
$\bar{\mathcal{S}}f$.

######  Theorem 4.3 ()

Under A1 and ${\mathbf{A}}^{\text{op}}$ being a reflective subcategory of
$\mathbf{Kl}(T)$ having coequalisers, the above defined $\bar{\mathcal{S}}$ is
a functor and left adjoint to $\bar{\mathcal{T}}=\mathrm{Eq}\circ\mathcal{T}$.

##  5 Lifting of predicate and relation liftings

In this paper, the indexed categories corresponding to predicates (or
relations) on our working category (like (co)Kleisli or Eilenberg-Moore
categories) are always induced by lifting an indexed category on the
underlying base category $\mathbf{Set}$ (for instance, recall $\Psi$ from
(4)). In a similar spirit, our aim is to construct indexed morphisms on our
working category by lifting an indexed morphism on $\mathbf{Set}$. So consider
an indexed category $\Phi$ of predicates given by
$\Phi=\hat{\mathcal{P}}\circ|\\_|$ and an endofunctor
$\mathbf{C}\rTo^{\bar{F}}\mathbf{C}$ modelling the branching type of behaviour
of interest.

#### Lifting of predicate liftings

Next we give a recipe to construct a predicate lifting, i.e., an indexed
morphism of type $\Phi\rTo^{\lambda}\Phi\bar{F}$. In particular, we need an
endofunctor $\mathbf{Set}\rTo^{G}\mathbf{Set}$, a predicate lifting
$\hat{\mathcal{P}}\rTo^{\sigma}\hat{\mathcal{P}}G$, and a natural
transformation $\gamma$ as indicated below on the left.

As a result, we can define $\lambda$ by the composition:

$\hat{\mathcal{P}}|X|\rTo^{\sigma_{|X|}}\hat{\mathcal{P}}G|X|\rTo^{\gamma_{X}^{*}}\hat{\mathcal{P}}|FX|.$
(6)

###### Theorem 5.1

The above mapping $\lambda$ is an indexed morphism.

Note that in the case of coKleisli and Eilenberg-Moore categories, we simply
let $G=F$ and $\bar{F}$ be a coKleisli extension/Eilenberg-Moore lifting of
$F$, which results in a distributive law of type
$|\bar{F}\\_|\rTo^{\gamma}G|\\_|$; in the case of Eilenberg-Moore categories,
such natural transformations are also known as EM-laws [20].

In the case of Kleisli categories, the situation is slightly complicated. This
stems from the fact that the distributive law $FT\rTo^{\vartheta}TF$ (which
induces a Kleisli extension $\bar{F}$ of $F$) results in a natural
transformation in the ‘wrong’ direction $F|\\_|\rTo^{\vartheta}|\bar{F}\\_|$.
However, in various applications, $G$ is typically associated with the
branching type of a deterministic version of the corresponding system of
interest (such as $G=\\_^{\mathit{Act}}\times 2$ in the case of NDA) exists.
The next result helps in finding such a distributive law $\gamma$ for a given
$G$ in a more elementary way.

######  Lemma 2 ()

Let $\bar{F}$ be a Kleisli extension of $F$ induced by a distributive law
$FT\rTo^{\vartheta}TF$. Then a natural transformation $TF\rTo^{\gamma}GT$
compatible with $\vartheta$ and $\mu$ (i.e., Square
LABEL:eq:thetamu_compatible commutes) induces a distributive law
$|\\_|\circ\bar{F}\rTo G\circ|\\_|$. Moreover, the converse also holds.

###### Remark 4

Note that the compatibility property in the above lemma appeared in [20] as
part of an ‘extension’ natural transformation. In short, the properties of an
extension natural transformation are more stringent than of Lemma 2.

#### Lifting of relation liftings

The above idea can also be used to construct a relation lifting, i.e., an
indexed morphism of type $\Psi\rTo\Psi\bar{F}$, where $\Psi$ is the indexed
category of abstract relations given in (4). So now given a relation lifting
$\hat{\mathcal{P}}(X\times X)\rTo^{\sigma_{X}}\hat{\mathcal{P}}(GX\times GX)$
of $G$, then we can define $\Psi\rTo^{\bar{\lambda}}\Psi\bar{F}$: Here, we use
the fact that $\mathbb{E}(\hat{\mathcal{P}})$ is a bifibration [16], i.e., for
any function $X\rTo^{f}Y$ the reindexing functor ${f}^{-1}$ has the direct
image functor $f_{!}$ as its left adjoint. Now under the following assumption
we can show that the $\bar{\lambda}$ is indeed an indexed morphism.

  1. A4

The square drawn in (LABEL:eq:squarepbk) is a weak pullback in $\mathbf{Set}$
for every $f\in\mathbf{C}$.

The above assumption ensures that, in the context of
$\mathbb{E}(\hat{\mathcal{P}})$, the square in (LABEL:eq:squarepbk) satisfies
the Beck-Chevalley condition, i.e., the following equation holds

$\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}\circ{(f\otimes
f)}^{-1}={(|f|\times|f|)}^{-1}\circ\langle|\pi_{1}^{Y}|,|\pi_{2}^{Y}|\rangle_{!}\enspace.$

In turn this equation is used in diagram chasing to show that $\bar{\lambda}$
is a natural transformation. Furthermore, A4 trivially holds when $\mathbf{C}$
is a Kleisli or Eilenberg-Moore category (cf. Corollary 1) because the
canonical function $\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle$ is a bijection
for each $X\in\mathbf{C}$. In other words, when $\mathbf{C}$ is a Kleisli or
Eilenberg-Moore category, $\Psi$ can be alternatively defined as the
composition $\hat{\mathcal{P}}\circ(|\\_|\times|\\_|)$.

######  Theorem 5.2 ()

Under A4 $\bar{\lambda}$ as defined in (LABEL:eq:liftofRlift) is an indexed
morphism.

###### Corollary 1

If the forgetful functor $\mathbf{C}\rTo^{|\\_|}\mathbf{Set}$ is product
preserving, then A4 is always satisfied. As a result, $\bar{\lambda}$ defined
in (LABEL:eq:liftofRlift) is an indexed morphism.

##  6 Nondeterministic automata (NDA)

Recall the necessary parameters from Example 1 for coalgebraic modelling of an
NDA, i.e., $T=\mathcal{P}$,
$\mathbf{C}=\mathbf{Kl}(\mathcal{P})\cong\mathbf{Rel}$,
$F=\mathit{Act}\times{\\_}+1$, the distributive law $\vartheta$ given in (2),
and the free-forgetful adjunction $\iota\dashv|\\_|$ associated with any
Kleisli category. To apply Theorem 4.3, we also recall the reflective
subcategory ${\mathbf{Set}}^{\text{op}}$ of $\mathbf{Rel}$ from [1]. Below
$X\rTo^{f}Y\in\mathbf{Set}$ and $X\rTo^{g}Y\in\mathbf{Rel}$:

$\displaystyle\jmath X=$ $\displaystyle X$ $\displaystyle Y\rTo^{\jmath
f}X\in\mathbf{Rel}$ $\displaystyle y\mathrel{\jmath f}x\iff fx=y$
$\displaystyle\mathfrak{r}X=$ $\displaystyle\mathcal{P}X$
$\displaystyle\mathfrak{r}X\rTo^{\mathfrak{r}g}\mathfrak{r}Y\in{\mathbf{Set}}^{\text{op}}$
$\displaystyle\mathfrak{r}g(V)=\\{x\mid\exists_{y\in V}\ x\mathrel{g}y\\}.$

$x$$z$$a$$y$$a,b$

Next we illustrate the definition of $\bar{\mathcal{S}}$ and how the unit of
$\bar{\mathcal{S}}\dashv\bar{\mathcal{T}}$ maps an NDA to the largest
subautomaton (respecting language equivalence) obtained after backward
determinisation of the given NDA. It is worthwhile to note that the abstract
and concrete state space coincide (up to isomorphism) in the case of NDA
because forgetful functor preserves products, i.e.,
$\mathcal{P}(X+X)=|X+X|\cong|X|\times|X|=\mathcal{P}X\times\mathcal{P}X$.
Therefore, as mentioned earlier, we will simplify our presentation by working
with the indexed category $\hat{\mathcal{P}}\circ(|\\_|\times|\\_|)$.

###### Example 4

Consider the NDA drawn above on the right with the accepting state $z$ as a
coalgebra $X\rTo^{\alpha}\mathit{Act}\times X+1\in\mathbf{Kl}(\mathcal{P})$.
Logical equivalence $\simeq$ is the least equivalence that equates $\\{x,y\\}$
with $\\{y\\}$ (both accept the language $\\{a,b\\}$) and $\\{x,y,z\\}$ with
$\\{y,z\\}$ (both accept the language $\\{a,b,\epsilon\\}$). Also, for any
$U,U^{\prime}\subseteq X$ such that $U\mathrel{R}U^{\prime}$ we have
$(U,U^{\prime})\mathrel{p_{1}^{\prime}}x\iff x\in U$ and
$(U,U^{\prime})\mathrel{p_{2}^{\prime}}x\iff x\in U^{\prime}$. Note that
$p_{i}^{\prime}$ are transpose of $p_{i}$ for $i\in\\{1,2\\}$ (see
(LABEL:eq:coequaliser)). So the equaliser $\bar{\mathcal{S}}(X,\simeq)$ of
$\mathfrak{r}p_{i}^{\prime}$ can be computed as follows:

$\bar{\mathcal{S}}(X,\simeq)=\big{\\{}W\in\mathcal{P}X\mid\forall_{U,V}\
(U\cap W\neq\emptyset\land U\simeq V)\implies V\cap W\neq\emptyset\big{\\}}.$

The arrow
$\bar{\mathcal{S}}(X,\simeq)\rTo^{\beta}F\bar{\mathcal{S}}(X,\simeq)\in{\mathbf{Set}}^{\text{op}}$
is defined by the following (depicted on the left) universal property of
equaliser in $\mathbf{Set}$. Here, $\bar{\mathfrak{r}}\alpha$ is the backward
determinisation of the given coalgebra (as described, e.g. in [1] as a
deterministic automaton accepting the reverse language), i.e. it maps
$(a,U)\mapsto\\{x\mid\exists_{x^{\prime}\in U}(a,x^{\prime})\in\alpha(x)\\}$
and $\bullet\mapsto\\{x\mid\bullet\in\alpha(x)\\}$. Thus, in essence, $\beta$
acts like $\bar{\mathfrak{r}}\alpha$ on the elements of
$\bar{\mathcal{S}}(X,\simeq)$.

$\emptyset$$\\{x,y\\}$$\\{y\\}$$\\{z\\}$$\\{y,z\\}$$\\{x,y,z\\}$$y$$x$$z$$a,b$$a,b$$a$$b$$a$$b$$a$$b$$a,b$$a$$a,b$

In this example, we obtain as $\beta$ the automaton drawn above on the right
with six states. The relation $\kappa_{X}$ indicated by dotted line is the
transpose of $e_{X}$ w.r.t. $\mathfrak{r}\dashv\jmath$; concretely,
$x\mathrel{\kappa_{X}}U\iff x\in U$. Furthermore $\kappa_{X}\in\mathbf{Rel}$
is a witnessing coalgebra homomorphism because
$\bar{F}(\kappa_{X})\circ\alpha=\beta\circ\kappa_{X}$. Note that
$|\kappa_{X}|$ maps both $\\{x,y\\},\\{y\\}$ to
$\\{\\{x,y\\},\\{y\\},\\{y,z\\},\\{x,y,z\\}\\}$, witnessing the fact that they
are language equivalent. Hence, the coequaliser gives us the largest sub-
automaton of the backwards determinisation that respects logical equivalence
(removing $\emptyset$, $\\{y,z\\}$, and $\\{x,y,z\\}$ will result in the
smallest such sub-automaton).

#### Predicate liftings for NDAs

To apply techniques from Section 5, we set $G=\\_^{\mathit{Act}}\times 2$ and
define $\gamma$ as follows:

$\displaystyle\mathcal{P}(\mathit{Act}\times
X+1)\rTo^{\gamma_{X}}(\mathcal{P}X)^{\mathit{Act}}\times
2\qquad\quad\quad\bar{U}\mapsto(\gamma_{X}^{\mathit{Act}}\bar{U},\gamma_{X}^{2}\bar{U}),$
where $\displaystyle\
\gamma_{X}^{\mathit{Act}}\bar{U}(a)=\\{x\mid(a,x)\in\bar{U}\\}\qquad\text{and}\qquad\gamma_{X}^{2}\bar{U}=1\iff\bullet\in\bar{U}.$

Moreover, from [20] we know that $\gamma$ is compatible with $\theta$ and
$\bigcup$ in the sense of Lemma 2. Next consider the family of liftings
$\hat{\mathcal{P}}X\rTo^{\sigma_{X}^{a}}\hat{\mathcal{P}}(X^{\mathit{Act}}\times
2)$ (for each $a\in\mathit{Act}$) and
$\hat{\mathcal{P}}X\rTo^{\sigma_{X}^{\downarrow}}\hat{\mathcal{P}}(X^{\mathit{Act}}\times
2)$: $U\mapsto\\{(p,b)\in X^{\mathit{Act}}\times 2\mid p(a)\in U\\}$ and
$U\mapsto\\{(p,1)\mid p\in X^{\mathit{Act}}\\}$, respectively.

######  Lemma 3 ()

The above mappings $\sigma_{X}^{a}$ and $\sigma_{X}^{\downarrow}$ are indexed
morphisms.

Thanks to Theorem 5.1,
$\lambda^{a}={\gamma}^{-1}\circ\sigma^{a},\lambda^{\downarrow}={\gamma}^{-1}\circ\sigma^{\downarrow}$
are valid predicate liftings for the functor
$\mathbf{Rel}\rTo^{\overline{\mathit{Act}\times\\_+1}}\mathbf{Rel}$. Moreover,
for any $\mathbb{U}\subseteq\mathcal{P}X$ we find:

$\displaystyle\lambda_{X}^{a}$ $\displaystyle(\mathbb{U})=\
{\gamma_{X}}^{-1}\sigma_{\mathcal{P}X}^{a}(\mathbb{U})$
$\displaystyle\lambda_{X}^{\downarrow}$ $\displaystyle(\mathbb{U})=\
{\gamma_{X}}^{-1}\sigma_{\mathcal{P}X}^{\downarrow}(\mathbb{U})$
$\displaystyle=$ $\displaystyle\
{\gamma_{X}}^{-1}\\{(p,b)\in(\mathcal{P}X)^{\mathit{Act}}\times 2\mid
p(a)\in\mathbb{U}\\}$ $\displaystyle=$ $\displaystyle\
{\gamma_{X}}^{-1}\\{(p,1)\mid p\in(\mathcal{P}X)^{\mathit{Act}}\\}$
$\displaystyle=$ $\displaystyle\ \left\\{\bar{U}\in\mathit{Act}\times
X+1\mid\\{x\mid(a,x)\in\bar{U}\\}\in\mathbb{U}\right\\}$ $\displaystyle=$
$\displaystyle\ \left\\{\bar{U}\in\mathit{Act}\times
X+1\mid\bullet\in\bar{U}\right\\}.$

The above indexed morphisms $\lambda^{a},\lambda^{\downarrow}$ induce
modalities that can be interpreted on determinised automata. Given an NDA
$(X,\mathit{Act},\rightarrow,\downarrow)$ with $\downarrow\subseteq X$ being
the termination predicate (or $X\rTo^{\alpha}\mathcal{P}(\mathit{Act}\times
X+1)\in\mathbf{Set}$), then the determinised automaton has state space
$\mathcal{P}X$ with dynamics given by the SOS rules or abstractly by the
composition $\gamma_{X}\circ\bigcup\circ\mathcal{P}\alpha$:

$U\xrightarrow{a}U_{\alpha}U\subseteq X\quad
U_{\alpha}=\\{x^{\prime}\mid\exists_{x\in U}\
x\xrightarrow{a}x^{\prime}\\}\qquad U\downarrow U\subseteq
X\qquad\exists_{x\in U}\ x\downarrow\enspace.$

In turn, we can now rewrite the two modalities to a simpler form:

$\displaystyle{|\alpha|}^{-1}$ $\displaystyle\lambda_{X}^{a}\mathbb{U}=\
{|\alpha|}^{-1}\\{\bar{U}\mid\\{x\mid(a,x)\in\bar{U}\\}\in\mathbb{U}\\}$
$\displaystyle{|\alpha|}^{-1}$
$\displaystyle\lambda_{X}^{\downarrow}\mathbb{U}=\
{|\alpha|}^{-1}\left\\{\bar{U}\mid\bullet\in\bar{U}\right\\}$ $\displaystyle=$
$\displaystyle\ \\{U\mid U\xrightarrow{a}U_{\alpha}\implies
U_{\alpha}\in\mathbb{U}\\}$ $\displaystyle=$ $\displaystyle\ \\{U\mid
U\downarrow\\}.$

#### Language equivalence through relation lifting

First note that products exists in $\mathbf{Kl}(\mathcal{P})$ and are given by
disjoint union. Moreover, Assumption A4 is trivially satisfied since the
forgetful functor preserves all limits (cf. Corollary 1). So we can create a
relation lifting of $\bar{F}$ from the following relation lifting
$\hat{\mathcal{P}}(X\times X)\rTo^{\bar{\sigma}_{X}}\hat{\mathcal{P}}(GX\times
GX)$ of $G$ (below $R\subseteq X\times X$):

$(p,b)\mathrel{\bar{\sigma}_{X}R}(p^{\prime},b^{\prime})\iff
b=b^{\prime}\land\forall_{a\in\mathit{Act}}\
pa\mathrel{R}p^{\prime}a\enspace.$

######  Lemma 4 ()

The mapping $\bar{\sigma}$ defined above is an indexed morphism.

So $\Psi\rTo^{\bar{\lambda}}\Psi\bar{F}$ given in (LABEL:eq:liftofRlift) is an
indexed morphism. Concretely, it maps a relation
$R\subseteq\mathcal{P}X\times\mathcal{P}X$ to a relation
$\bar{\lambda}_{X}R\subseteq\mathcal{P}FX\times\mathcal{P}FX$:
$\bar{U}\mathrel{\bar{\lambda}_{X}R}\bar{U}^{\prime}$ iff

$\left(\bullet\in\bar{U}\iff\bullet\in\bar{U}^{\prime}\right)\land\left(\forall_{a\in\mathit{Act}}\
\\{x\mid(a,x)\in\bar{U}\\}\mathrel{R}\\{x\mid(a,x)\in\bar{U}^{\prime}\\}\right)\enspace.$

######  Lemma 5 ()

The indexed morphism $\bar{\sigma}$ preserves arbitrary intersections at each
component; therefore, so does the predicate lifting $\bar{\lambda}$. Moreover,
$\bar{\lambda}$ satisfies A2.

######  Theorem 6.1 ()

Let $X\rTo^{\alpha}FX\in\mathbf{Rel}$ be an NDA. Then language equivalence
$\simeq_{X}\subseteq\mathcal{P}X\times\mathcal{P}X$ on the determinised system
is a $\Psi(\alpha)\circ\bar{\lambda}_{X}$-coalgebra, i.e.,
$\simeq_{X}\subseteq{(|\alpha|\times|\alpha|)}^{-1}(\bar{\lambda}_{X}\simeq_{X})$.
Moreover, $\simeq_{X}={(|f|\times|f|)}^{-1}\simeq_{Y}$ for any coalgebra
homomorphism $f$ between $(X,\alpha)$ and $(Y,\beta)$; thus, there is a
behavioural conformance functor
$\mathbf{Coalg}_{\mathbf{Rel}}(\bar{F})\rTo^{\mathbbm{1}^{\bar{\lambda}}}\mathbf{Coalg}_{\mathbb{E}(\Psi)}(\bar{F}_{\lambda})$.

#### Logical characterisation of language equivalence

Recall the adjoint situation $\mathfrak{r}\dashv\jmath$ that witnesses
${\mathbf{Set}}^{\text{op}}$ is a reflective subcategory of $\mathbf{Rel}$. We
use this dual adjunction to model our logic because (intuitively) conjunction
is not needed to characterise language equivalence. Thus we fix
$\mathbf{A}=\mathbf{Set}$, $S=\mathfrak{r}$, and $T=\jmath$. Moreover, a left
adjoint $\bar{\mathcal{S}}$ of $\bar{\mathcal{T}}$ exists due to Theorem 4.3.

Since to establish language equivalence one needs to ascertain whether a word
in ${\mathit{Act}}^{\star}$ is accepting or not, so we take our syntax functor
$L=\mathit{Act}\times{\\_}+1$. Note that the initial algebra of $L$ exists and
is given by $\mathcal{A}={\mathit{Act}}^{\star}$. As for the one-step
semantics given by a natural transformation $\delta$, we are going to define
it (indirectly) by defining its mate
$L\mathcal{S}X=\mathit{Act}\times\mathcal{P}X+1\rTo^{\theta_{X}}\mathcal{P}(\mathit{Act}\times
X+1)=\mathcal{S}\bar{F}X\in\mathbf{Set}$ that acts on objects like the
distributive law $\vartheta_{X}$ (see (2)). Note that, however, they differ in
their naturality conditions.

######  Proposition 4 ()

The above defined mapping $\theta$ is a natural transformation.

The algebra
$\mathit{Act}\times{\mathit{Act}}^{\star}+1\rTo^{h}{\mathit{Act}}^{\star}$ is
given by the unary concatenation of words and the constant $\varepsilon$
(i.e., $h(a,w)=aw$ and $h\bullet=\varepsilon$). Consider the map
$X\rTo^{\llparenthesis\\_\rrparenthesis}\mathcal{A}\in\mathbf{Rel}$ that maps
a state to the language accepted by it.

######  Corollary 2 ()

The above map $\llparenthesis\\_\rrparenthesis$ is indeed the theory map for a
given NDA. So the logic $(L,\delta)$ is both adequate and expressive for
language equivalence on determinised systems.

##  7 Conditional transition systems: an application in coKleisli categories

We next consider conditional transition systems (CTSs) [1], strongly related
to the featured transition systems used for modelling software product lines
[9]. A conditional transition system is a compact representation of several
transition systems – one for each condition or product – where transitions are
labelled by products. Here we consider the simpler case of conditional
transition systems without upgrades and action labels; their full treatment
[3, 5] is left for the future. In our earlier work, CTSs were coalgebras
living in the Kleisli category induced by the reader monad $\\_^{\mathbb{K}}$
(for a fixed set of conditions $\mathbb{K}$). It is however more convenient to
treat CTSs as coalgebras in coKleisli categories, hence we start with a
relevant comonad $G=\mathbb{K}\times\\_$ whose counit is given by the
projection of the second component and comultiplication $\Delta$ is given by
the diagonal map. The map $\mathbb{K}\times
X\rTo^{\Delta_{X}}\mathbb{K}\times\mathbb{K}\times X$ is given by
$(k,x)\mapsto(k,k,x)$ (for $k\in\mathbb{K},x\in X$).

Consider the coKleisli category $\mathbf{coKl}(G)$ whose objects, just like in
any Kleisli category, are sets; an arrow $X\rTo^{f}Y$ corresponds to a
function $GX\rTo^{f}Y$. Now there is a forgetful functor
$\mathbf{coKl}(G)\rTo^{|\\_|}\mathbf{\mathbf{Set}}$; however, in contrast to
the Kleisli setting, it is now left adjoint to the inclusion
$\mathbf{\mathbf{Set}}\rTo^{\iota}\mathbf{coKl}(G)$. Concretely, this
forgetful functor maps an object $X\mapsto GX$ and an arrow
$X\rTo^{f}Y\in\mathbf{coKl}(G)$ to a function $|f|$ mapping
$(k,x)\mapsto(k,f(k,x))$.

Next to model the branching type of CTSs, take $\bar{F}$ to be the coKleisli
extension [3] of $F=\mathcal{P}$ given by the following distributive law
$\mathbb{K}\times\mathcal{P}X\rTo^{\gamma_{X}}\mathcal{P}(\mathbb{K}\times
X)$: $\gamma_{X}(k,U)=\\{k\\}\times U$; concretely, $\bar{F}X=\mathcal{P}X$
and $\bar{F}f(k,U)=\\{f(k,x)\mid x\in U\\}$ for
$X\rTo^{f}Y\in\mathbf{coKl}(G)$. A CTS modelled as a coalgebra
$X\rTo^{\alpha}\bar{F}X\in\mathbf{coKl}(G)$ is a function $\mathbb{K}\times
X\rTo^{\alpha}\mathcal{P}X$ that assigns to each state $x\in X$ and each
condition $k\in\mathbb{K}$, the successors of $x$ under condition $k$.

As mentioned earlier in Section 5, it is easier (than in the Kleisli case) to
lift a predicate lifting $\hat{\mathcal{P}}\rTo^{\sigma}\hat{\mathcal{P}}F$ of
$F$ to define a predicate lifting
$\hat{\mathcal{P}}|\\_|\rTo^{\lambda}\hat{\mathcal{P}}|\bar{F}\\_|$ of
$\bar{F}$. In particular, $\lambda$ is given by the composition in (6) and,
moreover, Theorem 5.1 ensures that $\lambda$ is indeed an indexed morphism
once we have fixed the predicate lifting $\sigma$ of $F$. To this end, we
simply take $\sigma$ that corresponds to the box modality (cf. Example 2). To
answer whether these definitions give the right kind of ‘box’ modality for
CTSs, let us first instantiate $\lambda_{X}$ for any
$U\subseteq\mathbb{K}\times X$:

$\lambda_{X}U={\gamma}^{-1}_{X}\sigma_{X}U={\gamma}^{-1}_{X}\\{U^{\prime}\mid
U^{\prime}\subseteq U\\}=\\{(k,U^{\prime})\mid\\{k\\}\times
U^{\prime}\subseteq U\\}.$ (7)

Now given a coalgebra $\mathbb{K}\times
X\rTo^{\alpha}\mathcal{P}X\in\mathbf{Set}$, we derive the interpretation of
box modality for CTSs in the following way (below
$x\xrightarrow{k}x^{\prime}\iff x^{\prime}\in\alpha xk$):

${|\alpha|}^{-1}\lambda_{X}U=\\{(k,x)\mid\forall_{x^{\prime}}\
x\xrightarrow{k}x^{\prime}\implies(k,x^{\prime})\in U\\}.$ (8)

#### Conditional bisimilarity through relation lifting

Next we introduce conditional bisimilarity in which two states might be
bisimilar for all conditions or only under certain conditions.

###### Definition 6

Given a CTS $X\rTo^{\alpha}\bar{\mathcal{P}}X\in\mathbf{coKl}(G)$, a
_conditional bisimulation_ is a relation $R\subseteq(\mathbb{K}\times
X)\times(\mathbb{K}\times X)$ satisfying:

1

$\forall_{k,k^{\prime}\in\mathbb{K},x,x^{\prime}\in X}\
(k,x)\mathrel{R}(k^{\prime},x^{\prime})\implies k=k^{\prime}$.

2

$\forall_{x_{1},x_{2},x_{3},k}\big{(}x_{1}\xrightarrow{k}x_{3}\land(k,x_{1})\mathrel{R}(k,x_{2})\big{)}\Rightarrow\exists_{x_{4}\in
X}\big{(}x_{2}\xrightarrow{k}x_{4}\land(k,x_{3})\mathrel{R}(k,x_{4})\big{)}$.

Two states $x,x^{\prime}\in X$ are _conditional bisimilar under $k$_ iff there
is a conditional bismulation relation $R$ such that
$(k,x)\mathrel{R}(k,x^{\prime})$. Moreover, two states $x,x^{\prime}$ are
_conditional bisimilar_ , denoted $x\leftrightarroweq_{X}x^{\prime}$, iff $x$
and $x^{\prime}$ are conditional bisimilar under every condition
$k\in\mathbb{K}$.

In order to capture conditional bisimilarity, we first need a fibration $\Psi$
of binary relations on the state space. The first choice for $\Psi$ is to
consider the set of all binary relations on the underlying state space, i.e.,
$\Psi=\hat{\mathcal{P}}(|\\_|\times|\\_|)$. Unfortunately, Assumption A3 fails
to hold which we explain next.

###### Remark 5

We argue that $\mathrm{Eq}$ cannot have a left adjoint since it does not
preserve finite limits (in particular, terminal objects). Clearly, $\iota
1=1=\\{\bullet\\}$ is the terminal object in $\mathbf{coKl}(G)$ because
$\iota$ is the right adjoint of $|\\_|$. Now suppose
$\mathrm{Eq}1=(1,=_{\mathbb{K}\times 1})$ is the terminal object in
$\mathbb{E}(\Psi)$. Then, for any $(X,R)$, there is a unique arrow
$(X,R)\rTo^{!_{X}}\mathrm{Eq}1$, i.e., $X\rTo^{!_{X}}1\in\mathbf{coKl}(G)$ and
$R\subseteq{(|!_{X}|\times|!_{X}|)}^{-1}=_{\mathbb{K}\times 1}$. But we argue
that $!_{X}$ is _not_ a map in $\mathbb{E}(\Psi)$ for $|\mathbb{K}|\geq 2$. To
see this, let $k,k^{\prime}\in\mathbb{K}$ with $k\neq k^{\prime}$ and let
$R\subseteq(\mathbb{K}\times X)\times(\mathbb{K}\times X)$ be an equivalence
relation such that $(k,x)\mathrel{R}(k^{\prime},x)$. Then we find a
contradiction

$R\subseteq{(|!_{X}|\times|!_{X}|)}^{-1}=_{\mathbb{K}\times
1}\implies(k,!_{X}(k,x))=(k^{\prime},!_{X}(k^{\prime},x))\implies
k=k^{\prime}.$

So we need to restrict ourselves to relations satisfying the first property of
conditional bisimulation (see Definition 6). An elegant way to address this is
by working with the indexed category of abstract relations given in (4); thus,
enabling the applicability of constructions given in Section 5. Note that
binary products $\otimes$ exist in $\mathbf{coKl}(G)$ and is given by the
Cartesian product of two sets. Thus $\Psi$ in (4) is well defined.

######  Lemma 6 ()

Assumptions A3 and A4 are valid.

Now to invoke the definition of $\bar{\lambda}$ in (LABEL:eq:liftofRlift), it
suffices to define a relation lifting $\sigma$ of the set endofunctor
$F=\mathcal{P}$. We take $\sigma$ to be the relation lifting associated with
bisimulation relations as defined in Example 3.

######  Theorem 7.1 ()

Alternatively, the indexed morphism
$\Psi\rTo^{\bar{\lambda}}\Psi\bar{\mathcal{P}}$ given in
(LABEL:eq:liftofRlift) can be defined as follows:
$\bar{\lambda}_{X}R=\\{(k,U,U^{\prime})\mid\forall_{x\in
U}\exists_{x^{\prime}\in U^{\prime}}(k,x,x^{\prime})\in
R\land\forall_{x^{\prime}\in U^{\prime}}\exists_{x\in U}(k,x,x^{\prime})\in
R\\}$. Moreover, $\bar{\lambda}$ satisfies Assumption A2.

###### Corollary 3

Let $X\rTo^{\alpha}\mathcal{P}X\in\mathbf{coKl}(G)$ be a CTS. A relation $R$
on $\mathbb{K}\times X$ is a conditional bisimulation iff
${\langle\pi_{1}^{X},\pi_{2}^{X}\rangle}^{-1}R$ is an
$\alpha^{*}\circ\bar{\lambda}$-coalgebra in $\Psi X$. Moreover, for any
$(X,\alpha)\rTo^{f}(Y,\beta)\in\mathbf{coKl}(G)$ we have
$\leftrightarroweq_{X}={(|f|\times|f|)}^{-1}\leftrightarroweq_{Y}$; thus,
there is a functor
$\mathbf{Coalg}_{\mathbf{coKl}(G)}(\bar{\mathcal{P}})\rTo^{\mathbbm{1}^{\bar{\lambda}}}\mathbf{Coalg}_{\mathbb{E}(\Psi)}(\bar{\mathcal{P}}_{\bar{\lambda}}).$

#### Modal characterisation of conditional bisimilarity

Consider the above adjoint situations where the adjoint situation on the right
is the well known duality (see, for instance [29]) between $\mathbf{Set}$ and
the opposite category of Boolean algebras $\mathbf{BA}$; $\mathcal{S}$ is the
contravariant powerset functor $\hat{\mathcal{P}}$ and $\mathcal{T}$ maps a
Boolean algebra to its set of ultrafilters. We follow [21] and use the
proposed syntax functor $\mathbf{BA}\rTo^{L}\mathbf{BA}$ and the
interpretation $\mathcal{P}\mathcal{T}\rTo^{\delta}\mathcal{T}L$ induced by
the box modality on (unlabelled) transition systems. Since $\bar{\mathcal{P}}$
is a coKleisli extension of $\mathcal{P}$, i.e.,
$\bar{\mathcal{P}}\circ\iota=\iota\circ\mathcal{P}$, we consider the following
logical interpretation for CTSs: $\bar{\mathcal{P}}\circ\iota\circ
T=\iota\circ\mathcal{P}\circ T\rTo^{\iota\delta}\iota\circ T\circ L.$

###### Corollary 4

Since the lifting $\bar{\lambda}$ preserves equalities, the logic
$(L,\iota\delta)$ defined above is adequate for conditional bisimilarity.
Moreover, since $\delta$ is injective in each component [21], the function
$|\iota\delta_{\mathcal{A}}|$ is injective; thus $(L,\iota\delta)$ is
expressive.

##  8 Conclusions

To recapitulate, we gave a systematic way to construct both predicate and
relation liftings in (co)Kleisli categories and Eilenberg-Moore categories.
Relation liftings form the basis to define behavioural equivalence as a
coalgebra of certain lifted endofunctor in the fibre of relations, although in
some cases (such as CTSs) such fibres can be subtle to define.

Once behavioural equivalence is captured as a fibred notion, the Kupke and Rot
setup becomes applicable to obtain its corresponding logical characterisation.
In particular, we gave a recipe to find the left adjoint $\bar{\mathcal{S}}$
of $\bar{\mathcal{T}}$ which is a sufficient condition for both adequacy and
expressivity. For coKleisli and Eilenberg-Moore categories, the construction
(5) of $\bar{\mathcal{S}}$ is based on the existence of coequalisers in the
underlying categories, while in the Kleisli case one has to resort to a
reflective subcategory having coequalisers (cf. Theorem 4.3).

In the future, we plan to develop extend the 2-player game [28] to coalgebras
with side effects. Lastly, we also plan to investigate whether the given
recipe of constructing predicate/relation liftings can be extended to more
general monads (like the ones on pseudometric spaces). This should help in
developing quantitative modal logics for coalgebras with side effects; thus,
providing a pertinent litmus test for the categorical unification of
quantitiative expressivity as claimed in the recent work [26].

## References

  * [1] Adámek, J., Bonchi, F., Hülsbusch, M., König, B., Milius, S., Silva, A.: A coalgebraic perspective on minimization and determinization. In: Proc. of FOSSACS ’12. pp. 58–73. Springer (2012), LNCS/ARCoSS 7213
  * [2] Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and concrete categories: The joy of cats. No. 17, Reprints in Theory and Applications of Categories, online edn. (2006), originally published by: John Wiley and Sons, New York, 1990
  * [3] Beohar, H., König, B., Küpper, S., Silva, A., Wißmann, T.: A coalgebraic treatment of conditional transition systems with upgrades. Logical Methods in Computer Science Volume 14, Issue 1 (Feb 2018). https://doi.org/10.23638/LMCS-14(1:19)2018, https://lmcs.episciences.org/4330
  * [4] Beohar, H., König, B., Küpper, S., Mika-Michalski, C.: Predicate, relation liftings and modal logics for coalgebras with side effects. CoRR abs/2110.09911 (2021), https://arxiv.org/abs/2110.09911
  * [5] Beohar, H., König, B., Küpper, S., Silva, A.: Conditional transition systems with upgrades. Science of Computer Programming 186, 102320 (2020). https://doi.org/10.1016/j.scico.2019.102320
  * [6] Bonchi, F., Bonsangue, M., Caltais, G., Rutten, J., Silva, A.: A coalgebraic view on decorated traces. Mathematical Structures in Computer Science 26(7), 1234–1268 (2016). https://doi.org/10.1017/S0960129514000449
  * [7] Bonchi, F., König, B., Petrisan, D.: Up-To Techniques for Behavioural Metrics via Fibrations. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 118, pp. 17:1–17:17. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.17, http://drops.dagstuhl.de/opus/volltexte/2018/9555
  * [8] Bonchi, F., Petrişan, D., Pous, D., Rot, J.: Coinduction up-to in a fibrational setting. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2603088.2603149
  * [9] Cordy, M., Classen, A., Perrouin, G., Schobbens, P.Y., Heymans, P., Legay, A.: Simulation-based abstractions for software product-line model checking. In: Proc. of ICSE ’12 (International Conference on Software Engineering). pp. 672–682. IEEE (2012)
  * [10] Dorsch, U., Milius, S., Schröder, L.: Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum. In: Fokkink, W., van Glabbeek, R.J. (eds.) 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 140, pp. 36:1–36:16. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https://doi.org/10.4230/LIPIcs.CONCUR.2019.36, http://drops.dagstuhl.de/opus/volltexte/2019/10938
  * [11] Ghani, N., Johann, P., Fumex, C.: Indexed Induction and Coinduction, Fibrationally. Logical Methods in Computer Science Volume 9, Issue 3 (Aug 2013). https://doi.org/10.2168/LMCS-9(3:6)2013, https://lmcs.episciences.org/738
  * [12] Gorín, D., Schröder, L.: Simulations and bisimulations for coalgebraic modal logics. In: Heckel, R., Milius, S. (eds.) Algebra and Coalgebra in Computer Science. pp. 253–266. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)
  * [13] Hasuo, I., Jacobs, B.P.F., Sokolova, A.: Generic Trace Semantics via Coinduction. Logical Methods in Computer Science Volume 3, Issue 4 (Nov 2007). https://doi.org/10.2168/LMCS-3(4:11)2007, https://lmcs.episciences.org/864
  * [14] Hasuo, I., Kataoka, T., Cho, K.: Coinductive predicates and final sequences in a fibration. Mathematical Structures in Computer Science 28(4), 562–611 (2018). https://doi.org/10.1017/S0960129517000056
  * [15] Hermida, C.A., Jacobs, B.P.F.: Structural induction and coinduction in a fibrational setting. Information and Computation 145(2), 107 – 152 (1998)
  * [16] Jacobs, B.P.F.: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier, 1st edn. (Jan 1999)
  * [17] Jacobs, B.P.F.: Trace semantics for coalgebras. Electronic Notes in Theoretical Computer Science 106, 167 – 184 (2004), proceedings of the Workshop on Coalgebraic Methods in Computer Science (CMCS)
  * [18] Jacobs, B.P.F.: Predicate logic for functors and monads. Available from author’s website (2010), http://www.cs.ru.nl/~bart/PAPERS/predlift-indcat.pdf
  * [19] Jacobs, B.P.F.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2016). https://doi.org/10.1017/CBO9781316823187
  * [20] Jacobs, B.P.F., Silva, A., Sokolova, A.: Trace semantics via determinization. Journal of Computer and System Sciences 81(5), 859 – 879 (2015), 11th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2012 (Selected Papers)
  * [21] Jacobs, B.P.F., Sokolova, A.: Exemplaric expressivity of modal logics. Journal of Logic and Computation 20(5), 1041–1068 (Oct 2010)
  * [22] Kissig, C., Kurz, A.: Generic trace logics (2011), http://arxiv.org/abs/1103.3239, arXiv:1103.3239
  * [23] Klin, B.: The least fibred lifting and the expressivity of coalgebraic modal logic. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J.J.J.M. (eds.) Algebra and Coalgebra in Computer Science. pp. 247–262. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)
  * [24] Klin, B., Rot, J.: Coalgebraic trace semantics via forgetful logics. Logical Methods in Computer Science Volume 12, Issue 4 (Apr 2017). https://doi.org/10.2168/LMCS-12(4:10)2016, https://lmcs.episciences.org/2622
  * [25] Komorida, Y., Katsumata, S., Hu, N., Klin, B., Hasuo, I.: Codensity games for bisimilarity. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–13 (2019). https://doi.org/10.1109/LICS.2019.8785691
  * [26] Komorida, Y., Katsumata, S.y., Kupke, C., Rot, J., Hasuo, I.: Expressivity of quantitative modal logics: Categorical foundations via codensity and approximation. Accepted for publication in LICS’21 (June 2021)
  * [27] König, B., Küpper, S.: A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata. Soft Computing 22(4) (2018)
  * [28] König, B., Mika-Michalski, C.: (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In: Proc. of CONCUR ’18. LIPIcs, vol. 118, pp. 37:1–37:17. Schloss Dagstuhl – Leibniz Center for Informatics (2018)
  * [29] Kupke, C., Pattinson, D.: Coalgebraic semantics of modal logics: An overview. Theoretical Computer Science 412(38), 5070 – 5094 (2011). https://doi.org/10.1016/j.tcs.2011.04.023, CMCS Tenth Anniversary Meeting
  * [30] Kupke, C., Rot, J.: Expressive Logics for Coinductive Predicates. In: Fernández, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 152, pp. 26:1–26:18. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2020). https://doi.org/10.4230/LIPIcs.CSL.2020.26
  * [31] Mulry, P.S.: Lifting theorems for Kleisli categories. In: Proc. of MFPS (Mathematical Foundations of Programming Semantics). pp. 304–319. Springer (1993), LNCS 802
  * [32] Pattinson, D.: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theoretical Computer Science 309(1), 177 – 193 (2003)
  * [33] Pavlovic, D., Mislove, M.W., Worrell, J.B.: Testing semantics: Connecting processes and process logics. In: Johnson, M., Vene, V. (eds.) Algebraic Methodology and Software Technology. pp. 308–322. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)
  * [34] Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1), 3 – 80 (2000)
  * [35] Schröder, L.: Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science 390(2), 230 – 247 (2008)
  * [36] Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science Volume 9, Issue 1 (Mar 2013). https://doi.org/10.2168/LMCS-9(1:9)2013
  * [37] Sprunger, D., Katsumata, S.y., Dubut, J., Hasuo, I.: Fibrational bisimulations and quantitative reasoning. In: Cîrstea, C. (ed.) Coalgebraic Methods in Computer Science. pp. 190–213. Springer International Publishing, Cham (2018)

##  Appendix 0.A Omitted proofs

See 1

###### Proof

Let $X\rTo^{f}Y\in\mathbf{C}$. We need to show that $\equiv_{X}\subseteq
f^{*}\equiv_{Y}$. First consider the the following diagram, where
$p_{i}^{\Box}$ and $\pi_{i}^{\Box}$ (for $i\in\\{1,2\\}$ and
$\Box\in\\{X,Y\\}$) are the obvious projection arrows in $\mathbf{Set}$ and
$\mathbf{C}$, respectively. Note that all the dashed arrows exists due to the
universal property of products. Moreover, it is well known that projection
functions $p_{i}^{Y}$ are jointly monic. So it suffices to show that the
corresponding outermost paths for each $i$ from $|X\otimes X|$ to $|Y|$
commutes, which follows from diagram chasing. Now the result follows from the
following implications:

$\displaystyle=_{|X|}\subseteq{(|f|\times|f|)}^{-1}=_{|Y|}$
$\displaystyle\Rightarrow{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle}^{-1}\\!=_{|X|}\subseteq{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle}^{-1}{(|f|\times|f|)}^{-1}=_{|Y|}$
$\displaystyle\Rightarrow$ $\displaystyle\
{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle}^{-1}=_{|X|}\subseteq{|f\otimes
f|}^{-1}{\langle|\pi_{1}^{Y}|,|\pi_{2}^{Y}|\rangle}^{-1}=_{|Y|}.$

The second implication holds due to the commutative of rectangle drawn with
dashed edges. ∎

See 3.1

###### Proof

Let $(X,\alpha)\rTo^{f}(Y,\beta)\in\mathbf{Coalg}_{\mathbf{C}}(F)$ be a
coalgebra homomorphism and consider the following commutative diagram. Then
using Assumptions A1, A2 and Proposition 1 we find that
$\equiv_{Y}\subseteq\beta^{*}(\equiv_{FY})=\beta^{*}\lambda_{Y}(\equiv_{Y})$.
Furthermore, we derive

$f^{*}\equiv_{Y}\ \subseteq f^{*}\beta^{*}\lambda_{Y}\equiv_{Y}\implies
f^{*}\equiv_{Y}\
\subseteq\alpha^{*}\lambda_{X}f^{*}\equiv_{Y}.\qquad\squareforqed$

See 3.2

###### Proof

Let $R\in\Psi X$ such that $R\preceq\alpha^{*}\lambda_{X}R$ and let $\kappa$
be the unit of adjunction $\mathbb{Q}\dashv\mathrm{Eq}$. For a given coalgebra
$X\rTo^{\alpha}FX$, we are going to first construct a coalgebra of the form
$\mathbb{Q}(X,R)\rTo^{\alpha_{R}}F\mathbb{Q}(X,R)$ such that $p\kappa_{X}$ is
the witnessing coalgebra homomorphism. To define $\alpha_{R}$, consider the
following diagram in $\mathbb{E}(\Psi)$ without the dashed arrow.

$\begin{diagram}$ (9)

Note that by the assumption we have $\lambda_{X}(\equiv_{X})=\ \equiv_{FX}$
and, since the unit $\kappa_{X}\in\mathbb{E}(\Psi)$, we get that
$R\preceq\kappa_{X}^{*}\equiv_{\mathbb{Q}(X,R)}$. Thus,

$\displaystyle\lambda_{X}R\preceq\lambda_{X}\kappa_{X}^{*}(\equiv_{\mathbb{Q}(X,R)})\implies$
$\displaystyle\
\lambda_{X}R\preceq(F\kappa_{X})^{*}\lambda_{\mathbb{Q}(X,R)}\equiv_{\mathbb{Q}(X,R)}$
$\displaystyle\implies$ $\displaystyle\
\lambda_{X}R\preceq(F\kappa_{X})^{*}\equiv_{F\mathbb{Q}(X,R)}\enspace.$

Thus $F\kappa_{X}$ drawn in (9) is a valid arrow in $\mathbb{E}(\Psi)$. And
the universal property of the unit $\kappa_{X}$ gives a unique arrow
$\mathbb{Q}(X,R)\rTo^{\alpha_{R}}F\mathbb{Q}(X,R)$, i.e., a coalgebraic
structure on $\mathbb{Q}(X,R)$, such that Square (9) commutes. Clearly,
appyling the forgetful functor $p$ ensures that $p\kappa_{X}$ is a coalgebra
homomorphism. ∎

See 1

###### Proof

Define $\mathbbm{1}X=(X,1_{X})$ where $1_{X}$ is the final object in $\Phi X$.
Note for any $X\rTo^{f}Y$, we have
$1_{X}\rTo^{\text{id}_{1_{X}}}1_{X}=f^{*}1_{Y}$ since the reindexing functor
preserves the indexed final objects. Thus, we let
$\mathbbm{1}f=(f,\text{id}_{1_{X}})$. Next we show that $p\dashv\mathbbm{1}$.

$X\rTo^{f}Y\in\mathbf{C}p(X,U)\rTo^{f}Y\in\mathbf{C}(X,U)\rTo^{(g,\bar{g})}\mathbbm{1}Y\in\mathbb{E}(\Phi)(X,U)\rTo^{(g,\bar{g})}(Y,\text{id}_{1_{Y}})\in\mathbb{E}(\Phi)$

$\Uparrow$ Let $X\rTo^{f}Y\in\mathbf{C}$. Then take $g=f$ and let $\bar{g}$ be
the unique arrow $U\rTo^{\bar{g}}1_{X}\in\Phi X$ to the final object
$1_{X}=f^{*}1_{Y}$.

$\Downarrow$ Take $f=g$ and the implication follows from the construction of
$\mathbb{E}(\Phi)$. ∎

See 4.1

###### Proof

For adequacy, we show the conditions of [30, Theorem 18] are satisfied. It
remains to show that there is a natural transformation
$(F\mathcal{T}A,\equiv_{F\mathcal{T}A})=F_{\lambda}\bar{\mathcal{T}}A\rTo^{\bar{\delta}_{A}}\bar{\mathcal{T}}LA=(\mathcal{T}LA,\equiv_{\mathcal{T}LA})$.
We can simply let $\bar{\delta}=\delta$ because $\mathrm{Eq}$ is a functor.
For expressivity, we show that the conditions of [30, Theorem 19] are
satisfied, i.e., the arrow
$(FTA,=_{|T\mathcal{A}|})\rTo^{\delta_{\mathcal{A}}}(TL\mathcal{A},=_{|TL\mathcal{A}|})\in\mathbb{E}(\Psi)$
is Cartesian. But this follows directly from the injectivity of
$|\delta_{A}|$. To see this let $X\rTo^{f}Y$ be an arrow in $\mathbf{C}$ such
that $=_{|X|}\ =\ {(|f|\times|f|)}^{-1}=_{|Y|}$. Then we derive

$\displaystyle{|f\otimes f|}^{-1}(\equiv_{Y})=$ $\displaystyle\ {|f\otimes
f|}^{-1}{\langle|\pi_{1}^{Y}|,|\pi_{2}^{Y}|\rangle}^{-1}(=_{|Y|})$
$\displaystyle\stackrel{{\scriptstyle\eqref{eq:squarepbk}}}{{=}}$
$\displaystyle\
{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle}^{-1}{(|f|\times|f|)}^{-1}=_{|Y|}$
$\displaystyle=$ $\displaystyle\
{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle}^{-1}(=_{|X|})$ $\displaystyle=$
$\displaystyle\ \equiv_{X}.$

See 4.3

###### Proof

Due to A1 product exists in $\mathbf{Kl}(T)$ and the forgetful functor
preserves these products. So we can work with concrete equality $=_{|X|}$
instead of $\equiv_{X}$ (for $X\in\mathbf{Kl}(T)$) by showing that
$\bar{\mathcal{S}}\dashv\bar{\mathcal{T}}$, i.e., the following correspondence
holds

$Y\rTo^{g}\bar{\mathcal{S}}(X,R)\in\mathbf{A}\bar{\mathcal{S}}(X,R)\rTo^{g}Y\in{\mathbf{A}}^{\text{op}}(X,R)\rTo^{f}(\jmath
Y,=_{|\jmath|Y})\in\mathbb{E}(\Psi)X\rTo^{f}\jmath Y\in\mathbf{Kl}(T)\land
R\subseteq{(|f|\times|f|)}^{-1}=_{|\jmath Y|}$

$\Downarrow$ Let $X\rTo^{f}\jmath Y\in\mathbf{Kl}(T)$ such that
$R\subseteq{(|f|\times|f|)}^{-1}=_{|\jmath Y|}$. Then we find a unique
$Y\rTo^{g}\mathfrak{r}X\in\mathbf{A}$ as the transpose of $f$ under
$\mathfrak{r}\dashv\jmath$. Moreover, using the counit of $\iota\dashv|\\_|$
one can show that if $|f|\circ p_{1}=|f|\circ p_{2}\implies f\circ
p_{1}^{\prime}=f\circ p_{2}^{\prime}$. Thus, $\mathfrak{r}p_{1}^{\prime}\circ
g=\mathfrak{r}p_{2}^{\prime}\circ g$. And by the universal property of
equalisers we find a unique $Y\rTo^{u_{g}}\bar{\mathcal{S}}(X,R)$.

$\Uparrow$ Let $Y\rTo^{g}\bar{\mathcal{S}}(X,R)\in\mathbf{A}$. Then take $f$
as the transpose of $e\circ g$ under $\mathfrak{r}\dashv\jmath$. To show that
$f\circ p_{1}^{\prime}=f\circ p_{2}^{\prime}$ consider the following
commutative diagram in $\mathbf{Kl}(T)$, where $\eta$ is the unit of
$\mathfrak{r}\dashv\jmath$.

See 2

###### Proof

Let $C\rTo^{f}D\in\mathbf{Kl}(T)$. Then we need to show that the following
square on the left commutes. But this follows immediately by the commutative
diagram drawn on the right, where the top square commutes due to the
naturality of $\gamma$.

For the converse, take $f=\text{id}_{TC}$ and view it as a Kleisli arrow
$TC\rTo C$.

See 3

###### Proof

Let $V\subseteq Y$ and $X\rTo^{f}Y$ be a function. Then,

$\displaystyle{(f^{\mathit{Act}}\times
2)}^{-1}\sigma_{Y}^{a}V={(f^{\mathit{Act}}\times 2)}^{-1}\\{(q,b)\in
Y^{\mathit{Act}}\times 2\mid qa\in V\\}$ $\displaystyle=$ $\displaystyle\
\left\\{(p,b^{\prime})\in X^{\mathit{Act}}\times 2\mid(f^{\mathit{Act}}\times
2)(p,b^{\prime})\in\\{(q,b)\mid qa\in V\\}\right\\}$ $\displaystyle=$
$\displaystyle\ \left\\{(p,b^{\prime})\in X^{\mathit{Act}}\times 2\mid(f\circ
p,b^{\prime})\in\\{(q,b)\mid qa\in V\\}\right\\}$ $\displaystyle=$
$\displaystyle\ \\{(p,b)\mid f(pa)\in V\\}$ $\displaystyle=$ $\displaystyle\
\\{(p,b)\mid pa\in{f}^{-1}V\\}$ $\displaystyle=$ $\displaystyle\
\sigma_{X}^{a}{f}^{-1}V.$

For the mapping associated with termination, we derive

$\displaystyle{(f^{\mathit{Act}}\times
2)}^{-1}\sigma_{Y}^{\downarrow}V={(f^{\mathit{Act}}\times 2)}^{-1}\\{(q,1)\mid
q\in Y^{\mathit{Act}}\\}$ $\displaystyle=$ $\displaystyle\ \left\\{(p,b)\in
X^{\mathit{Act}}\times 2\mid(f^{\mathit{Act}}\times 2)(p,b)\in\\{(q,1)\mid
q\in Y^{\mathit{Act}}\\}\right\\}$ $\displaystyle=$ $\displaystyle\
\left\\{(p,1)\in X^{\mathit{Act}}\times 2\mid f\circ p\in
Y^{\mathit{Act}}\right\\}$ $\displaystyle=$ $\displaystyle\
\sigma_{X}^{\downarrow}{f}^{-1}V.\qquad\squareforqed$

See 4

###### Proof

Let $R,R^{\prime}$ be two binary relations on $X$ such that $R\subseteq
R^{\prime}$. We first show that
$\bar{\sigma}_{X}R\subseteq\bar{\sigma}_{X}R^{\prime}$. Let
$(p,b)\mathrel{\bar{\sigma}_{X}R}(p^{\prime},b)$. Then we find
$\forall_{a\in\mathit{Act}}\ (pa\mathrel{R}p^{\prime}a\implies
pa\mathrel{R^{\prime}}p^{\prime}a)$. Thus,
$(p,b)\mathrel{\bar{\sigma}_{X}R}(p^{\prime},b)$.

Lastly, we need to show that the equation $\bar{\sigma}_{X}\circ{(f\times
f)}^{-1}={(Gf\times Gf)}^{-1}\circ\bar{\sigma}_{Y}$ holds. Below $S$ is a
relation on $Y$.

$\displaystyle(p,b)\mathrel{\bar{\sigma}_{X}\circ{(f\times
f)}^{-1}S}(p^{\prime},b^{\prime})$ $\displaystyle\iff\
b=b^{\prime}\land\forall_{a}\ pa\mathrel{{(f\times f)}^{-1}}p^{\prime}a$
$\displaystyle\iff$ $\displaystyle\ b=b^{\prime}\land\forall_{a}\
fpa\mathrel{R}fp^{\prime}a$ $\displaystyle\iff$ $\displaystyle\ (f\circ
p,b)\mathrel{\bar{\sigma}_{Y}S}(f\circ p^{\prime},b^{\prime})$
$\displaystyle\iff$ $\displaystyle\
Gf(p,b)\mathrel{\bar{\sigma}_{Y}S}Gf(p^{\prime},b^{\prime})$
$\displaystyle\iff$ $\displaystyle\ (p,b)\mathrel{{(Gf\times
Gf)}^{-1}\circ\bar{\sigma}_{Y}S}(p^{\prime},b^{\prime})\enspace.\squareforqed$

See 5

###### Proof

Let $R_{i}$ (for $i\in\mathbb{N}$) be relations on $X$. Then

$\displaystyle(p,b)\mathrel{\left(\sigma_{X}^{G}\left(\bigcap_{i\in\mathbb{N}}R_{i}\right)\right)}(p^{\prime},b^{\prime})\iff$
$\displaystyle\ b=b^{\prime}\land\forall_{a\in\mathit{Act}}\
pa\mathrel{(\bigcap_{i\in\mathbb{N}}R_{i})}p^{\prime}a$ $\displaystyle\iff$
$\displaystyle\ b=b^{\prime}\land\forall_{a\in\mathit{Act},\mathbb{N}}\
pa\mathrel{R_{i}}p^{\prime}a$ $\displaystyle\iff$ $\displaystyle\
\forall_{i\in\mathbb{N}}\ \left(b=b^{\prime}\land\forall_{a\in\mathit{Act}}\
pa\mathrel{R_{i}}p^{\prime}a\right)$ $\displaystyle\iff$ $\displaystyle\
\forall_{i\in\mathbb{N}}\
(p,b)\mathrel{(\sigma_{X}^{G}R_{i})}(p^{\prime},b^{\prime})$
$\displaystyle\iff$
$\displaystyle(p,b)\left(\mathrel{\bigcap_{i\in\mathbb{N}}\
\sigma_{X}^{G}R_{i}}\right)(p^{\prime},b^{\prime})\enspace.$

ote that $\lambda$ is the composition
${(\gamma_{X}\times\gamma_{X})}^{-1}\circ\sigma^{G}$ and since inverse
functions preserve arbitrary intersections, we can conclude that $\lambda$
also preserves intersections at each component.

Lastly, to show that $\bar{\lambda}$ preserves equalities, let
$R==_{\mathcal{P}X}$. Let
$\bar{U},\bar{U}^{\prime}\subseteq\mathit{Act}\times{X}+1$ such that
$\bar{U}\mathrel{\lambda_{X}R}\bar{U}^{\prime}$. Clearly,
$\bullet\in\bar{U}\iff\bullet\in\bar{U}^{\prime}$. So consider
$(a,\bar{x})\in\bar{U}$. Then $\bar{x}\in\\{x\mid(a,x)\in\bar{U}\\}$ and since
the two sets $\\{x\mid(a,x)\in\bar{U}\\},\\{x\mid(a,x)\in\bar{U}^{\prime}\\}$
are the same, we find that $(a,x)\in\bar{U}^{\prime}$. Likewise, we can show
the other direction and we conclude that $\bar{U}=\bar{U}^{\prime}$.

See 6.1

###### Proof

Let $X\rTo^{\alpha}\mathit{Act}\times{X}+1\in\mathbf{Rel}$ be an NDA. Since
the relation lifting $\bar{\lambda}$ preserves intersections, so from Kleene
fixed point theorem, the largest fixpoint $\sim_{X}\in\Psi X$ of
$\alpha^{*}\circ\bar{\lambda}$ exists. That is, the following sequence
stabilises (below $1_{X}\in\Psi X$ is the total relation on $\mathcal{P}X$):

$1_{X}\mathrel{\supseteq}{(|\alpha|\times|\alpha|)}^{-1}\circ\lambda_{X}(\top_{X})\mathrel{\supseteq}({(|\alpha|\times|\alpha|)}^{-1}\circ\lambda_{X})^{2}(\top_{X})\mathrel{\supseteq}\cdots$

Let us denote the above projective sequence as a diagram
$\mathbf{N}\rTo^{D}\Psi X$, i.e.
$Di=({|\alpha|}^{-1}\circ\lambda_{X})^{i}\top_{X}$ (note that the zeroth
iteration of a function is assumed to return the full relation $\top_{X}$ and
$\mathbf{N}$ has the set $\mathbb{N}$ of natural numbers as objects and arrows
induced by the less-than-equal-to relation). So $\sim_{X}=\bigcap_{i}Di$ and
note that by definition $\sim_{X}$ is
$\alpha^{*}\circ\bar{\lambda}$-coalgebra.

Let $U_{w}$ is the unique state reached in the determinised system from the
state $U$ after performing the trace $w$. Note that for any $i>1$ we have:

$U\mathrel{D(i+1)}U^{\prime}\iff(U\downarrow\iff U^{\prime}\downarrow)\ \land\
\forall_{a\in\mathit{Act}}\ U_{a}\mathrel{Di}U_{a}^{\prime}.$

Moreover, it is not hard to show by induction on $w$ that we have

$U\simeq_{X}U^{\prime}\quad\iff\quad\forall_{w\in{\mathit{Act}}^{\star}}\
U_{w}\downarrow\iff U^{\prime}_{w}\downarrow.$

Next we show that $\sim_{X}=\simeq_{X}$. To show that
$\simeq_{X}\subseteq\sim_{X}$, it suffices to show that $\simeq_{X}$ is a
$\alpha^{*}\circ\bar{\lambda}_{X}$-coalgebra, i.e., for any
$U,U^{\prime}\subseteq X$, if $U\simeq_{X}U^{\prime}$ then
$|\alpha|U\mathrel{\lambda_{X}\simeq_{X}}|\alpha|U^{\prime}$. So let
$U\simeq_{X}U^{\prime}$, clearly, $U\downarrow\iff U^{\prime}\downarrow$.
Moreover, $U_{a}\simeq_{X}U_{a}^{\prime}$ (for any $a$) because
$U\simeq_{X}U^{\prime}$. So $\simeq_{X}\subseteq\sim_{X}$.

For the other direction, let $U\sim_{X}U^{\prime}$. Then for any
$w\in{\mathit{Act}}^{\star}$ we have $U\mathrel{D(\\#w+1)}U^{\prime}$, where
$\\#w$ is the length of the word $w$. Thus, $U_{w}\downarrow\iff
U^{\prime}_{w}\downarrow$. Therefore, $U\simeq_{X}U^{\prime}$.

Lastly, let
$(X,\alpha)\rTo^{f}(Y,\beta)\in\mathbf{Coalg}_{\mathbf{Rel}}(\bar{F})$, i.e.,
$X\rTo^{f}Y$ is a relation satisfying the following two transfer properties:

  * •

$\forall_{x,y^{\prime},a}\ \big{(}\exists_{y}\ (x\mathrel{f}y\land
y\xrightarrow{a}y^{\prime})\iff\exists_{x^{\prime}}\
(x^{\prime}\mathrel{f}y^{\prime}\land x\xrightarrow{a}x^{\prime})\big{)}$.

  * •

$\forall_{x}\ \big{(}x\downarrow\iff\exists_{y}\ (x\mathrel{f}y\land
y\downarrow)\big{)}$.

Note that the second transfer property ensures that
$U_{w}\downarrow\iff(|f|U)_{w}\downarrow$, for any $U\subseteq
X,w\in{\mathit{Act}}^{\star}$. This is because

$U_{w}\downarrow\iff\exists_{x\in U_{w}}\ x\downarrow\iff\exists_{x\in
U_{w},y}\ x\mathrel{f}y\land y\downarrow\iff(|f|U_{w})\downarrow.$

Thus, for any $w$ we have $(U_{w}\downarrow\iff
U^{\prime}_{w}\downarrow)\iff\big{(}(|f|U)_{w}\downarrow\iff(|f|U^{\prime})_{w}\downarrow\big{)}$.
Hence $\simeq_{X}={(|f|\times|f|)}^{-1}\simeq_{Y}$.

See 4

###### Proof

We show that the following square commutes for any
$X\rTo^{f}Y\in\mathbf{Rel}$. Let $a\in\mathit{Act},V\subseteq Y$. Then we find

$\displaystyle\mathfrak{r}\bar{(}Ff)\theta_{Y}(a,V)=$ $\displaystyle\
\mathfrak{r}(\bar{F}f)(\\{a\\}\times V)$ $\displaystyle=$ $\displaystyle\
\\{(a^{\prime},x)\mid\exists_{y\in V}\ (a^{\prime},x)\mathrel{Ff}(a,y)\\}$
$\displaystyle=$ $\displaystyle\ \\{(a,x)\mid\exists_{y\in V}\
x\mathrel{f}y\\}$ $\displaystyle=$ $\displaystyle\
\\{a\\}\times\\{x\mid\exists_{y\in V}\ x\mathrel{f}y\\}$ $\displaystyle=$
$\displaystyle\ \\{a\\}\times\mathfrak{r}f(V)$ $\displaystyle=$
$\displaystyle\ \theta_{X}(a,\mathfrak{r}f(V))=\theta_{X}\circ
L(\mathfrak{r}sf)(a,V).$

Likewise, the case for $\bullet\in 1$ can be verified; thus,
$L\mathcal{S}\rTo^{\theta}\mathcal{S}F$ is a natural transformation.

See 6

######  Proof (A4)

Consider the square drawn in (LABEL:eq:squarepbk) and let
$k,k^{\prime},y,y^{\prime},x,x^{\prime}$ be such that
$\langle|\pi_{1}^{Y}|,|\pi_{2}^{Y}|\rangle(k,y,y^{\prime})=|f|\times|f|((k,x),(k^{\prime},x^{\prime}))$.
I.e., $(k,y)=(k,f(k,x))$ and
$(k,y^{\prime})=(k^{\prime},f(k^{\prime},x^{\prime}))$. Thus, we find that
$k=k^{\prime}$. Therefore, we can conclude that $(k,x,x^{\prime})\in|X\otimes
X|$. Moreover, we also find that $|f\otimes f|(k,x,x^{\prime})=(k,f\otimes
f(k,x,x^{\prime}))=(k,f(k,x),f(k,x^{\prime}))=(k,y,y^{\prime})$. Lastly,
$\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle(k,x,x^{\prime})=((k,x),(k,x^{\prime})$.
I.e., the universal property of weak pullback in $\mathbf{Set}$ holds. ∎

######  Proof (A3)

Let $G=\mathbb{K}\times\\_$ and let $(X,R)\in\mathbb{E}(\Psi)$, i.e.,
$X\in\mathbf{Set}$ and $R\in\Psi X$. This means we have the following diagram
in $\mathbf{Set}$:

$R_{!}\pile{\rTo^{p_{1}}\\\ \rTo_{p_{2}}}GX\rTo^{q}GX/R_{!},$

where $GX/R_{!}$ is the coequaliser of $p_{1},p_{2}$ and
$R_{!}=\langle\pi_{1}^{X},\pi_{2}^{X}\rangle_{!}R=\\{((k,x),(k,x^{\prime}))\mid(k,x,x^{\prime})\in
R\\}$. So we define $\mathbb{Q}(X,R)$ to be the object $\iota(GX/R_{!})$. In
other words, $\mathbb{Q}$ can be defined by the composition:

$\mathbb{E}(\Psi)\rTo^{|\\_|_{!}}\mathbb{E}(\Psi^{\prime})\rTo^{\mathbb{Q}^{\prime}}\mathbf{Set}\rTo^{\iota}\mathbf{coKl}(G),$

where $\Psi^{\prime}$ is the standard indexed category of relations on sets
and $\mathbb{Q}^{\prime}$ is the usual quotient functor as described in Remark
2. The functor $|\\_|_{!}$ is defined as: $(X,R)\mapsto(|X|,R_{!})$ and
$f\mapsto|f|$. This is welldefined due to Beck-Chevalley property on the
indexed category $\hat{\mathcal{P}}$, which holds for weak pullback squares.
In particular, let $(X,R)\rTo^{f}(Y,S)\in\mathbb{E}(\Psi)$, i.e.,
$X\rTo^{f}Y\in\mathbf{C}$ and $R\subseteq{(f\otimes f)}^{-1}S$. By applying
the direct image functor we get

$\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}R\subseteq\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}{(f\otimes
f)}^{-1}S={(|f|\times|f|)}^{-1}\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}S.$

Note that the righmost equality holds due to Beck-Chevalley condition and A4.
Therefore $\mathbb{Q}$ is a functor.

Next we show that $\mathbb{Q}\dashv\mathrm{Eq}$, i.e., we establish the
following correspondence:

$X\rTo^{g}Y\in\mathbf{coKl}(G)\land R\subseteq{(|g\otimes
g|)}^{-1}\equiv_{Y}(X,R)\rTo^{g}\mathrm{Eq}Y=(Y,\equiv_{Y})\in\mathbb{E}(\Psi)\iota(GX/R_{!})\rTo^{f}Y\in\mathbf{coKl}(G)$

$\Uparrow$ Let $X\rTo^{g}Y\in\mathbf{coKl}(G)$ (i.e.,
$GX\rTo^{g}Y\in\mathbf{Set}$) and $R\subseteq{(|g\otimes g|)}^{-1}\equiv_{Y}$.
We claim that $g\circ p_{1}=g\circ p_{2}$. So let
$(k,x)\mathrel{R_{!}}(k^{\prime},x^{\prime})$. Then we find $k=k^{\prime}$
because of the construction of $R_{!}$ and $g(k,x)=g(k,x^{\prime})$ because of
the inequality $R\subseteq{(|g\otimes g|)}^{-1}\equiv_{Y}$. This proves the
claim. And from the universal property of coequalisers in $\mathbf{Set}$, we
find a unique function $GX/R\rTo^{g^{\prime}}Y$ satisfying $g^{\prime}\circ
q=g$. So fix $f=\iota g^{\prime}$ and clearly $f$ is uniquely determined by
$g$.

$\Downarrow$ Let $\iota(GX/R)\rTo^{f}Y\in\mathbf{coKl}(G)$. Recall the unit
$X\rTo^{\eta_{X}}\iota|X|\in\mathbf{coKl}(G)$ of the adjunction
$|\\_|\dashv\iota$. Then, let $g$ be the following composition:

$X\rTo^{\eta_{X}}\iota|X|\rTo^{\iota q}\mathbb{Q}(X,R)\rTo^{f}Y\
\in\mathbf{coKl}(G).$

Clearly, $g$ is uniquely determined by $f$. Now it remains to show that for
$k,x,x^{\prime}$, if $(k,x,x^{\prime})\in R$ then $|g\otimes
g|(k,x,x^{\prime})=(k,g\otimes
g(k,x,x^{\prime}))=(k,g(k,x),g(k,x^{\prime}))\in\equiv_{Y}$. Thus it remains
to show that $g(k,x)=g(k,x^{\prime})$.

To this end, we first evaluate $g$. Note that $\eta$ is given by the identity
arrow and using the definition of coKleisli composition we find that

$(k,x)\rMapsto^{\Delta_{X}}(k,k,x)\rMapsto^{G\eta_{X}}(k,k,x)\rMapsto^{\iota
q}q(k,x).$

Thus, $\iota q\circ\eta_{X}=q$. So computing the composition
$X\rTo^{q}\mathbb{Q}(X,R)\rTo^{f}Y\in\mathbf{coKl}(G)$ results in the
evaluation of $g$. In particular,

$g(k,x)=f(Gq(\Delta_{X}(k,x)))=f(k,q(k,x)).$

So if $(k,x,x^{\prime})\in R$ then $q(k,x)=q(k,x^{\prime})$. Thus,
$g(k,x)=f(k,q(k,x))=f(k,q(k,x^{\prime}))=g(k,x^{\prime})$.∎

See 7.1

###### Proof

Recall from (LABEL:eq:liftofRlift), the map $\bar{\lambda}$ is given by the
composition:

$\Psi
X\rTo^{\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}}\hat{\mathcal{P}}(|X|\times|X|)\rTo^{\sigma_{|X|}}\hat{\mathcal{P}}(\mathcal{P}|X|\times\mathcal{P}|X|)\\\
\rTo^{{\gamma_{X}\times\gamma_{X}}^{-1}}\hat{\mathcal{P}}(|\mathcal{P}X|\times|\mathcal{P}X|)\rTo^{{\langle|\pi_{1}^{FX}|,|\pi_{2}^{F}X|\rangle}^{-1}}\Psi\bar{\mathcal{P}}X.$

Let $R\subseteq G(X\times X)$, where $G=\mathbb{K}\times\\_$. Then we compute

$\displaystyle\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}R$ $\displaystyle=\
\\{((k,x),(k,x^{\prime}))\mid(k,x,x^{\prime})\in R\\}$
$\displaystyle\sigma_{|X|}\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}R$
$\displaystyle=\
\Big{\\{}(S,S^{\prime})\in\mathcal{P}|X|\times\mathcal{P}|X|\mid$
$\displaystyle\quad\forall_{k,x}\big{(}k\mathrel{S}x\implies\exists_{x^{\prime}}\
k\mathrel{S^{\prime}}x^{\prime}\land(k,x,x^{\prime})\in R\big{)}\land$
$\displaystyle\quad\forall_{k,x^{\prime}}\big{(}k\mathrel{S^{\prime}}x^{\prime}\implies\exists_{x}\
k\mathrel{S}x\land(k,x,x^{\prime})\in R\big{)}\Big{\\}}$
$\displaystyle{(\gamma_{X}\times\gamma_{X})}^{-1}(\sigma_{|X|}\langle|\pi_{1}^{X}|,|\pi_{2}^{X}|\rangle_{!}R)$
$\displaystyle=\\{((k,U),(k,U^{\prime}))\mid U,U^{\prime}\subseteq X\ \land$
$\displaystyle\forall_{x\in U}\exists_{x^{\prime}\in U^{\prime}}$
$\displaystyle(k,x,x^{\prime})\in R\land\forall_{x^{\prime}\in
U^{\prime}}\exists_{x\in U}(k,x,x^{\prime})\in R\\}$
$\displaystyle\bar{\lambda}R=\ \\{(k,U,U^{\prime})\mid\forall_{x\in
U}\exists_{x^{\prime}\in U^{\prime}}$ $\displaystyle(k,x,x^{\prime})\in
R\land\forall_{x^{\prime}\in U^{\prime}}\exists_{x\in U}(k,x,x^{\prime})\in
R\\}.$

For A2 we first find that

$(k,x,x^{\prime})\in\equiv_{X}\iff(k,x,x^{\prime})\in{\langle\pi_{1}^{X},\pi_{2}^{X}\rangle}^{-1}=_{|X|}\iff(k,x)=(k,x^{\prime}).$

Thus, $\bar{\lambda}_{X}$ preserve abstract equalities. ∎

##  Appendix 0.B Linear Weighted Automaton (LWA)

We consider (linear) weighted automata (LWA) as coalgebras as studied in [20].
LWA are modelled as coalgebras of the endofunctor
$\mathcal{M}_{\mathbb{F}}(1+\mathit{Act}\times\\_)$, where $\mathbb{F}$ is a
field and $\mathcal{M}_{\mathbb{F}}$ is the multiset monad. The set of
functions $\mathbb{F}^{X}$ having finite support is
$\mathcal{M}_{\mathbb{F}}X$ and on arrows it is given by
$\mathcal{M}_{\mathbb{F}}f(\tau)(y)=\sum_{x\in f^{-1}(y)}\tau(x)$ (for
$X\rTo^{f}Y\in\mathbf{Set}$). We write $x\downarrow_{s}$ and
$x\xrightarrow{a,s^{\prime}}x^{\prime}$ whenever $\alpha(x)(\bullet)=s$ and
$\alpha(x)(a,x^{\prime})=s^{\prime}$ for a given LWA
$X\rTo^{\alpha}\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times X+1)$.

Recall the language of a given LWA $\alpha$ starting from a state $x\in X$ is
an inductively defined function
${\mathit{Act}}^{\star}\rTo^{\mathbf{tr}(x)}\mathbb{F}$ described below, where
$a\in\mathit{Act}$, $w\in{\mathit{Act}}^{\star}$, and $\varepsilon$ is the
empty word.

$\mathbf{tr}(x)(\varepsilon)=\alpha(x)(\bullet),\qquad\quad\mathbf{tr}(x)(aw)=\sum\\{s\cdot\mathbf{tr}(x^{\prime})(w)\mid
x\xrightarrow{a,s}x^{\prime}\\}.$

Two states $x,x^{\prime}\in X$ are _(weighted) language equivalent_ iff
$\mathbf{tr}(x)=\mathbf{tr}(x^{\prime})$. This coincides with coalgebraic
behavioural equivalence in $\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$ (see [20,
27]). Note that probabilistic automata can be encoded by letting
$\mathbb{F}=\mathbb{R}$ and restricting the weights to the interval $[0,1]$.

#### Predicate lifting for weighted automata

We employ a similar simplification as carried out in NDA, by working with the
indexed category $\hat{\mathcal{P}}\circ(|\\_|\times|\\_|)$. Now to apply
techniques of Section 5, we fix
$F=\mathit{Act}\times\\_+1,G=\\_^{\mathit{Act}}\times\mathbb{F}$, and recall
from [20, Section 7.3] the distributive laws
$F\mathcal{M}_{\mathbb{F}}X\rTo^{\vartheta_{X}}\mathcal{M}_{\mathbb{F}}FX$ and
$\mathcal{M}_{\mathbb{F}}FX\rTo^{\gamma_{X}}G\mathcal{M}_{\mathbb{F}}X$:

$\displaystyle\quad\vartheta_{X}(\bullet)(\heartsuit)$
$\displaystyle=\begin{cases}1,&\text{if }\ \heartsuit=\bullet\\\
0,&\text{otherwise}.\end{cases}\quad\vartheta_{X}(a,\tau)(\heartsuit)=\begin{cases}\tau(x),&\text{if}\
\heartsuit=(a,x),\text{ for some $x\in X$}\\\ 0,&\text{otherwise}.\end{cases}$
$\displaystyle\gamma_{X}(\bar{p})$
$\displaystyle=(\gamma_{X}^{\mathit{Act}}\bar{p},\bar{p}(\bullet)),\
\text{where}\ \gamma_{X}^{\mathit{Act}}\bar{p}(a)(x)=\bar{p}(a,x)\ \text{(for
$x\in X,\bar{p}\in\mathcal{M}_{\mathbb{F}}FX$)}.$

We know (from [20]) that $\gamma$ is compatible with $\theta$ and $\mu$ (the
multiplication of the monad $\mathcal{M}_{\mathbb{F}}$) in the sense of Lemma
2. Similar to NDAs, consider the following predicate liftings
$\hat{\mathcal{P}}X\rTo^{\sigma_{X}^{a},\sigma_{X}^{s}}\hat{\mathcal{P}}(X^{\mathit{Act}}\times\mathbb{F})$
(for $a\in\mathit{Act}$ and $s\in\mathbb{F}$):

$U\mapsto\\{(p,s)\in X^{\mathit{Act}}\times\mathbb{F}\mid p(a)\in
U\\}\quad\text{and}\quad U\mapsto\\{(p,s)\mid p\in X^{\mathit{Act}}\\},\
\text{respectively.}$

The proof of the following lemma is similar to the proof of Lemma 3. And
thanks to Theorem 5.1, we know that ${\gamma}^{-1}\circ\sigma^{a}$ and
${\gamma}^{-1}\circ\sigma^{s}$ are valid predicate liftings.

###### Lemma 7

The above mappings $\sigma_{X}^{a},\sigma_{X}^{s}$ (for
$a\in\mathit{Act},s\in\mathbb{F}$) are indexed morphisms.

######  Lemma 8 ()

For any $\mathbb{U}\subseteq\mathcal{M}_{\mathbb{F}}X$ we find that
$\lambda_{X}^{a}(\mathbb{U})=\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\gamma_{X}^{\mathit{Act}}\bar{p}(a)\in\mathbb{U}\\}$ and
$\lambda_{X}^{s}(\mathbb{U})=\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\bar{p}(\bullet)=s\\}$.

###### Proof

For any $\mathbb{U}\subseteq\mathcal{M}_{\mathbb{F}}X$ we find that

$\displaystyle\lambda_{X}^{a}(\mathbb{U})=$ $\displaystyle\
{\gamma_{X}}^{-1}\sigma_{\mathcal{M}_{\mathbb{F}}X}^{a}(\mathbb{U})$
$\displaystyle=$ $\displaystyle\
{\gamma_{X}}^{-1}\\{(p,s)\in(\mathcal{M}_{\mathbb{F}}X)^{\mathit{Act}}\times\mathbb{F}\mid
p(a)\in\mathbb{U}\\}$ $\displaystyle=$ $\displaystyle\
\left\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\gamma_{X}\bar{p}\in\\{(p,s)\in(\mathcal{M}_{\mathbb{F}}X)^{\mathit{Act}}\times\mathbb{F}\mid
p(a)\in\mathbb{U}\\}\right\\}$ $\displaystyle=$ $\displaystyle\
\left\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\gamma_{X}^{\mathit{Act}}\bar{p}(a)\in\mathbb{U}\right\\}.$

Similarly, in the context of termination, we find (for each $s\in\mathbb{F}$):

$\displaystyle\lambda_{X}^{s}(\mathbb{U})=$ $\displaystyle\
{\gamma_{X}}^{-1}\sigma_{\mathcal{M}_{\mathbb{F}}X}^{s}(\mathbb{U})$
$\displaystyle=$ $\displaystyle\ {\gamma_{X}}^{-1}\\{(p,s)\mid
p\in(\mathcal{M}_{\mathbb{F}}X)^{\mathit{Act}}\\}$ $\displaystyle=$
$\displaystyle\ \left\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\gamma_{X}\bar{p}\in\\{(p,s)\mid
p\in(\mathcal{M}_{\mathbb{F}}X)^{\mathit{Act}}\\}\right\\}$ $\displaystyle=$
$\displaystyle\ \left\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\bar{p}(\bullet)=s\right\\}.$

The proof that $\lambda^{a}_{X},\lambda^{s}$ preserves finite meet is similar
to the Boolean case (cf. Lemma 3).

Just like in our running example, the determinisation of an LWA $\alpha$ is
the composition:

$\mathcal{M}_{\mathbb{F}}X\rTo^{\mathcal{M}_{\mathbb{F}}\alpha}\mathcal{M}_{\mathbb{F}}\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\rTo^{\mu_{\mathit{Act}\times
X+1}}\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\rTo^{\gamma_{X}}(\mathcal{M}_{\mathbb{F}}X)^{\mathit{Act}}\times\mathbb{F}.$

More concretely, it maps a $p\in\mathcal{M}_{\mathbb{F}}X$ to a pair
$(\hat{p},s)$, where $\hat{p}(a)(x^{\prime})=\sum_{x\in
X}p(x)\cdot\alpha(x)(a,x^{\prime})$ and $s=\sum_{x\in
X}p(x)\cdot\alpha(x)(\bullet)$. In terms of SOS rules, determinisation is
given as follows:

$p\xrightarrow{a}\hat{p}(a)p\in\mathcal{M}_{\mathbb{F}}X\qquad
p\downarrow_{s}p\in\mathcal{M}_{\mathbb{F}}X\quad s=\sum_{x\in
X}p(x)\cdot\alpha(x)(\bullet)$

######  Lemma 9 ()

For any $\mathbb{U}\subseteq\mathcal{M}_{\mathbb{F}}X$ and
$X\rTo^{\alpha}\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times X+1)$, we have
${|\alpha|}^{-1}\lambda_{X}^{a}\mathbb{U}=\\{p\in\mathcal{M}_{\mathbb{F}}X\mid
p\xrightarrow{a}\hat{p}(a)\implies\hat{p}(a)\in\mathbb{U}\\}$ and
${|\alpha|}^{-1}\lambda_{X}^{s}\mathbb{U}=\\{p\in\mathcal{M}_{\mathbb{F}}X\mid
s=\sum_{x\in X}\ p(x)\cdot\alpha(x)(\bullet)\\}$.

###### Proof

Let $\mathbb{U}\subseteq\mathcal{M}_{\mathbb{F}}X$ and a given LWA
$X\rTo^{\alpha}\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times X+1)$. Then we
derive

$\displaystyle{|\alpha|}^{-1}\lambda_{X}^{a}\mathbb{U}=\ $
$\displaystyle{|\alpha|}^{-1}\left\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\gamma_{X}^{\mathit{Act}}\bar{p}(a)\in\mathbb{U}\right\\}$
$\displaystyle=\ $
$\displaystyle\left\\{p\in\mathcal{M}_{\mathbb{F}}X\mid|\alpha|p\in\left\\{\bar{p}\in\mathcal{D}(\mathit{Act}\times
X+1)\mid\gamma_{X}^{\mathit{Act}}\bar{p}(a)\in\mathbb{U}\right\\}\right\\}$
$\displaystyle=\ $
$\displaystyle\left\\{p\in\mathcal{M}_{\mathbb{F}}X\mid\gamma_{X}^{\mathit{Act}}(\mu_{\mathit{Act}\times
X+1}\mathcal{M}_{\mathbb{F}}\alpha(p))a\in\mathbb{U}\right\\}$
$\displaystyle=\ $ $\displaystyle\left\\{p\in\mathcal{M}_{\mathbb{F}}X\mid
p\xrightarrow{a}\hat{p}(a)\implies\hat{p}(a)\in\mathbb{U}\right\\}.$

Similarly, we have a modality to handle termination that can be derived as
follows:

$\displaystyle{|\alpha|}^{-1}\lambda_{X}^{s}\mathbb{U}=\ $
$\displaystyle{|\alpha|}^{-1}\left\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\bar{p}(\bullet)=s\right\\}$ $\displaystyle=\ $
$\displaystyle\left\\{p\in\mathcal{M}_{\mathbb{F}}X\mid|\alpha|p\in\left\\{\bar{p}\in\mathcal{M}_{\mathbb{F}}(\mathit{Act}\times
X+1)\mid\bar{p}(\bullet)=s\right\\}\right\\}$ $\displaystyle=\ $
$\displaystyle\\{p\in\mathcal{M}_{\mathbb{F}}X\mid s=\sum_{x\in X}\
p(x)\cdot\alpha(x)(\bullet)\\}.$

#### Weighted language equivalence through relation lifting

Consider the relation lifting $\bar{\sigma}$ of $G$ that maps a relation $R$
on $X$ to $\bar{\sigma}_{X}R$ defined as:
$(p,s)\mathrel{\bar{\sigma}_{X}R}(p^{\prime},s^{\prime})\iff
s=s^{\prime}\land\forall_{a\in\mathit{Act}}\ pa\mathrel{R}p^{\prime}a.$ So
(LABEL:eq:liftofRlift) gives a relation lifting $\bar{\lambda}$ for $\bar{F}$.
Concretely, $\bar{\lambda}$ maps a relation $R$ on $\mathcal{M}_{\mathbb{F}}X$
to a relation $\bar{\lambda}_{X}R$ on $\mathcal{M}_{\mathbb{F}}FX$ given as:
$\bar{p}\mathrel{\bar{\lambda}_{X}R}\bar{p}^{\prime}\ \iff\
\bar{p}(\bullet)=\bar{p}^{\prime}(\bullet)\ \land\ \forall_{a\in\mathit{Act}}\
\gamma_{X}^{\mathit{Act}}\bar{p}(a)\mathrel{R}\gamma_{X}^{\mathit{Act}}\bar{p}^{\prime}(a).$

######  Theorem 0.B.1 ()

Let $X\rTo^{\alpha}FX\in\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$ be an LWA. Then
weighted language equivalence
$\equiv_{X}\subseteq\mathcal{M}_{\mathbb{F}}X\times\mathcal{M}_{\mathbb{F}}X$
on the determinised system is a
$\Psi(\alpha)\circ\bar{\lambda}_{X}$-coalgebra. Moreover,
$\equiv_{X}={(|f|\times|f|)}^{-1}\equiv_{Y}$ for any coalgebra homomorphism
$(X,\alpha)\rTo^{f}(Y,\beta)$; thus, there is a behavioural conformance
functor
$\mathbf{Coalg}_{\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})}(\bar{F})\rTo^{\mathbbm{1}^{\bar{\lambda}}}\mathbf{Coalg}_{\mathbb{E}(\Psi)}(\bar{F}_{\lambda})$.

###### Proof

Let $X\rTo^{\alpha}FX\in\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$ be an LWA. Just
like in the proof of Theorem 6.1, we will show that weighted language
equivalence $\equiv_{X}$ coincides with the relation $\sim$ defined as the
limit of the diagram $\mathbf{N}\rTo^{D}\Psi X$ defined in the proof of
Theorem 6.1. Recall the determinisation of an LWA in terms of SOS rules:

$p\xrightarrow{a}p_{a}p\in\mathcal{M}_{\mathbb{F}}X\qquad
p\downarrow_{s}p\in\mathcal{M}_{\mathbb{F}}X\quad s=\sum_{x\in
X}p(x)\cdot\alpha(x)(\bullet),$

where $p_{a}(x^{\prime})=\sum_{x\in X}p(x)\cdot\alpha(x)(a,x^{\prime})$. We
can extend this notation to words as follows: $p_{\varepsilon}=p$ and
$p_{aw}=(p_{a})_{w}$. Thus, $p\equiv_{X}p^{\prime}\iff\forall_{w,s}\
p_{w}\downarrow_{s}\iff p^{\prime}_{w}\downarrow_{s}$.

Note that for any $i>1$ and $p,p^{\prime}\in\mathcal{M}_{\mathbb{F}}X$ we have

$p\mathrel{D(i+1)}p^{\prime}\iff\forall_{s\in\mathbb{F}}\ (p\downarrow_{s}\iff
p^{\prime}\downarrow_{s})\ \ \land\ \ p_{a}\mathrel{Di}p_{a}^{\prime}.$

Clearly, $\equiv_{X}\subseteq\sim$ because
$\equiv_{X}\subseteq\alpha^{*}\lambda_{X}\equiv_{X}$. For the other direction,
suppose $p\sim p^{\prime}$. Then for any word $w\in{\mathit{Act}}^{\star}$ we
have $p\mathrel{D(\\#w+1)}p^{\prime}$ which results $p_{w}\downarrow_{s}\iff
p_{w}^{\prime}\downarrow_{s}$, for any $s\in\mathbb{F}$. Since $w$ was chosen
arbitrarily, we find that $p\equiv_{X}p^{\prime}$.

#### Logical characterisation of weighted language equivalence

Just like language equivalence, its weighted variant is a ‘linear’ notion of
behavioural equivalence; thus, we set $\mathbf{A}=\mathbf{Set}$ and $L=F$. As
for the dual adjunction, first recall that
$\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$ is equivalent to the Eilenberg-Moore
category $\mathbf{EM}(\mathcal{M}_{\mathbb{F}})=\mathbf{Vect}_{\mathbb{F}}$
[20], which is due to the fact that every vector space has a basis. In
particular, the comparison functor
$\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})\rTo^{\mathcal{K}}\mathbf{EM}(\mathcal{M}_{\mathbb{F}})$
is fully faithful and essentially surjective. As a result, $\mathcal{K}$ has
an inverse $\mathcal{K}^{\prime}$ that maps every vector space to its basis
which can be arranged as $\mathcal{K}\dashv\mathcal{K}^{\prime}$. Moreover,
the category of vector spaces is related with the category of sets by a dual
adjunction [20] as indicated below. So
$\mathcal{S}=\hom(\mathcal{K}\\_,\mathbb{F})$ and
$\mathcal{T}=\mathcal{K}^{\prime}\mathbb{F}^{\\_}$. Note that for any set $X$
we have $\mathcal{S}X\cong\mathbb{F}^{X}$ and
$\mathcal{K}^{\prime}(\mathbb{F}^{X})\cong X$. The former is true because
$\hom(\mathcal{M}_{\mathbb{F}}X,\mathbb{F})\cong\mathbf{Set}(X,\mathbb{F})$,
while the latter is because the basis of a vector space generated by a set is
isomorphic to the set itself. So ${\mathbf{Set}}^{\text{op}}$ is a subcategory
of $\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$ and Theorem 4.3 ensures that
$\mathrm{Eq}\circ\mathcal{T}$ has a left adjoint $\bar{\mathcal{S}}$. Finally,
$\delta_{X}$ (for any set $X$) should be a natural transformation of type
$FTX=FX\rTo^{\delta_{X}}FX=TLX$. Therefore, we simply take $\delta_{X}$ to be
an identity arrow on $FX$ in $\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$. Lastly,
the theory map
$X\rTo^{\llparenthesis\\_\rrparenthesis_{X}}\mathcal{T}{\mathit{Act}}^{\star}\in\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$
is given by the trace function $\mathbf{tr}$.

######  Theorem 0.B.2 ()

The above defined map $\llparenthesis\\_\rrparenthesis$ is a theory map for a
given LWA. As a result, the logic $(L,\delta)$ is both adequate and expressive
for weighted language equivalence.

###### Proof

We show the square associated with theory map is commutative, i.e.,
$\mathcal{T}h\circ\llparenthesis\\_\rrparenthesis_{X}=\delta_{{\mathit{Act}}^{\star}}F\llparenthesis\\_\rrparenthesis_{X}\circ\alpha$;
the uniqueness follows from structural recursion. Since
$\delta_{{\mathit{Act}}^{\star}}$ is identity arrow, so it suffices to show
that $\llparenthesis\\_\rrparenthesis_{X}$ is a coalgebra homomorphism;
$\mathcal{T}h\circ\llparenthesis\\_\rrparenthesis_{X}=\bar{F}\llparenthesis\\_\rrparenthesis_{X}\circ\alpha$.
Note that we follow [27] by using matrix multiplication to denote the
composition of arrows in $\mathbf{Kl}(\mathcal{M}_{\mathbb{F}})$. Also, for a
function $Y\rTo^{f}X$, $\mathcal{K}^{\prime}(\mathbb{F}^{f})$ corresponds to
unit matrix; namely, the cell $(\delta_{x},\delta_{y})$ in $\mathbb{F}^{f}$
corresponds to $1$ if $F^{f}(\delta_{x})=\delta_{x}\circ f=\delta_{y}$; $0$
otherwise. So concretely, $\mathcal{T}f$ is a function defined as follows:
$\mathcal{T}fxy=1$ if $fy=x$; 0, otherwise.

$\displaystyle F\llparenthesis\\_\rrparenthesis_{X}\circ\alpha(x,(a,w))=$
$\displaystyle\ \sum_{(a^{\prime},x^{\prime})\in\text{supp}(\alpha
x)}\alpha(x,(a^{\prime},x^{\prime}))\cdot\bar{F}\llparenthesis\\_\rrparenthesis_{X}((a^{\prime},x^{\prime}),(a,w))$
$\displaystyle=$ $\displaystyle\ \sum_{(a,x^{\prime})\in\text{supp}(\alpha
x)}\alpha(x,(a,x^{\prime}))\cdot\llparenthesis x^{\prime}\rrparenthesis(w)$
$\displaystyle=$ $\displaystyle\ \llparenthesis x\rrparenthesis_{X}(aw)$
$\displaystyle=$ $\displaystyle\ \sum_{w^{\prime}=aw}\llparenthesis
x\rrparenthesis_{X}w^{\prime}\cdot\mathcal{T}h(w^{\prime},(a,w))$
$\displaystyle=$ $\displaystyle\ \mathcal{T}h\circ\alpha(x,(a,w)).$

Adequacy follows from Theorem 4.1. Furthermore, expressivity follows since
$|\delta_{{\mathit{Act}}^{\star}}|$ is injective.

##  Appendix 0.C Eilenberg-Moore categories

Although, in this paper, there are no case studies (see [4] for predicate
liftings in generalised Moore automata) worked out in the setting of
Eilenberg-Moore categories, it is still worthwhile to report that Eilenberg-
Moore categories (at least when $T$ is finitary) are more well-behaved than
Kleisli categories in satisfying the assumptions of this paper. First it is
straightforward to show that every predicate lifting $F$ induces a predicate
lifting of $\bar{F}$.

###### Proposition 5

Let $\bar{F}$ be a lifting of $F$ to $\mathbf{EM}(T)$ with
$\mathbf{C}\rTo^{T}\mathbf{C}$. Then,

  1. 1.

every indexed category on $\mathbf{C}$ induces an indexed category
$\mathbf{EM}(T)$ by composing with $|\\_|$.

  2. 2.

every indexed morphism $\Phi\rTo\Phi F$ induces an indexed morphism of type
$\Phi|\\_|\rTo\Phi|\\_|\bar{F}$.

Second, the adjunction $\mathbb{Q}\dashv\mathrm{Eq}$ does exist when $T$ is
finitary and $\Phi,\Psi$ are instantiated as in the Kleisli case, i.e.,
$\Phi=\hat{\mathcal{P}}(|\\_|)$ and
$\Psi=\hat{\mathcal{P}}(|\\_|\times|\\_|)$. Intuitively, $\mathbb{Q}$ creates
quotients w.r.t. the smallest congruence relation generated by a relation on
the underlying algebra. Formally, for an algebra $(X,h)\in\mathbf{EM}(T)$, let
$\mathrm{Cong}(X,h)$ denote the poset of congruences on $X$ ordered by
$\subseteq$. Next we claim that arbitrary meets exist in $\mathrm{Cong}(X,h)$
since $\mathbf{EM}(T)$ is complete. Therefore, we can construct

$\mathcal{C}(R)=\bigwedge\\{(R^{\prime},h^{\prime})\mid(R^{\prime},h^{\prime})\in\mathrm{Cong}(X,h)\land
R\subseteq R^{\prime}\\}\enspace.$

Now the algebraic structure on $\mathcal{C}(R)$, i.e., a function
$T\mathcal{C}(R)\rTo\mathcal{C}(R)$ exists due to the universal property of
limits, which we denote simply $h_{R}$. So we take $\mathbb{Q}((X,h),R)$ to be
the coequaliser of $(\mathcal{C}(R),h_{R})\rTo^{p_{i}}(X,h)$ in
$\mathbf{EM}(T)$.

###### Theorem 0.C.1

Suppose $T$ has a finite presentation, then the mapping $\mathbb{Q}$ is left
adjoint to $\mathrm{Eq}$ functor.

###### Proof

We need to show that the following correspondence holds.

$(X,h)\rTo^{g}(Y,k)\in\mathbf{EM}(T)\land R\subseteq{(g\times
g)}^{-1}=_{Y}(X,h,R)\rTo^{g}\mathrm{Eq}(Y,k)\in\mathbb{E}(\Psi)\mathbb{Q}(X,h,R)\rTo^{f}(Y,k)\in\mathbf{EM}(T)$

The direction from top to bottom is easy. Let $q_{R}$ be the coequaliser map
of type $(X,h)\rTo^{q_{R}}\mathbb{Q}(X,h,R)$. Then, we take $g$ to be the
arrow $f\circ q_{R}$.

For the converse, let $(X,h)\rTo^{g}(Y,k)\in\mathbf{EM}(T)$ be an algebra map
such that $R\subseteq{(g\times g)}^{-1}=_{Y}$. Now it suffices to show that
$g\circ p_{1}=g\circ p_{2}$ because the universal property of coequaliser then
gives the unique arrow $f$.

To prove this we recall the construction of the congruence $\mathcal{C}(R)$
generated by $R$ when $T$ has a finite presentation $\mathbb{T}=(\Sigma,E)$,
where $\Sigma$ is a set of function symbols with finite arity and $E$ is a set
of equations.

  * •

Define $R_{0}$ the reflexive and symmetric closure of $R$.

  * •

Define $R_{i+1}=R_{i}\circ
R_{i}\cup\\{(f(x_{1},\cdots,x_{n}),f(x_{1}^{\prime},\cdots,x_{n}^{\prime}))\mid\forall_{j}\
x_{j}R_{i}x_{j}^{\prime}\\}$, where $f$ is an $n$-ary operator in $\Sigma$.

  * •

$\mathcal{C}(R)=\bigcup_{i}R_{i}$.

Now by induction we show that $\forall_{i}\
t\mathrel{R_{i}}t^{\prime}\implies\mathbb{T}\vdash gt=gt^{\prime}$. The base
case is trivial. So assume the property is true for some $i\geq 0$. Let
$t\mathrel{R_{i+1}}t^{\prime}$. Then we identify two cases: either
$t\mathrel{R_{i}\circ R_{i}}t^{\prime}$ or there is an $n$-ary operator and
variables $x_{j},x_{j}^{\prime}$ (for $1\leq j\leq n$) such that
$t=f(x_{1},\cdots,x_{n})$,
$t^{\prime}=f(x_{1}^{\prime},\cdots,x_{n}^{\prime})$ and
$x_{j}\mathrel{R_{i}}x_{j}^{\prime}$ (for all $j$). If the former is true then
the property holds due to the inductive hypothesis and the transitivity of
$\vdash$. So suppose the latter is true. Then by the inductive hypothesis we
find that $\mathbb{T}\vdash gx_{j}=gx_{j}^{\prime}$ (for each $1\leq j\leq
n$). Since $g$ is a homomorphism, so applying the context rule of $\vdash$
gives us

$\mathbb{T}\vdash
gt=f(gx_{1},\cdots,gx_{n})=f(gx_{1}^{\prime},\cdots,gx_{n}^{\prime})=gt^{\prime}.\qquad\squareforqed$

### Predicate liftings for generalised Moore machines

In [6, 36], the authors captured failure/ready/trace equivalences as
behavioural equivalence for coalgebras living in the Eilenberg-Moore category
introduced by a finitary power set monad $\mathcal{P}_{\omega}$.
Interestingly, these linear equivalences can be seen as an instance of
behavioural equivalence induced by a common ‘generalised Moore’ endofunctor
$F_{S}=S\times\\_^{\mathit{Act}}$ [6, Section 3], where
$S\in\mathbf{EM}(\mathcal{P}_{\omega})$ is an arbitrary semi-lattice.

Given a map $X\rTo^{o}S\in\mathbf{EM}(\mathcal{P}_{\omega})$, then the
generalised determinisation [7] of an LTS
$X\rTo^{\alpha}(\mathcal{P}_{\omega}X)^{\mathit{Act}}$ is a coalgebra
$\mathcal{P}_{\omega}X\rTo^{(o^{\prime},\alpha^{\prime})}F_{S}(\mathcal{P}_{\omega}X)\in\mathbf{EM}(\mathcal{P}_{\omega})$,
where the two functions are given as follows (cf. [6]):

$o^{\prime}(U)=\bigvee_{x\in
U}o(x)\quad\text{and}\quad\alpha^{\prime}(U)(a)=\bigcup_{x\in U}\
\alpha(x)(a)\quad\text{(for $U\subseteq X,a\in\mathit{Act}$)}\enspace.$

In other words, the generalised determinisation induces a transition relation
on $\mathcal{P}_{\omega}X$ and a predicate on $\mathcal{P}_{\omega}X\times S$
defined by the following SOS rules:

$U\xrightarrow{a}U_{\alpha}U\subseteq X\quad
U_{\alpha}=\\{x^{\prime}\mid\exists_{x\in U}\
x\xrightarrow{a}x^{\prime}\\}\qquad U\downarrow o^{\prime}(U)U\subseteq
X\qquad o^{\prime}(U)=\bigvee_{x\in U}o(x)\enspace.$

The next theorem is recalled from [36] and captures the aforementioned linear
equivalences as instances of behavioural equivalence.

###### Theorem 0.C.2

Two states $U,U^{\prime}\subseteq X$ in the coalgebra
$\mathcal{P}_{\omega}X\rTo^{(o^{\prime},\alpha^{\prime})}F_{S}(\mathcal{P}_{\omega}X)\in\mathbf{EM}(\mathcal{P}_{\omega})$
are behaviourally equivalent iff they get mapped to a common point in the
final coalgebra (which exists for the Moore functor $F_{S}$). Moreover,

  1. 1.

For $S=2$ and $o$ as constant 1, behavioural equivalence coincides with trace
equivalence.

  2. 2.

For $S=\mathcal{P}_{\omega}\mathcal{P}_{\omega}\mathit{Act}$ and $o(x)$ (for
each $x\in X$) is the set of sets of actions that are refused by the state
$x$, behavioural coincides with failure equivalence.

  3. 3.

For $S=\mathcal{P}_{\omega}\mathcal{P}_{\omega}\mathit{Act}$ and $o(x)$ (for
each $x\in X$) is the singleton containing the set of actions enabled at $x$,
behavioural coincides with ready equivalence.

Next we define two families of indexed morphisms
$\hat{\mathcal{P}}\rTo^{\lambda^{a}}\hat{\mathcal{P}}\circ F_{S}$ (for each
$a\in\mathit{Act}$) and
$\hat{\mathcal{P}}\rTo^{\lambda^{s}}\hat{\mathcal{P}}\circ F_{S}$ (for each
$s\in S$).

  * •

$\lambda^{a}_{X}U=\\{(s^{\prime},p)\in S\times X^{\mathit{Act}}\mid p(a)\in
U\\}$

  * •

$\lambda^{s}_{X}U=\\{(s,p)\mid p\in X^{\mathit{Act}}\\}$, for $U\subseteq X$.

######  Proposition 6 ()

The above mappings
$\hat{\mathcal{P}}\rTo^{\lambda^{a},\lambda^{s}}\hat{\mathcal{P}}\circ F_{S}$
are indexed morphisms.

###### Proof

Let $V\subseteq Y$ and $X\rTo^{f}Y\in\mathbf{Set}$. Then we derive

$\displaystyle\lambda_{X}^{a}{f}^{-1}V=$ $\displaystyle\ \\{(s,p)\mid
p(a)\in{f}^{-1}V\\}$ $\displaystyle=$ $\displaystyle\ \\{(s,p)\mid f(pa)\in
V\\}$ $\displaystyle=$ $\displaystyle\
\\{(s,p)\mid(F_{S}f)(s,p)\in\\{(s,q)\mid qa\in V\\}\\}$ $\displaystyle=$
$\displaystyle\ {(F_{S}f)}^{-1}\lambda_{Y}^{a}V.$

Moreover, $\lambda_{X}^{a}$ preserves arbitrary meets since

$\lambda_{X}^{a}\bigcap_{i\in I}U_{i}=S\times\\{p\mid
pa\in\bigcap_{i}U_{i}\\}=\bigcap_{i}S\times\\{p\mid pa\in
U_{i}\\}=\bigcap_{i}\lambda_{X}^{a}U_{i}.$

Likewise, we derive the related facts for $\lambda_{X}^{s}$.

$\displaystyle\lambda_{X}^{s}{f}^{-1}V=$ $\displaystyle\ \\{(s,p)\mid p\in
X^{\mathit{Act}}\\}$ $\displaystyle=$ $\displaystyle\ \\{(s,p)\mid(s,f\circ
p)\in\\{s\\}\times Y^{\mathit{Act}}\\}$ $\displaystyle=$ $\displaystyle\
\\{(s,p)\mid(F_{S}f)(s,p)\in\\{s\\}\times Y^{\mathit{Act}}\\}$
$\displaystyle=$ $\displaystyle\ {(F_{S}f)}^{-1}\lambda_{Y}^{s}V.$

Moreover, $\lambda_{X}^{s}$ preserves arbitrary meets since

$\lambda_{X}^{s}\bigcap_{i\in I}U_{i}=\\{s\\}\times
X^{\mathit{Act}}=\bigcap_{i}(\\{s\\}\times
X^{\mathit{Act}})=\bigcap_{i}\lambda_{X}^{s}U_{i}.$

As a result, thanks to Proposition 5, the mappings $\lambda^{a},\lambda^{s}$
are also indexed morphisms of type
$\hat{\mathcal{P}}|\\_|\rTo\hat{\mathcal{P}}|\\_|\bar{F}_{s}$. Recall the
determinised systems

$\mathcal{P}_{\omega}X\rTo^{(o^{\prime},\alpha^{\prime})}F_{S}(\mathcal{P}_{\omega}X)\in\mathbf{EM}(\mathcal{P}_{\omega}),$

which is induced by an LTS
$X\rTo^{\alpha}(\mathcal{P}_{\omega}X)^{\mathit{Act}}$. We are now ready to
derive the action and observation modalities on the determinised system.

######  Theorem 0.C.3 ()

Consider the compositions for $\heartsuit\in\\{a,s\\}$:

$\hat{\mathcal{P}}|\mathcal{P}_{\omega}X|\rTo^{\lambda_{\mathcal{P}_{\omega}X}^{\heartsuit}}\hat{\mathcal{P}}|\bar{F}_{S}\mathcal{P}_{\omega}X|\rTo^{{|(o^{\prime},\alpha^{\prime})|}^{-1}}\hat{\mathcal{P}}|\mathcal{P}_{\omega}X|.$

Let $\mathbb{U}$ be a predicate on $\mathcal{P}_{\omega}X$. Then,
${|(o^{\prime},\alpha^{\prime})|}^{-1}\lambda^{a}_{\mathcal{P}_{\omega}X}\mathbb{U}=\\{U\subseteq
X\mid U\xrightarrow{a}U_{\alpha}\implies U_{\alpha}\in\mathbb{U}\\}$ and
${|(o^{\prime},\alpha^{\prime})|}^{-1}\lambda^{s}_{\mathcal{P}_{\omega}X}\mathbb{U}=\\{U\subseteq
X\mid U\downarrow s\\}$.

###### Proof

Let $\mathbb{U}\subseteq\mathcal{P}_{\omega}X$. Then we derive the modality
for action transition:

$\displaystyle{|(o^{\prime},\alpha^{\prime})|}^{-1}\lambda^{a}_{\mathcal{P}_{\omega}X}\mathbb{U}=$
$\displaystyle\ {(o^{\prime},\alpha^{\prime})}^{-1}\\{(s^{\prime},p)\in
S\times(\mathcal{P}_{\omega}X)^{\mathit{Act}}\mid p(a)\in\mathbb{U}\\}$
$\displaystyle=$ $\displaystyle\ \\{U\subseteq
X\mid(o^{\prime},\alpha^{\prime})U\in\\{(s^{\prime},p)\in
S\times(\mathcal{P}_{\omega}X)^{\mathit{Act}}\mid p(a)\in\mathbb{U}\\}\\}$
$\displaystyle=$ $\displaystyle\ \\{U\subseteq
X\mid\alpha^{\prime}(U)\in\mathbb{U}\\}$ $\displaystyle=$ $\displaystyle\
\\{U\subseteq X\mid U\xrightarrow{a}U_{\alpha}\implies
U_{\alpha}\in\mathbb{U}\\}.$

Likewise, we derive the modalities for observations living in $S$:

$\displaystyle{|(o^{\prime},\alpha^{\prime})|}^{-1}\lambda^{s}_{\mathcal{P}_{\omega}X}\mathbb{U}=$
$\displaystyle\ {(o^{\prime},\alpha^{\prime})}^{-1}\\{(s,p)\mid
p\in(\mathcal{P}_{\omega}X)^{\mathit{Act}}\\}$ $\displaystyle=$
$\displaystyle\ \\{U\subseteq
X\mid(o^{\prime},\alpha^{\prime})U\in\\{(s,p)\mid
p\in(\mathcal{P}_{\omega}X)^{\mathit{Act}}\\}\\}$ $\displaystyle=$
$\displaystyle\ \\{U\subseteq X\mid o^{\prime}(U)=s\\}$ $\displaystyle=$
$\displaystyle\ \\{U\subseteq X\mid U\downarrow s\\}.$
$\displaystyle\quad\squareforqed$

Furthermore, a well-known application of the Linton’s theorem when the monad
$T$ is finitary is that the category of Eilenberg-Moore algebras is
cocomplete. So, in particular, the finite powerset monad
$\mathcal{P}_{\omega}$ is finitary, thus, $\mathbf{EM}(\mathcal{P}_{\omega})$
has all coequalisers. Therefore, A3 is satisfied.