11institutetext: University of Strathclyde 22institutetext: Radboud
Universiteit Nijmegen

# A Categorical Approach to
Coalgebraic Fixpoint Logic††thanks: This research is partially supported by
the Leverhulme Trust Research Project Grant RPG-2020-232 and NWO grant No.
OCENW.M20.053.

Ezra Schoen 11 Clemens Kupke 11 Jurriaan Rot 22 Ruben Turkenburg 22

###### Abstract

We define a framework for incorporating alternation-free fixpoint logics into
the dual-adjunction setup for coalgebraic modal logics. We achieve this by
using order-enriched categories. We give a least-solution semantics as well as
an initial algebra semantics, and prove they are equivalent. We also show how
to place the alternation-free coalgebraic $\mu$-calculus in this framework, as
well as PDL and a logic with a probabilistic dynamic modality.

##  1 Introduction

Coalgebra provides a versatile framework for representing different types of
state-based dynamic systems in a uniform way [26]. At the heart of the
coalgebraic theory lie the semantic notions of behaviour and behavioural
equivalence. It is well-known that modal logics provide the appropriate
syntactic tools to specify and reason about labelled transition systems in a
fully abstract way, i.e., in a way that ensures that the language precisely
characterises behavioural equivalence [14]. This is the basis for research
into coalgebraic modal logics, i.e., modal logics that are developed
parametric in the type of the coalgebra that the logic is supposed to be
interpreted on. Many different modal logics, such as monotone modal logic,
graded modal logic and various probabilistic modal logics, have been shown to
be instances of coalgebraic modal logics [27, 5, 20]. By placing those logics
in a common framework, one is able to provide generic proofs of expressivity,
soundness and completeness of the logics that can then be instantiated to each
of the logics, thus avoiding the need for proving those results for each logic
individually. Mathematically, the close connection between coalgebras and
their corresponding coalgebraic modal logics has been represented in the
elegant framework of a dual adjunction that links $B$-coalgebras over a
category $\mathcal{C}$ to $L$-algebras over a category $\mathcal{D}$ [19, 16,
23]. This category $\mathcal{D}$ should be thought of as the category of
algebras for the propositional logic of predicates, whereas $L$ encodes the
modal operators of the logic. The “one-step” semantics of the modal operators
is then provided by a certain type of natural transformation connecting $L$
and $B$ across the adjunction.

The biggest stumbling block for studying coalgebraic modal logics abstractly
is probably the inherent “one-stepness” of the theory: the transition
structure typically only allows to look one step ahead in the model.
Consequently, modal operators are usually one-step and axioms of the logics
are assumed to be non-iterative [9] i.e., not allowing nesting of modal
operators (exceptions such as [7] confirm the rule). Fixpoint operators pose a
problem in this context as they specify properties that can look arbitrarily
deep into the model. There are several existing approaches to adding fixpoint
operators to coalgebraic modal logics [29, 4, 28] and even a coalgebraic
model-checking tool for those logics [12]. However, none of the existing
approaches to fixpoint logics provide a categorical treatment of the fixpoints
within the above outlined dual adjunction framework. This means that existing
coalgebraic fixpoint logics are developed on the category of sets and that
results such as invariance under behavioural equivalence cannot be proven in
an abstract, diagrammatic way.

The main contribution of this paper is to extend the dual adjunction framework
to incorporate alternation-free fixpoint logics. We will first introduce the
key concept of an unfolding system that contains as ingredients a one-step
logic, a functor corresponding to the fixpoint operators and a natural
transformation that we call unfolding and that is used to represent the
unfolding of fixpoints. In order to ensure existence of fixpoints we will
assume that both the category $\mathcal{D}$ and the functors on $\mathcal{D}$
corresponding to the logic are $\mathbf{Poset}$-enriched. We will define the
semantics of a given unfolding system as the least solution of an unfolding
operation. After we present the abstract framework for fixpoint logics in
Section 3 we will demonstrate how to place several examples in the framework:
a positive modal logic with a transitive closure modality, a probabilistic
version of a similar logic whose fixpoint operator resembles iteration in PPDL
[17, 10] and finally the positive fragment of PDL [25] without tests. We will
then prove key technical results: a diagrammatic proof of “adequacy” of the
given fixpoint logic and, in Section 4, the fact that the semantics can
equivalently be obtained as more standard initial algebra semantics.

In the final part of the paper, consisting of Section 5 and Section 6, we show
how to place the alternation-free fragment of the coalgebraic $\mu$-calculus
(in the sense of [4]) into our framework. This is done in two stages: first,
in Section 5, we translate the positive fragment of the coalgebraic
$\mu$-calculus into a syntax that allows us to place the logic into our
framework by representing the logic and its semantics as an unfolding system.
In Section 6 we then provide a general recipe for adding negations to a
fixpoint logic represented in our framework. The latter will in particular
show that the full alternation-free fragment of the coalgebraic $\mu$-calculus
can be represented using a suitable functor $L$ and the associated initial
$L$-algebra semantics. Finally, in Section 7, we conclude with some ideas for
ongoing and future work.

##  2 Preliminaries

We will assume familiarity with basic category theory, coalgebra and modal
logic.

####  2.0.1 Notation

Throughout the paper we will use $\mathscr{P}$ to denote the covariant
powerset functor. The functor $P$ denotes the left adjoint of the dual
adjunction we will be working with. In many concrete instances of this
adjunction, $P$ will thus denote the contravariant power set functor.

####  2.0.2 Fixpoints

We will heavily rely on Kleene’s fixpoint theorem and its generalisation by
Cousot & Cousot [6] that states that the least fixpoint of a monotone function
$f:L\to L$ on a complete lattice $L$ exists and can be obtained as the limit
of the sequence $f^{0}=\perp$, $f^{i+1}=f(f^{i})$ for an arbitrary ordinal $i$
and $f^{j}=\bigvee_{i<j}f^{i}$ for limit ordinals $j$. We will not make
explicit use of the dual statement concerning greatest fixpoints.

###  2.1 One-step Logics

We model coalgebraic modal logics via the dual adjunction approach, cf. e.g.
[16]. Throughout the paper we will assume to work in a setting where we are
given:

  * •

A category $\mathcal{C}$ of _spaces_ , which are the carriers for coalgebras;

  * •

A category $\mathcal{D}$ of _algebras_ for some underlying ‘propositional’
logic;

  * •

A dual adjunction $P:\mathcal{C}\to\mathcal{D}^{\text{op}}$ and
$Q:\mathcal{D}^{\text{op}}\to\mathcal{C}$ with $P\dashv Q$, i.e., for all
$X\in\mathcal{C}$, $A\in\mathcal{D}$ we have
$\operatorname{Hom}_{\mathcal{C}}(X,QA)\cong\operatorname{Hom}_{\mathcal{D}}(A,PX)$
and this isomorphism is natural in both $X$ and $A$;

  * •

and an endofunctor $B:\mathcal{C}\to\mathcal{C}$ specifying the coalgebra
type.

The adjunctions $P\dashv Q$ we consider are _logical connections_ , as in
[21]. That is to say, $P$ and $Q$ are both of the form
$\operatorname{Hom}(-,\Omega)$, where $\Omega$ is a so-called ‘ambimorphic’
object, living in both $\mathcal{C}$ and $\mathcal{D}$.

###### Definition 1

Given a functor $B:\mathcal{C}\to\mathcal{C}$, a pair $(L_{0},\delta)$
consisting of a functor $L_{0}:\mathcal{D}\to\mathcal{D}$ and a natural
transformation $\delta:L_{0}P\to PB$ is called a one-step logic for $B$.

The natural transformation captures the “one-step semantics” of the logic.
Crucially, while we will be able to place fixpoint logics into the dual
adjunction framework, we will see that those logics cannot be described as
one-step logics. This reflects the fact that fixpoint logics are inherently
multi-step, as fixpoint operators can be used to inspect the model arbitrarily
deep.

####  2.1.1 Examples of One-Step Logics

###### Example 1

We take $\mathcal{C}$ to be the category $\mathbf{Sets}$, and $\mathcal{D}$ to
be the category $\mathbf{DL}$ of distributive lattices. One half of the
adjunction is formed by the powerset functor
$P:\mathbf{Sets}\to\mathbf{DL}^{\text{op}}$, which can be seen as
exponentiation $2^{-}$. Similarly, for
$Q:\mathbf{DL}^{\text{op}}\to\mathbf{Sets}$ we use
$\operatorname{Hom}_{\mathbf{DL}}(-,2)$. It is well known that $P\dashv Q$,
forming the logical connection using $2$ as the ambimorphic object.

For our behavior functor, we fix a set $\operatorname{Prop}$ of propositional
letters, and define $B:\mathbf{Sets}\to\mathbf{Sets}$ as
$BX=\mathscr{P}\operatorname{Prop}\times\mathscr{P}X$. For our one-step logic,
we let $L_{0}:\mathbf{DL}\to\mathbf{DL}$ be given by
$L_{0}\mathbb{A}=\operatorname{Free}\left(\\{\Diamond a\mid a\in
A\\}\cup\\{p\mid p\in\operatorname{Prop}\\}\right)/{\approx}$ where
$\operatorname{Free}$ generates the free distributive lattice on a set of
generators, and $\approx$ is the least congruence satisfying $\Diamond
a\approx(\Diamond a\wedge\Diamond b)$ whenever $a\leq b$.

We note for future reference that quotienting out $\approx$ exactly ensures
that $\Diamond a\leq\Diamond b$ whenever $a\leq b$. We obtain a one-step
semantics $\delta:L_{0}P\to PB$ via

$\delta:\begin{cases}p&\mapsto\\{\langle m,U\rangle\mid p\in m\\}\\\ \Diamond
v&\mapsto\\{\langle m,U\rangle\mid v\cap u\neq\varnothing\\}\end{cases}$

