11institutetext: Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen,
Germany 11email:
<EMAIL_ADDRESS>
# Predicate Liftings and Functor Presentations in Coalgebraic Expression
Languages††thanks: Work forms part of the DFG project COAX (MI 717/5-1 / SCHR
1118/11-1)

Ulrich Dorsch  0000-0001-8678-7876 Stefan Milius  0000-0002-2021-1644
Lutz Schröder  0000-0002-3146-5906 Thorsten Wißmann  0000-0001-8993-6486

###### Abstract

We introduce a generic expression language describing behaviours of finite
coalgebras over sets; besides relational systems, this covers, e.g., weighted,
probabilistic, and neighbourhood-based system types. We prove a generic
Kleene-type theorem establishing a correspondence between our expressions and
finite systems. Our expression language is similar to one introduced in
previous work by Myers but has a semantics defined in terms of a particular
form of predicate liftings as used in coalgebraic modal logic; in fact, our
expressions can be regarded as a particular type of modal fixed point
formulas. The predicate liftings in question are required to satisfy a natural
preservation property; we show that this property holds in particular for the
Moss liftings introduced by Marti and Venema in work on lax extensions.

##  1 Introduction

Expression languages that support the syntactic description of system
behaviour are one of the classical topics in computer science. The prototypic
example are regular expressions; further examples include Kleene algebra with
tests [17] and expression languages for labelled transition systems [1].

There has been recent interest in phrasing such expression languages
generically, obtaining their syntax and semantics as well as meta-theoretic
results including Kleene theorems by instantiation of a parametrized
framework. This is achieved by abstracting the type of systems as coalgebras
for a given type functor. This line of work originates with expression
languages for a specific class of functors that essentially covers relational
systems, so-called _Kripke polynomial functors_ [34], and was subsequently
extended to cover also weighted systems [32]. A generic expression language
for arbitrary finitary functors can be based on algebraic functor
presentations [25]. Here, we introduce a similar and, as it will turn out, in
fact largely equivalent generic expression language for finitary functors,
which we base on coalgebraic modalities in predicate lifting style, following
the paradigm of coalgebraic logic [9]; on predicate liftings, we impose strong
conditions, notably including preservation of singletons. Marti and Venema
[20] have shown that for functors admitting a _lax extension_ (in particular
for functors that admit a separating set of monotone predicate liftings), one
can convert operations from the functor presentation into predicate liftings,
the so-called _Moss liftings_. We show that the Moss liftings preserve
singletons; the converse does not hold in general, i.e. not all singleton-
preserving predicate liftings are Moss liftings under a given lax extension.

We thus arrive at a generic expression language that covers, e.g., various
flavours of relational, weighted, and probabilistic systems, as well as
monotone neighbourhood systems as in the semantics of game logic [26] and
concurrent dynamic logic [29]. We prove a Kleene theorem stating that every
expression denotes the behavioural equivalence class of some state in a finite
system, and that conversely every such behavioural equivalence class is
denoted by some expression.

We make no claim to novelty for the design of a generic expression language as
such, and in fact the expression language developed by Myers in his PhD
dissertation [25] appears to be even more general. In particular, unlike
Myers’ language our expression language is currently restricted to describing
behavioural equivalence classes in set-based coalgebras, and does not yet
support algebraic operations (e.g. a join semilattice structure as in Silva et
al.’s language for Kripke-polynomial functors [34] or in fact in standard
regular expressions). The main point we are making is, in fact, a different
one: we show that

> _coalgebraic expression languages embed into coalgebraic logic_ ,

specifically into (the conjunctive fragment of) the coalgebraic $\mu$-calculus
[8], extending the classical result that every bisimilarity class of states in
finite labelled transition systems is expressible by a _characteristic
formula_ in the $\mu$-calculus [14, 10, 35, 2]. This result provides a direct
link between descriptions of processes and their property-oriented
specification; as indicated above, the key to lifting it to a coalgebraic
level of generality are singleton-preserving predicate liftings.

Related Work As mentioned above, we owe much to work by Marti and Venema on
Moss liftings [20], and moreover we use a notion of _$\Lambda$ -bisimulation_
[12] that turns out to be an instance of their definition of bisimulation via
lax extensions. Besides the mentioned work on generic expression languages for
Kripke polynomial [34], weighted [32], and finitary [25] functors, there is
work on expression languages for _reactive $T$-automata_ [11], which introduce
an orthogonal dimension of genericity: The coalgebra functor as such remains
fixed but the computational capacities of the automaton model at hand are
encapsulated as a computational monad [23]. Venema [38] proves that for weak-
pullback preserving fuctors, every bisimilarity class of finite coalgebras is
expressible in coalgebraic fixpoint logic over Moss’ $\nabla$ modality.

##  2 Preliminaries

In the standard paradigm of universal coalgebra, types of state-based systems
are encapsulated as endofunctors. We recall details on presentations of set
functors and on their property-oriented description via predicate-lifting
based coalgebraic modalities.

#### Functor Presentations

describe set functors by signatures of operations and a certain restricted
form of equations, so-called _flat_ equations, alternatively by a suitable
natural surjection. A _signature_ is a sequence
$\Sigma=(\Sigma_{n})_{n\in\omega}$ of sets. Elements of $\Sigma_{n}$ are
regarded as $n$-ary operation symbols (we write $\tau/n\in\Sigma$ for
$\tau\in\Sigma_{n}$). Every signature $\Sigma$ determines the corresponding
polynomial endofunctor $T_{\Sigma}$ on $\mathbf{Set}$, which maps a set $X$ to
the set

$T_{\Sigma}X=\coprod\limits_{n\in\omega}\Sigma_{n}\times X^{n}$

and similarly on maps.

###### Definition 2.1

A _presentation_ of a functor $T:\mathbf{Set}\to\mathbf{Set}$ is a pair
$(\Sigma,\alpha)$ consisting of a signature $\Sigma$ and a natural
transformation $\alpha:T_{\Sigma}\twoheadrightarrow T$ with surjective
components $\alpha_{X}$. In the following, we abuse notation and denote, for
every $\tau/n\in\Sigma$, the corresponding coproduct component of
$\alpha:T_{\Sigma}\twoheadrightarrow T$ again by $\tau:(-)^{n}\to T$, and
refer to it as an _operation_ of $T$.

Most of our results concern finitary set functors. Recall that a functor is
_finitary_ if it preserves filtered colimits. Over $\mathbf{Set}$, we have the
following equivalent characterizations:

######  Theorem 2.2 (Adámek and Trnkova [3])

Let $T:\mathbf{Set}\to\mathbf{Set}$ be a functor. Then the following are
equivalent:

  1. 1.

$T$ is finitary;

  2. 2.

$T$ is _bounded_ , i.e. for every element $x\in TX$ there exists a finite
subset $m:Y\hookrightarrow X$ and an element $y\in TY$ such that $x=Tm(y)$;

  3. 3.

$T$ has a presentation.

Indeed, for the equivalence of (1) and (3) note that every polynomial functor
$T_{\Sigma}$ is finitary, and finitary functors are closed under taking
quotient functors. Conversely, given a finitary functor $T$, let
$\Sigma_{n}=Tn$ and define $\alpha_{X}:T_{\Sigma}X\to TX$ by
$\alpha_{X}(\tau,t)=Tt(\tau)$, where $t\in X^{n}$ is considered as a function
$n\to X$. It is easy to show that this yields a natural transformation with
surjective components.

###### Remark 2.3

As indicated above, the natural surjection $\alpha$ in a functor presentation
$(\Sigma,\alpha)$ can be replaced with a set of flat equations over $\Sigma$,
where an equation is called _flat_ if both sides consist of an operation
symbol applied to variables [3]. Incidentally, this (standard) term should not
be confused with the same term introduced in the context of our expression
language in Section 5.

###### Example 2.4

  * (1)

Let $A$ be an input alphabet. The functor $TX=2\times X^{A}$, whose coalgebras
are deterministic automata, is polynomial, and finitary if $A$ is finite.
Thus, $T$ has a presentation $(\Sigma,\alpha)$ by a signature $\Sigma$ with
two $|A|$-ary operations and no equations, i.e. $\alpha$ is the natural
isomorphism $T_{\Sigma}\cong 2\times(-)^{A}$.

  * (2)

For a commutative monoid $(M,+,0_{M})$ the monoid-valued functor
$M^{(-)}:\mathbf{Set}\to\mathbf{Set}$ is defined by

$M^{(X)}=\\{\mu:X\to M\mid\mu(x)=0_{M}\text{ for all but finitely many }x\in
X\\}$

and by $M^{(h)}(\mu)=y\mapsto\sum_{h(x)=y}\mu(x)$ on maps $h:X\to Y$. We view
elements of $M^{(X)}$ as finitely supported additive measures on $X$, and in
particular write $\mu(A)=\sum_{x\in A}\mu(x)$ for $A\subseteq X$; in this
view, maps $M^{(h)}$ just take image measures. For a set $G\subseteq M$ of
generators (i.e. there exists a surjective monoid morphism
$G^{*}\twoheadrightarrow M$), $M^{(-)}$ is represented by

$\alpha_{X}:\coprod_{n\in\omega}G^{n}\times X^{n}\twoheadrightarrow
M^{(X)},\qquad\alpha_{X}(\tau,t)=M^{(t)}(\tau),$

where $\tau\in G^{n}$ is considered as an element of $M^{(n)}$.

  * (3)

The finite powerset functor $\mathcal{P}_{\omega}$ (with
$\mathcal{P}_{\omega}(X)$ being the set of finite subsets of $X$) is the
monoid-valued functor for the monoid $(\\{0,1\\},\vee,0)$. Since this is
generated by $G=\\{1\\}$, we have one $n$-ary operation symbol for each
$n\in\omega$:

$\alpha_{X}:\coprod_{n\in\omega}X^{n}\twoheadrightarrow\mathcal{P}_{\omega}X,\quad\quad\alpha_{X}(x_{1},\ldots,x_{n})=\\{x_{1},\ldots
x_{n}\\};$

e.g. $\alpha$ identifies the tuples $(x_{1},x_{1},x_{2})$ and $(x_{1},x_{2})$.

  * (4)

For the monoid $\mathds{N}$ of natural numbers with addition, one obtains the
bag functor $\mathcal{B}$ as $\mathds{N}^{(-)}$. Concretely, $\mathcal{B}$
maps a set $X$ to the set $\mathcal{B}X$ of bags (i.e. finite multisets) on
$X$. Since $(\mathds{N},+,0)$ is generated by $G=\\{1\\}$, we have the same
signature as for $\mathcal{P}_{\omega}$, namely one $n$-ary operation symbol
per $n\in\omega$; of course, the presentation $\alpha$ now identifies fewer
tuples, e.g. distinguishes $(x_{1},x_{2},x_{1})$ and $(x_{1},x_{2})$.

  * (5)

The _finite distribution functor_ $\mathcal{D}$ is a subfunctor of the monoid-
valued functor $\mathbb{R}_{\geq 0}^{(-)}$ for the additive monoid of the non-
negative reals, given by $\mathcal{D}X=\\{\mu\in\mathbb{R}_{\geq
0}^{(-)}\mid\sum_{x\in X}\mu(x)=1\\}$. Note that elements of $\mathcal{D}X$
can be represented as formal convex combinations $\sum_{i=1}^{n}p_{i}x_{i}$,
$p_{i}\in\mathbb{R}_{\geq 0},x_{i}\in X$ for $i=1,\ldots,n$, with
$p_{1}+\cdots+p_{n}=1$. Taking $\mathbb{R}_{\geq 0}$ itself as the set of
generators and restricting to $\mathcal{D}$, we obtain a presentation
$(\Sigma,\alpha)$ with an $n$-ary operation symbol for each $n$-tuple
$(p_{1},\dots,p_{n})\in\mathbb{R}_{\geq 0}^{n}$ such that
$p_{1}+\cdots+p_{n}=1$, and $\alpha_{X}$ maps
$((p_{1},\ldots,p_{n}),(x_{1},\ldots,x_{n}))$ to the formal convex combination
$\sum_{i=1}^{n}p_{i}x_{i}$.

  * (6)

The _finitary monotone neighbourhood functor_ $\mathcal{M}_{\omega}$, i.e. the
finitary part of the standard monotone neighbourhood functor $\mathcal{M}$,
can be described as follows. To begin, $\mathcal{M}$ is the subfunctor of the
double contravariant powerset functor $\mathcal{Q}\mathcal{Q}^{\mathsf{op}}$
given on objects by

$\mathcal{M}X=\\{\mathfrak{A}\subseteq\mathcal{Q}(X)\mid\mathfrak{A}\text{
upwards closed under $\subseteq$}\\}.$

We can then describe $\mathcal{M}_{\omega}X$ as consisting of all
$\mathfrak{A}\in\mathcal{M}X$ having finitely many minimal elements, all of
them finite, such that every element of $\mathfrak{A}$ is above a minimal one.
We have the following presentation of $\mathcal{M}_{\omega}$: For every choice
of numbers $n\geq 0$, $k_{1},\dots,k_{n}\geq 0$, we have a
$\sum_{i=1}^{n}k_{i}$-ary operation mapping
$(x_{ij})_{i=1,\dots,n;j=1,\dots,k_{i}}$ to the upwards closure of the set
system

