# On Coalgebras with Internal Moves

Tomasz Brengos

► To cite this version:

Tomasz Brengos. On Coalgebras with Internal Moves. 12th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2014, Grenoble, France. pp.75-97, 10.1007/978-3-662-44124-4_5. hal-01408753

HAL Id: hal-01408753

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

Submitted on 5 Dec 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# On coalgebras with internal moves

Tomasz Brengos *

Faculty of Mathematics and Information Science
Warsaw University of Technology
Koszykowa 75
00-662 Warszawa, Poland
t.brengos@mini.pw.edu.pl

**Abstract.** In the first part of the paper we recall the coalgebraic approach to handling the so-called invisible transitions that appear in different state-based systems semantics. We claim that these transitions are always part of the unit of a certain monad. Hence, coalgebras with internal moves are exactly coalgebras over a monadic type. The rest of the paper is devoted to supporting our claim by studying two important behavioural equivalences for state-based systems with internal moves, namely: weak bisimulation and trace semantics. We continue our research on weak bisimulations for coalgebras over order enriched monads. The key notions used in this paper and proposed by us in our previous work are the notions of an order saturation monad and a saturator. A saturator operator can be intuitively understood as a reflexive, transitive closure operator. There are two approaches towards defining saturators for coalgebras with internal moves. Here, we give necessary conditions for them to yield the same notion of weak bisimulation. Finally, we propose a definition of trace semantics for coalgebras with silent moves via a uniform fixed point operator. We compare strong and weak bisimulation together with trace semantics for coalgebras with internal steps.

**Keywords:** bisimulation, coalgebra, Conway operator, epsilon transition, fixed point operator, internal transition, logic, monad, saturation, trace, trace semantics, traced monoidal category, uniform fixed point operator, weak bisimulation, weak trace semantics, van Glabbeek spectrum

## 1 Introduction

In recent years we have witnessed a rapid development of the theory of coalgebras as a unifying theory for state-based systems [13, 22, 21, 16]. Coalgebras to some extent are one-step entities in their nature. They can be thought of and understood as a representation of a single step of visible computation of a given process. Yet, for many state-based systems it is useful to consider a part of computation branch that is allowed to take several steps and in some sense remains

<footnote>* This work has been supported by the grant of Warsaw University of Technology no. 504M for young researchers.</footnote>
neutral (invisible) to the structure of the process. For instance, the so-called τ-
transitions also called invisible transitions for labelled transition systems [29,30]
or ε-transitions for non-deterministic automata [18]. As will be witnessed here,
these special branches of computation are the same in their nature, yet they are
used in order to develop different notions of equivalence of processes, e.g. weak
bisimulation for LTS [29] or trace semantics for non-deterministic automata with
ε-moves, we call ε-NA in short [18]. These are not the only state-based systems
considered in the literature with a special invisible computational branch. Fully
probabilistic systems [3] or Segala systems [37,38] are among those, to name a
few. All these systems are instances of a general notion of a coalgebra. If so, then
how should we consider the invisible part of computation coalgebraically? As we
will see further on, the invisible part of the computation can be and should be,
in our opinion, considered as part of the unit of a monad. Before we state basic
results let us summarize known literature on the topic of invisible transitions
from perspective of weak bisimulation, trace semantics and coalgebra.

**Weak bisimulation** The notion of a strong bisimulation for different transition systems plays an important role in theoretical computer science. A weak bisimulation is a relaxation of this notion by allowing silent, unobservable transitions. Here, we focus on the weak bisimulation and weak bisimilarity proposed by R. Milner [29,30] (see also [36]). Analogues of Milner’s weak bisimulation are established for different deterministic and probabilistic transition systems (e.g. [3,36,37,38]). It is well known that one can introduce Milner’s weak bisimulation for LTS in several different but equivalent ways.

The notion of a strong bisimulation, unlike the weak bisimulation, has been
well captured coalgebraically (see e.g. [14,35,43]). Different approaches to defin-
ing weak bisimulations for coalgebras have been presented in the literature. The
earliest paper is [34], where the author studies weak bisimulations for while
programs. In [32] the author introduces a definition of weak bisimulation for
coalgebras by translating a coalgebraic structure into an LTS. This construc-
tion works for coalgebras over a large class of functors but does not cover the
distribution functor, hence it is not applicable to different types of probabilistic
systems. In [33] weak bisimulations are introduced via weak homomorphisms. As
noted in [42] this construction does not lead to intuitive results for probabilistic
systems. In [42] the authors present a definition of weak bisimulation for classes
of coalgebras over functors obtained from bifunctors. Here, weak bisimulation of
a system is defined as a strong bisimulation of a transformed system. In [7] we
proposed a new approach to defining weak bisimulation in two different ways.
Two definitions of weak bisimulation described by us in [7] were proposed in
the setting of coalgebras over ordered functors. The key ingredient of the defi-
nitions is the notion of a saturator. As noted in [7] the saturator is sometimes
too general to model only weak bisimulation and may be used to define other
known equivalences, e.g. delay bisimulation [36]. Moreover, the saturators from
[7] do not arise in any natural way. To deal with this problem we have presented
a canonical way to consider weak bisimulation saturation in our previous paper
[8]. Part of the results from [8] are recalled in this paper.

We should also mention [13,27] which appeared almost at the same time
as our previous paper [8]. The former is a talk on the on-going research by
S. Goncharov and D. Pattinson related to weak bisimulation for coalgebras.
Their approach is similar to ours as it uses fixed points. It is worth noting that
the authors cover some examples that do not fit our framework (e.g. fully proba-
bilistic systems). However, they do not hide the invisible steps inside a monadic
structure. The latter is a paper in which the authors study weak bisimulation
for labelled transition systems weighted over semirings. They propose a coalge-
braic approach towards defining weak bisimulation which relies on $\varepsilon$-elimination
procedure presented in [39].

**Weak trace semantics** Trace semantics is a standard behavioural equivalence for many state-based systems. Generic trace semantics for coalgebras has been proposed in [17,22]. If $T$ is a monad on a category $C$ and $F : C \to C$ is an endofunctor then the trace semantics of $TF$-coalgebras is final semantics for coalgebras considered in a different category, namely the Kleisli category for the monad $T$ [17,20]. It is worth noting that trace semantics can also be defined for $GT$-coalgebras for an endofunctor $G : C \to C$ [22,40] via the so-called $\mathcal{EM}$-extension semantics. In our paper however, we focus only on $TF$-coalgebras and do not consider $GT$-coalgebras. Trace semantics can also be defined for different state-based systems with internal, invisible moves. In order to distinguish trace semantics for systems with and without silent steps we will sometimes call the former “weak trace semantics”. One coalgebraic approach towards defining trace semantics for systems with $\varepsilon$-moves (invisible moves) is based on a very simple idea, has been presented in [16,39] and can be summarized as follows. In the first step we consider invisible moves as visible. Then we find the trace semantics for an “all-visible-steps” coalgebra and finally, we remove all occurrences of the invisible label and get the desired weak trace semantics. We discuss this approach in our paper and call it the “top-down” approach. The term “top-down” refers to the fact that we somewhat artificially treat the invisible moves as if they were visible and then we remove their occurrences from the trace. Such an approach does not use any structural properties of silent moves. A dual approach, a “bottom-up” method, should make use of their structural properties. Here, we present a “bottom-up” method for coalgebras with internal steps that treats silent moves as part of the unit of a certain monad.

**Content and organization of the paper** The paper is organized as follows. Section 2 recalls basic notions in category theory, algebra and coalgebra. Section 3 describes two very general methods for dealing with silent steps via a monadic structure that have been proposed in our previous work [8]. We will see that these two methods appear in classical definitions of a weak bisimulation for LTS's. In Section 4 we recall the definition of an order saturation monad that comes from [8] and claim that this object is suitable for defining weak bisimu-
lations for coalgebras. An order saturation monad is an order enriched monad equipped with an extra operator, a saturator $(-)^*$, that assigns to any coalgebra $\alpha : X \to TX$ a coalgebra $\alpha^* : X \to TX$ and can be thought of as a reflexive, transitive closure operator. It turns out that in the classical literature on labelled transition systems and weak bisimulation one can find two different saturators yielding the same notion of equivalence. These two saturators are natural consequences of the two stategies towards handling invisible steps via monadic structure. What is new in this section is the following:

- Weak bisimulation is defined as a kernel bisimulation [43] on a saturated structure and not via lax- and oplax-homomorphisms in Aczel-Mendler style as it was done in [8].

- We present both saturators in a general setting and ask when they yield the same notion of weak bisimulation. We give sufficient conditions functors should satisfy so that weak bisimulation coincides for both approaches.

In Section 5 we discuss a novel approach towards defining trace semantics for coalgebras with internal moves. Here, weak trace semantics morphism is obtained axiomatically by the so-called coalgebraic trace operator, i.e. a uniform fixed point operator. For Cappo-enriched monads, a coalgebraic trace operator is given by the least fixed point operator $\mu x.(x \cdot \alpha)$. Moreover, we show that the coalgebraic trace operator for $\varepsilon$-NA's arises from properties of the so-called free LTS monad. To be more precise, Kleisli category for the free LTS monad is traced monoidal category in the sense of Joyal et al. [19]. In Section 6, in a fairly general setting, we formulate how strong bisimulation, weak bisimulation and weak trace semantics are related. Hence, according to our knowledge we present the first paper that considers a comparison of three different behaviour equivalences in van Glabbeek's spectrum for systems with internal moves [11] from coalgebraic perspective.

## 2 Basic notions and properties