and extending freely. This yields the expected semantics of (positive) modal
logic as follows: consider a $B$-coalgebra $(X,\gamma)$, let $(\Psi,\alpha)$
be the initial $L_{0}$-algebra (to be thought of as algebra of formulas) and
consider the $L_{0}$-algebra $P\gamma\circ\delta:L_{0}PX\to PX$. The initial
algebra map $\llbracket-\rrbracket$ will satisfy the following

$\displaystyle\llbracket\alpha(\Diamond a)\rrbracket$ $\displaystyle=$
$\displaystyle P\gamma(\delta_{X}(L\llbracket-\rrbracket(\Diamond a)))=\\{x\in
X\mid\gamma(x)\in\delta_{X}(\Diamond\llbracket a\rrbracket)\\}$
$\displaystyle=$ $\displaystyle\\{x\in X\mid\gamma(x)\in\\{\langle
m,U\rangle\in BX\mid U\cap\llbracket a\rrbracket\not=\emptyset\\}\\}$

which expresses precisely that $\Diamond a$ will be true at those states that
have at least one successor “satisfying” $a$.

###### Example 2

For $\mathcal{C}$ we again take the category of sets. For $\mathcal{D}$, we
take distributive lattices that come equipped with subconvex combinations. By
this, we mean that if $\lambda_{1},\dots,\lambda_{n}\in[0,1]$ with
$\sum_{i}\lambda_{i}<1$, then for each $a_{1},\dots,a_{n}\in\mathbb{A}$, we
obtain an element

$\sum_{i}\lambda_{i}a_{i}=a\in\mathbb{A}$

Moreover, we demand that

$1\cdot
a=a,\quad\sum_{i}\lambda_{i}(\sum_{j}\mu_{i,j}a_{i,j})=\sum_{i,j}(\lambda_{i}\cdot\mu_{i,j})a_{i,j}$

and

$\lambda a+\mu(b\vee c)=(\lambda a+\mu b)\vee(\lambda a+\mu b)$

and similar for $\wedge$. Let $\mathbf{SCL}$ be the category with objects
subconvex lattices, and morphisms the maps preserving both subconvex and
lattice structure.

A key example of a subconvex lattice is given by $[0,1]$, with $\max$ and
$\min$ as lattice operations, and subconvex structure given in the obvious
way. Note also that if $\mathbb{A}$ is a subconvex lattice, then so is
$\mathbb{A}^{X}$ with pointwise structure; hence, we obtain our main examples
as $[0,1]^{X}$, with $X$ any set.

Note also that if $f:X\to Y$ is any function, then
$f^{*}:[0,1]^{Y}\to[0,1]^{X}$ is a subconvex lattice homomorphism. Hence, we
obtain a functor $P:\mathbf{Sets}\to\mathbf{SCL}^{\text{op}}$ given by
$X\mapsto[0,1]^{X}$. Vice versa, we clearly have a morphism
$Q:\mathbf{SCL}^{\text{op}}\to\mathbf{Sets}$ given by
$\mathbb{A}\mapsto\operatorname{Hom}_{\mathbf{SCL}}(\mathbb{A},[0,1])$. It is
easy to see that there is an adjunction $P\dashv Q$, since they are both of
the form $\operatorname{Hom}(-,[0,1])$. Finally, for our fixpoint extensions
later on, note that $\mathbf{SCL}$ is enriched in posets in the obvious way,
and that $PX$ is a complete lattice for all $X$.

For a set $X$, let $\Delta(X)$ be the set of finitely supported
subdistributions on $X$:

$\Delta(X)\mathrel{:=}\\{\mu:X\to[0,1]\mid\mu(x)=0\text{ all but finitely many
}x,\sum_{x\in X}\mu(x)\leq 1\\}.$

$\Delta$ is an endofunctor on $\mathbf{Sets}$, where $\Delta f$ maps a
distribution $\mu$ on $X$ to $\mu_{f}$ with $\mu_{f}(y)=\sum_{f(x)=y}\mu(x).$
Now fix a set $A$ of labels, and let $B$ be the functor
$BX=[0,1]^{A}\times\Delta(X)$. We can think of a $B$-coalgebra as a
probabilistic 1-player game, where in a given state, the player may select a
label $A$ to obtain a ‘payout’, or probabilistically transition to a next
state; but if the player takes the probabilistic transition, there is a
possibility of failure, since the probabilities need not add up to 1.

In this context, we may posit the following one-step logic
$L_{0}:\mathbf{SCL}\to\mathbf{SCL}$: for a given subconvex lattice
$\mathbb{A}$, we let $L_{0}\mathbb{A}$ be the free subconvex lattice generated
by $\\{\Diamond a\mid a\in\mathbb{A}\\}\cup\\{p\mid p\in A\\}$, quotiented by
the equations

$\displaystyle\sum_{i}\lambda_{i}\Diamond a_{i}$
$\displaystyle\approx\Diamond(\sum_{i}\lambda_{i}a_{i})$
$\displaystyle\Diamond a\wedge\Diamond b$ $\displaystyle\approx\Diamond a$
$\displaystyle\text{ whenever }a\wedge b=a$

Intuitively, $\Diamond a$ should be read as ‘the expected value of $a$’; this
is why we demand that $\Diamond$ acts linearly and preserves the order, but
does _not_ necessarily preserve lattice structure (as $\mathbb{E}[\max(X,Y)]$
is usually strictly greater than both $\mathbb{E}X$ and $\mathbb{E}Y$). Using
the intuition of ‘expectation’, we obtain a one-step semantics
$\delta:L_{0}P\to PB$ by

$\displaystyle\delta(\Diamond u)$
$\displaystyle:\langle\pi,\mu\rangle\mapsto\sum_{x\in
X}\mu(x)u(x)=:\mathbb{E}_{\mu}(u)$ $\displaystyle\delta(p)$
$\displaystyle:\langle\pi,\mu\rangle\mapsto\pi(p)$

and extending freely; it is easy to verify that $\delta$ respects the
equations for $L_{0}$, so this indeed is a well-defined subconvex lattice
morphism $L_{0}P\to PB$. Naturality is also easy to verify.

###  2.2 Enriched Categories

We review the concepts from enriched categories that we use in this paper.
Since we only consider categories enriched in $\mathbf{Poset}$, some things
simplify. In particular, for our purposes we do not need the general case of
weighted (co)limits, which allows us to stick close to unenriched category
theory. For a more in-depth treatment of enriched categories see [15].

###### Definition 2

A _$\mathbf{Poset}$ -enriched category_ $\mathcal{C}$ is a category
$\mathcal{C}$, together with a partial order ${\leq}={\leq_{A,B}}$ on each
homset $\operatorname{Hom}_{\mathcal{C}}(A,B)$, such that

$-\circ-:\operatorname{Hom}_{\mathcal{C}}(B,C)\times\operatorname{Hom}_{\mathcal{C}}(A,B)\to\operatorname{Hom}_{\mathcal{C}}(A,C)$

is an order-preserving map for all $A,B,C$.

A key example of a $\mathbf{Poset}$-enriched category is $\mathbf{Poset}$
itself: one can order morphisms ‘pointwise’, that is, $f\leq_{A,B}g\text{ iff
}f(x)\leq_{B}g(x)\text{ for all }x\in A$. In fact, all examples of
$\mathbf{Poset}$-enriched categories in this paper are ordered pointwise in a
similar way. That is, we consider categories $\mathcal{D}$ where objects are
ordered structures, and the morphisms respect the orders; we then enrich
$\mathcal{D}$ in $\mathbf{Poset}$ by ordering the morphisms pointwise. There
is also a notion of enriched functor.

###### Definition 3

Let $\mathcal{C},\mathcal{D}$ be $\mathbf{Poset}$-enriched categories. A
_$\mathbf{Poset}$ -enriched functor_ is a functor
$F:\mathcal{C}\to\mathcal{D}$ such that for all parallel arrows $f,g:A\to B$
in $\mathcal{C}$, we have $f\leq g\implies Ff\leq Fg$.

Finally, we have a notion of enriched coproduct:

###### Definition 4

Let $\mathcal{C}$ be a $\mathbf{Poset}$-enriched category, and let $A,B$ be
objects in $\mathcal{C}$. We get a functor $F:\mathcal{C}\to\mathbf{Poset}$
given by
$FX=\operatorname{Hom}_{\mathcal{C}}(A,X)\times\operatorname{Hom}_{\mathcal{C}}(B,X)$.
We call an object $C$ of $\mathcal{C}$ an _enriched coproduct of $A$ and $B$_
if there is a natural isomorphism of functors
$F\cong\operatorname{Hom}_{\mathcal{C}}(C,-)$.

That is to say, an enriched coproduct of $A$ and $B$ is a coproduct $A+B$ such
that the (natural) isomorphism
$\operatorname{Hom}_{\mathcal{C}}(A,X)\times\operatorname{Hom}_{\mathcal{C}}(B,X)\cong\operatorname{Hom}_{\mathcal{C}}(A+B,X)$
is an isomorphism of _posets_ , not merely sets.

##  3 Semantics of Fixpoint Logics

###  3.1 Unfolding Systems

To define a fixpoint logic, we take a ‘two-tiered’ approach: one starts with a
‘base’ modal (one-step) logic, to which one adds fixpoint modalities. Hence we
will work in a setting where we are given a one-step logic as in Definition 1,
together with an enrichment that supports fixpoint operators.

####  3.1.1 Enriching the Dual Adjunction

To define the semantics of a fixpoint formula as a ‘least solution’, it is
necessary to be able to compare predicates (i.e., elements of objects in
$\mathcal{D}$). Since we intend a fully diagrammatic approach, we generalize
comparing elements to comparing _maps_ $X\to Y$ in $\mathcal{D}$. This is a
generalization indeed: if $\mathcal{D}$ is a concrete category where each
object is an ordered set, then maps can be ordered pointwise. To be able to
compare maps, we fix an enrichment of $\mathcal{D}$ in $\mathbf{Poset}$. We
need some additional assumptions:

###### Assumption 1

  1. (i)

We assume that $\operatorname{Hom}_{\mathcal{D}}(X,PY)$ is a complete lattice
for each $Y\in\mathcal{C}$, and that for each morphism $f:Y^{\prime}\to Y$,
the map
$Pf\circ-:\operatorname{Hom}_{\mathcal{D}}(X,PY)\to\operatorname{Hom}_{\mathcal{D}}(X,PY^{\prime})$
preserves the lattice structure and arbitrary directed joins.

  2. (ii)

Since $P$ is a left adjoint, it preserves colimits; however, we require the
stronger condition that $P$ maps coproducts to _enriched_ coproducts.

###### Remark 1

A natural candidate for $\mathcal{D}$ is the category $\mathbf{BA}$ of Boolean
algebras, as we have the powerset-ultrafilter adjunction $P\dashv\mathbf{uf}$
between $\mathbf{Sets}$ and $\mathbf{BA}^{\text{op}}$. Note, however, that if
we enrich $\mathbf{BA}$ by pointwise order on the morphisms, the morphisms end
up being ordered discretely. For, if $f\leq g$ in
$\operatorname{Hom}_{\mathbf{BA}}(\mathbb{A},\mathbb{B})$, then for each
$x\in\mathbb{A}$ we have $f(\neg x)\leq g(\neg x)$. Hence, $g(x)=\neg g(\neg
x)\leq\neg f(\neg x)=f(x)$, showing $g\leq f$ as well.

It may be possible to enrich $\mathbf{BA}$ via a different, non-pointwise
strategy; however, it can be shown that there is no enrichment of
$\mathbf{BA}$ that makes $\operatorname{Hom}(X,PY)$ a complete lattice for all
$X,Y$; hence, we will work with the category $\mathbf{DL}$ of distributive
lattices, rather than $\mathbf{BA}$. This could be seen as an analogue of the
constraint on fixpoint equations, that fixpoint variables only occur
_positively_. In section 6, we outline how negations can be added into the
picture outside of the fixpoint equations.

####  3.1.2 Logical Functors

In order to be able to enrich a given logic with fixpoints we will assume to
be given a one-step logic $(L_{0},\delta)$ for $B$ and posit a functor
$L:\mathcal{D}\to\mathcal{D}$ representing the fixpoint modalities. We assume
moreover that both $L_{0}$ and $L$ are $\mathbf{Poset}$-enriched functors, and
that $L$ has an initial algebra. Throughout the paper we will write $\Phi$ for
the initial $L$-algebra, with structure map $\alpha:L\Phi\to\Phi$ (note that
$\alpha$ is an isomorphism); it should be thought of as the ‘algebra of
formulas’.

###### Remark 2

Intuitively the assumption that the functor $L_{0}$ is enriched means that all
modal operators in the base logic are monotone.

We will now define a (alternation-free) fixpoint logic as an extension of a
basic one-step logic. A key element is the so-called unfolding operation for
the fixpoints.

###### Definition 5

Let $\mathcal{D}$ be a $\mathbf{Poset}$-enriched category. Let
$B:\mathcal{C}\to\mathcal{C}$ be a functor, and let
$L_{0}:\mathcal{D}\to\mathcal{D}$ be a $\mathbf{Poset}$-enriched functor. An
unfolding system for $L_{0}$ is a pair
$(\operatorname{\mathsf{u}}:L\to\operatorname{id}+L_{0}L,\delta:L_{0}P\to PB)$
where $L:\mathcal{D}\to\mathcal{D}$ is a $\mathbf{Poset}$-enriched functor
that has an initial algebra $\Phi$, $\operatorname{\mathsf{u}}$ is a natural
transformation and $(L_{0},\delta)$ is a one-step logic for $B$ in the sense
of Def. 1.

The natural transformation
$\operatorname{\mathsf{u}}:L\to\operatorname{id}+L_{0}L$ provides the key to
define the semantics of fixpoint modalities.

Intuitively, if we think of an element $\ell$ of $L\mathbb{A}$ as being a loop
of some type, we see that there are two ‘branches’ to unfolding $\ell$; we may
exit the loop, which yields an element of $\mathbb{A}$, or we may take a step
in the model (represented by a modality taken from $L_{0}$), after which we
continue with a loop.

In more detail, a generic element of $L\mathbb{A}$ may look like
$\ell(x_{1},\dots,x_{n})$, with $\ell$ some fixpoint modality, and
$\bar{x}=(x_{1},\dots,x_{n})\in\mathbb{A}^{n}$. We want $\ell$ to satisfy a
fixpoint equation

$\ell(\bar{x})=\sigma(\bar{x},g_{1}\cdot\ell_{1}(\bar{x}),\dots,g_{k}\cdot\ell_{k}(\bar{x}))$

Here $\sigma$ is some ‘propositional’ expression, and each $\ell_{j}$ occurs
_guarded_ by a one-step modality $g_{i}$. The transformation
$\operatorname{\mathsf{u}}$ replaces the LHS of each such expression with the
RHS; and the RHS lives in $\mathbb{A}+L_{0}L\mathbb{A}$.

###  3.2 Definition of the Semantics

We are now ready to define the semantic map $\llbracket-\rrbracket$.

###### Definition 6

Let $(\operatorname{\mathsf{u}},\delta)$ be an unfolding system for $B$ and
let $(X,\gamma)$ be a $B$-coalgebra. The semantic map
$\llbracket-\rrbracket_{\gamma}:\Phi\to PX$ on $(X,\gamma)$ is defined as the
least map $t:\Phi\to PX$ making the following diagram commute:

${\Phi}$${PX}$${L\Phi}$${PX+PBX}$${\Phi+L_{0}L\Phi}$${\Phi+L_{0}\Phi}$${PX+L_{0}PX}$$\scriptstyle{\alpha^{-1}}$$\scriptstyle{t}$$\scriptstyle{\operatorname{\mathsf{u}}}$$\scriptstyle{[PX,P\gamma]}$$\scriptstyle{\operatorname{id}+L_{0}\alpha}$$\scriptstyle{t+L_{0}t}$$\scriptstyle{\delta}$

When the $X$ is clear from the context we often will drop the subscript and
simply denote the semantic map by $\llbracket-\rrbracket$.

Intuitively, the left-hand side of the above diagram takes a formula, and
unfolds the top-level fixpoint modalities, to obtain a one-step
$L_{0}$-formula over $\Phi$. Using the semantic map, this can be interpreted
as a one-step $L_{0}$-formula over $PX$, which we can reduce to a predicate in
$PX$ using the one-step semantics $\delta$, and the coalgebra structure
$\gamma$.

In order to see that $\llbracket-\rrbracket$ is well-defined, we note that the
above formulation is equivalent to saying that $\llbracket-\rrbracket$ is the
least fixpoint of the operator

$\begin{array}[]{rcl}\Xi_{\gamma}:\operatorname{Hom}_{\mathcal{D}}(X,PX)&\to&\operatorname{Hom}_{\mathcal{D}}(X,PX)\\\
\\\
t&\mapsto&[PX,P\gamma]\circ\delta\circ(t+L_{0}t)\circ(\operatorname{id}+L_{0}\alpha)\circ\operatorname{\mathsf{u}}\circ\alpha^{-1}\end{array}$
(1)

That $\Xi_{\gamma}$ is a monotone operator can be seen as follows:

  1. 1.

as $\mathcal{D}$ is order-enriched, both pre- and post-composition of
morphisms are monotone, and

  2. 2.

the operation that maps $t$ to $t+L_{0}t$ is monotone.

The first fact is immediate from the definition of enriched categories. The
second fact follows from the operation $t\mapsto L_{0}t$ being monotone
($L_{0}$ is an enriched functor) and because the cotupling operation is
monotone as we have

$\operatorname{Hom}(X+Y,Z)\cong\operatorname{Hom}(X,Z)\times\operatorname{Hom}(Y,Z)$

by definition of the coproduct and because the above isomorphism is an
isomorphism of posets. As $\Xi$ is monotone and as
$\operatorname{Hom}_{\mathcal{D}}(X,PX)$ is a complete lattice by assumption,
the least fixpoint $\llbracket-\rrbracket$ of $\Xi$ exists.

###### Remark 3

While the definition of $\llbracket-\rrbracket$ is in terms of a least
fixpoint, the same setup can be used to define greatest fixpoints as well, by
inverting the order on the homsets. However, we are as yet restricted to only
a single _type_ of fixpoint.

###  3.3 Examples

###### Example 3

As a first example, we give a simple logic of transitive closure in Kripke
frames.

We start with the one-step logic as given in example 1. To obtain an unfolding
system, we take $L:\mathbf{DL}\to\mathbf{DL}$ similarly to $L_{0}$, but using
$\Diamond^{*}$ rather than $\Diamond$:

$L\mathbb{A}=\operatorname{Free}\left(\\{\Diamond^{*}a\mid a\in
A\\}\cup\\{p\mid p\in\operatorname{Prop}\\}\right)/{\approx}$

where $\approx$ is as in example 1. We get an unfolding transformation
$\operatorname{\mathsf{u}}:L\to\operatorname{id}+L_{0}L$ by

$\operatorname{\mathsf{u}}:\begin{cases}p&\mapsto\operatorname{inr}(p)\\\
\Diamond^{*}a&\mapsto\operatorname{inl}(a)\vee\operatorname{inr}(\Diamond\Diamond^{*}a)\end{cases}$

To spell out the concrete description of the above logic, we have formulas
defined via

$\phi,\psi::=p\in\operatorname{Prop}\mid\top\mid\bot\mid\phi\wedge\psi\mid\phi\vee\psi\mid\Diamond^{*}\phi$