$\\{\\{x_{i1},\dots,x_{ik_{i}}\\}\mid i=1,\dots,n\\}.$

#### Coalgebraic Logic

Since coalgebras serve as generic models of reactive systems, it is natural to
specify properties of coalgebras in terms of suitable modalities. The
semantics of coalgebraic modalities can be defined using _predicate liftings_
[27, 30], which specify how a predicate on a base set $X$ induces a predicate
on the set $TX$ where $T$ is the coalgebraic type functor:

###### Definition 2.5

For $n\in\omega$ an $n$-ary _predicate lifting_ for a functor
$T:\mathbf{Set}\rightarrow\mathbf{Set}$ is a natural transformation

$\lambda:\mathcal{Q}{}^{n}\rightarrow\mathcal{Q}{T^{\mathsf{op}}}$

where $\mathcal{Q}{}:\mathbf{Set}^{\mathsf{op}}\rightarrow\mathbf{Set}$ is the
contravariant powerset functor, with $\mathcal{Q}f$ taking preimages, i.e.

$\mathcal{Q}f(A)=f^{-1}[A].$

We write $\lambda/n$ to indicate that $\lambda$ has arity $n$. A predicate
lifting $\lambda$ is _monotone_ if it preserves set inclusion in every
argument. A set $\Lambda$ of predicate liftings is _separating_ [28, 30] if
every $t\in TX$ is uniquely determined by the set

$\mathcal{T}_{\Lambda}(t)=\\{(\lambda,A_{1},\ldots,A_{n})\mid\lambda/n\in\Lambda,A_{i}\in\mathcal{Q}X\text{
and }t\in\lambda_{X}(A_{1},\ldots,A_{n})\\}.$

###### Example 2.6

The basic example is the interpretation of the standard box modality $\Box$
over the covariant powerset functor $\mathcal{P}$ (with $\mathcal{P}f$ taking
direct images), given by the monotone unary predicate lifting $\lambda$
defined by

$\lambda_{X}(A)=\\{B\in\mathcal{P}(X)\mid B\subseteq A\\}.$

For a further monotone example, we interpret the box modality over the
monotone neighbourhood functor $\mathcal{M}$ (Example 2.4) by the monotone
unary predicate lifting

$\lambda_{X}(A)=\\{\mathfrak{A}\in\mathcal{M}X\mid A\in\mathfrak{A}\\}.$

It is easy to see that in both these examples, the predicate lifting for
$\Box$ alone is separating.

Predicate-lifting-based modalities can be embedded into _coalgebraic logics_
of varying degrees of expressiveness. Our expression language introduced in
Section 5 will live inside the _coalgebraic $\mu$-calculus_ [8], more
precisely its _conjunctive fragment_ [13]. We defer details to Section 5.

##  3 Singleton-Preserving Predicate Liftings

Our generic expression language will depend on a specific type of predicate
liftings, as well as on a strengthening of separation:

###### Definition 3.1

An $n$-ary predicate lifting $\lambda$ _preserves singletons_ if

$|\lambda_{X}(\\{x_{1}\\},\dots,\\{x_{n}\\})|=1$

for all $x_{1},\dots,x_{n}\in X$. Moreover, a set $\Lambda$ of predicate
liftings is _strongly expressive_ if for every $t\in TX$ there exist
$\lambda/n\in\Lambda$ and $x_{1},\ldots,x_{n}\in X$ such that

$\\{t\\}=\lambda_{X}(\\{x_{1}\\},\ldots,\\{x_{n}\\}).$

Singleton preservation will serve to ensure that expressions of our language
denote unique behaviours, while strong expressivity will guarantee that all
(finite) behaviours are expressible. The following is immediate:

###### Lemma 3.2

Every strongly expressive set of predicate liftings is separating.

###### Example 3.3

The predicate liftings in Example 2.6 both fail to preserve singletons. Our
main source of singleton-preserving predicate liftings are Moss liftings as
introduced in general terms in the next section. For the finite powerset
functor $\mathcal{P}_{\omega}$ consider the predicate liftings $\lambda^{n}/n$
given by

$\textstyle\begin{array}[]{r@{}l}\lambda^{n}_{X}(A_{1},\ldots,A_{n})=\\{B\in\mathcal{P}_{\omega}X\mid&B\subseteq\bigcup_{i=1}^{n}A_{i}\text{
and }\\\ &B\cap A_{i}\neq\emptyset\text{ for $i=1,\ldots,n$}\\}\end{array}$
(3.1)

(which can be seen as arising from the above lifting for $\Box$ by Boolean
combination). Then
$\lambda^{n}_{X}(\\{x_{1}\\},\dots,\\{x_{n}\\})=\\{\\{x_{1},\dots,x_{n}\\}\\}$
for $x_{1},\dots,x_{n}\in X$, which shows that the $\lambda^{n}$ preserve
singletons and that the set $\\{\lambda^{n}\mid n\in\omega\\}$ is strongly
expressive.

###### Remark 3.4

Singleton-preserving predicate liftings should not be confused with Kurz and
Leal’s _singleton liftings_ [19, 18]. The definition of the latter is based on
the one-to-one correspondence between subsets of $T(2^{n})$ and $n$-ary
predicate liftings for $T$ [30], which maps an $n$-ary predicate lifting
$\lambda$ to
$\lambda_{2^{n}}(\pi_{1}^{-1}(\\{\top\\}),\ldots,\pi_{n}^{-1}(\\{\top\\}))\subseteq
T(2^{n})$, and $C\subseteq T(2^{n})$ to the lifting $\lambda$ defined by
$\lambda_{X}(A_{1},\ldots,A_{n})=\\{t\in TX\mid
T\langle\chi_{A_{1}},\ldots,\chi_{A_{n}}\rangle(t)\in C\\}$, where
$\pi_{i}:2^{n}\to 2$ is the $i$-th projection and $\chi_{A}:X\to 2$ denotes
the characteristic function of $A\subseteq X$. An $n$-ary predicate lifting is
a _singleton lifting_ if it corresponds to a singleton subset of $T(2^{n})$.

It is then indeed immediate that every _unary_ singleton-preserving predicate
lifting $\lambda$ is a singleton lifting, since the above correspondence maps
$\lambda$ to the singleton $\lambda_{2}(\\{\top\\})$. The following examples
show that this implication breaks down at higher arities, and that the
converse also fails in general.

###### Example 3.5

  * (1)

The unary singleton lifting for $\mathcal{P}$ corresponding to
$\\{\\{\bot\\}\\}\subseteq\mathcal{P}2$ fails to preserve singletons. Of
course, this lifting fails to be monotone.

  * (2)

Binary monotone singleton liftings need not preserve singletons. E.g. for the
distribution functor $\mathcal{D}$, the monotone singleton lifting $\lambda$
corresponding to $\\{1\cdot(\top,\top)\\}\subseteq\mathcal{D}(2^{2})$ is given
by $\lambda(A,B)=\\{\mu\mid\mu(A)=\mu(B)=1\\}$, so
$\lambda(\\{x\\},\\{y\\})=\varnothing$ for $x\neq y$. We leave it as an open
question whether unary monotone singleton liftings preserve singletons.

  * (3)

The binary singleton-preserving predicate lifting

$\lambda(A,B)=\\{\mu\mid\mu(A)\geq 1/2,\mu(B)\geq 1/2,\mu(A\cup B)=1\\}$

for the distribution functor $\mathcal{D}$ (see Example 4.7 for details) is
not a singleton lifting, as it corresponds to the following infinite subset of
$\mathcal{D}(2^{2})$:

$\\{\mu\mid\mu(2\times\\{\top\\})\geq 1/2,\mu(\\{\top\\}\times 2)\geq
1/2,\mu(2\times\\{\top\\}\cup\\{\top\\}\times 2)=1\\}.$

It is not hard to see that we can recover operations for a functor from
_monotone_ singleton preserving predicate liftings; in detail:

###### Lemma 3.6

Let $T:\mathbf{Set}\to\mathbf{Set}$. Then the following hold.

  1. 1.

For each monotone singleton-preserving predicate lifting $\lambda/n$,

$\\{\tau_{\lambda,X}(x_{1},\ldots,x_{n})\\}:=\lambda_{X}(\\{x_{1}\\},\ldots,\\{x_{n}\\})$
(3.2)

defines a natural transformation $\tau_{\lambda}:(-)^{n}\to T$.

  2. 2.

If $\Lambda$ is a strongly expressive set of monotone singleton-preserving
predicate liftings, then taking operation symbols $\tau_{\lambda}$ for each
$\lambda\in\Lambda$, with associated interpretation as per (3.2), yields a
functor presentation of $T$.

###### Example 3.7

The singleton-preserving predicate liftings $\lambda^{n}$ from Example 2.6
induce, according to the above construction, the operations
$X^{n}\to\mathcal{P}_{\omega}(X)$,
$(x_{1},\dots,x_{n})\mapsto\\{x_{1},\dots,x_{n}\\}$.

The other direction, generating predicate liftings from functor presentations,
is more involved, and treated next.

##  4 Moss Liftings

Marti and Venema [20] introduce _Moss liftings_ , predicate liftings that are
constructed from functor presentations with the help of a generalized form of
the nabla operator, extending an earlier construction for weak-pullback
preserving functors by Kurz and Leal [18]. Recall that for a weak-pullback-
preserving functor $T$, Moss’ [24] classical nabla operator
$\nabla:T\mathcal{Q}\Rightarrow\mathcal{Q}T^{\mathsf{op}}$ is the natural
transformation defined by

$\nabla(\Phi)=\\{t\in TX\mid(t,\Phi)\in\overline{T}(\in_{X})\\}.$

Here, $\mathord{\in_{X}}\subseteq X\times\mathcal{Q}X$ is the element-of
relation for $X$, and $\overline{T}$ is the _Barr extension_ of $T$, viz. the
functor $\overline{T}$ on the category of sets and relations defined on a
relation $R\subseteq X\times Y$ by
$\overline{T}R=\\{(T\pi_{1}(r),T\pi_{2}(r))\mid r\in TR\\}$, where
$\pi_{1}:R\to X$ and $\pi_{2}:R\to Y$ are the projection maps (cf. [24]). Barr
[5] (see also Trnková [37]) proved that $\overline{T}$ is a functor if and
only if $T$ preserves weak pullbacks.

Further recall that the _converse_ of a relation $R\subseteq X\times Y$ is the
relation $R^{\circ}=\\{(y,x)\mid x\mathbin{R}y\\}\subseteq Y\times X$. We
denote the composite of two relations $R\subseteq X\times Y$ and $S\subseteq
Y\times Z$ diagrammatically by $R;S\subseteq X\times Z$. Also, for $A\subseteq
X$ we denote by $R[A]\subseteq Y$ the relational image $R[A]=\\{y\mid\exists
x\in A.\,xRy\\}$. The construction $T\mapsto\overline{T}$ is generalized and
abstracted in the notions of _relation lifting_ and, more specifically, _lax
extension_ of a functor, as recalled next.

######  Definition 4.1 (Relation lifting, lax extension [20])

A _relation lifting_ $L$ for a functor $T$ is an assignment mapping every
relation $R\subseteq X\times Y$ to a relation $LR\subseteq TX\times TY$ such
that converses are preserved: $L(S^{\circ})=(LS)^{\circ}$. A relation lifting
$L$ is a _lax extension_ if for all relations $R,R^{\prime}\subseteq X\times
Z$, $S\subseteq Z\times Y$ and functions $f:X\rightarrow Z$ (identified with
their graph relation) the following hold:

$\displaystyle R^{\prime}\subseteq R\Rightarrow LR^{\prime}\subseteq LR,$
$\displaystyle LR;LS\subseteq L(R;S),$ $\displaystyle Tf\subseteq Lf.$

A lax extension $L$ _preserves diagonals_ if for all sets $X$

$L\Delta_{X}\subseteq\Delta_{TX}.$

######  Proposition 4.2 (Properties of Lax Extensions [20])

Let $L$ be a lax extension for a functor $T$. Then for all functions
$f:X\rightarrow Z$, $g:Y\rightarrow Z$ and relations $R\subseteq X\times Z$,
$S\subseteq Z\times Y$,

  * i)

$\Delta_{TX}\subseteq L\Delta_{X}$,

  * ii)

$Tf;LS=L(f;S)$ and $LR;(Tg)^{\circ}=L(R;g^{\circ})$,

and if $L$ preserves diagonals, then

  * iii)

$\Delta_{TX}=L\Delta_{X}$ and $Tf=Lf$,

  * iv)

$Tf;(Tg)^{\circ}=L(f;g^{\circ})$.

One use of relation liftings is to determine coalgebraic notions of
bisimulation:

######  Definition 4.3 ($L$-Bisimulation [20])