**Algebras and coalgebras** Let $C$ be a category and let $F: C \to C$ be a functor. An $F$-algebra is a morphism $a: FA \to A$ in $C$. A *homomorphism* between algebras $a: FA \to A$ and $b: FB \to B$ is a morphism $f: A \to B$ in $C$ such that $b \circ F(f) = f \circ a$. Dually, an *$F$-coalgebra* is a morphism $\alpha: X \to FX$ in $C$. The domain $X$ of $\alpha$ is called *carrier* and the morphism $\alpha$ is sometimes also called *structure*. A *homomorphism* from an $F$-coalgebra $\alpha: X \to FX$ to an $F$-coalgebra $\beta: Y \to FY$ is a morphism $f: X \to Y$ in $C$ such that $F(f) \circ \alpha = \beta \circ f$. The category of all $F$-coalgebras ($F$-algebras) and homomorphisms between them is denoted by $C_F$ (resp. $C^F$). Many transition systems can be captured by the notion of coalgebra. In this paper we mainly focus on labelled transition systems with a silent label and non-deterministic automata with $\varepsilon$-moves. These two structures have been defined and thoroughly studied in the computer science literature (see e.g. [18,29,30,36]). Let $\Sigma$ be a fixed set of alphabet letters. A labelled transition system over the alphabet $\Sigma = \Sigma + \{\tau\}$ (or an LTS in short)
is a triple $\langle X, \Sigma_{\tau}, \rightarrow \rangle$, where $X$ is called a set of states and $\rightarrow \subseteq X \times \Sigma_{\tau} \times X$ is a transition. The label $\tau$ is considered a special label sometimes called silent or invisible label. For an LTS $\langle X, \Sigma_{\tau}, \rightarrow \rangle$ instead of writing $(x, \sigma, x') \in \rightarrow$ we write $x \xrightarrow{\sigma} x'$. Labelled transition systems can be viewed as coalgebras over the type $\mathcal{P}(\Sigma_{\tau} \times \mathcal{I}d)$ [35]. From coalgebraic perspective, a non-deterministic automaton with $\varepsilon$-transitions, or $\varepsilon$-NA in short, over alphabet $\Sigma$ is a coalgebra of the type $\mathcal{P}(\Sigma_{\varepsilon} \times \mathcal{I}d + 1)$, where $1 = \{\surd\}$ is fixed one element set and $\Sigma_{\varepsilon} = \Sigma + \{\varepsilon\}$. Note that LTS's differ from $\varepsilon$-NA's in the presence of 1 in the type. It is responsible for specifying which states are final and which are not. To be more precise for $\varepsilon$-NA $\alpha: X \rightarrow \mathcal{P}(\Sigma_{\varepsilon} \times X + 1)$ we call a state $x \in X$ final if $\surd \in \alpha(x)$. For more information on automata the reader is referred to e.g. [18].

**Strong bisimulation for coalgebras** Notions of strong bisimulation have been well captured coalgebraically [2,14,35,43]. Let $F$ be a Set-endofunctor and consider an $F$-coalgebra $\alpha: X \to FX$. In Aczel-Mendler style [2,43], a (strong) bisimulation is a relation $R \subseteq X \times X$ for which there is a structure $\gamma: R \to TR$ making $\pi_1: R \to X$ and $\pi_2: R \to X$ homomorphisms between $\gamma$ and $\alpha$. In this paper however we consider defining bisimulation as the so-called kernel bisimulation [43]. Let $F: C \to C$ be an endofunctor on an arbitrary category. Let $\alpha: X \to FX$ and $\beta: Y \to FY$ be $F$-coalgebras. A relation $R$ on $X$ and $Y$ (i.e. a jointly-monic span $X \stackrel{\pi_1}{\rightleftharpoons} R \stackrel{\pi_2}{\longrightarrow} Y$ in $C$) is kernel bisimulation or bisimulation in short if there is a coalgebra $\gamma: Z \to FZ$ and homomorphisms $f$ from $\alpha$ to $\gamma$ and $g$ from $\beta$ to $\gamma$ such that $R$ with $\pi_1, \pi_2$ is the pullback of $X \stackrel{f}{\longrightarrow} Z \stackrel{g}{
leftarrow} Y$. For a thorough study of the relation between Aczel-Mendler style of defining bisimulation and kernel bisimulation the reader is referred to [43] for details.

**Monads** A monad on $C$ is a triple $(T, \mu, \eta)$, where $T: C \to C$ is an endofunctor and $\mu: T^2 \Rightarrow T$, $\eta: \mathcal{I}d \Rightarrow T$ are two natural transformations for which the following two diagrams commute: The transformation $\mu$ is called multiplication and $\eta$ unit. Each monad gives rise to a canonical category - Kleisli category for $T$. If $(T, \mu, \eta)$ is a monad on category $C$ then Kleisli category $Kl(T)$ for $T$ has the class of objects equal to the class of objects of $C$ and for two objects $X, Y$ in $Kl(T)$ we have $\operatorname{Hom}_{Kl(T)}(X, Y) = \operatorname{Hom}_C(X, TY)$ with the composition $\cdot$ in $Kl(T)$ defined between two morphisms $f: X \to TY$ and $g: Y \to TZ$ by $g \cdot f := \mu_Z \circ T(g) \circ f$ (here, $\circ$ denotes the composition in $C$).

**Example 1.** The powerset endofunctor $\mathcal{P}: \text{Set} \to \text{Set}$ is a monad with the multiplication $\mu: \mathcal{P}^2 \Rightarrow \mathcal{P}$ and the unit $\eta: \mathcal{I}d \Rightarrow \mathcal{P}$ given on their $X$-components by $\mu_X: \mathcal{P}PX \to PX; S \mapsto S \cup \{x\}$ and $\eta_X: X \to PX; x \mapsto \{x\}$. For any category $C$ with binary coproducts and an object $A \in C$ define $M_A: C \to C$ as $M_A = \mathcal{I}d + A$. The functor carries a monadic structure $(M_A, \mu, \eta)$, where the $X$-components of the multiplication and the unit are the following: $\mu_X: (X + A) + A \to X + A; \mu_X = [id_{X+A}, \iota^2]$ and $\eta_X: X \to X + A; \eta_X = \iota^1$. Here,
ι¹ and ι² denote the coprojections into the first and the second component of X + A respectively. The monad $\mathcal{M}_A$ is sometimes called *exception monad*.

Since in many cases we will work with two categories at once: C and $Kl(T)$, morphisms in C will be denoted using standard arrow $\to$, whereas for morphisms in $Kl(T)$ we will use the symbol $\to^o$. For any object $X$ in C (or equivalently in $Kl(T)$) the identity map from $X$ to itself in C will be denoted by $id_X$ and in $Kl(T)$ by $1_X$ or simply 1 if the domain can be deduced from the context.

The category C is a subcategory of $Kl(T)$ where the inclusion functor $\Sigma^\sharp$ sends each object $X \in C$ to itself and each morphism $f: X \to Y$ in C to the morphism $f^\sharp: X \to^o Y$ given by $f^\sharp: X \to TY$; $f^\sharp = \eta_Y \circ f$. Each monad $(T, \mu, \eta)$ on a category C arises as the composition of left and right adjoint:
Here, $U_T: Kl(T) \to C$ is a functor defined as follows. For any object $X \in Kl(T)$ (i.e. $X \in C$) the object $U_T X$ is given by $U_T X := TX$ and for any morphism $f: X \to^o Y$ in $Kl(T)$ (i.e. $f: X \to TY$ in C) the morphism $U_T f: TX \to TY$ is given by $U_T f = \mu_Y \circ Tf$.

We say that a functor $F: C \to C$ *lifts to* an endofunctor $\bar{F}: Kl(T) \to Kl(T)$ provided that the following diagram commutes [17,22]:

There is a one-to-one correspondence between liftings $\bar{F}$ and distributive laws $\lambda: FT \implies TF$ [22,26]. Given a distributive law $\lambda: FT \implies TF$ a lifting $\bar{F}: Kl(T) \to Kl(T)$ is defined by:

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

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

$$ \bar{F}X := FX \text{ for any object } X \in Kl(T), $$

$$ \bar{F}f: FX \to TFY; \bar{F}f = \lambda_Y \circ Ff \text{ for any morphism } f: X \to TY. $$

Conversely, a lifting $\bar{F}: Kl(T) \to Kl(T)$ of $F$ gives rise to a distributive law $\lambda: FT \implies TF$ defined by $\lambda_X: FTX \to TFX$; $\lambda_X = \bar{F}(id_{TX})$. A monad $T$ on a cartesian closed category C is called *strong* if there is a transformation $\text{st}_{X,Y}: X \times TY \to T(X \times Y)$ called *tensorial strength* satisfying the strength laws listed in e.g. [23]. Existence of strength guarantees that for any object $\Sigma$ the functor $\Sigma \times \mathcal{I}d: C \to C$ admits a lifting $\bar{\Sigma}: Kl(T) \to Kl(T)$. To be more precise we define a functor $\bar{\Sigma}: Kl(T) \to Kl(T)$ as follows. For any object $X \in Kl(T)$ (i.e. $X \in C$) we put $\bar{\Sigma}X := \Sigma \times X$, and for any morphism $f: X \to^o Y$ (i.e. $f: X \to TY$ in C) we define $\bar{\Sigma}f: \Sigma \times X \to T(\Sigma \times Y)$ by $\bar{\Sigma}f := \text{st}_{\Sigma,Y} \circ (id_{\Sigma} \times f)$. Existence of the transformation $\text{st}_{X,Y}$ is not a strong assumption. For instance all monads on Set are strong.

A category is *order enriched* if each hom-set is a poset with order preserved by composition. An endofunctor on an order enriched category is *locally monotonic* if it preserves order. A category C is *Cppo-enriched* if for any objects $X, Y$:

- the hom-set $\text{Hom}_C(X, Y)$ is a poset with a least element $\bot$,

- for any ascending $\omega$-chain $f_0 \le f_1 \le \dots$ in $\text{Hom}_C(X, Y)$ the supremum $\bigvee_{i \in \mathbb{N}} f_i$ exists,

- $g \circ \bigvee_{i \in \mathbb{N}} f_i = \bigvee_{i \in \mathbb{N}} g \circ f_i$ and $(\bigvee_{i \in \mathbb{N}} f_i) \circ h = \bigvee_{i \in \mathbb{N}} f_i \circ h$ for any ascending $\omega$-chain $f_0 \le f_1 \le \dots$ and $g, h$ with suitable domain and codomain.
Note that it is not necessarily the case that $f \circ \perp = \perp$ or $\perp \circ f = \perp$ for any morphism $f$. An endofunctor on a **Cppo**-enriched category is called locally continuous if it preserves suprema of ascending $\omega$-chains. For more details on **Cppo**-enriched categories the reader is referred to e.g. [1,17].

**Example 2.** The Kleisli category for the powerset monad $\mathcal{P}$ is **Cppo**-enriched [17]. The order on the hom-sets is imposed by the natural point-wise order. The strength map for $\mathcal{P}$ is given by

$$ \mathrm{st}_{X,Y}: X \times \mathcal{P}Y \to \mathcal{P}(X \times Y); (x, S) \mapsto \{(x, y) \mid y \in S\}. $$

The lifting $\bar{\Sigma}: \mathrm{Kl}(\mathcal{P}) \to \mathrm{Kl}(\mathcal{P})$ of $\Sigma \times \mathcal{I}d: \mathrm{Set} \to \mathrm{Set}$ is a locally continuous functor [17]. The Kleisli category for the monad $M_1$ on $\mathrm{Set}$ is also **Cppo**-enriched [17]. Order on hom-sets is imposed by the point-wise order and for any $X$ the set $M_1X = X+1 = X+\{\perp\}$ is a poset whose partial order $\leq$ is given by $x \leq y$ iff $x=\perp$ or $x=y$.

**Monads on Kleisli categories** In this paper we will often work with monads on Kleisli categories. Here we list basic properties of such monads. Everything presented below with the exception of the last theorem follows easily by classical results in category theory (see e.g. [24]). Assume that $(T, \mu, \eta)$ is a monad on $\mathcal{C}$ and $S: \mathcal{C} \to \mathcal{C}$ is a functor that lifts to $\bar{S}: \mathrm{Kl}(T) \to \mathrm{Kl}(T)$ with the associated distributive law $\lambda: ST \Rightarrow TS$. Moreover, let $(\bar{S}, m, e)$ be a monad on $\mathrm{Kl}(T)$. We have the following two adjoint situations whose composition is an adjoint situation [24].

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

This yields a monadic structure on the functor $TS: \mathcal{C} \to \mathcal{C}$. The $X$-components of the multiplication $\mathfrak{m}$ and the unit $\mathfrak{e}$ of the monad $TS$ are given by:

$$ \mathfrak{m}_X = \mu_{SX} \circ T\mu_{SX} \circ TTm_X \circ T\lambda_{SX} \quad \text{and} \quad \mathfrak{e}_X = e_X. $$

The composition $\circ$ in $\mathrm{Kl}(TS) = \mathrm{Kl}(\bar{S})$ is given in terms of the composition in $\mathcal{C}$ as follows. For $f: X \to TSY$ and $g: Y \to TSZ$ we have:

$$ \begin{array}{ccc} X & \xrightarrow{f} & TSY \\ \multicolumn{2}{c}{g \cdot f} & TSTSZ \\ \cline{3-3} TSZ & \leftarrow & T^2SZ \end{array} \quad \begin{array}{ccc} \multicolumn{2}{c}{T^{\lambda_{SZ}} S^2 Z} & \\ \multicolumn{2}{c}{\downarrow T^2(m_Z)} & \\ \multicolumn{2}{c}{T^{\mu_{SZ}} Z} & \end{array} $$

The following result can be proved by straightforward verification.

**Theorem 1.** Assume that $\mathrm{Kl}(T)$ is **Cppo**-enriched and $\bar{S}$ is locally continuous. Then $\mathrm{Kl}(TS) = \mathrm{Kl}(\bar{S})$ is **Cppo**-enriched.
### 3 Hiding internal moves inside a monadic structure

Throughout this paper we assume that $(T, \mu, \eta)$ is a monad on a category $C$ with binary coproducts. Let $+$ denote the binary coproduct operator in $C$. Assume that $F: C \to C$ is a functor and let $F_\tau = F + \mathcal{I}d$. In this paper we deal with functors of the form $TF_\tau = T(F + \mathcal{I}d)$. Labelled transition system and $\varepsilon$-NA functor are of this form since

$$ \mathcal{P}(\Sigma_\tau \times \mathcal{I}d) \cong \mathcal{P}(\Sigma \times \mathcal{I}d + \mathcal{I}d) = \mathcal{P}(F + \mathcal{I}d) \text{ for } F = \Sigma \times \mathcal{I}d \text{ and} $$

$$ \mathcal{P}(\Sigma_\varepsilon \times \mathcal{I}d + 1) \cong \mathcal{P}(\Sigma \times \mathcal{I}d + 1 + \mathcal{I}d) = \mathcal{P}(F + \mathcal{I}d) \text{ for } F = \Sigma \times \mathcal{I}d + 1. $$

The functor $F$ represents the visible part of the structure, whereas the functor $\mathcal{I}d$ represents silent moves. Functors of this type were used to consider $\varepsilon$-elimination from coalgebraic perspective in [16,39]. In [8] we noticed that given some mild assumptions on the monad $T$, the functor $TF_\tau$ can itself be turned into a monad or embedded into one. The aim of this section is to recall these results here. Before we do it, we will list basic definitions and properties concerning categories and monads used in the construction.

**Basic definitions and properties** For a family of objects $\{X_k\}_{k \in I}$ if the coproduct $\coprod_i X_i$ exists then by $t^k: X_k \to \coprod_k X_k$ we denote the coprojection into $k$-th component of $\coprod_k X_k$.

We say that a category is a category with zero morphisms if for any two objects $X, Y$ there is a morphism $0_{X,Y}$ which is an annihilator w.r.t. composition. To be more precise $f \circ 0 = 0 \circ g$ for any morphisms $f, g$ with suitable domain and codomain.

**Example 3.** For the monad $T \in \{\mathcal{P}, \mathcal{M}_1\}$ on Set the category $\mathcal{Kl}(T)$ is a category with zero morphisms given by $\perp: X \to \mathcal{P}Y; x \mapsto \emptyset$ for $\mathcal{P}$ and $\perp: X \to \mathcal{M}_1Y; x \mapsto \perp$ for the monad $\mathcal{M}_1$.

Given two monads $(S, \mu^S, \eta^S)$ and $(S', \mu^{S'}, \eta^{S'})$ a monad morphism $h$ is a natural transformation $h: S \to S'$ which preserves unit and multiplication of monads, i.e. $h \circ \eta^S = \eta^{S'}$ and $h \circ \mu^S = \mu^{S'} \circ hh$. A free monad over a functor $F: C \to C$ [9,25] is a monad $(F^*, m, e)$ together with a natural transformation $\nu: F \to F^*$ such that for any monad $(S, m^S, e^S)$ on $C$ and a natural transformation $s: F \to S$ there is a unique monad morphism $h: (F^*, m, e) \to (S, m^S, e^S)$ such that the following diagram commutes:

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

**Theorem 2.** [9] Assume that for an endofunctor $F: C \to C$ and any object $X$ the free $F$-algebra over $X$ (=initial $F(-) + X$-algebra) $i_X$ exists in $\mathbb{C}^F$. For an object $X$ and a morphism $f: X \to Y$ in $C$ let $F^*X$ denote the carrier of $i_X$
and $F^*f: F^*X \to F^*Y$ denote the unique morphism for which the following diagram commutes:

$$ \begin{array}{ccc} FF^*X + X & \xrightarrow{i_X} & F^*X \\ \begin{array}{c} F(F^*f)+i_{X} \\ \multicolumn{1}{c}{|} \\ \multicolumn{1}{c}{\Psi} \end{array} & & \begin{array}{c} F^*f \\ \multicolumn{1}{c}{|} \\ \multicolumn{1}{c}{\Psi} \end{array} \\ FF^*Y + X & \xrightarrow{id+f} & FF^*Y + Y \\ & & \xrightarrow{i_Y} F^*Y \end{array} $$

The assignment $F^*$ is functorial and can be naturally equipped with a monadic structure $(F^*, m, e)$ which is a consequence of the universal properties of $i_X$. Moreover, this monad is the free monad over $F$.

In the sequel we assume the following:

- The functor $F: C \to C$ lifts to $\overline{F}: Kl(T) \to Kl(T)$. As a direct consequence we get that $F_\tau = F + \mathcal{I}d$ lifts to a functor $\overline{F}_\tau = \overline{F} + \mathcal{I}d$ on $Kl(T)$. This follows by the fact that coproducts in $Kl(T)$ come from coproducts in the base category (see also e.g. [17] for a discussion on liftings of coproducts of functors).

- The functor $F$ admits the free $F$-algebra $i_X$ in $C^F$ for any object $X$. By theorem above this yields the free monad $(F^*, m, e)$ over $F$ in $C$.

**Monadic structure on $TF_\tau$** The aim of this subsection is to present the first strategy towards handling the invisible part of computation by a monadic structure. Note that in the following result all morphisms, in particular all co-projections and mediating morphisms, live in $Kl(T)$.

**Theorem 3.** [8] If $Kl(T)$ is a category with zero morphisms then the triple $(\overline{F}_\tau, m', e')$, where $e' : \mathcal{I}d \to \overline{F} + \mathcal{I}d; e'_X = i_X^2$ and

$$ m' : \overline{F}(\overline{F} + \mathcal{I}d) + (\overline{F} + \mathcal{I}d) \xrightarrow{\overline{F}([0,id])+id} \overline{F} + (\overline{F} + \mathcal{I}d) \xrightarrow{[i^1,id]} \overline{F} + \mathcal{I}d $$

is a monad on $Kl(T)$. Two adjoint situations $C \leftrightarrow Kl(T) \leftrightarrow Kl(\overline{F}_\tau)$ yield a monadic structure on $TF_\tau$.

The composition $\cdot$ in $Kl(TF_\tau) = Kl(\overline{F}_\tau)$ is given as follows. Let $\lambda: F_\tau T \implies TF_\tau$ denote the distributive law associated with the lifting $\overline{F}_\tau$ of $F_\tau$. For any $f: X \to TF_\tau Y, g: Y \to TF_\tau Z$ we have:

$$ g \cdot f = \mu_{F_\tau Z} \circ T\mu_{F_\tau Z} \circ TTm'_Z \circ T\lambda_{F_\tau Z} \circ TF_\tau g \circ f. $$

We illustrate the above construction in the following example, where $T = \mathcal{P}$ and $F_\tau = \Sigma_\tau \times \mathcal{I}d$.

**Example 4.** As mentioned before, the monad $\mathcal{P}$ (as any other monad on Set) comes with strength st which lifts the functor $\Sigma_\tau \times \mathcal{I}d: \text{Set} \to \text{Set}$ to the functor $\overline{\Sigma_\tau}: Kl(\mathcal{P}) \to Kl(\mathcal{P})$. For the functor $\overline{\Sigma_\tau} \cong \overline{\Sigma} + \mathcal{I}d$ we define the
multiplication $m'$ and the unit $e'$ as in Theorem 3. For any set $X \in \mathcal{Kl}(\mathcal{P})$ we put $m'_X : \overline{\Sigma_\tau \Sigma_\tau} X \to \overline{\Sigma_\tau} X$ and $e'_X : X \to \overline{\Sigma_\tau} X$ to be:

$$m'_{X}(\sigma_{1}, \sigma_{2}, x) = \begin{cases} \{(\sigma_{1}, x)\} & \text{if } \sigma_{2} = \tau, \\ \{(\sigma_{2}, x)\} & \text{if } \sigma_{1} = \tau, \\ \emptyset & \text{otherwise} \end{cases} \qquad e'_{X}(x) = \{(\tau, x)\}.$$

By Theorem 3 the triple $(\overline{\Sigma_\tau}, m', e')$ is a monad on $\mathcal{Kl}(\mathcal{P})$. By composing the two adjoint situations we get a monadic structure on the LTS functor. The composition in $\mathcal{Kl}(\mathcal{P}(\Sigma_\tau \times \mathcal{I}d))$ is given as follows. For $f : X \to \mathcal{P}(\Sigma_\tau \times Y)$ and $g : Y \to \mathcal{P}(\Sigma_\tau \times Z)$ we have $g \cdot f : X \to \mathcal{P}(\Sigma_\tau \times Z)$:

$$g \cdot f(x) = \{(\sigma, z) \mid x \xrightarrow{\sigma} f \quad y \xrightarrow{\tau} g \quad z \text{ or } x \xrightarrow{\sigma} f \quad y \xrightarrow{\tau} g \quad z \text{ for some } y \in Y\}.$$

The construction provided by Theorem 3 can be applied only when $\mathcal{Kl}(T)$ is a category with zero morphisms. Some monads fail to have this property. For example, if instead of considering the monad $\mathcal{P}$ we consider the non-empty powerset monad $\mathcal{P}_{\neq \emptyset}$. In what follows we focus on the second strategy for handling internal transitions by a monadic structure on the functor which does not require from $\mathcal{Kl}(T)$ to be a category with zero morphisms.

**Monadic structure on $TF^*$** Here, we present an approach towards dealing with silent moves which uses free monads. At the beginning of this section we stated clearly that the coalgebras we are dealing with are of the type $TF_\tau$. Any $TF_\tau$-coalgebra $\alpha : X \to TF_\tau X$ can be turned into a $TF^*$-coalgebra $\underline{\alpha} : X \to TF^* X$ by putting

$$\underline{\alpha} = T([\nu_X, e_X]) \circ \alpha,$$

where the mono-transformation $[\nu, e] : F_\tau \implies F^*$ comes from the definition of a free monad.

**Example 5.** Consider the LTS functor $\mathcal{P}(\Sigma_\tau \times \mathcal{I}d) \cong \mathcal{P}(\Sigma \times \mathcal{I}d + \mathcal{I}d)$ and let $F = \Sigma \times \mathcal{I}d$. The free monad over $F$ in Set is given by $(\Sigma^* \times \mathcal{I}d, m, e)$, where $\Sigma^*$ is the set of finite words over $\Sigma$ together with the empty string $\varepsilon \in \Sigma^*$ and $m$ and $e$ are given for any set $X$ as follows:

$$m_X : \Sigma^* \times \Sigma^* \times X \to \Sigma^* \times X; (s, s', x) \mapsto (ss', x) \text{ and} \\ e_X : X \to \Sigma^* \times X; x \mapsto (\varepsilon, x).$$

For any $\alpha : X \to \mathcal{P}(\Sigma_\tau \times X)$ we define $\underline{\alpha} : X \to \mathcal{P}(\Sigma^* \times X)$ by

$$\underline{\alpha}(x) = \{(a, y) \mid (a, y) \in \alpha(x) \text{ and } a \in \Sigma\} \cup \{(\varepsilon, y) \mid (\tau, y) \in \alpha(x)\}.$$

**Example 6.** The $\varepsilon$-NA's are coalgebras of the type $TF_\tau$ for the monad $T = \mathcal{P}$ and $F = \Sigma \times \mathcal{I}d + 1$. The functor $F = \Sigma \times \mathcal{I}d + 1$ lifts to $\mathcal{Kl}(\mathcal{P})$ [17] and admits all free $F$-algebras. Let $F^*$ denote the free monad over $F$. The functor $F^* : \mathcal{Set} \to \mathcal{Set}$ is defined on objects and morphisms by

$$F^*X = \Sigma^* \times X + \Sigma^*, \\ F^*f : \Sigma^* \times X + \Sigma^* \to \Sigma^* \times Y + \Sigma^*; F^*f = (id_{\Sigma^*} \times f) + id_{\Sigma^*} \text{ for } f : X \to Y.$$
The monadic structure $(F^*, m, e)$ is given by:

$$ m_X : \Sigma^* \times (\Sigma^* \times X + \Sigma^*) + \Sigma^* \to \Sigma^* \times X + \Sigma^*; \\ m_X(s_1, s_2, x) = (s_1 s_2, x) \quad m_X(s_1, s_2) = s_1 s_2 \quad m_X(s_1) = s_1, \\ e_X : X \to \Sigma^* \times X + \Sigma^*; x \mapsto (\varepsilon, x). $$

For any $\varepsilon$-NA coalgebra $\alpha : X \to \mathcal{P}(\Sigma_\varepsilon \times X + 1)$ we define

$$ \underline{\alpha} : X \to \mathcal{P}(\Sigma^* \times X + \Sigma^*); x \mapsto \{(a, y) \in \Sigma^* \times X \mid (a, y) \in \alpha(x)\} \cup A_x, $$

where $A_x = \text{if } \forall \in \alpha(x) \text{ then } \{\varepsilon\} \text{ else } \emptyset$.

In order to proceed with the construction we need one additional lemma.

**Lemma 1.** [8] The algebra $i_X^\sharp = \eta_{F^*X} \circ i_X : FF^*X + X \to TF^*X$ is the free $\overline{F}$-algebra over $X$ in $\mathcal{Kl}(T)^{\overline{F}}$.

Let $\overline{F}^* : \mathcal{Kl}(T) \to \mathcal{Kl}(T)$ be the functor obtained by following the guidelines of Theorem 2 using the family $\{i_X^\sharp\}_{X \in \mathcal{Kl}(T)}$ of free algebras in $\mathcal{Kl}(T)^{\overline{F}}$.

**Theorem 4.** [8] We have the following:

1. $F^* : C \to C$ lifts to $\overline{F}^* : \mathcal{Kl}(T) \to \mathcal{Kl}(T)$,

2. $(\overline{F}^*, m^\sharp, e^\sharp)$ is the free monad over $\overline{F}$ in $\mathcal{Kl}(T)$.

Two adjoint situations $C \rightleftharpoons \mathcal{Kl}(T) \rightleftharpoons \mathcal{Kl}(\overline{F}^*)$ yield a monadic structure on $TF^*$.

The composition $\cdot$ in $\mathcal{Kl}(TF^*) = \mathcal{Kl}(\overline{F}^*)$ is given as follows. Let $\lambda : F^*T \Rightarrow TF^*$ denote the distributive law associated with the lifting $\overline{F}^*$ of $F^*$. The composition of $f : X \to TF^*Y, g : Y \to TF^*Z$ in $\mathcal{Kl}(TF^*)$ is given by:

$$ \begin{aligned} g \cdot f = \mu_{F^*Z} \circ T\mu_{F^*Z} \circ TTm_Z^\sharp \circ T\lambda_{F^*Z} \circ TF^*g \circ f &= \mu_{F^*Z} \circ T\mu_{F^*Z} \circ TT(\eta_Z \circ m_Z) \circ T\lambda_{F^*Z} \circ TF^*g \circ f = \mu_{F^*Z} \circ TTm_Z \circ T\lambda_{F^*Z} \circ TF^*g \circ f. \end{aligned} $$

**Example 7.** The composition $\cdot$ in $\mathcal{Kl}(\mathcal{P}(\Sigma^* \times \mathcal{I}d))$ is given by the following formula. For $f : X \to \mathcal{P}(\Sigma^* \times Y)$ and $g : Y \to \mathcal{P}(\Sigma^* \times Z)$ we have $g \cdot f : X \to \mathcal{P}(\Sigma^* \times Z)$:

$$ g \cdot f(x) = \{(s_1 s_2, z) \mid x \xrightarrow{s_1} f \quad y \xrightarrow{s_2} g \quad z \text{ for some } y \in Y \text{ and } s_1, s_2 \in \Sigma^*\}. $$

We call the monad $\mathcal{P}(\Sigma^* \times \mathcal{I}d)$ free LTS monad.

**Example 8.** The composition $\cdot$ in $\mathcal{Kl}(\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*))$ is given by the following formula. For $f : X \to \mathcal{P}(\Sigma^* \times Y + \Sigma^*)$ and $g : Y \to \mathcal{P}(\Sigma^* \times Z + \Sigma^*)$ we have $g \cdot f : X \to \mathcal{P}(\Sigma^* \times Z + \Sigma^*)$:

$$ \begin{aligned} g \cdot f(x) = &\{(s_1 s_2, z) \mid x \xrightarrow{s_1} f \quad y \xrightarrow{s_2} g \quad z \text{ for some } y \in Y \text{ and } s_1, s_2 \in \Sigma^*\} \cup \\ &\{s_1 s_2 \mid x \xrightarrow{s_1} f \text{ and } s_2 \in g(y) \cap \Sigma^*, \text{ for some } y \in Y\} \cup \\ &\{s_1 \in \Sigma^* \mid s_1 \in f(x)\}. \end{aligned} $$

We call $\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*)$ monad free $\varepsilon$-NA monad or $\varepsilon$-NA monad in short.
We see that if we deal with functors of the form $T(F + \mathcal{I}d)$, where $T$ is a
monad, given some mild assumptions on $T$ and $F$ we may deal with the silent
and observable part of computation inside a monadic structure on the functor
$TF_\tau$ itself or by embedding the functor $TF_\tau$ into the monad $TF^*$ by the natural
transformation $F_\tau \Rightarrow F^*$. Therefore, from now on the term "coalgebras with
internal moves" becomes synonymous to "coalgebras over a monadic type". Weak
bisimulation and, as we will also see, trace equivalence are defined for coalgebras
over monadic types, without the need for specifying visible and silent part of the
structure.