For a given coalgebra seen as a Kripke model $\mathfrak{M}=(W,R,V)$, consider
the usual definition of satisfaction of formulas, given by

$\displaystyle x\Vdash p$ $\displaystyle\text{ iff }x\in V(p)$ $\displaystyle
x\Vdash\Diamond^{*}\phi$ $\displaystyle\text{ iff }\exists
v_{1},\dots,v_{n}\text{ such that }xRv_{1}R\dots Rv_{n}\text{ and
}v_{n}\Vdash\phi$

We claim that our approach yields the same semantics, in the sense that

$\llbracket\phi\rrbracket=\\{x\in W\mid x\Vdash\phi\\}$

To see this, first note that the map $t:\Phi\to PW$ given by
$\phi\mapsto\\{x\in W\mid x\Vdash\phi\\}$ is a solution to the diagram in
definition 6; hence, $\llbracket\phi\rrbracket\subseteq t(\phi)$, as
$\llbracket-\rrbracket$ is the least solution. For the other direction, let
$t^{(k)}$ be the map that interprets $\Diamond^{*}$ as ‘reachability _in at
most $k$ steps_’; by induction on $k$, one can show that each $t^{(k)}$ is
below all solutions to the diagram, and hence each
$t^{(k)}\leq\llbracket-\rrbracket$. Since $t$ is clearly the supremum of the
$t^{(k)}$, we also have $t(\phi)\subseteq\llbracket\phi\rrbracket$ for all
formulas $\phi$.

###### Example 4

The above example may be extended to cover Propositional Dynamic Logic (PDL).
We take the same base adjunction, but adjust $B$ and $L_{0}$ to include a set
of modalities. That is, for a set $\Pi$ of ‘atomic programs’, we let
$BX=\mathscr{P}\operatorname{Prop}\times(\mathscr{P}X)^{\Pi}$, and take
$L_{0}:\mathbf{DL}\to\mathbf{DL}$ to be

$L_{0}\mathbb{A}=\operatorname{Free}(\operatorname{Prop}\cup\\{\langle\pi\rangle
a\mid\pi\in\Pi,a\in\mathbb{A}\\})/{\approx}$

with obvious action on morphisms. Then just as before, we obtain a one-step
semantics as

$\delta:\begin{cases}p&\mapsto\\{\langle m,u\rangle\mid p\in m\\}\\\
\langle\pi\rangle v&\mapsto\\{\langle m,u\rangle\mid v\cap
u(\pi)\neq\varnothing\\}\end{cases}$

For PDL, we define (composite) programs via the following grammar:

$\alpha::=\pi\in\Pi\mid\epsilon\mid\alpha\cup\alpha\mid\alpha;\alpha\mid\alpha^{*}$

We write $\bar{\Pi}$ for the set of programs. There is a function
$g:\bar{\Pi}\to\bar{\Pi}$ such that $g(\alpha)$ is equivalent to $\alpha$, and
$g(\alpha)$ is of the form $\sum_{i}\pi_{i};\alpha_{i}$ or
$(\sum_{i}\pi_{i};\alpha_{i})\cup\epsilon$. Existence of $g$ can be proven as
the normal form in [3, Thm. 4.4] using the Brzozowski derivative.

We let $L:\mathbf{DL}\to\mathbf{DL}$ be given by

$L\mathbb{A}:=\operatorname{Free}(\operatorname{Prop}\cup\\{\langle\alpha\rangle
a\mid\alpha\in\bar{\Pi},a\in\mathbb{A}\\})/{\approx}$

with obvious action on morphisms. We define
$\operatorname{\mathsf{u}}:L\to\operatorname{id}+L_{0}L$ as

$\displaystyle\operatorname{\mathsf{u}}(p)$
$\displaystyle:=\operatorname{inr}(p)$
$\displaystyle\operatorname{\mathsf{u}}(\langle\alpha\rangle a)$
$\displaystyle:=\begin{cases}\operatorname{inr}\left(\bigvee_{i}\langle\pi_{i}\rangle\langle\alpha_{i}\rangle
a\right)&g(\alpha)=\sum_{i}\pi_{i};\alpha_{i}\\\
\operatorname{inr}\left(\bigvee_{i}\langle\pi_{i}\rangle\langle\alpha_{i}\rangle
a\right)\vee\operatorname{inl}(a)&g(\alpha)=(\sum_{i}\pi_{i};\alpha_{i})\cup\epsilon\end{cases}$

Concretely, we see that $g(\pi^{*})=\pi;\pi^{*}\cup\epsilon$, and hence
(omitting coproduct inclusions) we have

$\operatorname{\mathsf{u}}(\langle\pi^{*}\rangle
a)=\langle\pi\rangle\langle\pi^{*}\rangle a\vee a$

Just like $\Diamond^{*}$ above, it can be shown that
$\llbracket\langle\alpha\rangle\phi\rrbracket$ has the usual denotation.

###### Example 5

As a third example, we give a quantitative logic for one-player games.

In example 2, we gave a simple quantitative modal logic. We may define a
functor $L$ by setting

$L\mathbb{A}:=\operatorname{Free}(\\{\sigma_{q}a,\Diamond^{*}a\mid
a\in\mathbb{A},q\in[0,1]\\})$

(where $\operatorname{Free}$ denotes the ‘free subconvex lattice’-functor) and
unfolding the generators as

$\displaystyle\operatorname{\mathsf{u}}(\sigma_{q}a)$
$\displaystyle=qa+(1-q)\Diamond\sigma_{q}a$
$\displaystyle\operatorname{\mathsf{u}}(\Diamond^{*}a)$
$\displaystyle=a\vee\Diamond\Diamond^{*}a$

Under this unfolding, $\llbracket\sigma_{q}\phi\rrbracket$ will assign to a
state $x$ the expected outcome of a $q$-probabilistic strategy, where with
probability $q$, the player chooses the payout corresponding to $\phi$, and
with probability $(1-q)$ she decides to play on.

On the other hand $\llbracket\Diamond^{*}\phi\rrbracket$ assigns to a state
$x$ the expected outcome of the _optimal_ strategy, where the player chooses
to play on only if the outcome she can expect from playing on is greater than
the payout she can get now.

###  3.4 Invariance Under Behavioural Equivalence

A fundamental property of coalgebraic modal logic is that the semantics of the
logic is invariant under behavioural equivalence. This follows from invariance
under coalgebra morphisms which can be concisely expressed as in (2) below.
The proposition shows that invariance under behavioural equivalence also holds
in the presence of fixpoint operators.

###### Proposition 1

For all coalgebra morphisms $f:(X_{1},\gamma_{1})\to(X_{2},\gamma_{2})$ we
have

$Pf\circ\llbracket-\rrbracket_{\gamma_{2}}=\llbracket-\rrbracket_{\gamma_{1}}$
(2)

###### Proof

Recall the defintion of $\Xi$ from (1) on page 1. Using naturality of $\delta$
it is a matter of routine checking that

$\Xi_{\gamma_{1}}=\operatorname{Hom}(-,Pf)\circ\Xi_{\gamma_{2}}.$

As a consequence we have
$Pf\circ\llbracket-\rrbracket_{\gamma_{2}}\geq\llbracket-\rrbracket_{\gamma_{1}}$
because

$\Xi_{\gamma_{1}}(Pf\circ\llbracket-\rrbracket_{\gamma_{2}})=Pf\circ\Xi_{\gamma_{2}}(\llbracket-\rrbracket_{\gamma_{2}})=Pf\circ\llbracket-\rrbracket_{\gamma_{2}},$

i.e., $Pf\circ\llbracket-\rrbracket_{\gamma_{2}}$ is a fixpoint of
$\Xi_{\gamma_{1}}$ and $\llbracket-\rrbracket_{\gamma_{1}}$ is the least such
fixpoint.

We will now show by ordinal induction that for all $i\in\mathrm{ORD}$ we have

$\Xi_{\gamma_{1}}^{i}\geq\operatorname{Hom}(-,Pf)\circ\Xi_{\gamma_{2}}^{i}$

where $\Xi_{\gamma_{1}}^{i}$ and $\Xi_{\gamma_{2}}^{i}$ are the approximants
defined in Section 2.0.2.

Case

$i=j+1$. Then

$\displaystyle\Xi_{\gamma_{1}}^{i}$ $\displaystyle=$
$\displaystyle\Xi_{\gamma_{1}}(\Xi_{\gamma_{1}}^{j})\geq\Xi_{\gamma_{1}}(\operatorname{Hom}(-,Pf)\circ\Xi_{\gamma_{2}}^{j})$
$\displaystyle=$
$\displaystyle\operatorname{Hom}(-,Pf)\circ\Xi_{\gamma_{2}}(\Xi_{\gamma_{2}}^{j})=\operatorname{Hom}(-,Pf)\circ\Xi_{\gamma_{2}}^{i}$

Case

$i$ is a limit ordinal. then

$\displaystyle\Xi_{\gamma_{1}}^{i}$ $\displaystyle=$
$\displaystyle\bigvee_{j<i}\Xi_{\gamma_{1}}^{j}\geq\bigvee_{j<i}\operatorname{Hom}(-,Pf)\circ\Xi_{\gamma_{2}}^{j}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny Ass.\leavevmode\nobreak\
\ref{ass:P}}}}{{=}}$
$\displaystyle\operatorname{Hom}(-,Pf)\circ\bigvee_{j<i}\Xi_{\gamma_{2}}^{j}=\operatorname{Hom}(-,Pf)\circ\Xi_{\gamma_{2}}^{i}$

The claim follows now as $\mathcal{D}$ is locally small which implies the hom
sets $\operatorname{Hom}(\Phi,PX_{i})$ for $i=1,2$ are sets, and thus
$\llbracket-\rrbracket_{\gamma_{i}}=\Xi_{\gamma_{i}}^{i}$ for a suitably large
ordinal $i$.