Let $L$ be a relation lifting for a functor $T:\mathbf{Set}\to\mathbf{Set}$,
and let $(X,\xi)$, $(Y,\zeta)$ be $T$-coalgebras. A relation $S\subseteq
X\times Y$ is an _$L$ -simulation_ if for all $x\in X$ and $y\in Y$,

$x\mathbin{S}y\quad\text{implies}\quad\xi(x)\mathbin{LS}\zeta(y).$

An _$L$ -bisimulation_ is a relation $S$ such that $S$ and $S^{\circ}$ are
$L$-simulations. Two states are _$L$ -bisimilar_ if there exists an
$L$-bisimulation relating them.

Marti and Venema [20, Theorem 11] show that if $L$ is a lax extension that
preserves diagonals, then $L$-bisimilarity coincides with behavioural
equivalence.

###### Assumption 4.4

From now on we fix a finitary endofunctor $T:\mathbf{Set}\to\mathbf{Set}$
having a diagonal-preserving lax extension $L$ and a presentation
$(\Sigma,\alpha)$ of $T$.

Another key feature of lax extensions is that they induce canonical
modalities, generalizing Moss’ coalgebraic logic [24]:

######  Definition 4.5 (Lax Nabla [20])

The _lax nabla_ of $L$ is the family of functions

$\displaystyle\nabla^{L}_{X}:T\mathcal{Q}X$
$\displaystyle\rightarrow\mathcal{Q}T^{\mathsf{op}}X$ $\displaystyle\Phi\quad$
$\displaystyle\mapsto\\{t\in TX\mid(t,\Phi)\in L(\in_{X})\\},$

where ${\in_{X}}\subseteq X\times\mathcal{Q}X$ is the element-of relation for
$X$.

As shown by Marti and Venema [20], the lax nabla is in fact a natural
transformation $\nabla^{L}:T\mathcal{Q}\Rightarrow\mathcal{Q}T^{\mathsf{op}}$,
and coincides with Moss’ classical $\nabla$ for $L$ being the Barr extension
of $T$ (and $T$ preserving weak pullbacks). In combination with a functor
presentation, the lax nabla gives rise to a family of predicate liftings:

######  Definition 4.6 (Moss Liftings [20])

Every operation symbol $\tau/n\in\Sigma$ yields a predicate lifting $\lambda$
defined by

$\lambda=(\mathcal{Q}^{n}\overset{\tau\mathcal{Q}}{\Longrightarrow}T\mathcal{Q}\overset{\nabla^{L}}{\Longrightarrow}\mathcal{Q}T^{\mathsf{op}}),$

that is,

$\lambda_{X}(X_{1},\ldots X_{n})=\\{t\in
TX\mid(t,\tau_{\mathcal{Q}X}(X_{1},\ldots,X_{n}))\in L(\in_{X})\\}.$

These predicate liftings are called the _Moss liftings_ of $T$.

###### Example 4.7

Some standard functor presentations are converted into Moss liftings as
follows.

  * (1)

For the deterministic automata functor $TX=2\times X^{A}$ consider the Barr
extension $L=\overline{T}$. Then elements of $T\mathcal{Q}X$ are pairs
$(b,(Y_{a})_{a\in A})$, where each $Y_{a}$ is a subset of $X$, and

$\nabla_{X}(b,(Y_{a})_{a\in A})=\\{(b,(x_{a})_{a\in A})\mid\forall a\in
A:x_{a}\in Y_{a}\\}\qquad\text{for $b=0,1$}.$

The two Moss liftings
$\lambda^{0},\lambda^{1}:\mathcal{Q}^{A}\to\mathcal{Q}(2\times(-)^{A})$
corresponding to the two $|A|$-ary operation symbols from the presentation in
Theorem 2.4.1 are thus defined (slightly abusing notation) by

$\lambda^{i}((Y_{a})_{a\in A})=\\{(i,(x_{a})_{a\in A})\mid\forall a\in
A:x_{a}\in Y_{a}\\}\qquad\text{for $i=0,1$}.$

  * (2)

As indicated in Theorem 2.4, the finite powerset functor
$\mathcal{P}_{\omega}$ has operations $\tau^{n}/n$ given by
$\tau^{n}(x_{1},\dots,x_{n})=\\{x_{1},\dots,x_{n}\\}$. The Moss lifting
$\lambda^{n}$ associated to $\tau^{n}$ when using the Barr extension is
exactly the one given by (3.1) above.

  * (3)

Recall from Theorem 2.4 that the operations of the finite distribution functor
$\mathcal{D}$ take formal convex combinations. Via the Barr extension, such an
operation, determined by coefficients $p_{1},\dots,p_{n}$ such that $\sum
p_{i}=1$, induces the predicate lifting $\lambda$ given by
$\lambda_{X}(A_{1},\dots,A_{n})$ consisting of all $\mu\in\mathcal{D}X$ such
that there exists a distribution on $\in_{X}$ (a subset of
$X\times\mathcal{Q}(X)$) whose marginal distributions are $\mu$ (on $X$) and
the distribution $\nu$ on $\mathcal{Q}(X)$ given by $\nu(\\{A_{i}\\})=p_{i}$,
respectively. In fact, however, this description can be substantially
simplified; e.g. one readily checks that in the case $n=2$, we actually have

$\lambda(A_{1},A_{2})=\\{\mu\in\mathcal{D}(X)\mid\mu(A_{1})\geq
p_{1},\mu(A_{2})\geq p_{2},\mu(A_{1}\cup A_{2})=1\\}.$

(The generalization to higher arities is via what is nowadays known as the
_splitting lemma_ [36, Theorem 11].)

  * (4)

For the finitary monotone neighbourhood functor $\mathcal{M}_{\omega}$
(Example 2.4), we obtain Moss liftings as follows. Marti and Venema [20]
define a diagonal-preserving lax extension $L$ for $\mathcal{M}$ (which, then,
restricts to $\mathcal{M}_{\omega}$) by means of nested Egli-Milner liftings.
An explicit description of $L$ is

$LR=\\{(\mathfrak{A},\mathfrak{B})\in\mathcal{M}X\times\mathcal{M}Y\mid\forall
A\in\mathfrak{A}.\,R[A]\in\mathfrak{B},\forall
B\in\mathfrak{B}.\,R^{\circ}[B]\in\mathfrak{A}\\}$

for $R\subseteq X\times Y$. In particular, for $\mathfrak{A}\in\mathcal{M}X$
and
$\Phi\in\mathcal{M}\mathcal{Q}X\subseteq\mathcal{Q}\mathcal{Q}\mathcal{Q}X$,
we have

$\displaystyle\mathfrak{A}\in\nabla^{L}_{X}(\Phi)\quad\text{iff}\quad\mathfrak{A}\mathbin{L(\in)}\Phi\quad\text{iff}\quad$
$\displaystyle\textstyle\forall\beta\in\Phi.\,\bigcup\beta\in\mathfrak{A}\text{
and }$ $\displaystyle\forall A\in\mathfrak{A}.\,\\{B\in\mathcal{Q}X\mid B\cap
A\neq\emptyset\\}\in\Phi.$

Combining $\nabla^{L}$ with the presentation of $\mathcal{M}_{\omega}$
(Example 2.4) produces, for each choice of numbers $n\geq 0$ and
$k_{1},\dots,k_{n}\geq 0$, a $\sum_{i=1}^{n}k_{i}$-ary Moss lifting $\lambda$
given by

$\displaystyle\lambda((A_{ij})_{i=1,\dots,n;j=1,\dots,k_{i}})=\\{\mathfrak{A}\in\mathcal{M}_{\omega}X\mid\,$
$\displaystyle\textstyle\forall i.\,\bigcup_{j}A_{ij}\in\mathfrak{A}\text{ and
}$ $\displaystyle\forall B\in\mathfrak{A}.\,\exists i.\,\forall j.\,B\cap
A_{ij}\neq\emptyset\\}.$

Since $\mathcal{M}_{\omega}$ preserves finite sets and the box modality $\Box$
as described in Example 2.6 is separating, it is clear that the Moss liftings
are expressible using $\Box$ and Boolean operators. Concretely, this works as
follows. For readability, we denote the predicate lifting interpreting $\Box$
by $\Box$ as well, similarly for the dual modality $\Diamond$, so that
$\Diamond_{X}(A):=\mathcal{M}X\setminus\Box_{X}(X\setminus
A)=\\{\mathfrak{A}\in\mathcal{M}X\mid\forall B\in\mathfrak{A}.\,B\cap
A\neq\emptyset\\}$. Then the Moss lifting $\lambda$ as described above can be
written as

$\textstyle\lambda((A_{ij}))=\bigcap_{i}\Box_{X}(\bigcup_{j}A_{ij})\cap\bigcap_{\pi}\Diamond_{X}(\bigcup_{i}A_{i\pi(i)})$

where $\pi$ ranges over all selection functions assigning to each
$i\in\\{1,\dots,n\\}$ an index $\pi(i)\in\\{1,\dots,k_{i}\\}$.

Moss liftings are always monotone [20, Proposition 24]. We show that they also
preserve singletons:

###### Proposition 4.8

Moss liftings preserve singletons. More specifically, let $\lambda$ be the
Moss lifting induced by $\tau/n\in\Sigma$. Then for all $x_{1},\ldots,x_{n}\in
X$,

$\lambda_{X}(\\{x_{1}\\},\dots,\\{x_{n}\\})=\\{\tau_{X}(x_{1},\dots,x_{n})\\}.$

Marti and Venema already establish that the Moss liftings are separating [20,
Proposition 25]; we show that they are even strongly expressive:

###### Proposition 4.9

The set $\Lambda$ of all Moss liftings of $T$ is strongly expressive.

###### Remark 1

Incidentally, this also means that for finitary functors the existence of a
separating set of monotone predicate liftings is equivalent to the existence
of a strongly expressive set of monotone singleton-preserving predicate
liftings. The right-to-left implication is trivial; the converse follows from
Theorem 4.8, Theorem 4.9, and the fact that for finitary functors the
existence of a separating set of monotone predicate liftings is equivalent to
the existence of a lax extension [20].

We have thus seen that given a fixed diagonal-preserving lax extension, from
every natural transformation $\tau:(-)^{n}\to T$ we obtain the corresponding
Moss lifting $\lambda^{\tau}/n$, which is a monotone singleton-preserving
predicate lifting. Conversely, every monotone singleton-preserving predicate
lifting $\lambda$ yields a natural transformation $\tau^{\lambda}:(-)^{n}\to
T$ (Theorem 3.6.1). From Theorem 4.8, it is immediate that for
$\tau:(-)^{n}\to T$ we have

$\tau=\tau^{(\lambda^{\tau})}.$

In particular, taking Moss liftings is an injection from functor operations to
monotone singleton-preserving predicate liftings. Conversely, however,
$\lambda=\lambda^{(\tau^{\lambda})}$ need not hold in general – recall that
the construction of Moss liftings depends on the choice of a diagonal-
preserving lax extension, and a functor may have more than one such extension.
We report an example due to Paul Levy:

###### Example 1

Let $M$ be the monoid of non-negative reals. This monoid in fact forms a
division semiring in the expected sense (e.g. [39]), i.e. it is a semiring,
and its non-zero elements form a multiplicative group. We note that every
division semiring is _refinable_ in the sense of Gumm and Schröder [15], i.e.
$n$ specified row sums $b_{1},\dots,b_{n}$ and $k$ specified column sums
$c_{1},\dots,c_{k}$ that induce the same total sum $d=\sum b_{i}=\sum c_{j}$
can always be realized by some $n\times k$-matrix $(a_{ij})$ – in fact, one
can just put $a_{ij}=b_{i}c_{j}/d$. Now let $b\in(0,1)$ be a transcendental
number, and let $N\subseteq M$ be generated by $b$ in $M$ as a division
semiring. Concretely, elements of $N$ have the form $f(b)/g(b)$ where $f(X)$
and $g(X)\neq 0$ are polynomials with non-negative rational coefficients. In
particular, $1-b\notin N$: If we could write $1-b$ in the prescribed form
$f(b)/g(b)$, then by transcendentality of $b$, $f(X)/g(X)=1-X$, in
contradiction to the leading coefficients of $f$ and $g$ being positive.

Both $M$ and $N$ are _positive_ ($x+y=0$ implies $x=y=0$) and refinable, so
that the monoid-valued functors $F=M^{(-)}$ and $G=N^{(-)}$ both preserve weak
pullbacks [15]. As recalled above, it follows that in both cases, the Barr
extension is functorial, in particular is a diagonal-preserving lax extension.
Now diagonal-preserving lax extensions are easily seen to be inherited by
subfunctors, so that the Barr extension $\overline{F}$ induces a diagonal-
preserving lax extension $L$ of $G$. This extension differs from the Barr
extension $\overline{G}$; we immediately cast the counterexample in the form
that interests us here:

Let $X=\\{u,v\\}$. Representing elements of $GX$ as formal linear
combinations, we have a binary functor operation $\tau(x,y)=x+by$ for $G$. We
write $\lambda^{1}$ and $\lambda^{2}$ for the Moss liftings induced from
$\tau$ via $\overline{G}$ and via $L$, respectively (by the above, both
$\lambda^{1}$ and $\lambda^{2}$ induce $\tau$). Then
$u+bv\in\lambda^{1}(\\{u,v\\},\\{u\\})$ but
$u+bv\notin\lambda^{2}(\\{u,v\\},\\{u\\})$: For the former, we have a unique
witnessing element of $F{\in_{X}}$, namely
$(1-b)(u,\\{u,v\\})+b(v,\\{u,v\\})+b(u,\\{u\\})$; but in $G\,\\!{\in_{X}}$,
there is no witnessing element since $1-b\notin N$.

Summing up, even for weak-pullback preserving functors, singleton-preserving
monotone predicate liftings are not in general uniquely determined by the
functor operation they induce. In the above example, both singleton predicate
liftings inducing the given functor operation arise as Moss liftings, via
different diagonal-preserving lax extensions; we currently do not know whether
every singeleton-preserving monotone predicate lifting is a Moss lifting for
some diagonal-preserving lax extension.

###### Remark 2

It is fairly easy to see that for monotone singleton-preserving _unary_
predicate liftings $\lambda$, we do have $\lambda=\lambda^{(\tau^{\lambda})}$.

##  5 Generic Expressions

We proceed to define, given a set of monotone and singleton-preserving
predicate liftings for a functor $T$, syntactic expressions describing the
behaviour of states of $T$-coalgebras. Our main result is a Kleene-type
theorem stating that for every state of a $T$-coalgebra there exists an
equivalent expression, and conversely, every expression describes the
behaviour of some state of a finite $T$-coalgebra. As indicated above, our
expression language is a small fragment of the coalgebraic $\mu$-calculus,
essentially restricted to modalities and greatest fixed points $\nu z.\,\phi$.

######  Definition 5.1 (Expressions)

We fix a set $\mathsf{V}$ of _fixed point variables_ and a set $\mathcal{L}$
of _modalities_ equipped with an arity function
$\operatorname{ar}:\mathcal{L}\rightarrow\omega$; we write $L/n\in\mathcal{L}$
if $L\in\mathcal{L}$ and $\operatorname{ar}(L)=n$. The set $\mathcal{E}$ of
_expressions_ $\phi,\dots$ is then defined by the grammar

$\phi::=z\mid\nu
z.\,\phi\mid\textit{L}(\phi_{1},\dots\phi_{n})\qquad(z\in\mathsf{V},L/n\in\mathcal{L}).$

An expression is _closed_ if all its fixed point variables are bound by a
fixed point operator. An expression is _guarded_ if all its fixed point
variables are separated from their binding fixed point operator by at least
one modality. We write $\mathcal{E}_{0}$ for the set of closed and guarded
expressions. We have the usual notion of _$\alpha$ -equivalence_ of
expressions modulo renaming of bound variables. An occurrence of a fixed point
operator in an expression is _top-level_ if it is not in scope of a modality.

We next define the semantics of expressions, which agrees with their
interpretation as formulas in coalgebraic logic. We fix the requisite data:

###### Assumption 5.2

For the rest of the paper, we fix a set $\mathcal{L}$ of modalities and an
assignment of a singleton-preserving monotone $n$-ary predicate lifting
$\llbracket L\rrbracket$ for $T$ to each $L/n\in\mathcal{L}$ such that the set
$\Lambda:=\\{\llbracket L\rrbracket\mid L\in\mathcal{L}\\}$ is strongly
expressive.

By the results of the previous section, these assumptions imply that $T$ has a
presentation and is thus finitary (Theorem 2.2).

######  Definition 5.3 (Semantics)

Given a $T$-coalgebra $C=(X,\xi)$ and a valuation
$\kappa:\mathsf{V}\rightarrow\mathcal{Q}X$, the semantics
$\llbracket\phi\rrbracket_{C}^{\kappa}\subseteq X$ of expressions
$\phi\in\mathcal{E}$ is given by

$\displaystyle\llbracket z\rrbracket_{C}^{\kappa}$ $\displaystyle=\kappa(z)$
$\displaystyle\llbracket\textit{L}(\phi_{1},\dots\phi_{n})\rrbracket_{C}^{\kappa}$
$\displaystyle=\xi^{-1}[\llbracket
L\rrbracket_{X}(\llbracket\phi_{1}\rrbracket_{C}^{\kappa},\dots\llbracket\phi_{n}\rrbracket_{C}^{\kappa})]$
$\displaystyle\llbracket\nu z.\phi\rrbracket_{C}^{\kappa}$ $\displaystyle=\nu
Y.\llbracket\phi\rrbracket_{C}^{\kappa[z\mapsto Y]}$

where as usual, we use $\nu$ to denote greatest fixed points of monotone maps.
When $\phi$ is closed, we simply write $\llbracket\phi\rrbracket_{C}$ in lieu
of $\llbracket\phi\rrbracket_{C}^{\kappa}$, and we drop the subscript $C$
whenever $C$ is clear from the context.

Note that since the predicate liftings $\llbracket L\rrbracket$ are monotone
and $\xi^{-1}$ is a monotone map, the requisite greatest fixed points exist by
the Knaster-Tarski fixed point theorem. Moreover, the assumption that the
predicate liftings are singleton-preserving will ensure that every expression
describes exactly one behavioural equivalence class (see Theorem 5.14).

By dint of the fact that our expression language is contained in the
coalgebraic $\mu$-calculus, the following is an immediate consequence of the
fact that the latter is invariant under behavioural equivalence (e.g. [31]):

######  Lemma 5.4 (Invariance under behavioural equivalence)

For every closed expression $\phi$ and coalgebras $C=(X,\xi)$, $D=(Y,\zeta)$,
if states $x\in X$ and $y\in Y$ are behaviourally equivalent, then
$x\in\llbracket\phi\rrbracket_{C}$ iff $y\in\llbracket\phi\rrbracket_{D}$.

###### Lemma 5.5

For all expressions $\phi\in\mathcal{E}$, $\llbracket\nu
z.\phi\rrbracket=\llbracket\phi[\nu z.\phi/z]\rrbracket$.

###### Example 5.6

  * (1)

For the deterministic automaton functor $TX=2\times X^{A}$ with $A=\\{a,b\\}$,
we let $\mathcal{L}$ be the set of two binary modalities $\langle
0,a.(-),b.(-)\rangle$ and $\langle 1,a.(-),b.(-)\rangle$ (corresponding to the
two Moss liftings of Theorem 4.7.1). We interpret expressions in the final
$T$-coalgebra $\nu T$ carried by all formal languages over $A$. Here are a few
closed and guarded expressions and their semantics in $\nu T$ (as usual
$|w|_{b}$ denotes the number of $b$’s in $w$):

$\displaystyle\llbracket\nu v.\langle 0,a.v,b.v\rangle\rrbracket$
$\displaystyle=\\{\emptyset\\}$ $\displaystyle\llbracket\nu z.\langle
1,a.z,b.z\rangle\rrbracket$ $\displaystyle=\\{A^{*}\\}$
$\displaystyle\llbracket\nu x.\langle 1,a.x,b.\nu y.\langle
0,a.y,b.x\rangle\rangle\rrbracket$ $\displaystyle=\\{\\{w\in A^{*}\mid|w|_{b}\
\text{even}\\}\\}$ va,bza,bxyabab

Note that the semantics of each of these expressions is a singleton (up to
behavioural equivalence); in fact, for an arbitrary $T$-coalgebra $X$, the
semantics of the above expressions is the set of states accepting the language
in the singleton on the right. In Theorem 5.11 further below we prove that
this holds in general.

  * (2)

Consider $T=\mathcal{P}_{\omega}(A\times-)$ where $A$ is a finite set of
labels. A presentation of $T$ is given by the signature containing for each
$n$-tuple $\vec{a}=(a_{1},\ldots,a_{n})\in A^{n}$ one $n$-ary operation
symbol, and the corresponding natural transformation
$\tau^{\vec{a}}:(-)^{n}\to T$ is defined by

$\tau^{\vec{a}}_{X}:(x_{1},\ldots,x_{n})\mapsto\\{(a_{1},x_{1}),\ldots,(a_{n},x_{n})\\}.$

The corresponding Moss lifting is $\lambda^{\vec{a}}/n$ given by

$\textstyle\lambda^{\vec{a}}_{X}(Y_{1},\ldots,Y_{n})=\\{Z\in\mathcal{P}_{\omega}(A\times
X)\mid Z\subseteq\bigcup_{i=1}^{n}(\\{a_{i}\\}\times Y_{i})\\\ \text{and
}Z\cap\\{a_{i}\\}\times Y_{i}\neq\emptyset\text{ for $i=1,\ldots,n$}\\}$

(cf. (3.1)). Now put $\mathcal{L}=\\{[\vec{a}]/n\mid\vec{a}\in
A^{n},n\in\omega\\}$ and interpret each $[\vec{a}]$ by $\lambda^{\vec{a}}$.
For example, for $A=\\{a,b\\}$ the expression $\nu
x.[a]([a,b,a](x,[()],[()]))$, where $[()]$ is the unique nullary modality in
$\mathcal{L}$, describes the left-hand state in the following labelled
transition system

xyzwaaab

  * (3)

For $T=\mathcal{D}$ we have the presentation with an $n$-ary operation
$\tau^{\vec{p}}$ for every $\vec{p}=(p_{1},\ldots,p_{n})$ with
$\sum_{i=1}^{n}p_{i}=1$ and corresponding Moss liftings as described in
Theorem 4.7.3. For each such $\vec{p}$, we introduce a modality
$[\vec{p}]/n\in\mathcal{L}$, and interpret it as $\lambda^{\vec{p}}$. Now
consider the Markov chain (i.e. $\mathcal{D}$-coalgebra)

xyz$\nicefrac{{2}}{{3}}$$\nicefrac{{1}}{{3}}$$\nicefrac{{1}}{{3}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{3}}{{4}}$$\nicefrac{{1}}{{4}}$

The behaviour of the left-hand state is described by the expression

$\nu x.[\nicefrac{{2}}{{3}},\nicefrac{{1}}{{3}}](x,\nu
y.[\nicefrac{{1}}{{6}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{2}}](x,y,\nu
z.[\nicefrac{{1}}{{4}},\nicefrac{{3}}{{4}}](x,z))).$

###### Remark 3

The syntax of our expressions is determined purely by the finitary coalgebraic
type functor, more precisely, by a given strongly expressive set $\Lambda$ of
monotone singleton-preserving predicate lifting. In contrast, existing
expression calculi such as standard regular expressions for deterministic
automata or the coalgebraic expression calculi in [34, 32] use extra
operations (e.g. expressing union or concatenation of languages). These
operations are not dictated by the setting, viz. an endofunctor on
$\mathbf{Set}$. Rob Myers’ PhD thesis [25] explains nicely how such extra
operations are obtained naturally in an expression calculus when one works
over an algebraic category (such as the one of join-semilattices or vector
spaces over the reals, i.e. algebras for the monad $\mathbb{R}^{(-)}$). We
leave the extension of our expression language to this more general setting
for future work.

Our Kleene theorem requires a number of technical lemmas:

###### Lemma 5.7

Let $\lambda/n$ and $\lambda^{\prime}/n^{\prime}$ be monotone singleton-
preserving predicate liftings for $T$. Let $S$ be an equivalence relation on a
set $X$, let $A_{1},\dots,A_{n}$, be $S$-equivalence classes or empty, and let
$B_{1},\dots,B_{n^{\prime}}$ be $S$-closed subsets of $X$. Then the following
holds.

  1. (1)

$\lambda_{X}(A_{1},\dots A_{n})\subseteq\lambda_{X}^{\prime}(B_{1},\dots
B_{n^{\prime}})\text{ or }\lambda_{X}(A_{1},\dots
A_{n})\cap\lambda_{X}^{\prime}(B_{1},\dots B_{n^{\prime}})=\varnothing.$

  2. (2)

If the $B_{1},\ldots,B_{n^{\prime}}$ are even $S$-equivalence classes or
empty, then

$\displaystyle\lambda_{X}(A_{1},\dots A_{n})=\lambda_{X}^{\prime}(B_{1},\dots
B_{n^{\prime}})\text{ or }\lambda_{X}(A_{1},\dots
A_{n})\cap\lambda_{X}^{\prime}(B_{1},\dots B_{n^{\prime}})=\varnothing.$

######  Proof (Sketch)

Apply naturality to the quotient map $q:X\twoheadrightarrow X/S$.

In the proof of Theorem 5.11 further below, we will make use of a
$\Lambda$-bisimulation. We briefly recall the essentials of this notion [12]:

######  Definition 5.8 ($\Lambda$-Simulation)

Given a pair of $T$-coalgebras $(X,\xi)$ and $(Y,\zeta)$, a _$\Lambda$
-simulation_ is a relation $S\subseteq X\times Y$ such that for all predicate
liftings $\lambda\in\Lambda$ and $X_{i}\subseteq X$, $x\mathbin{S}y$ implies