4 Weak bisimulation

In this section we recall classical definition(s) of weak bisimulation for labelled
transition systems and coalgebraic constructions from [8]. Weak bisimulation
for labelled transition systems can be defined as a strong bisimulation on a
saturated structure. Process of saturation can be described as taking the reflexive
and transitive closure of a given structure w.r.t. the suitable composition and
order. First of all we present a paragraph devoted to classical definitions of weak
bisimulation for LTS. Then we show how Kleisli compositions from Examples 4
and 7 play role in the LTS saturation. These examples motivate the definition
of an order saturation monad and weak bisimulation [8]. What is essentially
new in this section is the following. First of all we present a definition of weak
bisimulation in terms of a kernel bisimulation on the saturated structure and
not via lax- and oplax-homomorphisms in Aczel-Mendler style as it was done
in [8]. Second of all, the last paragraph compares the two generalizations of the
strategies towards saturation from the point of view of weak bisimulation which
was not done in [8].

**Weak bisimulation for LTS** Let $\alpha : X \to \mathcal{P}(\Sigma_{\tau} \times X)$ be a labelled transition system coalgebra. For $\sigma \in \Sigma_{\tau}$ and $s \in \Sigma^{*}$ define the relations $\underset{\sigma}{\Rightarrow} \stackrel{s}{\to}$, $\underset{s}{\Rightarrow} \subseteq$
$X \times X$ by