###  3.5 Guarded Equations of Arbitrary Depth

The framework presented so far seems to place some restrictions on the shape
of the fixpoint equations; consider the following toy logic:

$\phi::=\top\mid\bot\mid\phi\vee\phi\mid\phi\wedge\phi\mid\Diamond^{2*}\phi$

with the intended interpretation of $\Diamond^{2*}$ in a transition system
$(X,\to)$ being the least solution to
$\llbracket\Diamond^{2*}\phi\rrbracket=\llbracket\phi\rrbracket\vee\\{x\in
X\mid\exists y,z:x\to y\to z\text{ and
}z\in\llbracket\Diamond^{2*}\phi\rrbracket\\}$ The natural guarding 1-step
logic is positive modal logic; but this would yield an unfolding
transformation $\operatorname{\mathsf{u}}:\Diamond^{2*}a\mapsto
a\vee\Diamond\Diamond\Diamond^{2*}a$ and the RHS is not of the form
$\mathbb{A}+L_{0}L\mathbb{A}$. A possible remedy would be to add an extra
operator $\Diamond^{2*+1}$ to the logic, which would allow the depth-one
transformation

$\displaystyle\Diamond^{2*}a\mapsto a\vee\Diamond\Diamond^{2*+1}a$
$\displaystyle\Diamond^{2*+1}a\mapsto\Diamond\Diamond^{2*}a$

but this requires an extension of the logic, and is somewhat ad-hoc.

A second issue is that in the current presentation, _all_ modalities are
treated as fixpoint modalities. But most fixpoint logics contain a mixture of
fixpoint and one-step modalities. In fact both fixpoint modalities of higher
depth and one-step modalities (which may be seen as ‘depth 0 fixpoint
modalities’) can be accomodated by our setup, in a uniform way.

###### Proposition 2

Assume that $L+L_{0}$ generates an algebraically free monad $T$. Let
$\operatorname{\mathsf{u}}:L\to\operatorname{id}+L_{0}T$ be a natural
transformation. Then we obtain a natural transformation
$\operatorname{\mathsf{u}}^{*}:T\to\operatorname{id}+L_{0}T$ such that
$\operatorname{\mathsf{u}}$ factors through $\operatorname{\mathsf{u}}^{*}$.

Note that the assumption is satisfied whenever $L$ and $L_{0}$ are given via a
finitary presentation, i.e. as a quotient of a free algebra on some finitary
operations. The above proposition allows us to apply our results even in the
less restrictive case where the codomain of $\operatorname{\mathsf{u}}$ is
expanded to allow formulas of arbitrary depth, and including both one-step and
fixpoint modalities. For instance, in the above toy logic, we get a
transformation $\operatorname{\mathsf{u}}:L\to\operatorname{id}+L_{0}L_{0}L$
sending $\Diamond^{2*}a$ to $a\vee\Diamond\Diamond\Diamond^{2*}a$, and clearly
$L_{0}L$ is a subfunctor of the algebraically-free monad $T$ on $L_{0}+L$.

###### Proof

We know that if $T$ is the algebraically free monad on $L_{0}+L$, then
$T\mathbb{A}$ is a free $L_{0}+L$-algebra on $\mathbb{A}$. Hence, to obtain
$\operatorname{\mathsf{u}}^{*}$, we need to exhibit
$\mathbb{A}+L_{0}T\mathbb{A}$ as an algebra

$k:\mathbb{A}+L_{0}(\mathbb{A}+L_{0}T\mathbb{A})+L(\mathbb{A}+L_{0}T\mathbb{A})\to\mathbb{A}+L_{0}T\mathbb{A}$

The first component can simply be included; on the second component, we have a
natural map
$\mathbb{A}+L_{0}T\mathbb{A}\overset{\operatorname{inl}}{\to}\mathbb{A}+L_{0}T\mathbb{A}+LT\mathbb{A}\to
T\mathbb{A}$ using the free $(L_{0}+L)$-algebra structure on $T\mathbb{A}$;
applying $L_{0}$ to this map yields a map
$L_{0}(\mathbb{A}+L_{0}T\mathbb{A})\to L_{0}T\mathbb{A}$; finally, for the
third component, we get

${L(\mathbb{A}+L_{0}T\mathbb{A})}$${\mathbb{A}+L_{0}T\mathbb{A}+L_{0}T(\mathbb{A}+L_{0}T\mathbb{A})}$${\mathbb{A}+L_{0}T\mathbb{A}+L_{0}TT\mathbb{A}}$${\mathbb{A}+L_{0}T\mathbb{A}+L_{0}T\mathbb{A}}$${\mathbb{A}+L_{0}T\mathbb{A}}$$\scriptstyle{\operatorname{\mathsf{u}}}$algebramonadcodiagonal

The resulting algebra map
$\operatorname{\mathsf{u}}^{*}:T\mathbb{A}\to\mathbb{A}+L_{0}T\mathbb{A}$ is
natural in $\mathbb{A}$ as it is induced by the composition of natural
transformations.

##  4 Initial Algebra Semantics

The definition of the semantic map above is somewhat different from the usual
definition in terms of initial algebra semantics. The reason for this is that
a coalgebra map $\gamma:X\to BX$ does not directly give rise to an $L$-algebra
structure on $PX$. With some additional work, we can exhibit the semantic map
in this way as well. This section is devoted to presenting an initial algebra
semantics, and proving it equivalent to the least-solution semantics.

Before we start, however, we will give our reasons for choosing the above
construction as fundamental. Firstly, the definition of
$\llbracket-\rrbracket$ as a ‘least solution’ corresponds more closely to
intuitions about the semantics of (least) fixpoint formulas. Secondly, it
yields a direct proof technique via the ordinal approximation sequence. The
proof of invariance under behavioral equivalence from section 3.4 would be
more involved if one were to work with the initial algebra semantics.

For the main result of this section, the proof of equivalence between initial
and least-solution semantics, we need the following very mild categorical
assumption.

###### Assumption 2

We assume that in $\mathcal{D}$ pre-composition with morphisms distributes
over arbitrary joins, i.e., for $g:\mathbb{A}\to\mathbb{A}^{\prime}$, an index
set $I$ and $f_{i}:\mathbb{A}^{\prime}\to\mathbb{A}^{\prime\prime}$ for all
$i\in I$ we have

$\bigvee_{i\in I}(f_{i}\circ g)=(\bigvee_{i\in I}f_{i})\circ g$

where the equality means that if the join on the right side of the equation
exists, the join on the left side also exists and in this case both morphisms
are equal.

It can be easily verified that Assumption 2 is always satisfied in case the
poset structure on
$\operatorname{Hom}_{\mathcal{D}}(\mathbb{A},\mathbb{A}^{\prime})$ is induced
pointwise, as is usually the case.

For the definition of the initial algebra semantics we first recall that any
$L$-algebra structure on an object $\mathbb{B}$ induces a morphism from the
initial $L$-algebra.

###### Definition 7

For an $L$-algebra $\beta:L\mathbb{B}\to\mathbb{B}$ we let $\ulcorner
m\urcorner:\Phi\to\mathbb{B}$ denote the unique $L$-algebra morphism from the
initial $L$-algebra $(\Phi,\alpha)$ to $(\mathbb{B},\beta)$.

We now define a suitable $L$-algebra structure on the algebra of predicates.

###### Definition 8

Let $\gamma:X\to BX$ be a coalgebra. We define $m_{\gamma}:LPX\to PX$ as the
least map $m$ making

${LPX}$${PX}$${PX+PBX}$${PX+L_{0}LPX}$${PX+L_{0}PX}$$\scriptstyle{m}$$\scriptstyle{\operatorname{\mathsf{u}}}$$\scriptstyle{[PX,P\gamma]}$$\scriptstyle{PX+L_{0}m}$$\scriptstyle{PX+\delta}$

commute. We define $\|-\|:\Phi\to PX$ as $\ulcorner m_{\gamma}\urcorner$,
i.e., as the unique $L$-algebra morphism; that is, the unique map making the
following diagram commute

${\Phi}$${PX}$${L\Phi}$${LPX}$$\scriptstyle{\|-\|}$$\scriptstyle{\alpha}$$\scriptstyle{L\|-\|}$$\scriptstyle{m_{\gamma}}$

Similarly as for the semantic map $\llbracket-\rrbracket$ it is easy to see
that $m_{\gamma}$ \- and thus $\|-\|$ \- is well-defined as $m_{\gamma}$ is
the least fixpoint of the monotone operator $\mathrm{m}$ given by
$\mathrm{m}(m)\mathrel{:=}[PX,P\gamma\circ\delta]\circ(PX+L_{0}m)\circ\operatorname{\mathsf{u}}$.
We wish to prove that $\|-\|=\llbracket-\rrbracket$. We first consider the
easier direction of the statement.

###### Lemma 1

We have $\|-\|\geq\llbracket-\rrbracket$.

######  Proof (Sketch)

The lemma can be proven by showing that $\|-\|$ makes the definition square of
$\llbracket-\rrbracket$ commute. As $\llbracket-\rrbracket$ is the least such
map, the claim follows.

In order to prove the other inequality, we first prove the following lemma.

###### Lemma 2

Let $\\{\mathrm{m}^{i}\\}_{i\in\mathrm{Ord}}$ denote the approximants of
$m_{\gamma}$ in $\operatorname{Hom}_{\mathcal{D}}(LPX,PX)$. We have that
$\ulcorner\mathrm{m}^{i}\urcorner\leq\llbracket-\rrbracket$ for all ordinals
$i\in\mathrm{Ord}$.

###### Proof

We first prove that for all ordinals $i$ we have