$\xi(x)\in\lambda_{X}(X_{1},\dots,X_{n})\Rightarrow\zeta(y)\in\lambda_{Y}(S[X_{1}],\dots,S[X_{n}]).$

A _$\Lambda$ -bisimulation_ is a $\Lambda$-simulation $S$ such that
$S^{\circ}$ is also a $\Lambda$-simulation. Elements $(x,y)\in X\times Y$ are
_$\Lambda$ -bisimilar_ if there is a $\Lambda$-bisimulation relating $x$ and
$y$.

###### Theorem 5.9

$\Lambda$-bisimilarity concides with behavioural equivalence.

###### Remark 5.10

In fact, for Theoren 5.9 it is sufficient that $\Lambda$ is separating and the
predicate liftings in $\Lambda$ are monotone. It turns out that Theorem 5.9 is
actually a special case of [20, Theorem 11], applied to the case where the lax
extension is induced by a separating set of monotone predicate liftings.

###### Lemma 5.11

Let $(X,\xi)$ be a $T$-coalgebra, let $\lambda_{i}/k\in\Lambda$,
$i=1,\ldots,k$, and let $(A_{1},\dots,A_{k})$ be the greatest fixed point of
the map $h:(\mathcal{Q}X)^{k}\rightarrow(\mathcal{Q}X)^{k}$ defined by

$\begin{pmatrix}X_{1}\\\ \vdots\\\
X_{k}\end{pmatrix}\mapsto\begin{pmatrix}\xi^{-1}[\lambda_{1,X}(X_{1},\dots,X_{k})]\\\
\vdots\\\ \xi^{-1}[\lambda_{k,X}(X_{1},\dots,X_{k})]\end{pmatrix}$ (5.1)

Then for each $i$, all elements of $A_{i}$ are behaviourally equivalent, and
for all $i$, $j$, either $A_{i}\cap A_{j}=\varnothing$ or $A_{i}=A_{j}$.

(In the above lemma, we restrict to all $\lambda_{i}$ having full arity $k$
and using their arguments in the given order only in the interest of
readability; this is w.l.o.g. since we can just reorder arguments and add
dummy arguments.)

######  Proof (Sketch)

Let $S\subseteq X\times X$ be the relation

$S=\\{(x_{1},x_{2})\mid\exists A_{i}\,.\,x_{1}\in A_{i}\wedge x_{2}\in
A_{i}\\}\cup\Delta_{X}.$

Using Theorem 5.7 one shows first that $S$ is an equivalence relation, which
already takes care of the second part of the claim, and then that $S$ is a
$\Lambda$-bisimulation. The first claim of the lemma then follows by Theorem
5.9.

The final ingredient of our Kleene-type correspondence is the following
adaptation of Bekič’s bisection lemma [6]:

###### Lemma 5.12

For complete lattices $(X,\leq)$, $(Y,\leq)$ and for every pair of monotone
maps $f:X\times Y\rightarrow X$ and $g:X\times Y\rightarrow Y$, we have

$\nu(x,y).(f(x,y),g(x,y))=(x_{0},y_{0})\quad\text{ with
}\quad\begin{array}[]{rl}x_{0}&=\nu x.f(x,\nu y.g(x,y))\\\ y_{0}&=\nu
y.g(x_{0},y).\end{array}$

Although in [6] this lemma only covers least fixed points in a slightly
different setting, the proof is the same. For completeness, we provide it in
the appendix.

Using Theorem 5.12 we can transform every expression $\phi\in\mathcal{E}_{0}$
into a system of flat equations $(z_{1}=\phi_{1},\dots,z_{k}=\phi_{k})$ for
some $k\in\omega$, i.e. equations without nested modalities or fixed point
operators: This is done by first ensuring that every fixed point operator uses
a different fixed point variable and then binding every modality that is not
nested directly under a fixed point operator with a new fixed point operator
using a fresh variable. Thus we can rewrite every expression
$\phi\in\mathcal{E}_{0}$ in the form

$\phi\equiv\nu z_{1}.\,\textit{L}_{1}(z_{1},\nu
z_{2}.\textit{L}_{2}(\dots),\dots,\nu z_{k}.\textit{L}_{k}(\dots))$

for some modalities $L_{i}\in\mathcal{L}$, $i=1,\ldots,k$. If we now
inductively apply Theorem 5.12 and, for readability, additionally normalize
every modality to have as many arguments as there are different fixed point
variables in such an expression, introducing dummy arguments where necessary,
then we can write $\phi$ as a system

$\displaystyle z_{1}$ $\displaystyle=\textit{L}_{1}(z_{1},z_{2},\dots,z_{k})$
(5.2) $\displaystyle z_{2}$
$\displaystyle=\textit{L}_{2}(z_{1},z_{2},\dots,z_{k})$ $\displaystyle\vdots$
$\displaystyle z_{k}$ $\displaystyle=\textit{L}_{n}(z_{1},z_{2},\dots,z_{k})$

of flat equations. Given any coalgebra $C=(X,\xi)$, the above system induces
an obvious map of the form (5.1) (replacing $z_{i}$ by $X_{i}$ and $L_{i}$ by
$\lambda_{i}=\llbracket L_{i}\rrbracket$), and the first components of its
greatest fixed point is the semantics $\llbracket\phi\rrbracket_{C}$. The
following example shows a concrete case.

######  Example 5.13 (Applying Bekič’s bisection lemma)

Consider the expression

$\phi=\nu x.\textit{L}_{1}(x,\textit{L}_{2}(x),\nu y.\textit{L}_{3}(y,\nu
z.\textit{L}_{2}(z)))$

In order to transform it as per the procedure indicated, we first need to add
a fixed point operator with a fresh variable to the first occurrence of
$\textit{L}_{2}$:

$\phi=\nu x.\textit{L}_{1}(x,\nu w.\textit{L}_{2}(x),\nu
y.\textit{L}_{3}(y,\nu z.\textit{L}_{2}(z)))$

Then we can form the equation system for the variables $x,w,y,z$

$\displaystyle x$
$\displaystyle=\overline{}\textit{L}_{1}(x,w,y,z)=\textit{L}_{1}(x,w,y)$
$\displaystyle w$
$\displaystyle=\overline{}\textit{L}_{2}(x,w,y,z)=\textit{L}_{2}(x)$
$\displaystyle y$
$\displaystyle=\overline{}\textit{L}_{3}(x,w,y,z)=\textit{L}_{3}(y,z)$
$\displaystyle z$
$\displaystyle=\overline{}\textit{L}_{4}(x,w,y,z)=\textit{L}_{2}(z)$

where we extend $\mathcal{L}$ with additional operators
$\overline{}\textit{L}_{i}$ having dummy arguments, defined as indicated. The
semantics of this equation system in a coalgebra $C=(X,\xi)$ is defined as the
greatest fixpoint $(A_{0},A_{1},A_{2},A_{3})$ of the map
$h:\mathcal{Q}^{n}X\to\mathcal{Q}^{n}X$ defined by

$h:\begin{pmatrix}X_{1}\\\ X_{2}\\\ X_{3}\\\
X_{4}\end{pmatrix}\mapsto\begin{pmatrix}\xi^{-1}[\llbracket\textit{L}_{1}\rrbracket_{X}(X_{1},X_{2},X_{3})]\\\
\xi^{-1}[\llbracket\textit{L}_{2}\rrbracket_{X}(X_{1})]\\\
\xi^{-1}[\llbracket\textit{L}_{1}\rrbracket_{X}(X_{2},X_{4})]\\\
\xi^{-1}[\llbracket\textit{L}_{2}\rrbracket_{X}(X_{4})]\end{pmatrix}.$

The semantics of $\phi$ in $C$ is then $\llbracket\phi\rrbracket_{C}=A_{0}$.

The following two results together establish a Kleene-type correspondence for
the generic expressions of Theorem 5.1.

###### Theorem 5.14

Every expression $\phi\in\mathcal{E}_{0}$ describes exactly one behavioural
equivalence class, which is moreover realized in a finite coalgebra.
Explicitly: there exists a state $x$ in a finite coalgebra such that for every
coalgebra $C$, $\llbracket\phi\rrbracket_{C}$ contains precisely the states of
$C$ that are behaviourally equivalent to $x$.

######  Proof (Sketch)

By Theorem 5.4, it suffices to show that any two states (w.l.o.g. in the same
coalgebra, using coproducts) satisfying $\phi$ are bisimilar. Since $\phi$ can
transformed into a system (5.2) of flat equations, this follows by Theorem
5.11. Realization in a finite coalgebra follows from the finite model property
of the coalgebraic $\mu$-calculus [8], and alternatively is shown by
constructing a model from the variables in a flat equation system.

###### Theorem 5.15

Let $C=(X,\xi)$ be a finite $T$-coalgebra. For every $x\in X$, there exists an
expression $\phi\in\mathcal{E}_{0}$ such that
$x\in\llbracket\phi\rrbracket_{C}$.

###### Proof

Let $X=\\{x_{1},\dots,x_{k}\\}$ and w.l.o.g. $x=x_{1}$. Since $\Lambda$ is
strongly expressive, for every $x_{i}\in X$ there is a modality $L_{i}$,
w.l.o.g. with arity $k$ and prescribed argument ordering, such that

$\\{\xi(x_{i})\\}=\llbracket
L_{i}\rrbracket_{X}(\\{x_{1}\\},\ldots,\\{x_{k}\\}).$

That is, the $\\{x_{i}\\}$ solve the system
$(x_{i}=L_{i}(x_{1},\dots,x_{k}))_{i=1,\dots,k}$ of flat fixed point
equations, so for the greatest fixed point $(A_{1},\dots,A_{k})$ of the
system, we have $x_{i}\in A_{i}$ for every $i$, in particular $x=x_{1}\in
A_{1}$. It now just remains to convert the equation system into an equivalent
single expression in the standard manner [7] (incurring exponential blow-up);
then $x\in\llbracket\phi\rrbracket_{C}$ as desired.

###### Corollary 1

Every expression denotes a behavioural equivalence class of a state in a
finite coalgebra, and conversely every such class is denoted by some
expression.

###### Example 5.16

  * (1)

For the functor $TX=2\times X^{A}$ for $A=\\{a,b\\}$ consider the coalgebra
with carrier $X=\\{x_{1},x_{2}\\}$ and with coalgebra structure $\xi:X\to
2\times X^{A}$ with $\xi(x_{0})=(1,(a\mapsto x_{0},b\mapsto x_{1}))$ and
$\xi(x_{1})=(0,(a\mapsto x_{1},b\mapsto x_{0}))$. Then we clearly have
$\\{\xi(x_{1})\\}=\lambda^{1}(\\{x_{1}\\},\\{x_{2}\\})$ and
$\\{\xi(x_{2})\\}=\lambda^{1}(\\{x_{2}\\},\\{x_{1}\\})$. Using the syntax of
Theorem 5.6.1 and following the proof of Theorem 5.15, we obtain the following
expression for the behavioural equivalence class (i.e. formal language) for
$x_{1}$:

$\nu x_{1}.\langle 1,a.x_{1},b.\nu x_{2}.\langle
0,a.x_{2},b.x_{1}\rangle\rangle.$

Note that this is the same expression (modulo $\alpha$-equivalence) as the
third expression from Theorem 5.6.1.

  * (2)

For the functor $\mathcal{P}_{\omega}(A\times-)$ and $A=\\{a,b\\}$ the
coalgebra $C=(\\{x,y,z,w\\},\xi)$ depicted in Theorem 5.6.2 satisfies the
following equations:

$\\{\xi(x)\\}=\lambda_{C}^{(a)}(\\{y\\}),\;\\{\xi(y)\\}=\lambda_{C}^{(a,b,c)}(\\{x,w,z\\}),\;\\{\xi(w)\\}=\lambda_{C}^{()}(),\;\\{\xi(w)\\}=\lambda_{C}^{()}()$

By Theorem 5.15 $\\{\\{x\\},\\{y\\},\\{z\\},\\{w\\}\\}$ solves the following
system, reusing the same variable names,

$x=[a](y),\quad y=[a,b,a](x,w,z),\quad w=[()],\quad z=[()]$

which can be transformed as demonstrated in Theorem 5.13 to the expression
given in Theorem 5.6.2, describing the behaviour of the state $x$.

  * (3)

For the functor $T=\mathcal{D}$ consider the expression from Theorem 5.6.3:
$\nu x.[\nicefrac{{2}}{{3}},\nicefrac{{1}}{{3}}](x,\nu
y.[\nicefrac{{1}}{{6}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{2}}](x,y,\nu
z.[\nicefrac{{1}}{{4}},\nicefrac{{3}}{{4}}](x,z)))$, which transforms to the
system

$x=[\nicefrac{{2}}{{3}},\nicefrac{{1}}{{3}}](x,y),\quad
y=[\nicefrac{{1}}{{6}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{2}}](x,y,z),\quad
z=[\nicefrac{{1}}{{4}},\nicefrac{{3}}{{4}}](x,z).$