$$
\begin{align*}
\stackrel{\sigma}{\Rightarrow} &= \left\{ \begin{array}{ll} (\xrightarrow{\tau})^* & \text{if } \sigma = \tau \\ (\xrightarrow{\tau})^* \circ \xrightarrow{\sigma} \circ (\xrightarrow{\tau})^* & \text{otherwise,} \end{array} \right. & \stackrel{s}{\Rightarrow} &= \left\{ \begin{array}{ll} \xrightarrow{\tau} & \text{if } s = \varepsilon \\ \xrightarrow{\sigma_1} \circ \dots \circ \xrightarrow{\sigma_n} & \text{for } s = \sigma_1 \dots \sigma_n, \end{array} \right. \\
\stackrel{s}{\Rightarrow} &= \left\{ \begin{array}{ll} (\xrightarrow{\tau})^* & \text{if } s \text{ is the empty word} \\ (\xrightarrow{\tau})^* \circ \xrightarrow{\sigma_1} \circ (\xrightarrow{\tau})^* \circ \dots \circ (\xrightarrow{\tau})^* \circ \xrightarrow{\sigma_n} \circ (\xrightarrow{\tau})^* & \text{for } s = \sigma_1 \dots \sigma_n \end{array} \right.
\end{align*}
$$

where, given any relation $R \subseteq X \times X$, the symbol $R^*$ denotes the reflexive and transitive closure of $R$. We now present four different but equivalent definitions of weak bisimulation for LTS's. Due to limited space we do so in one definition block.

**Definition 1.** [29,30,36] A relation $R \subseteq X \times X$ is called weak bisimulation on $\alpha$ if the following condition holds. If $(x, y) \in R$ then
(i) for any $\sigma \in \Sigma_\tau$ the condition $x \stackrel{\sigma}{\to} x'$ implies $y \stackrel{\sigma}{\Rightarrow} y'$

(ii) for any $\sigma \in \Sigma_\tau$ the condition $x \stackrel{\sigma}{\Rightarrow} x'$ implies $y \stackrel{\sigma}{\Rightarrow} y'$

(iii) for any $s \in \Sigma^*$ the condition $x \stackrel{s}{\to} x'$ implies $y \stackrel{s}{\Rightarrow} y'$

(iv) for any $s \in \Sigma^*$ the condition $x \stackrel{s}{\Rightarrow} x'$ implies $y \stackrel{s}{\Rightarrow} y'$

and $y' \in X$ such that $(x', y') \in R$ and a symmetric statement holds.

In this paper we will focus on Definitions 1.ii and 1.iv and their generalization. They both suggest that weak bisimulation can be defined as a strong bisimulation on a *saturated model*. It is worth noting that in our previous paper we focused on analogues of Def 1.i and 1.iii and comparison with Def 1.ii and 1.iv respectively (see [8] for details).

**Saturation for LTS coalgebraically** Let us assume that $\cdot$ is a composition in $Kl(P(\Sigma_\tau \times \mathcal{I}d))$ as in Example 4. Given an LTS coalgebra $\alpha : X \to P(\Sigma_\tau \times X)$ the saturated LTS $\alpha^* : X \to P(\Sigma_\tau \times X)$ is obtained as follows: $\alpha^* = 1_X \vee \alpha \vee \alpha \cdot \alpha \vee \dots = \bigvee_{n=0,1,2,\dots} \alpha^n$, where $\bigvee$ denotes supremum in the complete lattice $(P(\Sigma_\tau \times X)^X, \leq)$, where the relation $\leq$ is given by $\alpha \leq \beta \iff \alpha(x) \subseteq \beta(x)$ for any $x \in X$. We see that for $(\sigma, y) \in \Sigma_\tau \times X: (\sigma, y) \in \alpha^*(x)$ if and only if $x \stackrel{\sigma}{\Rightarrow} \alpha y$. Weak bisimulation on $\alpha$ according to Definition 1.ii is a strong bisimulation on $\alpha^*$.

If we now consider $\cdot$ to be composition in $Kl(P(\Sigma^* \times \mathcal{I}d))$ as in Example 7 for an LTS considered as a $P(\Sigma^* \times \mathcal{I}d)$-coalgebra $\alpha : X \to P(\Sigma^* \times X)$ define $\alpha^* : X \to P(\Sigma^* \times X)$ to be $\alpha^* = 1_X \vee \alpha \vee \alpha \cdot \alpha \vee \dots = \bigvee_{n=0,1,2,\dots} \alpha^n$. Then $(s, y) \in \alpha^*(x)$ if and only if $x \stackrel{s}{\Rightarrow} \alpha y$ for any $s \in \Sigma^*$. Weak bisimulation from Def. 1.iv is a strong bisimulation on $\alpha^*$.

**Saturation for T-coalgebras** A monad $T$ whose Kleisli category is order-enriched is called *ordered $*$-monad or *ordered saturation monad* [8] provided that in $Kl(T)$ for any morphism $\alpha : X \to X$ there is a morphism $\alpha^* : X \to X$ satisfying the following conditions:

(a) $1 \leq \alpha^*$,

(b) $\alpha \leq \alpha^*$,

(c) $\alpha^* \cdot \alpha^* \leq \alpha^*$,

(d) if $\beta : X \to X$ satisfies $1 \leq \beta$, $\alpha \leq \beta$ and $\beta \cdot \beta \leq \beta$ then $\alpha^* \leq \beta$,

(e) for any $f : X \to Y$ in $C$ and any $\beta : Y \to X$ in $Kl(T)$ we have:

$$f^{\sharp} \cdot \alpha \sqcap \beta \cdot f^{\sharp} \Rightarrow f^{\sharp} \cdot \alpha^* \sqcap \beta^* \cdot f^{\sharp} \text{ for } \sqcap \in \{\leq, \geq\}.$$

For the rest of the section we assume that $T$ is an order saturation monad with the saturator operator $(-)^*$.

**Remark 1.** We could try and define $\alpha^*$ as the least fix point $\mu x.(1 \vee x \cdot \alpha)$. Indeed, if $T$ is e.g. complete join-semilattice enriched monad then the saturated structure is defined this way. We believe that our definition is slightly more general as it does not require for the mapping $x \mapsto 1 \vee x \cdot \alpha$ to be well defined. Intuitively however, $\alpha^*$ should and will be associated with $\mu x.(1 \vee x \cdot \alpha)$.
**Example 9.** The powerset monad $\mathcal{P}$ and the non-empty powerset monad $\mathcal{P}_{\neq\emptyset}$ are examples of order saturation monads [8]. The monads from Examples 4 and 7 are order saturation monads [8]. Also the $\mathcal{CM}$ monad of convex distributions described in [20] is an order saturation monad [8]. Although we will not focus on $\mathcal{CM}$ in this paper it is a very important monad that is used to model Segala systems, their trace semantics and probabilistic weak bisimulations [8,20,37,38]. Any Kleene monad [12] is also an order saturation monad [8].

Since $\mathcal{P}$, $\mathcal{P}(\Sigma_{\tau} \times \mathcal{I}d)$ and $\mathcal{P}(\Sigma^{*} \times \mathcal{I}d)$ are order saturation monads, the following question arises: is the saturation operator for LTS monads related to saturation in $\mathcal{Kl}(\mathcal{P})$? The following theorem answers that question in general and shows the relation between a saturation operator in $\mathcal{Kl}(T)$ and $\mathcal{Kl}(TS)$ for a monad $\bar{S}$ on $\mathcal{Kl}(T)$.

**Theorem 5.** [8] Assume $S: \mathcal{C} \to \mathcal{C}$ lifts to $\bar{S}: \mathcal{Kl}(T) \to \mathcal{Kl}(T)$ and $(\bar{S}, m, e)$ is a monad on $\mathcal{Kl}(T)$. If $\bar{S}$ is locally monotonic and satisfies the equation

$$m_X \cdot \bar{S}[(m_X \cdot \bar{S}\alpha)^* \cdot e_X] = (m_X \cdot \bar{S}\alpha)^*$$

for any $\alpha: X \to \bar{S}X$, then the monad $TS$ is an order saturation monad with the saturation operator $(-)^{\star}$ given by $\alpha^{\star} = (m_X \cdot \bar{S}\alpha)^* \cdot e_X$.

If $T = \mathcal{P}$ and $S$ is taken either to be $\Sigma_{\tau} \times \mathcal{I}d$ or $\Sigma^{*} \times \mathcal{I}d$, then the lifting $\bar{S}$ exists and is equipped with a monadic structure as in Section 3. Moreover, $\bar{S}$ satisfies the assumptions of Theorem 5 [8]. In other words, the LTS saturations for $\mathcal{P}(\Sigma_{\tau} \times \mathcal{I}d)$ and $\mathcal{P}(\Sigma^{*} \times \mathcal{I}d)$ are obtained respectively by

$$(m'_{X} \cdot \overline{\Sigma_{\tau} \alpha})^{*} \cdot e'_{X} \text{ and } (m''_{X} \cdot \overline{\Sigma^{*} \alpha})^{*} \cdot e''_{X}.$$

In sections to come we will deal with generalizations of these two saturations and check under which conditions they yield the same notion of weak bisimulation.

**Weak bisimulation for T-coalgebras** The following slogan should be in our opinion considered the starting point to the theory of weak bisimulation for T-coalgebras: weak bisimulation on $\alpha: X \to TX = \text{bisimulation on } \alpha^*: X \to TX$.

**Definition 2.** Let $\alpha: X \to TX$ be a T-coalgebra. A relation $X \stackrel{\pi_1}{\leftarrow} R \stackrel{\pi_2}{\to} X$ is weak bisimulation on $\alpha$ if it is a bisimulation on $\alpha^*$.

We see that the above definition coincides with the standard definition of weak bisimulation for LTS considered as $\mathcal{P}(\Sigma_{\tau} \times \mathcal{I}d)$- and $\mathcal{P}(\Sigma^{*} \times \mathcal{I}d)$-coalgebras.

**Weak bisimulation for $TF_{\tau}$- and $TF^{*}$-coalgebras** This subsection will be devoted to comparing both approaches towards defining weak bisimulation for $TF_{\tau}$-coalgebras that generalize Def. 1.ii and 1.iv for LTS. Here, we additionally assume that $\mathcal{Kl}(T)$ is a category with zero morphisms. Then we may either define a monadic structure on $TF_{\tau}$ or embed the functor into the monad $TF^{*}$.
These two approaches applied for LTS give two different saturations, yet the weak bisimulations coincide. It is natural to suspect that given some mild assumptions it will also be the case in a more general setting. We will now list all the necessary ingredients.

We assume $(\overline{F}_{\tau}, m', e')$ and $(\overline{F}^*, m^\sharp, e^\sharp)$ are monads as in Section 3 and that both satisfy the assumptions of Theorem 5 for the monad $\overline{S}$. For sake of simplicity and clarity of notation we will drop $\sharp$ and write $(\overline{F}^*, m, e)$ instead of $(\overline{F}^*, m^\sharp, e^\sharp)$. The consequences of these assumptions are the following:

- A natural transformation $\nu : \overline{F} \Rightarrow \overline{F}^*$ which arises by the definition of a free monad.

- A natural transformation $\iota^1 : \overline{F} \Rightarrow \overline{F}_{\tau} = \overline{F} + \mathcal{I}d = \overline{F} + \mathcal{I}d$. This transformation is given regardless of the assumptions.

- Unique monad morphism $h : (\overline{F}^*, m, e) \to (\overline{F}_{\tau}, m', e')$ in $\mathcal{Kl}(T)$ making the first three diagrams commute:

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

Commutativity of the first two diagrams implies commutativity of the fourth. Existence and uniqueness of $h$ follows by the fact that $\overline{F}^*$ is a free monad over $\overline{F}$ and $\iota^1 : \overline{F} \Rightarrow \overline{F}_{\tau}$ is a natural transformation.

- The monads $TF_{\tau}$ and $TF^*$ are order saturation monads. The saturation operators $(-)^{\star}$ and $(-)^*$ for $TF_{\tau}$- and $TF^$-coalgebras resp. are given as follows. Let $\alpha : X \to \overline{F}_{\tau}X$ (i.e. $\alpha : X \to TF_{\tau}X$) and $\beta : Y \to \overline{F}^*Y$ (i.e. $\beta : Y \to TF^*Y$). We have:

$$ \alpha^{\star} = (m'_{X} \cdot \overline{F}_{\tau}\alpha)^{*} \cdot e'_{X} \quad \text{and} \quad \beta^{*} = (m_{Y} \cdot \overline{F}^{*}\beta)^{*} \cdot e_{Y}. $$

*Example 10.* Let $T = \mathcal{P}$ and $F_{\tau} = \Sigma_{\tau} \times \mathcal{I}d$, $F^{*} = \Sigma^{*} \times \mathcal{I}d$. The morphism $h_{X} : \Sigma^{*}X \to \overline{\Sigma}_{\tau}X$ is given by:

$$ h_X : \Sigma^* \times X \to \mathcal{P}(\Sigma_\tau \times X); (s, x) \mapsto \begin{cases} \{(\tau, x)\} & \text{if } |s| = 0, \\ \{(s, x)\} & \text{if } |s| = 1, \\ \emptyset & \text{otherwise.} \end{cases} $$

Consider any coalgebra $\alpha : X \to \overline{F}_{\tau}X$ and let $\underline{\alpha} : X \to \overline{F}^*X$ be given by $\underline{\alpha} = [\nu_X, e_X] \cdot \alpha$. Note that this is the same coalgebra as in the paragraph on monadic structure on $TF^*$ in Section 3. Here, however, it is defined in terms of the composition in $\mathcal{Kl}(T)$ and not $\mathcal{C}$, and all superscripts $\sharp$ are dropped to simplify the notation. By commutativity of the last diagram above we have:

$$ h_X \cdot \underline{\alpha} = h_X \cdot [\nu_X, e_X] \cdot \alpha = \alpha. $$

We will now try to compare bisimulations for $\alpha^\star$ and $\underline{\alpha}^*$. In case of labelled transition systems a relation is a bisimulation on $\alpha^\star$ if and only if it is a bisimulation on $\underline{\alpha}^*$. Below we verify how general is this statement and what conditions are required to be satisfied for it to remain true.
**Lemma 2.** Assume that for any $\phi: \overline{F}^*X \to \overline{F}^*X$ and $\psi: \overline{F}_\tau X \to \overline{F}_\tau X$ if $\psi \cdot h_X = h_X \cdot \phi$ then $\psi^* \cdot h_X = h_X \cdot \phi^*$. In this case we have $h_X \cdot \underline{\alpha}^* = \alpha^*.$

**Remark 2.** Note that the assumption in Lemma 2 about the natural transformation $h$ is crucial even though $T$ is assumed to be an order saturation monad. Assumption (e) in the definition of order saturation monad does not guarantee that $h$ satisfies the desired property since it is not in general of the form $h'^{\#}$ for some $h': F^*X \to F_\tau X$ in $\mathcal{C}$. However, if $T$ is a Kleene monad [8,12] then this assumption is always satisfied. The powerset monad $\mathcal{P}$ is an example of a Kleene monad.

The following theorem follows directly from the above lemma.

**Theorem 6.** Assume that for any $\phi: \overline{F}^*X \to \overline{F}^*X$ and $\psi: \overline{F}_\tau X \to \overline{F}_\tau X$ if $\psi \cdot h_X = h_X \cdot \phi$ then $\psi^* \cdot h_X = h_X \cdot \phi^*$. Any bisimulation on $\underline{\alpha}^*$ is a bisimulation on $\alpha^*$.

Our aim now will be to prove the converse.

**Lemma 3.** We have $\underline{\alpha}^* \leq (\underline{\alpha^*})^*$.

**Remark 3.** Before we state the next result we have to make one essential remark. Note that the technical condition concerning the transformation $[\nu, e]$ in the lemma below would follow from $[\nu, e]$ being a monad morphism. However, $[\nu, e]: \overline{F}_\tau \Rightarrow \overline{F}^*$ is not a monad morphism. It does not satisfy the 2nd axiom of a monad morphism. To see this consider $T = \mathcal{P}$, $(\overline{\Sigma}_\tau, m', e')$, $(\overline{\Sigma}^*, m, e)$ as in Examples 4 and 7 and a visible label $a \in \Sigma$. We have

$$[\nu_X, e_X] \cdot m'_X(a, a, x) = \emptyset \text{ and} \\ m_X \cdot [\nu_{\overline{\Sigma}^*X}, e_{\overline{\Sigma}^*X}] \cdot \overline{\Sigma}_\tau[\nu_X, e_X](a, a, x) = \{(aa, x)\}.$$

**Lemma 4.** Assume $[\nu_X, e_X] \cdot m'_X \cdot \overline{F}_\tau \alpha \leq m_X \cdot \overline{F}^* \underline{\alpha} \cdot [\nu_X, e_X]$. Then $\underline{\alpha^*} \leq \underline{\alpha}^*$.

**Theorem 7.** Let $\alpha$ satisfy the inequality from the assumptions of the previous statement. Any bisimulation on $\alpha^*$ is a bisimulation on $\underline{\alpha}^*$.

*Proof.* We have $\alpha \leq \alpha^*$ and hence $\underline{\alpha} \leq \underline{\alpha^*}$. This, together with Lemma 4, implies that $\underline{\alpha}^* \leq (\underline{\alpha^*})^* \leq (\underline{\alpha}^*)^* \stackrel{\diamond}{=} \underline{\alpha}^*$ (see [8] for a proof of the equality marked with (◇)). Assume $X \stackrel{\pi_1}{\leftarrow} R \stackrel{\pi_3}{\rightarrow} X$ is a bisimulation on $\alpha^*$. It is also a bisimulation on $\underline{\alpha^*}$. Finally, since $\underline{\alpha}^* = (\underline{\alpha^*})^*$ the relation $R$ is a bisimulation on $\underline{\alpha}^*$.

**Theorem 8.** Assume that cotupling $[-, -]$ in $\mathcal{Kl}(T)$ is monotonic w.r.t. both arguments and the zero morphisms $0_{X,Y}: X \to Y$ are the least elements of the posets $\text{Hom}_{\mathcal{Kl}(T)}(X, Y)$. Then any bisimulation on $\alpha^*$ is a bisimulation on $\underline{\alpha}^*$.

**Remark 4.** The powerset monad $\mathcal{P}$ satisfies assumptions of the above theorem. It is worth mentioning that the $\mathcal{CM}$ monad used to model Segala systems does not satisfy them as the zero morphisms in $\mathcal{Kl}(\mathcal{CM})$ are not least elements of the partially ordered hom-sets [20]. The monad $\mathcal{CM}$ deserves a separate treatment and we leave this for future research.
## 5 Trace semantics for coalgebras with internal moves

The aim of this section is to present some ideas on how to approach the notion of trace semantics for structures with invisible moves. As mentioned before in order to distinguish the trace semantics for coalgebras with and without silent steps we will often use the term weak trace semantics or trace semantics for structures with internal moves to refer to the former.

Before we go into details we start this section by recalling a basic example of trace semantics for ε-NA's [18].

**Definition 3.** Given a non-deterministic automaton with ε-transitions α : X → P(Σε × X + 1) its trace semantics is a morphism trα : X → P(Σ*) which maps any state x ∈ X to the set of words over Σ it accepts. To be more precise, for a word w ∈ Σ* we have w ∈ trα(x) provided that either w = ε and ∨ ∈ α(x) or w = a₁...aₙ for aᵢ ∈ Σ and there is x' ∈ X such that

$$x(\xrightarrow{\varepsilon})^* \circ \xrightarrow{a_1} (\xrightarrow{\varepsilon})^* \circ \dots \circ (\xrightarrow{\varepsilon})^* \xrightarrow{a_n} (\xrightarrow{\varepsilon})^* x'$$

with ∨ ∈ α(x').

The above definition is an instance of what we call a “bottom-up” approach towards trace semantics for non-deterministic automata with internal moves. This approach considers ε steps as invisible steps that can wander around a structure freely. In other words, from our perspective ε-steps that are used in this definition are what they should be, i.e. are part of the unit of the ε-NA monad. There is a second obvious approach towards defining trace semantics for ε-NA's. We call this approach “top-down”, since at first we treat ε steps artificially as if they were standard visible steps. Given an ε-NA α : X → P(Σε × X + 1) we find its trace tr'α : X → P((Σ ∪ {ε})^*) and then map all words from (Σ ∪ {ε})^* to words in Σ* by removing all occurrences of the ε label. As a result we obtain the same trace as in Def. 3. Since in many cases we know how to find finite trace semantics for coalgebras with only visible steps [17] it is easy to generalize the “top-down” approach to coalgebras with internal activities. This is exactly how authors of [16,39] do it in their papers. We, however, will present a bottom-up approach towards weak trace semantics that works for a large family of coalgebras whose type is a monad.

**Coalgebraic view on weak trace semantics for ε-NA** In this subsection we focus on coalgebras for the monad P(Σ* × X + Σ*). Recall that by Example 6 any ε-NA coalgebra α : X → P(Σε × X + 1) can be considered a P(Σ* × X + Σ*)-coalgebra. For simplicity and clarity of notation put F = Σ × Id + 1 and F* = Σ* × Id + Σ*. Let us list two basic facts concerning ε-NA monad:

- The lifting $\bar{F}^*$ : Kl(P) → Kl(P) is locally continuous [17].

- The ε-NA monad PF* is Cppo-enriched. This follows by Theorem 1.
For any $\alpha: X \to X$ in $\mathcal{Kl}(\mathcal{PF}^*)$ (i.e. $\alpha: X \to \mathcal{PF}^*X$) define the following mapping $\text{tr}_\alpha: X \to \emptyset$ (i.e. $\text{tr}_\alpha: X \to \mathcal{P}(\Sigma^*)$):

$$ \text{tr}_{\alpha} = \bigvee_{n \in \mathbb{N}} \perp \cdot \alpha^{n}, $$

where $\perp: X \to \emptyset$ is given by $\perp: X \to \mathcal{P}(\Sigma^*); x \mapsto \emptyset$ and $\cdot$ denotes the composition in $\mathcal{Kl}(\mathcal{PF}^*)$ as in Example 8. It is simple to see that $\text{tr}_\alpha$ is the least morphism in $\text{Hom}_{\mathcal{Kl}(\mathcal{PF}^*)}(X, \emptyset) = \text{Hom}_{\text{Set}}(X, \mathcal{P}(\Sigma^*))$ satisfying $\text{tr}_\alpha = \text{tr}_\alpha \cdot \alpha$. In other words,

$$ \text{tr}_{\alpha} = \mu x.x \cdot \alpha. $$

Recursively, if we put $\text{tr}_0 = \perp$ and $\text{tr}_n = \text{tr}_{n-1} \cdot \alpha$ then $\text{tr}_\alpha = \bigvee_n \text{tr}_n$.

**Example 11.** Let $\Sigma = \{a, b\}$ and let $\alpha: X \to \mathcal{P}(\Sigma_\varepsilon \times X + 1)$ be given by the following diagram (\varepsilon-labels are omitted). We have $\text{tr}_0: X \to \mathcal{P}(\Sigma^*), x \mapsto \emptyset$ and

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

$\text{tr}_1: x \mapsto \emptyset, y \mapsto \emptyset, z \mapsto \{\varepsilon\},$

$\text{tr}_2: x \mapsto \emptyset, y \mapsto \{b\}, z \mapsto \{\varepsilon\},$

$\text{tr}_3: x \mapsto \{b\}, y \mapsto \{ab, b\}, z \mapsto \{\varepsilon\},$

$\text{tr}_4: x \mapsto \{ab, b\}, y \mapsto \{aab, ab, b\},$

$z \mapsto \{b, \varepsilon\}$

The following result can be shown by straightforward verification.

**Theorem 9.** For any $\varepsilon$-NA coalgebra considered as $\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*)$-coalgebra the trace semantics morphism from Def. 3 and the morphism $\text{tr}_\alpha$ above coincide.

**Weak coalgebraic trace semantics via fixed point operator** We see that for $\varepsilon$-NA's their weak trace semantics is obtained as the least fixed point of the assignment $x \mapsto x \cdot \alpha$ in $\mathcal{Kl}(\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*))$. Interestingly, such a fixed point is not unique.

**Example 12.** Let $\Sigma = \{a\}, X = \{x\}$ and let $\varepsilon$-NA $\alpha: X \to \mathcal{P}(\Sigma_\varepsilon \times X + 1)$ be defined by the following diagram: $x \mathcal{C} \xrightarrow{\varepsilon}$. It is easy to check that the morphism $g: X \to \mathcal{P}(\Sigma^*); x \mapsto \{a\}$ satisfies $g = g \cdot \alpha$ and it is not the least fixed point since the least fixed point is given by $\text{tr}_\alpha(x) = \emptyset$.

Here we generalize the ideas presented in the previous subsection to T-coalgebras. It should be noted at the very beginning that this section should serve as merely a starting point for future research.

Let us first focus on a known approach for defining trace semantics via coinduction in Kleisli category [17] and translating these results to our setting. In [17] the authors present trace semantics definition via coinduction for TF-coalgebras, where T is a monad and F satisfies some reasonable assumptions. In our setting however, we do not consider a special functor F or in other words $F = \mathcal{I}d$ and our coalgebras are T-coalgebras. Consider the category $\mathcal{Kl}(T)_{\mathcal{I}d}$ of $\mathcal{I}d$-coalgebras
in $Kl(T)$. Note that any $T$-coalgebra $\alpha: X \to TX$ is $\alpha: X \to X$ and is a member of $Kl(T)_{\mathcal{I}d}$. Based on the approach from [17] trace semantics of $\alpha$ should be obtained via coinduction in $Kl(T)_{\bar{F}}$. In our setting however, i.e. when $F = \mathcal{I}d$, the category $Kl(T)_{\mathcal{I}d}$ rarely admits the terminal object. For instance if we consider our $\varepsilon$-NA monad $\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*)$, the category of $\mathcal{I}d$-coalgebras $Kl(\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*))_{\mathcal{I}d}$ has no terminal object. However, it still makes sense to talk about trace for coalgebras for the monad $\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*)$. We did it via the least fixed point of the assignment $x \mapsto x \cdot \alpha$. In the general case we do it via uniform fixed point operator [41].

Assume that $C$ is a category with the initial object $0$ (this object is also initial in $Kl(T)$). A fixed point operator $f$ on $Kl(T)$ is a family of morphisms:

$$f: \operatorname{Hom}_{Kl(T)}(X, X) \to \operatorname{Hom}_{Kl(T)}(X, 0)$$

satisfying $f(\alpha) \cdot \alpha = f(\alpha)$ for any $\alpha: X \to X$. A fixed point operator $f$ on $Kl(T)$ is uniform w.r.t. $(-)^{\sharp}: C \to Kl(T)$ [41] if

$$h^{\sharp} \cdot \alpha = \beta \cdot h^{\sharp} \implies f(\beta) \cdot h^{\sharp} = f(\alpha)$$

for any $\alpha: X \to X$, $\beta: Y \to Y$ in $Kl(T)$ and $h: X \to Y$ in $C$. Coalgebraically speaking, the premise of the above implication says that the morphism $h$ is a homomorphism between coalgebras $\alpha: X \to TX$ and $\beta: Y \to TY$ in $C_T$. We call a uniform fixed point operator on $Kl(T)$ a coalgebraic trace operator and we denote it by $\text{tr}_{(-)}$.

**Theorem 10.** Assume that $Kl(T)$ is a Cppo-enriched category and assume that for any $f: X \to Y$ in $C$ we have $\perp \cdot f^{\sharp} = \perp$. For $\alpha: X \to X$ define $\text{tr}_{\alpha}: X \to 0$ by $\text{tr}_{\alpha} = \mu x.(x \cdot \alpha) = \bigvee_{n \in \mathbb{N}} \perp \cdot \alpha^n$. Then $\text{tr}_{(-)}$ is a coalgebraic trace operator on $Kl(T)$.

It may not be instantly clear for the reader why we choose uniformity as a property of a coalgebraic trace operator. Uniformity is a powerful notion which, in some forms, determines the least fixed point to be the unique uniform fixed point operator [41]. For the $\varepsilon$-NA monad $\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*)$ the least fixed point operator is a uniform fixed point operator w.r.t.

$$^{\sharp}: \mathbf{Set} \to Kl(\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*))$$