$\mathrm{m}^{i}\circ
L\llbracket-\rrbracket\circ\alpha^{-}\leq\llbracket-\rrbracket$ (3)

In other words, we show that $\llbracket-\rrbracket$ is a pre-fixpoint of the
following monotone operator on $\operatorname{Hom}_{\mathcal{D}}(\Phi,PX)$
given by$g\mapsto\mathrm{m}^{i}\circ Lg\circ\alpha^{-1}$. The claim of the
lemma follows that by the fact that $\ulcorner\mathrm{m}^{i}\urcorner$ is the
unique fixpoint of the above operator and thus also the smallest pre-fixpoint.
The proof of (3) is by ordinal induction on $i$. For $i=0$ the claim is
trivial. For the successor ordinal case we calculate:

$\displaystyle\llbracket-\rrbracket$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny Def.}}}{{=}}$
$\displaystyle[PX,P\gamma\circ\delta]\circ(\llbracket-\rrbracket+L_{0}L\llbracket-\rrbracket)\circ(\Phi+L_{0}\alpha)\circ\operatorname{\mathsf{u}}\circ\alpha^{-}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny(*)}}}{{\geq}}$
$\displaystyle[PX,P\gamma\circ\delta]\circ(PX+L_{0}\mathrm{m}^{i})\circ(\llbracket-\rrbracket+L_{0}L\llbracket-\rrbracket)\circ\operatorname{\mathsf{u}}\circ\alpha^{-}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny nat of
$\operatorname{\mathsf{u}}$}}}{{=}}$
$\displaystyle[PX,P\gamma\circ\delta]\circ(PX+L_{0}\mathrm{m}^{i})\circ\operatorname{\mathsf{u}}\circ
L\llbracket-\rrbracket\circ\alpha^{-}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny Def of
$\mathrm{m}^{i+1}$}}}{{=}}$ $\displaystyle\mathrm{m}^{i+1}\circ
L\llbracket-\rrbracket\circ\alpha^{-}$

Here (*) is a consequence of the I.H. and the fact that composition in
$\mathcal{D}$ is monotonic. For the limit case consider
$\mathrm{m}^{i}=\bigvee_{j<i}\mathrm{m}^{j}$. We have:

$\llbracket-\rrbracket\stackrel{{\scriptstyle\mbox{\tiny
I.H.}}}{{\geq}}\bigvee_{j<i}\left(\mathrm{m}^{j}\circ
L\llbracket-\rrbracket\circ\alpha^{-}\right)\stackrel{{\scriptstyle\mbox{\tiny
Ass.}}}{{\geq}}\left(\bigvee_{j<i}\mathrm{m}^{j}\right)\circ
L\llbracket-\rrbracket\circ\alpha^{-}$

where for the second inequality we made use of Assumption 2 that pre-
composition of morphisms in $\mathcal{D}$ distributes over joins.

We are now ready to prove the main result of this section.

###### Theorem 4.1

Let $(X,\gamma)$ be a $B$-coalgebra. and let
$(\operatorname{\mathsf{u}},\delta)$ be an unfolding system for $B$. The
semantic map $\llbracket-\rrbracket_{\gamma}:\Phi\to PX$ coincides with the
initial algebra map $\|-\|_{X}$ from $(\Phi,\alpha)$ to $(PX,m_{\gamma})$

###### Proof

By Lemma 1 we have $\llbracket-\rrbracket_{\gamma}\leq\|-\|_{X}$. For the
converse direction note that we have $m_{\gamma}=\mathrm{m}^{i}$ for some
$i\in\mathrm{Ord}$. Therefore we can apply Lemma 2 as follows:
$\|-\|_{PX}=\ulcorner
m_{\gamma}\urcorner=\ulcorner\mathrm{m}^{i}\urcorner\stackrel{{\scriptstyle\mbox{\tiny
Lem.\leavevmode\nobreak\
\ref{lem:sem2}}}}{{\leq}}\llbracket-\rrbracket_{\gamma}$

##  5 Correctness for Positive Alternation-Free Coalgebraic Fixpoint Logics

In this section, we show how our approach can express the alternation-free
fragment of the coalgebraic $\mu$-calculus as defined in [4]. More
specifically, we give a pair of logical functors $(L,L_{0})$ and an unfolding
system $(\operatorname{\mathsf{u}},\delta)$ such that the initial $L$-algebra
$\Phi$ contains ‘enough’ formulas of the $\mu$-calculus, and the induced
semantics $\llbracket-\rrbracket$ coincides with the ususal semantics for the
$\mu$-calculus.

Before we can give the unfolding system, we need to define a special syntax
for the $\mu$-calculus. The reason for this is that our setup is most suited
for logics with fixpoint _modalities_ ; however, in the $\mu$-calculus, there
is no syntactical distinction between formulas, and fixpoint modalities
applied to a formula.

In order to get the $\mu$-calculus into a more amenable form, we use a
presentation similar to the flat coalgebraic fixpoint logics from [28]. This
approach can also be compared to PDL, which similarly has a syntactic
distinction between _formulas_ and _programs_ , corresponding to our fixpoint
schemes.

Fix a countable set $V$ of ‘parametric variables’. Let $\Lambda$ be modal
similarity type, i.e. a countable set of modal operators of finite arity. Let
$x\notin V$ be a designated ‘fixpoint variable’. Then we define by mutual
induction the formulas $\phi$ and fixpoint schemes $\gamma$ as follows:

$\displaystyle\gamma$ $\displaystyle::=v\in V\mid
x\mid\phi\mid\gamma\vee\gamma\mid\gamma\wedge\gamma\mid\heartsuit(\bar{\gamma})\mid\sharp_{\gamma}(\bar{\gamma}/\bar{v})\mid\flat_{\gamma}(\bar{\gamma}/\bar{v})$
$\displaystyle\phi$
$\displaystyle::=\top\mid\bot\mid\phi\vee\phi\mid\phi\wedge\phi\mid\neg\phi\mid\heartsuit(\bar{\phi})\mid\sharp_{\gamma}({\bar{\phi}}/{\bar{v}})\mid\flat_{\gamma}(\bar{\phi}/\bar{v})$

where the notation $\bar{\gamma},\bar{\phi}$ indicates that operators might
have lists of fixpoint schemes/formulas as arguments. The intended reading of
$\sharp_{\gamma}$ and $\flat_{\gamma}$ is as taking the least and greatest
fixpoints respectively of the operator defined by $\gamma$. We also define the
set of _guarded_ fixpoint schemes via

$\gamma_{g}::=v\in
V\mid\gamma_{g}\vee\gamma_{g}\mid\gamma_{g}\wedge\gamma_{g}\mid\heartsuit(\bar{\gamma})$

That is, a guarded fixpoint scheme is a propositional combination of
parametric variables and one-step modalities applied to (non-guarded) fixpoint
schemes.

Note that negations may only occur in formulas, not fixpoint schemes; hence,
the fixpoint variable $x$ only ever occurs positively. Note also that on
formulas, the ‘greatest fixpoint operator’ $\flat_{\gamma}$ may be defined in
terms of $\sharp_{\gamma}$ via
$\flat_{\gamma}(\bar{\phi}/\bar{v}):=\neg\sharp_{\gamma}(\overline{\neg\phi}/{\bar{v}})$.
We write CFL for the above coalgebraic fixpoint logic and CFS for the set of
fixpoint schemes. We will also write CFS♯ for the set of fixpoint schemes not
containing $\flat$, CFL♯ for the set of formulas not containing $\flat$, and
CFL${}_{\sharp}^{+}$ for the set of formulas not containing $\flat$ or $\neg$.

###### Definition 9

Let $B$ be a $\mathbf{Sets}$-functor, and fix for every modality $\heartsuit$
of arity $n$ a monotone predicate lifting
$\llparenthesis\heartsuit\rrparenthesis:P^{n}\to PB$. Then for a $B$-coalgebra
$\sigma:X\mapsto BX$, we define by mutual recursion the semantics
$\llbracket\phi\rrbracket$ of a formula, and
$\llbracket\gamma\rrbracket_{p}^{\xi}$ of a fixpoint scheme, where $p:V\to PX$
is a valuation of the parametric variables, and $\xi\subseteq PX$ is the value
of the fixpoint variable

$\displaystyle\llbracket\phi\rrbracket_{p}^{\xi}:=\llbracket\phi\rrbracket$
$\displaystyle\llbracket v\rrbracket_{p}^{\xi}:=p(v)$
$\displaystyle\llbracket\top\rrbracket:=S$ $\displaystyle\llbracket
x\rrbracket_{p}^{\xi}:=\xi$
$\displaystyle\llbracket\bot\rrbracket:=\varnothing$
$\displaystyle\llbracket\gamma\vee\delta\rrbracket_{p}^{\xi}:=\llbracket\gamma\rrbracket_{p}^{\xi}\cup\llbracket\delta\rrbracket_{p}^{\xi}$
$\displaystyle\llbracket\phi\vee\psi\rrbracket:=\llbracket\phi\rrbracket\cup\llbracket\psi\rrbracket$
$\displaystyle\llbracket\gamma\wedge\delta\rrbracket_{p}^{\xi}:=\llbracket\gamma\rrbracket_{p}^{\xi}\cap\llbracket\delta\rrbracket_{p}^{\xi}$
$\displaystyle\llbracket\phi\wedge\psi\rrbracket:=\llbracket\phi\rrbracket\cap\llbracket\psi\rrbracket$
$\displaystyle\llbracket\heartsuit(\bar{\gamma})\rrbracket_{p}^{\xi}:=\sigma^{-1}\left(\llparenthesis\heartsuit\rrparenthesis(\llbracket\bar{\gamma}\rrbracket_{p}^{\xi})\right)$
$\displaystyle\llbracket\heartsuit(\bar{\phi})\rrbracket:=\sigma^{-1}\left(\llparenthesis\heartsuit\rrparenthesis(\llbracket\bar{\phi}\rrbracket)\right)$
$\displaystyle\llbracket\sharp_{\gamma}(\bar{\delta}/\bar{v})\rrbracket_{p}^{\xi}:=\mu\left(U\mapsto\llbracket\gamma\rrbracket_{\llbracket\bar{\delta}\rrbracket_{p}^{\xi}/\bar{v}}^{U}\right)$
$\displaystyle\llbracket\sharp_{\gamma}(\bar{\phi}/\bar{v})\rrbracket:=\mu\left(U\mapsto\llbracket\gamma\rrbracket_{\llbracket\bar{\phi}\rrbracket/\bar{v}}^{U}\right)$
$\displaystyle\llbracket\flat_{\gamma}(\bar{\delta}/\bar{v})\rrbracket_{p}^{\xi}:=\nu\left(U\mapsto\llbracket\gamma\rrbracket_{\llbracket\bar{\delta}\rrbracket_{p}^{\xi}/\bar{v}}^{U}\right)$
$\displaystyle\llbracket\flat_{\gamma}(\bar{\phi}/\bar{v})\rrbracket:=\nu\left(U\mapsto\llbracket\gamma\rrbracket_{\llbracket\bar{\phi}\rrbracket/\bar{v}}^{U}\right)$