By Theorem 5.14 we can construct a coalgebra $C=(\\{x,y,z\\},\xi)$ defined by:

$\displaystyle\\{\xi(x)\\}$
$\displaystyle=\lambda_{X}^{(\nicefrac{{2}}{{3}},\nicefrac{{1}}{{3}})}(\\{x\\},\\{y\\})$
$\displaystyle\\{\xi(y)\\}$
$\displaystyle=\lambda_{X}^{(\nicefrac{{1}}{{6}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{2}})}(\\{x\\},\\{y\\},\\{z\\})$
$\displaystyle\\{\xi(z)\\}$
$\displaystyle=\lambda_{X}^{(\nicefrac{{1}}{{4}},\nicefrac{{3}}{{4}})}(\\{x\\},\\{z\\})$

which is exactly the coalgebra depicted in Theorem 5.6.3 where $x$ is in the
behavioural equivalence class of the above expression.

An alternative approach to defining the semantics of expressions is to
construct a $T$-coalgebra structure on the set $\mathcal{E}_{0}$ of closed and
guarded expressions, similarly as in the work of Silva et al. [34] and also
Myers [25]. In Theorem 5.19 below we show that this new semantics coincides
with the previous one.

###### Definition 5.17

We define a $T$-coalgebra $\varepsilon:\mathcal{E}_{0}\rightarrow
T\mathcal{E}_{0}$ inductively by

$\displaystyle\varepsilon(\textit{L}(\phi_{1},\dots,\phi_{n}))$
$\displaystyle\in\llbracket L\rrbracket(\\{\phi_{1}\\},\dots,\\{\phi_{n}\\})$
(5.3) $\displaystyle\varepsilon(\nu x.\phi)$
$\displaystyle=\varepsilon(\phi[\nu x.\phi/x]).$ (5.4)

This is actually a definition of $\varepsilon$ because (a) in (5.3),
$\llbracket L\rrbracket$ preserves singletons and thus there is only one
element in $\llbracket L\rrbracket(\\{\phi_{1}\\},\dots,\\{\phi_{n}\\})$, and
(b) for the inductive part (5.4), one can use the number of top-level fixed
point operators as a termination measure, which decreases in each step because
the fixed points are guarded.

Now recall that a coalgebra $\xi:X\to TX$ is _locally finite_ if every $x\in
X$ is contained in a finite subcoalgebra of $\xi$. Locally finite coalgebras
are precisely the (directed) unions of finite coalgebras (see [21]). Thus, it
follows from Theorem 5.15 that for any $x\in X$ in a locally finite coalgebra
$\xi:X\to TX$, there exists a $\phi\in\mathcal{E}_{0}$ with
$x\in\llbracket\phi\rrbracket_{X}$.

Moreoever, $\mathcal{E}_{0}$ is obviously not finite; however, arguing via
finiteness of the Fischer-Ladner closure [16] we obtain

###### Proposition 5.18

The $T$-coalgebra $(\mathcal{E}_{0},\varepsilon)$ is locally finite.

The following theorem says that $(\mathcal{E}_{0},\varepsilon)$ serves as a
canonical model of the expression language:

###### Theorem 5.19

For every closed and guarded expression $\phi\in\mathcal{E}_{0}$ and every
state $x$ in a $T$-coalgebra $C$, $x\in\llbracket\phi\rrbracket_{C}$ iff $x$
is behaviourally equivalent to $\phi$ as a state in
$(\mathcal{E}_{0},\varepsilon)$.

In particular, the above implies that

$\phi\in\llbracket\phi\rrbracket_{\mathcal{E}_{0}}\qquad\text{for all
$\phi\in\mathcal{E}_{0}$,}$ (5.5)

essentially a truth lemma for $\mathcal{E}_{0}$. For the proof of Theorem
5.19, we note:

###### Lemma 5.20

$\alpha$-Equivalent expressions are behaviourally equivalent as states in
$(\mathcal{E}_{0},\varepsilon)$.

######  Proof (Theorem 5.19, sketch)

It suffices to prove (5.5): The ‘if’ direction of the claim then follows from
invariance of $\phi$ under behavioural equivalence (Theorem 5.4), and ‘only
if’ is by Theorem 5.14. We generalize (5.5) to expressions $\phi$ with free
variables: Whenever $\sigma$ is a substitution of the free variables of $\phi$
and $\kappa$ a valuation such that $\sigma(v)\in\kappa(v)$ for every free
variable $v$ of $\phi$, then

$\phi\sigma\in\llbracket\phi\rrbracket_{\mathcal{E}_{0}}^{\kappa}.$

We proceed by induction on $\phi$, using Lemma 5.20 in the fixpoint case.

###### Remark 5.21

To give a concrete example use of the connection between expression languages
and modal fixed point logics afforded by the above results, we note that we
now obtain an alternative handle on equivalence of expressions that
complements the standard approach via partition refinement: Expressions
$\phi,\psi$ are equivalent iff some state described by $\phi$ (obtained, e.g.,
via the one of the model constructions in Theorems 5.14 and 5.19) satisfies
$\psi$. Note that the latter is fairly easy to check as long as the modalities
are computationally tractable, since $\psi$ otherwise involves only greatest
fixed points. This approach is similar to reasoning algorithms in the
lightweight description logic $\mathcal{EL}$ [4], where checking validity of
$\phi\to\psi$ is reduced to model checking $\psi$ in a minimal model of
$\phi$; we leave a more detailed analysis to future work.

##  6 Conclusion and Further Work

We have defined a generic expression language for behaviours of finite set
coalgebras based on predicate liftings, specifically on a strongly expressive
set of singleton-preserving predicate liftings. There are mutual conversions
between such sets of predicate liftings and functor presentations, one
direction being via the Moss liftings introduced by Marti and Venema [20]; we
have however demonstrated that these fail to be mutually inverse in one
direction, i.e. in general not all singleton-preserving predicate liftings are
Moss liftings. Our language is presumably equivalent to the set-based instance
of Myer’s expression language [25]; our alternative presentation is aimed
primarily at showing that expression languages embed naturally into the
coalgebraic $\mu$-calculus, generalizing well-known results on the relational
$\mu$-calculus [14, 10, 35, 2]. The benefit of this insight is to tighten the
connection between expression languages and specification logics, e.g. it
allows for combining model checking, equivalence checking, and reasoning
within a single formalism. On a more technical note, we show, e.g., that one
can provide an alternative semantics of expressions by defining a coalgebra
structure on expressions, an approach pioneered by Silva et al. [34] and used
also by Myers [25]; in the light of the expressions/logic correspondence, this
construction is now seen as a canonical model construction for a fragment of
the coalgebraic $\mu$-calculus, and the core part of the proof that the two
semantics agree becomes just a truth lemma.

An important point for further work is to extend the current setup from the
base category $\mathbf{Set}$ to algebraic categories (such as join semi-
lattices or positive convex algebras) in order to generalize our results to
expression calculi involving convenient additional operations (reflecting the
ambient algebraic theory) such as addition. A closely related point is the
connection with coalgebraic determinization [33]; it should be interesting to
see whether our ideas can lead to expression calculi for coarser system
equivalences than bisimilarity, such as trace equivalence for transition
systems or distribution bisilimarity for Segala systems. Such a generalization
might be based on our recent approach to coalgebraic trace semantics via
graded monads [22].

##  Appendix 0.A Omitted Details and Proofs

### Proof of Theorem 3.6

_1.:_ First note that (3.2) is really a definition of $\tau_{\lambda}$ because
$\lambda$ is preserves singletons. Moreover, $\tau_{\lambda}$ is natural
because for $f:X\to Y$ and $x_{i}\in X$,

$\displaystyle\tau_{\lambda,X}(x_{1},\ldots,x_{n})$
$\displaystyle\in\lambda_{X}(\\{x_{1}\\},\ldots,\\{x_{n}\\})$ (by definition)
$\displaystyle\subseteq\lambda_{X}(f^{-1}[\\{f(x_{1})\\}],\ldots,f^{-1}[\\{f(x_{n})\\}])$
($\lambda$ monotone)
$\displaystyle=(Tf)^{-1}[\lambda_{Y}(\\{f(x_{1})\\},\ldots,\\{f(x_{n})\\})]$
(naturality of $\lambda$)
$\displaystyle=(Tf)^{-1}[\\{\tau_{\lambda,Y}(f(x_{1}),\ldots,f(x_{n}))\\}]$
(by definition) $\displaystyle\Rightarrow\ $ $\displaystyle
Tf(\tau_{\lambda,X}(x_{1},\ldots,x_{n}))=\tau_{\lambda,Y}(f(x_{1}),\ldots,f(x_{n}))$

_2.:_ By the previous item, we obtain a natural transformation
$\alpha=[\tau_{\lambda}]_{\lambda\in\Lambda}$, and strong expressivity implies
that $\alpha$ is componentwise surjective. ∎

### Proof of Theorem 4.8

Recall that $\lambda=\nabla^{L}\circ\tau\mathcal{Q}$ by definition. Let
$s_{X}:X\rightarrow\mathcal{Q}X$ be the function $s_{X}(x)=\\{x\\}$. Then we
have

$\displaystyle\lambda_{X}(\\{x_{1}\\},\ldots,\\{x_{n}\\})$
$\displaystyle=\\{t\in
TX\mid(t,\tau_{\mathcal{Q}X}(\\{x_{1}\\},\ldots,\\{x_{n}\\}))\in
L(\in_{X})\\}$ $\displaystyle=\\{t\in
TX\mid(t,\tau_{\mathcal{Q}X}(s_{X}(x_{1}),\dots,s_{X}(x_{n})))\in
L(\in_{X})\\}$ $\displaystyle=\\{t\in
TX\mid(t,Ts_{X}\circ\tau_{X}(x_{1},\dots,x_{n}))\in L(\in_{X})\\}$
$\displaystyle=\\{t\in TX\mid(t,\tau_{X}(x_{1},\dots,x_{n}))\in
L(\in_{X});(Ts_{X})^{\circ}\\}$ $\displaystyle=\\{t\in
TX\mid(t,\tau_{X}(x_{1},\dots,x_{n}))\in L(\in_{X};s_{X}^{\circ})\\}$
(Proposition 4.2) $\displaystyle=\\{t\in
TX\mid(t,\tau_{X}(x_{1},\dots,x_{n}))\in L(\Delta_{X})\\}$
$(s_{X};\mathord{\ni_{X}}=\Delta_{X})$
$\displaystyle=\\{\tau_{X}(x_{1},\dots,x_{n})\\}$ ∎

### Proof of Theorem 4.9

Let $t\in TX$; we need to show that
$\\{t\\}=\lambda(\\{x_{1}\\},\dots,\\{x_{n}\\})$ for some Moss lifting
$\lambda$ and $x_{1},\ldots,x_{n}\in X$. Since $\alpha:T_{\Sigma}\to T$ from
our functor presentation of $T$ has surjective components, there exists some
$\tau/n\in\Sigma$ such that
$t=\alpha_{X}(x_{1},\ldots,x_{n})=\tau_{X}(x_{1},\dots,x_{n})$ for some
$x_{1},\ldots,x_{n}\in X$. Because $L$ is a lax extension, we have
$Ts_{X}\subseteq Ls_{X}\subseteq L(\in_{X})$ for the function
$s_{X}:x\mapsto\\{x\\}$ and thus

$(t,Ts_{X}(t))=(t,\tau_{\mathcal{Q}X}(\\{x_{1}\\},\dots,\\{x_{n}\\}))\in
L(\in_{X})$

since
$Ts_{X}(t)=Ts_{X}(\tau_{X}(x_{1},\ldots,x_{n}))=\tau_{\mathcal{Q}X}(s_{X}(x_{1}),\ldots,s_{X}(x_{n}))$.
Thus $t\in\lambda(\\{x_{1}\\},\dots,\\{x_{n}\\})$ (see Theorem 4.6), and since
Moss liftings preserve singletons, we conclude
$\\{t\\}=\lambda(\\{x_{1}\\},\dots,\\{x_{n}\\})$ as desired. ∎

### Details for 2

We show that $\lambda=\lambda^{(\tau^{\lambda})}$ for monotone singleton-
preserving _unary_ predicate liftings $\lambda$. Let $\lambda/1$ and
$\lambda^{\prime}/1$ be predicate liftings that agree on singletons. Now for
any $X$ and $A\subseteq X$ consider the characteristic map $\chi_{A}:X\to
2=\\{\bot,\top\\}$, which satisfies $A=\chi_{A}^{-1}(\top)$. Then using
naturality and the fact that
$\lambda_{2}(\\{\top\\})=\lambda_{2}^{\prime}(\\{\top\\})$, we have

$\displaystyle\lambda_{X}(A)$
$\displaystyle=\lambda_{X}(\chi_{A}^{-1}(\\{\top\\}))=(T\chi_{A})^{-1}(\lambda_{2}(\\{\top\\}))$
$\displaystyle=(T\chi_{A})^{-1}(\lambda_{2}^{\prime}(\\{\top\\}))=\lambda_{X}^{\prime}(\chi_{A}^{-1}(\\{\top\\}))=\lambda_{X}^{\prime}(A).$