However, as we will see further on (Theorem 11 and Example 13), it is uniform also with respect to a richer category than $\mathbf{Set}$, namely, it is uniform w.r.t.:

$$^{\sharp}: Kl(\mathcal{P}(\Sigma^* \times \mathcal{I}d)) \to Kl(M_1) \cong Kl(\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*))$$

Uniqueness of a uniform fixed point operator on $Kl(T)$ can be imposed by initial algebra = final coalgebra coincidence in the base category $C$ [41]. This coincidence is the core of generic coalgebraic trace semantics theory [17]. This is why we believe that the uniform fixed point operators can and will serve as an extension of the generic coalgebraic trace semantics to weak trace semantics.
We end this section with a result that links weak trace semantics for ε-NA's to uniform traced monoidal categories in the sense of Joyal et al. [19]. However, instead of a uniform categorical trace operator on a monoidal category with binary coproducts and initial object we will equivalently work with a uniform Conway operator [15,19]. The following theorem (modulo the uniformity) can be found in [5].

**Theorem 11.** Assume C is equipped with a uniform Conway operator

$$(-)^{\dagger}_{X,A} : \mathrm{Hom}(X, X + A) \to \mathrm{Hom}(X, A).$$

Let A be an object in C and $M_A = \mathcal{I}d + A$ the exception monad on C. Then the operator $\mathrm{tr}_{(-)} : \mathrm{Hom}_{\mathrm{Kl}(M_A)}(X, X) \to \mathrm{Hom}_{\mathrm{Kl}(M_A)}(X, 0)$ defined by $\mathrm{tr}_{\alpha} = \alpha^{\dagger}$ for $\alpha : X \to X + A$ in C (or equivalently $\alpha : X \to \mathcal{I}X$ in $\mathrm{Kl}(M_A)$) is a coalgebraic trace operator on the category $\mathrm{Kl}(M_A)$ which is uniform w.r.t. $\mathbb{1} : C \to \mathrm{Kl}(M_A)$.