We claim that CFL is equivalent to the coalgebraic $\mu$-calculus (CMC), and
CFL♯ is equivalent to the alternation-free fragment of the coalgebraic
$\mu$-calculus (AFCMC). We will illustrate by showing how to express two
$\mu$-calculus formulas in CFL.

###### Example 6

As a simple example, consider the PDL formula $\Diamond^{*}p$. In the
$\mu$-calculus, this formula may be expressed as $\phi:=\mu X.p\vee\Diamond
X$. We can express $\phi$ in CFL as follows: $\sharp_{\gamma}(p/v)$, where
$\gamma(v;x):=v\vee\Diamond x$. Note that this is not exactly the formula
generated by the translation; in fact we have

$trl(\phi)=\sharp_{\delta}(),\qquad\text{ where }\delta(x)=p\vee\Diamond x$

We have chosen $\sharp_{\gamma}(p/v)$ as our intuitive translation, since it
highlights how the fixpoint _modality_ $\Diamond^{*}$ may be expressed as the
modality $\sharp_{\gamma}$.

###### Example 7

As a second example, we look at the formula

$\phi=\mu X.p\wedge\mu Y.\left((q\wedge\Diamond Y)\vee(r\wedge\square
X)\right).$

This example exhibits intrinsic nesting of fixpoints. It is guarded as a
formula of the $\mu$-calculus; however, in CFL, guardedness also requires that
all fixpoint _quantifiers_ (other than the first) appear directly under a
modality. So, let $\psi$ be the formula bound by $Y$ \- i.e.,
$\psi=(q\wedge\Diamond Y)\vee(r\wedge\square X)$. Clearly, $\phi$ is
equivalent to

$\mu X.\big{(}p\wedge\left((q\wedge\Diamond(\mu Y.\psi))\vee(r\wedge\square
X)\right)\big{)}$

and in this formula, all but the outer quantifier appear guarded. Now
translation is a straightforward affair: consider

$\displaystyle\sharp_{\gamma}()$ where
$\displaystyle\gamma(x):=p\wedge\left((q\wedge\Diamond\sharp_{\delta}(x))\vee(r\wedge\square
x)\right)$ $\displaystyle\delta(v;x):=(q\wedge\Diamond x)\vee(r\wedge\square
v)$

Then $\binom{\sharp_{\gamma}()}{\sharp_{\delta}(\sharp_{\gamma}()/v)}$ is the
(mutual) least fixed point of

$\binom{X}{Y}\mapsto\binom{p\wedge((q\wedge\Diamond Y)\vee(r\wedge\square
X))}{(q\wedge\Diamond Y)\vee(r\wedge\square X)}$

which shows that $\sharp_{\gamma}()$ has the same interpretation as $\phi$.

Next, we show how CFL${}_{\sharp}^{+}$ fits into the dual-adjunction picture.
We take $\mathcal{C}$ to be the category $\mathbf{Sets}$, and $\mathcal{D}$ to
be the category $\mathbf{DL}$ of distributive lattices. $\mathbf{DL}$ is
enriched over $\mathbf{Poset}$ by the pointwise order. For the adjunction
$P\dashv Q$ we take the adjunction from Example 1 in Section 2.1.

Our behavior functor $B:\mathbf{Sets}\to\mathbf{Sets}$ was given, together
with a set of predicate liftings
$\\{\llparenthesis\heartsuit\rrparenthesis\mid\heartsuit\in\Lambda\\}$.
Similarly to the one-step logic from Example 1, we take $L_{0}$ to be given by

$L_{0}\mathbb{A}:=\operatorname{Free}(\\{\heartsuit(a_{1},\dots,a_{n})\mid
a_{i}\in A,\heartsuit\in\Lambda\text{ of arity }n\\})/{\approx}$

where $\approx$ is the least congruence such that if $a\leq b$, then
$\heartsuit a\leq\heartsuit b$. Now $\llparenthesis-\rrparenthesis$ can be
used to define a one-step semantics $\delta:L_{0}P\to PB$ (cf. [20, Ex.
3.11]). Next, we set

$\displaystyle L\mathbb{A}$ $\displaystyle:=$
$\displaystyle\operatorname{Free}(\\{\sharp_{\gamma}(\bar{a}/\bar{v})\mid\gamma\in\text{CFS}_{\sharp}^{\mu},\gamma\text{
guarded}\\})/{\approx}$

Note that $L_{0}+L$ generates an algebraically-free monad $T$, the monad of
_$L_{0}+L$ -terms_. Since each $\gamma$ is an $L_{0}+L$-term in free variables
$\bar{v}\cup x$, we obtain a natural transformation
$\operatorname{\mathsf{u}}:L\to T$ via
$\operatorname{\mathsf{u}}:\sharp_{\gamma}(\bar{a}/\bar{v})\mapsto\gamma(\bar{a}/\bar{v},\sharp_{\gamma}(\bar{a}/\bar{v})/x)$.
Since we stipulate that $\gamma$ is guarded, we know that
$\operatorname{\mathsf{u}}$ will in fact factor through
$\operatorname{id}+L_{0}T$. Hence, using proposition 2, we are able to define
the desired semantic maps $\llbracket-\rrbracket$.

###### Proposition 3

Let $\sigma:X\to BX$ be a $B$-coalgebra, and let
$\llbracket-\rrbracket:\Phi\to PX$ be the semantic map induced by the
unfolding system $(\delta,\operatorname{\mathsf{u}})$. Then
$\llbracket\phi\rrbracket$ is the subset of $X$ defined as in definition 9.

######  Proof (Sketch)

The argument for this is similar to the one given in example 3: let $t:\Phi\to
PX$ be the explicitly defined semantics. Then $t$ is clearly a solution to the
diagram from definition 6, and hence $t\geq\llbracket-\rrbracket$. For the
other direction, we can set up an approximation process for $t$, and prove by
induction that each approximant is contained in all solutions.

Now since we have shown how to faithfully translate the $\mu$-calculus into
CFL, this allows us to interpret the negation-free, $\nu$-free fragment of the
coalgebraic $\mu$-calculus. In section 6, we will sketch how to extend this to
the full alternation-free fragment of the coalgebraic $\mu$-calculus.

##  6 Negations

So far, we have only been working in the positive fragments of the modal
logics under consideration. However, many modal (fixpoint) logics come
equipped with operations that are not order preserving - think of negation
$\neg$ in Boolean algebras, or subtraction in quantitative algebras. We will
use the term ‘negation(s)’ as a stand-in for such operations generally. In
this section, we sketch how the semantics on a positive fragment may be
extended to the full logic with negations.

Let $\mathcal{D}^{\neg}$ be a category of ‘algebras-with-negations’, equipped
with a free-forgetful adjunction $F:\mathcal{D}\to\mathcal{D}^{\neg}$,
$U:\mathcal{D}^{\neg}\to\mathcal{D}$ with $F\dashv U$. This yields a
endofunctors $L_{0}^{\neg},L^{\neg}:\mathcal{D}^{\neg}\to\mathcal{D}^{\neg}$
given by $L^{\neg}=FLU,L_{0}^{\neg}=FL_{0}U$. We also assume that we have an
adjunction $P^{\neg}\dashv Q^{\neg}$ with
$P^{\neg}:\mathcal{C}\to(\mathcal{D}^{\neg})^{\text{op}}$, and moreover assume
that $UP^{\neg}=P$. Using this, the map $m$ from Section 4 has type
$m:LUP^{\neg}X\to UP^{\neg}X$. Hence, we can transpose it along $F\dashv U$ to
get

$m^{\neg}:FLUP^{\neg}=L^{\neg}P^{\neg}X\to P^{\neg}X$

So, if we write $\Phi^{\neg}$ for the initial $L^{\neg}$-algebra, we obtain an
initial algebra semantics for formulas with negations, which respects the
already defined semantics for negation-free formulas.

As an example, consider the logic CFL from Section 5. As written there, we can
only interpret CFL${}_{\sharp}^{+}$, corresponding to the fragment of CMC
without greatest fixpoints and negations. However, if we take
$\mathcal{D}^{\neg}$ to be $\mathbf{BA}$, the category of Boolean algebras, we
see that the adjunction $P_{\mathbf{DL}}\dashv Q$ factors as
$UP_{\mathbf{BA}}\dashv\mathbf{uf}F$, where $U:\mathbf{BA}\to\mathbf{DL}$ is
forgetful, $F:\mathbf{DL}\to\mathbf{BA}$ is free, $P_{\mathbf{DL}}$ and
$P_{\mathbf{BA}}$ are the powerset functors into $\mathbf{DL}$ and
$\mathbf{BA}$, respectively, and $P_{\mathbf{BA}}\dashv\mathbf{uf}$ is the
well-known powerset-ultrafilter adjunction.