Now observe that $\lambda$ and $\lambda^{(\tau^{\lambda})}$ agree on
singletons, thus they are equal as desired.

### Proof of Theorem 5.5

First we prove that for any expression $\phi\in\mathcal{E}$ that does not
contain free variables that are bound in another expression
$\psi\in\mathcal{E}$ the following holds:

$\displaystyle\llbracket\psi\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]}=\llbracket\psi[\phi/z]\rrbracket^{\kappa}$
(0.A.1)

Induction on $\psi$. If $\psi=x\neq z$ then $\llbracket
x\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]}=\llbracket
x\rrbracket^{\kappa}=\llbracket x[\phi/z]\rrbracket^{\kappa}$; if $\psi=z$
then $\llbracket
z\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]}=\llbracket\phi\rrbracket^{\kappa}=\llbracket
z[\phi/z]\rrbracket^{\kappa}$; for
$\psi=\textit{L}(\phi_{1},\ldots,\phi_{n})$:

$\displaystyle\llbracket\textit{L}(\psi_{1},\ldots,\psi_{n})\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]}=\xi^{-1}[\llbracket
L\rrbracket(\llbracket\psi_{1}\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]},\ldots,\llbracket\psi_{n}\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]})]$
$\displaystyle\overset{I.H.}{=}\xi^{-1}\big{[}\llbracket
L\rrbracket(\llbracket\psi_{1}[\phi/z]\rrbracket,\ldots,\llbracket\psi_{n}[\phi/z]\rrbracket)\big{]}=\llbracket\textit{L}(\psi_{1}[\phi/z],\ldots,\psi_{n}[\phi/z])\rrbracket$
$\displaystyle=\llbracket\textit{L}(\psi_{1},\ldots,\psi_{n})[\phi/z]\rrbracket;$

if $\psi=\nu z.\psi_{1}$ then $\llbracket\nu
z.\psi_{1}\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]}=\llbracket\nu
z.\psi_{1}\rrbracket^{\kappa}=\llbracket(\nu
z.\psi)[\phi/z]\rrbracket^{\kappa}$; if $\psi=\nu x.\psi_{1}$ with $x\neq z$
then:

$\displaystyle\llbracket\nu
x.\psi_{1}\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}]}=\nu
Y.\llbracket\psi_{1}\rrbracket^{\kappa[z\mapsto\llbracket\phi\rrbracket^{\kappa}][x\mapsto
Y]}=\nu Y.\llbracket\psi_{1}\rrbracket^{\kappa[x\mapsto
Y][z\mapsto\llbracket\phi\rrbracket^{\kappa}]}$
$\displaystyle\overset{I.H.}{=}\nu
Y.\llbracket\psi_{1}[\phi/z]\rrbracket^{\kappa[x\mapsto Y]}=\llbracket\nu
x.(\psi_{1}[\phi/z])\rrbracket^{\kappa}=\llbracket(\nu
x.\psi_{1})[\phi/z]\rrbracket^{\kappa}$

where the last equation holds because of the assumption that the free
variables of $\phi$ are not bound in $\psi$.

It follows that

$\llbracket\nu z.\phi\rrbracket=\nu Y.\llbracket\phi\rrbracket^{[z\mapsto
Y]}=\llbracket\phi\rrbracket^{[z\mapsto\llbracket\nu
z.\phi\rrbracket]}\overset{\eqref{eq:substitutionlemma}}{=}\llbracket\phi[\nu
z.\phi/z]\rrbracket.$

### Proof of Theorem 5.7

Denote by $q:X\twoheadrightarrow X/S$ the canonical quotient map, let
$C_{1},\ldots,C_{m}\subseteq X$ be $S$-closed, and let $\lambda/m$ be monotone
and preserve singletons. Then $C_{i}=q^{-1}[q[C_{i}]]$ for all $i$. Therefore,
we have for every $t\in\mathcal{Q}TX$:

$\displaystyle t\in\lambda_{X}(C_{1},\dots
C_{m})=\lambda_{X}(q^{-1}[q[C_{1}]],\dots,q^{-1}[q[C_{m}]])$
$\displaystyle\Rightarrow
t\in(Tq)^{-1}[\lambda_{X/S}(q[C_{1}],\dots,q[C_{m}])]$ (0.A.2)
$\displaystyle\Rightarrow Tq(t)\in\lambda_{X/S}(q[C_{1}],\dots,q[C_{m}]).$

  * (1)

If there is some $t\in\lambda_{X}(A_{1},\dots
A_{n})\cap\lambda_{X}^{\prime}(B_{1},\dots B_{n^{\prime}})$, then we show the
inclusion. For $s\in\lambda_{X}(A_{1},\dots A_{n})$, (0.A.2) provides

$\\{Tq(t),Tq(s)\\}\subseteq\lambda_{X/S}(q[A_{1}],\ldots,q[A_{n}]).$

Every $A_{i}\subseteq X$ is an $S$-equivalence class or empty, so $q[A_{i}]$
is at most a singleton. By monotonicity and singleton preservation of
$\lambda$, the right-hand side is at most a singleton, and thus $Tq(t)=Tq(s)$.
Applying $\eqref{eq:gat}$ to $t$ and $B_{1},\ldots,B_{n^{\prime}}$, we have
$Tq(s)=Tq(t)\in\lambda^{\prime}(q[B_{1}],\ldots,q[B_{n^{\prime}}])$, and
consequently $s\in\lambda^{\prime}(B_{1},\ldots,B_{n^{\prime}})$, again by
(0.A.2).

  * (2)

In the case where the sets are not disjoint, the equality is obtained by
proving both inclusions using point (1). ∎

### Proof of Theorem 5.11

Let $S\subseteq X\times X$ be the relation

$S=\\{(x_{1},x_{2})\mid\exists A_{i}\,.\,x_{1}\in A_{i}\wedge x_{2}\in
A_{i}\\}\cup\Delta_{X}.$

(1) We prove that $S$ is an equivalence relation. Let $\overline{S}$ be the
equivalence relation generated by $S$, and let $\overline{A_{i}}$ be the
$S$-closure of $A_{i}$. Then the $\overline{A_{i}}$ are also
$\overline{S}$-closed, and we have

$\overline{S}=\\{(x_{1},x_{2})\mid\exists\overline{A_{i}}\,.\,x_{1}\in\overline{A_{i}}\wedge
x_{2}\in\overline{A_{i}}\\}\cup\Delta_{X}.$

It follows that each $\overline{A_{i}}$ is either empty (if $A_{i}=\emptyset$)
or else an $\overline{S}$-equivalence class.

Now we show that $(\overline{A_{1}},\dots,\overline{A_{k}})$ is a post-fixed
point of $h$: Because $(A_{1},\dots,A_{n})$ is a fixed point and the
$\lambda_{i}$ are monotone, we have

$A_{j}=\xi^{-1}[\lambda_{j,X}(A_{1},\dots,A_{k})]\subseteq\xi^{-1}[\lambda_{j,X}(\overline{A_{1}},\dots,\overline{A_{k}})]\quad\text{for
all $j$}.$ (0.A.3)

We will show that the post-fixed point condition

$\overline{A_{j}}\subseteq\xi^{-1}[\lambda_{j,X}(\overline{A_{1}},\dots,\overline{A_{k}})]$
(0.A.4)

holds for all $j$. To see this, it suffices by (0.A.3) and the definition of
$\overline{A_{j}}$ to show that whenever $A_{l}\cap A_{p}\neq\emptyset$, then

$\lambda_{l,X}(\overline{A_{1}},\dots,\overline{A_{k}})=\lambda_{p,X}(\overline{A_{1}},\dots,\overline{A_{k}}).$
(0.A.5)

So let $x\in A_{l}\cap A_{p}$. Then by (0.A.3),
$\xi(x)\in\lambda_{l,X}(\overline{A_{1}},\dots,\overline{A_{k}})\cap\lambda_{p,X}(\overline{A_{1}},\dots,\overline{A_{k}})$,
and therefore (0.A.5) follows by Theorem 5.7.2.

Having shown that $(\overline{A_{1}},\dots,\overline{A_{k}})$ is a post-fixed
point of $h$, we obtain that $\overline{A_{i}}\subseteq A_{i}$ for all $i$,
which implies that $S=\overline{S}$ is an equivalence relation. Hence every
$A_{i}$ is either empty or an equivalence class of $S$, whence $A_{i}\cap
A_{j}=\emptyset$ or $A_{i}=A_{j}$ holds for all $i,j$ as claimed in the second
part of the lemma.

(2) Now we prove that $S$ is a $\Lambda$-bisimulation, i.e. $x\mathbin{S}y$
and $\xi(x)\in\lambda_{X}(B_{1},\dots,B_{n})$ implies
$\xi(y)\in\lambda_{X}(S[B_{1}],\dots,S[B_{n}])$ for every
$\lambda/n\in\Lambda$ and $B_{j}\subseteq X$. By Theorem 5.9, this implies the
first claim of the lemma, since $x,y\in A_{j}$ implies $x\,S\,y$ by
construction of $S$.

By point (1), $S$ is an equivalence relation, so
$S[B_{j}]=\overline{B_{j}}\supseteq B_{j}$ is the $S$-closure of $B_{j}$; and
since $\lambda$ is monotone,
$\xi(x)\in\lambda_{X}(\overline{B_{1}},\dots,\overline{B_{n}})$. Further,
$x\mathbin{S}y$ implies that either $x=y$, in which case there is nothing to
prove, or there exists $j$ such that $x,y\in A_{j}$ and therefore

$\xi(x),\xi(y)\in\lambda_{j,X}(A_{1},\dots,A_{k}).$

Because $\xi(x)$ also lies in
$\lambda_{X}(\overline{B_{1}},\dots,\overline{B_{n}})$, we obtain

$\lambda_{j,X}(A_{1},\dots,A_{k})\subseteq\lambda_{X}(\overline{B_{1}},\dots,\overline{B_{n}})$

by Theorem 5.7, and thus $\xi(y)\in\lambda_{X}(S[B_{1}],\dots,S[B_{n}])$. ∎

### Proof of Theorem 5.12

By Tarski, all fixed points exist. $(x_{0},y_{0})$ is a fixed point of
$\langle f,g\rangle:X\times Y\to X\times Y$, because $y_{0}=g(x_{0},y_{0})$
and thus also

$x_{0}=f(x_{0},\nu y.g(x_{0},y))=f(x_{0},g(x_{0},y_{0}))=f(x_{0},y_{0}).$

For any other fixed point $(x^{\prime},y^{\prime})$ of $\langle f,g\rangle$,
we have

$x^{\prime}=f(x^{\prime},y^{\prime})=f(x^{\prime},g(x^{\prime},y^{\prime}))\leq
f(x^{\prime},\nu y.g(x^{\prime},y)),$

so $x^{\prime}\leq x_{0}$ and furthermore
$y^{\prime}=g(x^{\prime},y^{\prime})\leq g(x_{0},y^{\prime})\leq\nu
y.g(x_{0},y)$.∎

### Proof of Theorem 5.14

We first show that $\phi$ denotes a single behavioural equivalence class, i.e.
(i) we have invariance under behavioural equivalence (Theorem 5.4) and (ii)
two states satisfying $\phi$ are bisimilar. In order to prove (ii) we may
w.l.o.g. assume that the two states live in the same coalgebra; indeed, given
two coalgebras $C$ and $D$ and states $x$ in $C$ and $y$ in $D$ satisfyfing
$\phi$, then $\operatorname{inl}(x),\operatorname{inr}(y)$ in $C+D$ are
behaviourally equivalent to $x$ and $y$, respectively, thus both satisfy
$\phi$ by Theorem 5.4.

Now let $C=(X,\xi)$ be a $T$-coalgebra; we need to show that any two elements
of $\llbracket\phi\rrbracket_{C}$ are behaviourally equivalent. As noted
above, we can transform $\phi$ into a system (5.2) of flat equations, and
$\llbracket\phi\rrbracket_{C}$ is the first component of the greatest fixed
point of the corresponding map of the form (5.1). The claim thus follows by
Theorem 5.11.

It remains to show that there exists a finite coalgebra $C$ such that
$\llbracket\phi\rrbracket_{C}\neq\emptyset$. This is immediate from the finite
model property of the coalgebraic $\mu$-calculus [8]; alternatively, avoiding
such overkill, it is seen as follows: We define $C=(X,\xi)$ on the set
$X=\\{x_{1},\dots,x_{k}\\}$ of the variables in the above flat equation system
by $\xi(x_{i})\in\llbracket
L_{i}\rrbracket_{X}(\\{x_{1}\\},\dots,\\{x_{k}\\})$ where
$\phi_{i}=L_{i}(x_{1},\dots,x_{k})$. Then by construction,
$(\\{x_{1}\\},\dots,\\{x_{k}\\})$ is a fixed point of the equation system,
hence contained in the greatest fixed point, which proves the desired non-
emptiness of the greatest fixed point.