*Example 13.* The ε-NA's and their trace semantics fits into the above setting since the ε-NA monad satisfies:

$$\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*) \cong \mathcal{P}(\Sigma^* \times (\mathcal{I}d + 1)).$$

Hence, if we put $T = \mathcal{P}(\Sigma^* \times \mathcal{I}d)$ to be the free LTS monad then the ε-NA monad is given by $T(\mathcal{I}d+1) = T\mathcal{M}_1$. Since the free LTS monad $\mathcal{P}(\Sigma^* \times \mathcal{I}d) \cong \mathcal{P}(\Sigma^*)^{\mathcal{I}d}$ is an example of a quantale monad [21] on Set its Kleisli category $\mathrm{Kl}(\mathcal{P}(\Sigma^* \times \mathcal{I}d))$ with binary coproducts and initial object is equipped with a uniform Conway operator (or equivalently a uniform categorical trace operator) [15,21]. Therefore, if we put $C = \mathrm{Kl}(\mathcal{P}(\Sigma^* \times \mathcal{I}d))$ then the Kleisli category for the exception monad $\mathcal{M}_1 = \mathcal{I}d+1$ defined on C is isomorphic to the Kleisli category for ε-NA monad, i.e. $\mathrm{Kl}(\mathcal{M}_1) \cong \mathrm{Kl}(\mathcal{P}(\Sigma^* \times \mathcal{I}d + \Sigma^*))$. The analysis of the Conway operator for the Kleisli category for the monad $\mathcal{P}(\Sigma^* \times \mathcal{I}d)$ [21] leads to a conclusion that $\mathrm{tr}_{\alpha}$ obtained for ε-NA's via Theorem 11 is exactly the least fixed point operator we introduced in the previous subsection.