By the above discussion, we also get an interpretation of $L^{\neg}$-formulas
in $P_{\mathbf{BA}}X$ for any coalgebra $\xi:X\to BX$. The concrete analogue
of this shift consists of adding in negations to the syntax of formulas (but
not fixpoint schemes)

$\displaystyle\gamma$ $\displaystyle::=v\in V\mid
x\mid\phi\mid\gamma\vee\gamma\mid\gamma\wedge\gamma\mid\heartsuit(\bar{\gamma})\mid\sharp_{\gamma}(\bar{\gamma}/\bar{v})$
$\displaystyle\phi$
$\displaystyle::=\top\mid\bot\mid\phi\vee\phi\mid\phi\wedge\phi\mid\heartsuit(\bar{\phi})\mid\sharp_{\gamma}({\bar{\phi}}/{\bar{v}})\mid\boldsymbol{\neg\phi}$

yielding CFL♯, which corresponds to the full alternation-free fragment of the
coalgebraic $\mu$-calculus.

The picture is similar to that in [1]. There, the authors define ‘positive
fragments’ of one-step logics (however restricted to the logical connection
between $\mathbf{Sets}$ and $\mathbf{BA}$). For our purposes, we would prefer
to start with a (positive) logic, and consider ‘negative extensions’. There is
also the interesting question of expanding the notion of a ‘positive
fragment’/ ‘negative extension’ beyond the pair $\mathbf{BA}/\mathbf{DL}$, to
more quantitative logics.

It is important to note that, while this section shows how to extend the
initial algebra semantics of the positive logic to a logic with negation, it
is not clear whether we can define the semantics for the logic with negation
directly, i.e., based on the unforlding system as in Definition 6.

##  7 Conclusion

We have provided a new categorical framework for studying coalgebraic fixpoint
logics based on the dual adjunction framework. The framework provides both a
least-solution and an initial algebra semantics. We exemplified the framework
using a number of different examples such as the positive modal logic of
transitive closure, its probabilistic variant, positive PDL and the positive
alternation-free fragment of the coalgebraic $\mu$-calculus. We also showed
how to add negations to these logics, but hasten to remark that in this case
we only have an initial algebra semantics. As a first simple example of how
the framework can be used we provided a generic proof of adequacy of our
fixpoint logics, i.e., the semantics of any logic that fits in the framework
is invariant under behavioural equivalence.

Our framework is based on adding recursion to coalgebraic modal logic where
the one-step semantics is given by a type of distributive law. In [24],
instead, it is shown how to add a form of recursion to _abstract GSOS
specifications_ —a different type of distributive laws that can be used to
study structural operational semantics at a high level of generality—using
“unfolding” natural transformations, similar to the current approach. An
interesting theoretical direction may be to try and unify these extensions; a
good starting point may be the steps-and-adjunctions framework studied in
[25].

The main contribution of this paper is the new categorical framework for
fixpoint logics. In the future we hope to exploit this in several ways:
Firstly, we will study proof systems [22] and reasoning procedures [13] for
alternation-free fixpoint logics and will lift soundness and completeness
proofs to our framework. Secondly, the alternation-free fragment of the modal
$\mu$-calculus has interesting model-theoretic properties [8] and we will
explore whether those can be recovered within our framework. Another important
question – suggested by two of the anonymous referees – is whether we can use
our framework to provide a completeness proof for the Segerberg axioms for PDL
[18] or their coalgebraic generalisation from [11]. These logics certainly do
fit into our framework, the key question to solve will be to formally connect
the induction axiom or the least fixpoint rule to the requirement that the
semantic map is defined as a least fixpoint. Finally, the standard dual
adjunction framework can be used to define certain filtrations [2]. We have
reasons to believe that our framework of unfolding systems can be used to show
that a (fixpoint) logic has filtrations. This opens an avenue for studying
filtrations and abstraction techniques for fixpoint logics in a categorical
way.

## Acknowledgments

The authors would like to thank the anonymous referees for instructive
comments and interesting questions for future work, as well as for suggesting
the formula in example 7.

## References

  * [1] Adriana Balan, Alexander Kurz, and Jirí Velebil.  Positive fragments of coalgebraic logics.  In CALCO, volume 8089 of Lecture Notes in Computer Science, pages 51–65. Springer, 2013.
  * [2] Simone Barlocco, Clemens Kupke, and Jurriaan Rot.  Coalgebra learning via duality.  In FoSSaCS, volume 11425 of Lecture Notes in Computer Science, pages 62–79. Springer, 2019.
  * [3] Janusz A. Brzozowski.  Derivatives of regular expressions.  J. ACM, 11(4):481–494, 1964.
  * [4] Corina Cîrstea, Clemens Kupke, and Dirk Pattinson.  EXPTIME tableaux for the coalgebraic mu-calculus.  Log. Methods Comput. Sci., 7(3), 2011.
  * [5] Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema.  Modal logics are coalgebraic.  In BCS Int. Acad. Conf, pages 128–140. British Computer Society, 2008.
  * [6] Patrick Cousot and Radhia Cousot.  Constructive versions of Tarski’s fixed point theorems.  Pacific Journal of Mathematics, 82(1):43 – 57, 1979.
  * [7] Fredrik Dahlqvist.  Coalgebraic completeness-via-canonicity - principles and applications.  In CMCS, volume 9608 of Lecture Notes in Computer Science, pages 174–194. Springer, 2016.
  * [8] Alessandro Facchini, Yde Venema, and Fabio Zanasi.  A characterization theorem for the alternation-free fragment of the modal $\mathrm{\mu}$-calculus.  In LICS, pages 478–487. IEEE Computer Society, 2013.
  * [9] Jonas Forster and Lutz Schröder.  Non-iterative modal logics are coalgebraic.  In AiML, pages 229–248. College Publications, 2020.
  * [10] Tao Gu, Alexandra Silva, and Fabio Zanasi.  Hennessy-Milner results for probabilistic PDL.  In MFPS, volume 352 of Electronic Notes in Theoretical Computer Science, pages 283–304. Elsevier, 2020.
  * [11] Helle Hvid Hansen and Clemens Kupke.  Weak completeness of coalgebraic dynamic logics.  In FICS, volume 191 of EPTCS, pages 90–104, 2015.
  * [12] Daniel Hausmann, Merlin Humml, Simon Prucker, Lutz Schröder, and Aaron Strahlberger.  Generic model checking for modal fixpoint logics in COOL-MC.  In VMCAI (1), volume 14499 of Lecture Notes in Computer Science, pages 171–185. Springer, 2024.
  * [13] Daniel Hausmann, Lutz Schröder, and Christoph Egger.  Global caching for the alternation-free $\mu$-calculus.  In CONCUR, volume 59 of LIPIcs, pages 34:1–34:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [14] Matthew Hennessy and Robin Milner.  On observing nondeterminism and concurrency.  In ICALP, volume 85 of Lecture Notes in Computer Science, pages 299–309. Springer, 1980.
  * [15] Max Kelly.  The basic concepts of enriched category theory.  Reprints in Theory and Applications of Categories [electronic only], 2005, 01 2005.
  * [16] Bartek Klin.  Coalgebraic modal logic beyond sets.  In MFPS, volume 173 of Electronic Notes in Theoretical Computer Science, pages 177–201. Elsevier, 2007.
  * [17] Dexter Kozen.  A probabilistic PDL.  J. Comput. Syst. Sci., 30(2):162–178, 1985.
  * [18] Dexter Kozen and Rohit Parikh.  An elementary proof of the completness of PDL.  Theor. Comput. Sci., 14:113–118, 1981.
  * [19] Clemens Kupke, Alexander Kurz, and Dirk Pattinson.  Algebraic semantics for coalgebraic logics.  In CMCS, volume 106 of Electronic Notes in Theoretical Computer Science, pages 219–241. Elsevier, 2004.
  * [20] Clemens Kupke and Dirk Pattinson.  Coalgebraic semantics of modal logics: An overview.  Theor. Comput. Sci., 412(38):5070–5094, 2011.
  * [21] Alexander Kurz and Jirí Velebil.  Enriched logical connections.  Appl. Categorical Struct., 21(4):349–377, 2013.
  * [22] Johannes Marti and Yde Venema.  A focus system for the alternation-free $\mu$-calculus.  In TABLEAUX, volume 12842 of Lecture Notes in Computer Science, pages 371–388. Springer, 2021.
  * [23] Dusko Pavlovic, Michael W. Mislove, and James Worrell.  Testing semantics: Connecting processes and process logics.  In AMAST, volume 4019 of Lecture Notes in Computer Science, pages 308–322. Springer, 2006.
  * [24] Jurriaan Rot and Marcello M. Bonsangue.  Structural congruence for bialgebraic semantics.  J. Log. Algebraic Methods Program., 85(6):1268–1291, 2016.
  * [25] Jurriaan Rot, Bart Jacobs, and Paul Blain Levy.  Steps and traces.  J. Log. Comput., 31(6):1482–1525, 2021.
  * [26] Jan J. M. M. Rutten.  Universal coalgebra: a theory of systems.  Theor. Comput. Sci., 249(1):3–80, 2000.
  * [27] Lutz Schröder and Dirk Pattinson.  PSPACE bounds for rank-1 modal logics.  ACM Trans. Comput. Log., 10(2):13:1–13:33, 2009.
  * [28] Lutz Schröder and Yde Venema.  Flat coalgebraic fixed point logics.  In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 524–538. Springer, 2010.
  * [29] Yde Venema.  Automata and fixed point logic: A coalgebraic perspective.  Inf. Comput., 204(4):637–678, 2006.