### Proof of Theorem 5.18

Recall that the Fischer-Ladner closure of a $\mu$-calculus formula is
standardly defined as the closure under subformulas, negation, and fixed point
unfolding. In the absence of negation, we adapt the definition to include only
closure under subformulas and fixed point unfolding. We then, of course,
inherit the standard result that the Fischer-Ladner closure is finite [16].
Now by construction of $\varepsilon$, the subcoalgebra of
$(\mathcal{E}_{0},\varepsilon)$ generated by $\phi\in\mathcal{E}_{0}$ contains
only states from the Fisher-Ladner-closure of $\phi$, hence is finite. ∎

### Proof of Theorem 5.19

It suffices to prove the truth lemma (5.5): The ‘if’ direction of the claim
then follows from invariance of $\phi$ under behavioural equivalence (Theorem
5.4), and ‘only if’ is by Theorem 5.14.

We strengthen (5.5) to a claim on expressions $\phi$ possibly having free
variables: Whenever $\sigma$ is a substitution of the free variables of $\phi$
and $\kappa$ a valuation such that $\sigma(v)\in\kappa(v)$ for every free
variable $v$ of $\phi$, then

$\phi\sigma\in\llbracket\phi\rrbracket_{\mathcal{E}_{0}}^{\kappa}.$ (0.A.6)

We prove (0.A.6) by induction over $\phi$. The case for fixed point variables
is just by the assumption on $\sigma$ and $\kappa$. For the modal case, we
calculate as follows:

$\displaystyle L(\phi_{1},\dots,\phi_{n})\sigma$
$\displaystyle=L(\phi_{1}\sigma,\dots,\phi_{n}\sigma)$
$\displaystyle\in\varepsilon^{-1}[\llbracket
L\rrbracket(\\{\phi_{1}\sigma_{1}\\},\dots,\\{\phi_{n}\sigma\\})$ (by
definition) $\displaystyle\subseteq\varepsilon^{-1}[\llbracket
L\rrbracket(\llbracket\phi_{1}\rrbracket_{\mathcal{E}_{0}}^{\kappa},\dots,\llbracket\phi_{n}\rrbracket_{\mathcal{E}_{0}}^{\kappa}\\})$
(induction, monotonicity) $\displaystyle=\llbracket
L(\phi_{1},\dots,\phi_{n})\rrbracket_{\mathcal{E}_{0}}^{\kappa}.$ (semantics)

Finally, for the fixed point case $\nu x.\,\phi$, first note that by Lemma
5.20, we can assume that $x$ does not occur as a free variable in $\sigma(v)$
for any free variable $v$ of $\nu x.\,\phi$. Moreover, since $x$ is not free
in $\nu x.\,\phi$, $\sigma$ does not touch $x$. Thus, $(\nu
x.\,\phi)\sigma=\nu x.\,(\phi\sigma)$. By construction of $\varepsilon$, $\nu
x.\,(\phi\sigma)$ is, as a state of $\mathcal{E}_{0}$, behaviourally
equivalent to $\phi\sigma[\nu x.\,\phi\sigma/x]$, which by the inductive
hypothesis is contained in
$\llbracket\phi\rrbracket_{\mathcal{E}_{0}}^{\kappa^{\prime}}$ where
$\kappa^{\prime}$ arises from $\kappa$ by assigning to $x$ the value $\\{\nu
x.\,\phi\sigma\\}=\\{(\nu x.\,\phi)\sigma\\}$. This shows that $\\{(\nu
x.\,\phi)\sigma\\}$ is a post-fixed point of the map defining $\llbracket\nu
x.\,\phi\rrbracket_{\mathcal{E}_{0}}^{\kappa}$, and hence contained in
$\llbracket\nu x.\,\phi\rrbracket_{\mathcal{E}_{0}}^{\kappa}$, which proves
the claim. ∎

### Proof of Theorem 5.20

Let $\pi_{\alpha}:\mathcal{E}_{0}\to\mathcal{E}_{0}/\alpha$ denote the
quotient map of $\mathcal{E}_{0}$ modulo $\alpha$-equivalence. Paralleling the
definition of $\varepsilon$, we define a $T$-coalgebra structure
$\varepsilon_{\alpha}$ on $\mathcal{E}_{0}/\alpha$ by

$\displaystyle\varepsilon_{\alpha}(\pi_{\alpha}(\textit{L}(\phi_{1},\dots,\phi_{n})))$
$\displaystyle\in\llbracket
L\rrbracket(\\{\pi_{\alpha}(\phi_{1})\\},\dots,\\{\pi_{\alpha}(\phi_{n})\\})$
$\displaystyle\varepsilon(\pi_{\alpha}(\nu x.\phi))$
$\displaystyle=\varepsilon(\pi_{\alpha}(\phi[\nu x.\phi/x])).$

One sees in largely the same way as for $\varepsilon$ that this is actually a
definition, noting additionally that $\alpha$-equivalent transformations of a
formula $L(\phi_{1},\dots,\phi_{n})$ necessarily happen in its arguments
$\phi_{i}$ and that the number of top-level fixed point operators is invariant
under $\alpha$-equivalence. We are done once we show that
$\pi_{\alpha}:(\mathcal{E}_{0},\varepsilon)\to(\mathcal{E}_{0}/\alpha,\varepsilon_{\alpha})$
is a coalgebra morphism. We proceed by case distinction over the shape of
states $\phi\in\mathcal{E}_{0}$:

First assume that $\phi$ has the form $\phi=L(\phi_{1},\dots,\phi_{n})$. We
have to show
$T\pi_{\alpha}(\varepsilon(L(\phi_{1},\dots,\phi_{n})))\in\llbracket
L\rrbracket(\\{\pi_{\alpha}(\phi_{1})\\},\dots,\\{\pi_{\alpha}(\phi_{n})\\})$.
By naturality, this is equivalent to
$\varepsilon(L(\phi_{1},\dots,\phi_{n}))\in\llbracket
L\rrbracket(\pi_{\alpha}^{-1}[\\{\pi_{\alpha}(\phi_{1})\\}],\dots,\pi_{\alpha}^{-1}[\\{\pi_{\alpha}(\phi_{n})\\}])$,
which follows by monotonicity from the fact that
$\varepsilon(L(\phi_{1},\dots,\phi_{n}))\in\llbracket
L\rrbracket(\\{\phi_{1}\\},\dots,\\{\phi_{n}\\})$ by definition.

Second, assume that $\phi$ has the form $\phi=\nu x.\psi$. We proceed by
induction on the number of top-level fixed point operators in $\phi$: We have

$\displaystyle T\pi_{\alpha}(\varepsilon(\nu x.\psi))$
$\displaystyle=T\pi_{\alpha}(\varepsilon(\psi[\nu x.\psi/x]))$ (by definition)
$\displaystyle=\varepsilon_{\alpha}(\pi_{\alpha}(\psi[\nu x.\psi/x]))$
(induction) $\displaystyle\varepsilon_{\alpha}(\pi_{\alpha}(\nu x.\psi))$ .
(by definition)

Since $\phi$ is closed, these are the only cases. ∎

## References

  * [1] Aceto, L., Hennessy, M.: Termination, deadlock, and divergence. J. ACM 39, 147–187 (1992)
  * [2] Aceto, L., Ingólfsdóttir, A., Larsen, K., Srba, J.: Reactive systems: modelling, specification and verification. Cambridge University Press (2007)
  * [3] Adámek, J., Trnková, V.: Automata and Algebras in Categories, Mathematics and its Applications, vol. 37. Kluwer (1990)
  * [4] Baader, F., Brandt, S., Lutz, C.: Pushing the $\mathcal{EL}$ envelope. In: International Joint Conference on Artificial Intelligence, IJCAI 2005. Morgan-Kaufmann (2005)
  * [5] Barr, M.: Relational algebras. In: Proc. Midwest Category Seminar. LNM, vol. 137. Springer (1970)
  * [6] Bekič, H.: Definable operations in general algebras, and the theory of automata and flowcharts. In: Programming Languages and Their Definition - Hans Bekic (1936-1982). pp. 30–55. Springer (1984)
  * [7] Bradfield, J., Stirling, C.: Modal logics and mu-calculi. In: Handbook of Process Algebra, pp. 293–332. Elsevier (2001)
  * [8] Cîrstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic mu-calculus. Log. Meth. Comput. Sci. 7 (2011)
  * [9] Cîrstea, C., Kurz, A., Pattinson, D., Schröder, L., Venema, Y.: Modal logics are coalgebraic. Comput. J. 54, 31–41 (2011)
  * [10] Godskesen, J., Ingólfsdóttir, A., Zeeberg, M.: Fra Hennessy-Milner logik til CCS-processer. Master’s thesis, Aalborg University (1987)
  * [11] Goncharov, S., Milius, S., Silva, A.: Towards a coalgebraic Chomsky hierarchy (extended abstract). In: Theoretical Computer Science, IFIP TCS 2014. LNCS, vol. 8705, pp. 265–280. Springer (2014)
  * [12] Gorín, D., Schröder, L.: Simulations and bisimulations for coalgebraic modal logics. In: Algebra and Coalgebra in Computer Science, CALCO 2013. LNCS, vol. 8089, pp. 253–266. Springer (2013)
  * [13] Gorín, D., Schröder, L.: Subsumption checking in conjunctive coalgebraic fixpoint logics. In: Advances in Modal Logic, AiML 2014. pp. 254–273. College Publications (2014)
  * [14] Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. Inf. Control 68, 125–145 (1986)
  * [15] Gumm, H.P., Schröder, T.: Monoid-labeled transition systems. In: Coalgebraic Methods in Computer Science, CMCS 2001. ENTCS, vol. 44, pp. 185–204. Elsevier (2001)
  * [16] Kozen, D.: Results on the propositional $\mu$-calculus. Theor. Comput. Sci. 27, 333–354 (1983)
  * [17] Kozen, D.: Kleene algebra with tests. ACM Trans. Prog. Lang. Syst. 19, 427–443 (1997)
  * [18] Kurz, A., Leal, R.: Equational coalgebraic logic. In: Mathematical Foundations of Programming Semantics, MFPS 2009. ENTCS, vol. 249, pp. 333–356. Elsevier (2009)
  * [19] Leal, R.: Predicate liftings versus nabla modalities. In: Coalgebraic Methods in Computer Science, CMCS 2008. ENTCS, vol. 203, pp. 195–220. Elsevier (2008)
  * [20] Marti, J., Venema, Y.: Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci. 81(5), 880–900 (2015)
  * [21] Milius, S.: A sound and complete calculus for finite stream circuits. In: Proc. 25th Annual Symposium on Logic in Computer Science (LICS 2010). pp. 449–458. IEEE Computer Society (2010)
  * [22] Milius, S., Pattinson, D., Schröder, L.: Generic trace semantics and graded monads. In: Coalgebraic and Algebraic Methods in Computer Science, CALCO 2015\. LIPIcs, vol. 35, pp. 253–269 (2015)
  * [23] Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)
  * [24] Moss, L.: Coalgebraic logic. Ann. Pure Appl. Log. 96, 277–317 (1999)
  * [25] Myers, R.: Rational Coalgebraic Machines in Varieties: Languages, Completeness and Automatic Proofs. Ph.D. thesis, Imperial College London (2013)
  * [26] Parikh, R.: Propositional game logic. In: Foundations of Computer Science, FOCS 1983\. IEEE (1983)
  * [27] Pattinson, D.: Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theor. Comput. Sci. 309, 177–193 (2003)
  * [28] Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log. 45, 19–33 (2004)
  * [29] Peleg, D.: Concurrent dynamic logic. J. ACM 34, 450–479 (1987)
  * [30] Schröder, L.: Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci. 390, 230–247 (2008)
  * [31] Schröder, L., Venema, Y.: Completeness of flat coalgebraic fixpoint logics. ACM Trans. Comput. Log. 19, 4:1–4:34 (2018)
  * [32] Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Quantitative Kleene coalgebras. Inf. Comput. 209, 822–849 (2011)
  * [33] Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing determinization from automata to coalgebras. Log. Meth. Comput. Sci. 9(1:9) (2013)
  * [34] Silva, A., Bonsangue, M., Rutten, J.: Non-deterministic Kleene coalgebras. Log. Meth. Comput. Sci. 6(3) (2010)
  * [35] Steffen, B., Ingólfsdóttir, A.: Characteristic formulae for processes with divergence. Inf. Comput. 110, 149–163 (1994)
  * [36] Strassen, V.: The existence of probability measures with given marginals. Ann Math. Stat. 36, 423–439 (1965)
  * [37] Trnková, V.: General theory of relational automata. Fund. Inform. 3, 189–234 (1980)
  * [38] Venema, Y.: Automata and fixed point logic: A coalgebraic perspective. Inf. Comput. 204, 637–678 (2006)
  * [39] Weinert, H.J.: On $0$-simple semirings, semigroup semirings, and two kinds of division semirings. Semigroup Forum 28, 313–333 (1984)