To conclude, when allowing invisible steps into our setting, i.e. considering coalgebras over monadic types, weak trace semantics becomes a categorical fixed point operator. Moreover, as the above example states, there is a strong connection between coalgebraic trace operator for ε-NA coalgebras and traced monoidal categories. Although traced categories have been studied from coalgebraic perspective in [21] they were considered a special instance of the generic coalgebraic trace theory. With Example 13 at hand we believe that it should be the other way around in many cases, i.e. coalgebraic trace semantics for coalgebras with internal moves is a direct consequence of the fact that certain Kleisli categories are traced monoidal categories.

# 6 Weak bisimulation and weak trace semantics

We have shown that two behavioural relations, namely, weak bisimulation and weak trace equivalence can be defined using fixed points of certain maps. In case
of trace equivalence this map is given by $x \mapsto x \cdot \alpha$, in case of weak bisimulation
it is $x \mapsto 1 \lor x \cdot \alpha$. We see that both equivalences should be considered individ-
ually, as they require different assumptions. Yet, in a restrictive enough setting
we should be able to compare these notions at once. Indeed, in the setting of
monads whose Kleisli category has hom-sets being complete join semilattices
and whose composition preserves all non-empty joins, it is possible for us to talk
about three behavioural equivalences at once, namely, weak trace semantics,
weak bisimilarity and bisimilarity. In this case we can prove the following.

**Theorem 12.** Let $T$ be a monad as above and let $\perp=\perp \cdot f^\sharp$ for any $f : X \to Y$ in C. A strong bisimulation on $\alpha : X \to TX$ is also a weak bisimulation on $\alpha$. Moreover, if we define the trace map to be $\text{tr}_\alpha = \mu x.x \cdot \alpha$ then $\text{tr}_\alpha = \text{tr}_{\alpha^*}$. In other words, weak bisimilarity implies weak trace equivalence.

# 7 Summary and future work

This paper shows that coalgebras with internal moves can be understood as
coalgebras over a type which is a monad. We believe that such a treatment
makes formulation of many different properties and behavioural equivalences
simpler. It is natural to suspect that many other types of different behavioural
equivalences can be translated into the coalgebraic setting this way. One of these
is dynamic bisimulation [31] which should be obtained as a strong bisimulation
on $\mu x.(\alpha \lor x \cdot \alpha)$ (i.e. a transitive closure of $\alpha$). We believe that this paper may
serve as a starting point for a larger project to translate some of the equivalences
from van Glabbeek's spectrum of different equivalences for state-based systems
with silent labels [11,36] into the setting of coalgebras with internal activities.

Finally, as mentioned in Section 5 we should aim at extending the coalgebraic
trace semantics theory for systems without internal transitions [17] to systems
with silent moves. Uniform fixed point operator could serve as such an extension.
Moreover, we should build a more traced monoidal category oriented theory of
coalgebraic traces and refer it to known results for generic coalgebraic trace.

*Acknowledgements* I would like to thank Alexandra Silva for inspiring me with the literature on categorical fixed points. I am also very grateful to anonymous referees for various comments and remarks that hopefully made this work more interesting and easier to follow.

# References

1. Abramsky, S., Jung, A.: Domain Theory. Handbook of Logic in Computer Science (1994), pp. 1-168.

2. Aczel, P., Mendler, N.: A final coalgebra theorem. Proc. CTCS 1989, Lecture Notes in Computer Science 389 (1989), pp. 357-365.

3. Baier, Ch., Hermanns H.: Weak bisimulation for fully probabilistic processes. Proc. CAV 1997, Lecture Notes in Computer Science 1254 (1997), pp. 119-130.
4. Beck, J.: Distributive laws. Lecture Notes in Mathematics 80 (1969), pp. 119-140.

5. Benton, N., Hyland, M.: Traced premonoidal categories. Theoretical Informatics and Applications 37 (4) (2003), pp. 273-299.

6. Bloom, S. L., Ésik, Z.: Iteration Theories. The Equational Logic of Iterative Processes. Springer (1993).

7. Brengos, T.: Weak bisimulations for coalgebras over ordered functors. Proc. IFIP TCS 2012, Lecture Notes in Computer Science 7604 (2012), pp. 87-103.

8. Brengos, T.: Weak bisimulations for coalgebras over ordered monads. CoRR abs/1310.3656 (2013) (submitted)

9. Barr, M.: Coequalizers and free triples. Math. Z. 116 (1970) 307-322.

10. Ghani, N., Uustalu, T.: Coproducts of ideal monads. RAIRO - Theoretical Informatics and Applications 38 (2004), pp. 321-342.

11. Glabbeek van, R. J.: The Linear Time-Branching Time Spectrum II - The semantics of sequential systems with silent moves. Lecture Notes in Computer Science 715 (1993), pp 66-81.

12. Goncharov, S.: Kleene monads. Ph.D. thesis (2010).

13. Goncharov, S., Pattinson, D.: Weak Bisimulation for Monad-Type Coalgebras. (2013) Slides. http://www8.cs.fau.de/~sergey/talks/weak-talk.pdf

14. Gumm, H.P.: Elements of the general theory of coalgebras. LUATCS 99, Rand Afrikaans University, Johannesburg (1999)

15. Hasegawa, M.: Models of Sharing Graphs. A Categorical Semantics of let and letrec. Ph. D. thesis. University of Edinburgh (1997)

16. Hasuo, I., Jacobs, B., Sokolova, A.: Generic Forward and Backward Simulations. (Partly in Japanese) Proc. JSSST Annual Meeting (2006).

17. Hasuo, I., Jacobs, B., Sokolova, A.: Generic Trace Semantics via Coinduction. Logical Methods in Computer Science 3 (4:11) (2007) pp. 1-37.

18. Hopcroft, J.E., Motwani, R., Ullman, J. D.: Introduction to Automata Theory, Languages, and Computation. 3rd Edition. Prentice Hall (2006)

19. Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 3 (1996) pp. 447-468.

20. Jacobs, B.: Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. Electronic Notes in Theoretical Computer Science 203(5) (2008), pp. 131-152.

21. Jacobs, B.: From Coalgebraic to Monoidal Traces. Electronic Notes in Theoretical Computer Science 264(2) (2010), pp. 125-140.

22. Jacobs, B., Silva, A., Sokolova, A.: Trace Semantics via Determinization. Lecture Notes in Computer Science 7399 (2012), pp. 109-129.

23. Kock, A.: Strong functors and monoidal monads. Archiv der Mathematik 23(1) (1972), pp. 113-120.

24. Mac Lane S.: Categories for working mathematician. Springer 2nd edition (1998)

25. Manes, E.: Algebraic Theories. Springer 1st edition (1976)

26. Manes, E., Mulry, Ph.: Monad Compositions I: General constructions and recursive distributive laws. Theory and Applications of Categories 18 (7) (2007), pp. 172-208.

27. Miculan, M., Peressotti, M.: Weak bisimulations for labelled transition systems weighted over semirings. CoRR abs/1310.4106 (2013)

28. Milius, S.: On Iteratable Endofunctors. Electronic Notes in Theoretical Computer Science 69 (2003)

29. Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science 92 (1980)

30. Milner, R.: Communication and Concurrency. Prentice Hall (1989)
31. Montanari, U., Sassone, V.: Dynamic congruence vs. progressing bisimulation for CCS*. Fundamenta Informaticae 16 (2) (1992), pp. 171-199.

32. Rothe, J.: A syntactical approach to weak (bi)-simulation for coalgebras. In: Proc. CMCS02. Electronic Notes in Theoretical Computer Science 65 (2002), pp. 270-285.

33. Rothe, J., Masulović D.: Towards weak bisimulation for coalgebras. : Proc. Categorical Methods for Concurrency, Interaction and Mobility. Electronic Notes in Theoretical Computer Science 68(1), (2002), pp. 32-46.

34. Rutten, J.: A note on coinduction and weak bisimilarity for while programs. RAIRO - Theoretical Informatics and Applications 33 (4-5) (1999), pp. 393-400.

35. Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249 (2000), pp. 380.

36. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011)

37. Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Proc. CONCUR'94, Lecture Notes in Computer Science 836 (1994), pp. 481-496.

38. Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, MIT (1995)

39. Silva, A., Westerbaan, B.: A Coalgebraic View of epsilon-Transitions. Lecture Notes in Computer Science Volume 8089 (2013), pp. 267-281.

40. Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing the powerset construction, coalgebraically. Proc. FSTTCS 2010, LIPIcs 8 (2010), pp. 272-283.

41. Simpson, A., Plotkin, G.: Complete Axioms for Categorical Fixed-point Operators. Proc. 15th Annual Symposium on Logic in Computer Science (2000), pp. 30-41.

42. Sokolova, A., de Vink, E., Woracek, H.: Coalgebraic Weak Bisimulation for Action-Type Systems. Sci. Ann. Comp. Sci. 19 (2009), pp. 93-144.

43. Staton, S.: Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science 7 (1:13) (2011), pp. 1-21.