日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集

Codensity Games for Bisimilarity
Yuichi Komorida
Bartek Klin

Shin-ya Katsumata

Nick Hu

Ichiro Hasuo

Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent riseof interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended invarious ways: notably, bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extensionof bisimilarity games to quantitative settings has been actively pursued too.
In this paper, we present a general framework that uniformly describes game characterizations ofbisimilarity-like notions. Our framework is formalized categorically using ﬁbrations and coalgebras. In
particular, our characterization of bisimilarity in terms of ﬁbrational predicate transformers allows us toderive codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric) as well as new ones (including
what we call bisimulation topology).

1 Introduction
1. 1 Bisimilarity Notions and Games
Since the seminal works by Park and Milner [25,26], bisimilarity has played a central role in theoretical computer science. It is an equivalence notion
between branching systems; it abstracts away internal states and stresses the black-box observationoriented view on process semantics. Bisimilarity is
usually deﬁned as the largest bisimulation, which isa binary relation that satisﬁes a suitable mimicking
condition. In fact, a bisimulation R can be characterized as a post-ﬁxed point R ⊆ Φ(R) using asuitable relation transformer Φ; from this we obtainthat bisimilarity is the greatest ﬁxed point of Φ by
the Knaster–Tarski theorem. This order-theoretic
foundation is the basis of a variety of advanced∗

This is a short version of the conference paper [21].
The extended version is in arXiv [22].
小 森 田 祐 一, 勝 股 審 也 , 蓮 尾 一 郎 , 国 立 情 報 学 研 究 所,
National Institute of Informatics.
小森田祐一, 蓮尾一郎, 総合研究大学院大学, The Graduate
University for Advanced Studies(SOKENDAI).
Nick Hu, オックスフォード大学, University of Oxford.
Bartek Klin, ワルシャワ大学, University of Warsaw.

techniques for reasoning about (or using) bisimilarity, such as bisimulation up-to—see, e.g., [28].
Bisimilarity is conventionally deﬁned for statebased systems with nondeterministic branching.
However, as the applications of computer systems
become increasingly pervasive and diverse (such as
cyber-physical systems), extension of bisimilarity
to systems with other branching types has beenenergetically sought in the literature. One notable
example is the bisimulation notion for probabilistic
systems in [24]: it is a relation that witnesses that
two states are indistinguishable in their behaviors
henceforth. This qualitative notion has also been
made quantitative, as the notion of bisimulation
metric [8]. It replaces a relation with a metric thatis induced by the probabilistic transition structure.
There is a body of literature (including [2,4,5,13,
14, 23, 33]) that aims to identify the mathematicalessences that are shared by this variety of bisimilarity, and express the identiﬁed essences in a rigorous manner using category theory. Our particularinterest is in the correspondence between bisimilarity notions and (safety) games; three examples ofwhich are given below. This interest in bisimilarity
games is shared by the recent work [23], and thecomparison is discussed in §1. 4.

1. 1. 1 Bisimilarity Games
It is well-known that the following game characterizes the conventional notion of bisimilarity between Kripke frames. Let (X, →) be a Kripke frame
where → ⊆ X 2 ; the game is played between Duplicator (D) and Spoiler (S). In a position (x1 , x2 ),Spoiler challenges Duplicator’s claim that x1 andx2 are bisimilar, by choosing one of the states (sayx1 ) and further choosing a transition x1 → x′1 . Duplicator responds by choosing a transition x2 → x′2
from the other state, and the game is continued
from (x′1 , x′2 ). Duplicator wins if Spoiler gets stuck,or the game continues inﬁnitely long, and this witnesses that x1 and x2 are bisimilar.
1. 1. 2 Games for Probabilistic Bisimilarity
A recent step forward in the topic of bisimilarityand games is the characterization of probabilistic
bisimulation introduced in [11]. For simplicity, here
we describe its discrete version.
Let (X, c) be a Markov chain, where X is a countable set of states, and c : X → D≤1 X is a transition kernel that assigns to each state x ∈ X aprobability subdistribution c(x) ∈ D≤1 X. Here∑D≤1 X = {d : X → [0, 1] |x∈X d(x) ≤ 1} denotes the set of probability subdistributions over
X. For Z ⊆ X, let c(x)(Z) denote the probability
with which a successor of x is chosen from Z; that∑is, c(x)(Z) = x0 ∈Z c(x)(x′ ). Since c(x) is only a
sub-distribution over X, the probability c(x)(X) is≤ 1 rather than = 1. The remaining probability
1 − c(x)(X) can be thought of as the probability ofx getting stuck.
Recall from [24] that an equivalence relation
R ⊆ X 2 is a (probabilistic) bisimulation if, forany (x, y) ∈ R and each R-closed subset Z ⊆ X,
c(x)(Z) = c(y)(Z) holds.
Table 1The Game for Probabilistic
Bisimilarity from [11]positionpl.

possible moves(x, y) ∈ X 2
Z⊆X

S
D

Z ⊆ X s.t. c(x)(Z) ̸= c(y)(Z)(x′ , y ′ ) ∈ X 2 s.t. x′ ∈ Z ∧ y ′ ̸∈ Z

The game introduced in [11] is in Table 1. It
is shown in [11] that Duplicator is winning in thegame at (x, y) if and only if x and y are bisimilar, inthe sense of [24] (recalled above). It is not hard toﬁnd an intuitive correspondence between the gamein Table 1 and the deﬁnition of bisimulation [24]:Spoiler challenges the bisimilarity claim between
x, y by exhibiting Z such that c(x)(Z) = c(y)(Z) is
violated; Duplicator makes a counterargument byclaiming that Z is in fact not bisimilarity-closed,
exhibiting a pair of states (x′ , y ′ ) that Duplicator
claims are bisimilar.
1. 1. 3 Games for Probabilistic Bisimulation Metric
Our following observation marked the beginningof the current work: the game for (qualitative)
bisimilarity for probabilistic systems (from [11], Table 1) can be almost literally adapted to (quantitative) bisimulation metric for probabilistic systems.
This metric was ﬁrst introduced in [8].
For simplicity we focus on the discrete setting; wealso restrict to pseudometrics bounded by 1. Let(X, c) be a Markov chain with a countable state
space X. The bisimulation metric d(X,c) : X 2 →[0, 1] is deﬁned to be the smallest pseudometric(with respect to the pointwise order) that makes
the transition kernel()
c : (X, d(X,c) ) −→ D≤1 X, K(d(X,c) )non-expansive with respect to the speciﬁed pseudometrics. Here K(d(X,c) ) is the so-called Kantorovich metric over D≤1 X induced by the pseudometric d(X,c) over X. It is deﬁned as follows.
For µ, ν ∈ D≤1 X,
K(d(X,c) )(µ, ν) = sup |Eµ [f ] − Eν [f ]| ,(1)fwhere in the above sup, f ranges over all non()
expansive functions from (X, d(X,c) ) to [0, 1], d[0,1] ,d[0,1] denotes the usual Euclidean metric, and Eµ [f ]∑is the expectation x∈X f (x) · µ(x) of f with respect to µ.
Our observation is that the bisimulation metric d(X,c) is characterized by the game in Table 2:
Duplicator is winning at (x, y, ε) if and only ifd(X,c) (x, y) ≤ ε.
The game seems to be new, although its intuition is similar to the one for Table 1. Notethat the formula (1) appears in the condition of
Spoiler’s moves. Spoiler challenges by exhibiting a“predicate” f that suggests violation of the nonexpansiveness of c; and Duplicator makes a counterargument that f is in fact not non-expansive andthus invalid.

Table 2

The Game for (Probabilistic)

Bisimulation Metric, Adapting [11]positionpl.

possible moves(x, y, ε)∈ X 2 × [0, 1]
f : X → [0, 1]

S

f : X → [0, 1] such that
Ec(x) [f ] − Ec(y) [f ] > ε(x′ , y ′ , ε′ ) ∈ X 2 × [0, 1]
such that f (x′ ) − f (y ′ ) > ε′D

categorical
1 codensity○
bisimilarity game

concrete
instantiates

4 bisim○ilarity
gamecharacterizes (Cor. 4.4, 5.8)
2 codensity
induces (§4– ○
bisimilarity5)νΦΩ,τ ∈ EX

5 bisiminstantiates ○ilarityinduces (§3, [29])
3 codensity○
lifting (§3, [20])F Ω,τ : E → E

Fig. 1

Our Codensity-Based Framework for
Bisimilarity and Games1. 1. 4 Towards a Unifying Framework
The last two games (Table 1 from [11] and Table 2 that seems new) motivate a general framework that embraces both. There are some clear
analogies: the games are about indistinguishability of states x, y under a class of observations (Zand f respectively), and the predicates usable inthose observations are subject to certain preservation properties (bisimilarity-closedness in the former, and non-expansiveness in the latter).
1. 2 A Codensity-Based Framework for
Bisimilarity and GamesThe main contribution of the current paper isa categorical framework that derives a variety ofbisimilarity notions and corresponding game notions. The correspondence is proved once and forall on the categorical level of generality. It covers the three examples introduced earlier in §1. 1,much like the recent categorical framework in [23]does. However, our ﬁbration-based formalization
has another dimension of generality. For example,
besides relations and metrics, our examples include
what we call bisimulation topology.

The overview of our categorical framework is in
the left half of Fig. 1. We build on our previous
works [20] and [29]. In [20] a general construction
called codensity lifting is introduced: given a ﬁbration p : E → C and parameters (Ω, τ ) that embody
the kind of observations we can make, a functor
F : C → C is lifted to F Ω,τ : E → E. In [29], codensity lifting is used to introduce a generic family of
bisimulation notions called codensity bisimilarity—2
see ○.
In this paper, we extend these previous
results by• introducing the notion of codensity bisimi1 that comes in two variants
larity game (○)(untrimmed (§4) and trimmed (§5)),• establishing the correspondence between co2 and games (○)
1 ondensity bisimulations (○)
a ﬁbrational level of generality, and4• working out several concrete examples (○,5○).
4 directly
In general, devising a game notion (○)
5 is far from trivfrom a bisimilarity notion (○)
ial. Indeed, doing so for an individual bisimilarity notion has itself been deemed a scientiﬁc novelty [7, 11]. Our codensity-based framework (in theleft half of Fig. 1) can automate part of this process
in the following precise sense.
5
We derive concrete notions of bisimilarity (○)
4 as instances; then theand bisimilarity game (○)
correspondence between the two is guaranteed by
1 and ○.
2the categorical general result between ○We note, however, that this is no panacea. Whenone starts with a given concrete notion of bisimi5
larity (○),
their next task would be to identifyp
the right choice of the parameters E −→ C, Ω, τ for3
the codensity lifting (○).
This task is not easy ingeneral: we needed to get our hands dirty working out the examples in this paper, [20], and [29].
Nevertheless, we believe that the required passage
5 to ○
3 is much easier than the direct derivafrom ○5 to ○,
4 with our categorical frameworktion from ○providing templates of bisimilarity games (see Tables 7, 9 and 10). After all, our framework identiﬁes
5 to ○
4 can be autowhich part of the path from ○mated, and which part remains to be done individually. This is much like what many other categoricalframeworks oﬀer, as meta-level theories.
As an additional beneﬁt, our categorical framework can be used to discover new bisimilarity no5 starting from (choices of parameters for)tions (○),

3 We believe those derived new bisimilarity no○.
tions are useful, since our categorical theory embodies sound intuitions about observation, predicate transformation, and indistinguishability—see
e.g. §2. 2.

1. 3 Contributions
Our main technical contributions are as follows.
• We introduce a categorical framework thatuniformly describes various bisimulation notions (including metrics, preorders and topologies) and the corresponding game notions(Fig. 1). The framework is based on coalgebras, ﬁbrations, and codensity liftings in particular [20]. Our general game notion comes in
two variants.
– The ﬁrst (the untrimmed codensity
game: §4) arises naturally in a ﬁbration,using its objects and arrows as possible
moves. The untrimmed game is theoretically clean, but it tends to have a hugearena.
– We therefore introduce a method that
restricts these arenas, leading to the(trimmed ) codensity bisimilarity game(§5). The reduction method is also described in general ﬁbrational terms, specifically using ﬁbered separators and generating sets.
• From the general framework, we derive several concrete examples of bisimilarity and its
4 and ○
5 in Fig. 1). They are
related notions (○listed in Table 6. Among them, a few bisimilarity notions seem new (especially the bisimulation topology examples), and several gamenotions also seem new.
• Additionally, we conduct investigations of thegame notion in [11] (Table 1) in concrete,non-categorical terms. For one, we obtainits variation for bisimulation metric (as we
showed in Table 2). We also give a direct
proof of the equivalence to another game notion for probabilistic bisimilarity, previously introduced in [7], by exhibiting a mutual translation of winning strategies. See the extended
version [22].

1. 4 Related Work
Besides the one in [11], another game characterization of probabilistic bisimulation has been given
in [7]. It is described later in §2 (Table 3). The
latter game has a bigger arena than the one in [11]:in [7] both players have to play a subset Z ⊆ X,
while in [11] only Spoiler does so.
The work that is the closest to ours is the recent work [23] that studies bisimilarity games ina categorical setting. Their formalization uses(co)algebras (following the (co)algebraic generalization of the Kantorovich metric introducedin [2]), and therefore embraces a variety of diﬀerent
branching types. The major diﬀerences between
the two works are as follows.
• Our current work is ﬁbration-based (in particular CLat⊓ -ﬁbrations), while [23] is not. As
a consequence, ours accommodates an additional dimension of generality by changing ﬁbrations, which correspond to diﬀerent indistinguishability notions (relation, metric, topology, preorder, measurable structures, etc.). In
contrast, the works [23] and [2] deal exclusively
with two settings: binary relations and pseudometrics.
• A relationship to modal logic is beautifully established in [23], while it is not done in thiswork. We expect our ﬁbrational framework
can accommodate modal logic too: ﬁbrations
have been used for categorical modeling of logics [17]. We leave this aspect to future work.
• The categorical generalization [23] is based on
the game notion in [7], while ours is based onthat in [11]. Therefore, for some bisimulation
notions (including the bisimulation metric), we
obtain a game notion with a smaller arena.
Compare Table 2 (an instance of ours) and Table 4 (an instance of [23]).
There are a number of categorical studies ofbisimilarity notions; notable mentions include
open map-based approaches [19] and coalgebraic
ones [18, 27]. The ﬁbrational approach we adopt
also uses coalgebras; it was initiated in [14] and pursued, e.g., in [4,5,13], and [29]. For example, in the
recent work [4], ﬁbrational generality is exploited
to study up-to techniques for bisimilarity metric.
They use the Wasserstein lifting of functors introduced in [2] instead of the codensity lifting that weuse (it generalizes the Kantorovich lifting in [2], seeExample 3.4). It is known [2] that the Wasserstein
and Kantorovich liftings can diﬀer in general, while
they coincide for some speciﬁc functors such as the
distribution functor.
Some of our new examples are topological: we derive what we call bisimulation topology and a gamenotion that characterizes it. The relation between
these notions and the existing works on bisimulation and topology (including [6,31]) is left as futurework.
1. 5 Organization
In §2, we present preliminaries on a general theory of games (we can restrict to safety games),and on ﬁbrations. For the latter, we focus ona class called CLat⊓ -ﬁbrations, and argue thatthey oﬀer an appropriate categorical abstraction ofsets equipped with indistinguishability structures.
In §3, we present codensity lifting and codensity
2 ○3 in Fig. 1). The material isbisimilarity (○,based on [29], but we introduce some auxiliary notions needed for the correspondence with games.
Our ﬁrst game notion (the untrimmed one) is introduced in §4; in §5, we cut down the arenas and obtain trimmed codensity bisimilarity game. In §6 we
accommodate multiple observation domains, These
categorical observations give rise to the concrete examples in §7.
Some proofs and details are deferred to the appendix found in the extended version [22].

2 Preliminaries
We write P : Set → Set for the covariant powerset functor, and 2 for the two-point set 2 = {⊥, ⊤}.
We deﬁne the function ⋄ : P2 → 2 called maymodality by ⋄S = ⊤ if and only if ⊤ ∈ S. We write
EqI for the diagonal (equality) relation over a set
I.
2. 1 Safety Games
Here we recall some standard game-theoretic notions and results. In capturing bisimilarity-like notions, we can restrict ourselves to safety games—
they have a simple winning condition where every
inﬁnite play is won by the same player (namely Duplicator). This winning condition reﬂects the characterization of bisimilarity-like notions by suitable
greatest ﬁxed points; the correspondence general-izes, for example, to the one between parity gamesand nested alternating ﬁxed points—see [32]. The
term “safety game” occurs, e.g., in [3, 9].
Safety games are played between two players;
in this paper, they are called Duplicator (D) andSpoiler (S). We restrict to those games in which
Duplicator and Spoiler alternate turns.
Deﬁnition 2.1 (safety game). A (safety game)arena is a triple G = (QD , QS , E) of a set QD of Duplicator’s positions, a set QS of Spoiler’s positions,and a transition relation E ⊆ (QD × QS ) ∪ (QS ×
QD ). Hence G is a bipartite graph. We require that
QD and QS are disjoint, and that QD ∪ QS ̸= ∅. We
write Q = QD ∪ QS .
For a position q ∈ Q, the elements of the set{q ′ ∈ Q | (q, q ′ ) ∈ E} are called the possible moves
at q. Unlike some works, we allow positions thathave no possible moves at them.
A play in an arena G = (QD , QS , E) is a (ﬁnite
or inﬁnite) sequence of positions q0 q1 . . . , such that(qi−1 , qi ) ∈ E so long as qi belongs to the sequence.
A play in G is won by either player, according to
the following conditions: 1) a ﬁnite play q0 . . . qn is
won by Spoiler (or by Duplicator) if qn ∈ QD (orqn ∈ QS respectively); and 2) every inﬁnite play
q0 q1 . . . is won by Duplicator.
Deﬁnition 2.2 (strategy, winning position). In an
arena G = (QD , QS , E), a strategy of Duplicator isa partial function σD : Q∗ × QD ⇀ QS ; we requirethat σD (⃗q q) = q ′ implies (q, q ′ ) ∈ E. A strategy
of Spoiler is deﬁned similarly, as a partial function
σS : Q∗ × QS ⇀ QD that returns a possible move at
the last position in the history.
Given an initial position q ∈ Q and two strategies
σD and σS for Duplicator and Spoiler respectively,
the play from q induced by (σD , σS ) is deﬁned ina natural inductive manner. The induced play isdenoted by π σD ,σS (q).
A position q ∈ Q is said to be winning for Duplicator if there exists a strategy σD of Duplicator
such that, for any strategy σS of Spoiler, the induced play π σD ,σS (q) is won by Duplicator.
In what follows, for simplicity, we restrict the initial position q of a play π σD ,σS (q) to be in QS . (Notethat Spoiler’s position can be winning for Duplicator.)
Winning positions of safety games are witnessedby invariants (Prop. 2.4), which is a well-known
fact.

Deﬁnition 2.3 (invariant). Let G = (QD , QS , E)
be an arena. A subset P ⊆ QS is called an invariant for Duplicator if, for each q ∈ P and any
possible move q ′ ∈ QD at q, there exists a possible
move q ′′ at q ′ that is in P . That is, ∀q ∈ P. ∀q ′ ∈(QD . (q, q ′ ) ∈ E ⇒ ∃q ′′ ∈ QS . (q ′ , q ′′ ) ∈ E ∧ q ′′ ∈)P .
Proposition 2.4.
1. Any position q ∈ P in an
invariant P for Duplicator is winning for Duplicator.
2. Invariants are closed under arbitrary union.
Therefore, there exists a largest invariant for
Duplicator.
3. The largest invariant for Duplicator coincides
with the set of winning positions for Duplicatorin QS .
Examples of safety games have been given in Tables 1–2. We present two other examples (Tables 3–
4).
Example 2.5 (alternative games for probabilistic bisimilarity and bisimulation metric). In [7], agame notion that characterizes (qualitative) probabilistic bisimilarity is presented. It is in Table 3,
presented in a slightly adapted form.
This game notion is categorically generalizedin [23]; the generalization has freedom in the choiceof coalgebra functors (i.e. branching types), as wellas in the choice between relations and metrics. The
instance of this general game notion for bisimulation metric is shown in Table 4.
The two games (Tables 3–4) characterize thesame bisimilarity-like notions as the games in Tables 1–2, respectively; so they are equivalent. We
can go further and give a direct equivalence proof
by mutually translating winning strategies. Such a
proof is not totally trivial; we do so for the pair forprobabilistic bisimilarity. See [22, Appendix A].
We note that the game in Table 2 (an instance ofour current framework) is simpler than Table 4 (aninstance of [23]). Table 2 is not only structurally
simpler (it has fewer rows), but its set of moves are
smaller too, asking for functions X → [0, 1] only at
one place.
Our categorical framework based on codensity
liftings (presented in later sections) covers Tables 1–2 but not Tables 3–4. Accommodation of
the latter two is future work.

2. 2 CLat⊓ -ﬁbrations
2. 2. 1 Deﬁnition and Properties
Here we sketch a basic theory of ﬁbrations—see,e.g., [17] for a comprehensive account. In particular, we focus on a class of poset ﬁbrations called
CLat⊓ -ﬁbrations. We observe that the simple axiomatics of the class adequately capture all the examples of interest—and hence the mathematicalessences of the logical phenomena that we wish tomodel.
Our exposition here is largely based on thatin [29]. However, in this paper we introduce newnotation and terminology (such as indistinguishability order and decent map)—see §2. 2. 2. They
help to further clarify the intuitions.
A formal deﬁnition is as follows. (See [22,Appendix B] for a rather gentle introduction to
CLat⊓ -ﬁbration.)Deﬁnition 2.6 (CLat⊓ -ﬁbration). A CLat⊓ ﬁbration is a ﬁbration p : E → C such that eachﬁber EX (for each X ∈ C) is a complete lattice,and each pullback functor f ∗ : EY → EX (for eachdf : X → Y in C) preserves all meets .
Via the Grothendieck construction, a CLat⊓ ﬁbration is in a bijective correspondence with afunctor FE : Cop → CLat⊓ , where CLat⊓ is thecategory of complete lattices and functions preserving all meets—see [17] and [13], as well as [22, Appendix B]. The functor FE assigns• a complete lattice EX (called the ﬁber over X)
to each X ∈ C, and• a function f ∗ : EY → EX preserving all meetsto each f : X → Y in C. The map f ∗ is calleda pullback ; it is also called a pullback functor
since, in the general theory of ﬁbrations, a ﬁber
EX is a category rather than a poset.
Although the indexed category presentation FE : Cop →CLat⊓ may be more intuitive at ﬁrst, we shall stickto the ﬁbration presentation p : E → C since we will
eventually need some global structures in the total
category E. It turns out that CLat⊓ -ﬁbrations are
special kinds of topological functor [15] such thateach ﬁber category is a poset. Topological functors are a well-studied topic, and many examples
and results are available; a good summary is foundin [1].
The use of poset ﬁbrations is common in categorical modeling of logics [5, 13]. CLat⊓ -ﬁbrations
additionally require ﬁbered small meets; this sim-

Table 3

The Game for Probabilistic Bisimilarity, from [7]We omit labels that are needed to distinguish (x, y) ∈ X 2 (an S-position) from (s, t) ∈ X 2 (a D-position).
positionpl. possible moves(x, y) ∈ X 2

S(s, t) ∈ X 2 s.t. {s, t} = {x, y}(s, t) ∈ X 2

D(Z, Z ′ ) s.t. Z ⊆ Z ′ ⊆ X
and c(s)(Z) ≤ c(t)(Z ′ )(Z, Z ′ ) ∈ (PX)2S(Z, y ′ ) ∈ PX × X s.t. y ′ ∈ Z ′ \ Z(Z, y ′ ) ∈ PX × X

D(x′ , y ′ ) ∈ X 2 s.t. x′ ∈ Z

Table 4The Game for Bisimulation Metric, from [23]positionpl.

possible moves(x, y, ε) ∈ X 2 × [0, 1]

S(s, t, f, ε) ∈D(s, t) ∈ X 2 s.t. {s, t} = {x, y},and f : X → [0, 1]
g : X → [0, 1] such thatS

max{0, Ec(s) [f ] − Ec(t) [g]} ≤ ε()2(i, j) ∈ [0, 1]Xsuch thatX 2 × [0, 1]X × [0, 1](f, g, ε) ∈ ([0, 1] )X 2′

(x , i, j, ε) ∈X × ([0, 1]X )2 × [0, 1]D

ple assumption turns out to be a mathematicallypowerful one.
Proposition 2.7. Let p : E → C be a CLat⊓ ﬁbration.
1. p is split, and faithful as a functor.
2. Each arrow f : X → Y has its pushforwardf∗ : EX → EY , so that an adjunction f∗ ⊣ f ∗is formed. This is a consequence of Freyd’s
adjoint functor theorem; it makes p a biﬁbration [17].
3. pop : Eop → Cop is also a CLat⊓ -ﬁbration.
4. The change-of-base [17, Lemma 1.5.1] of palong any functor H : D → C is also a CLat⊓ ﬁbration.
5. If C is (co)complete, then the total category
E is also (co)complete. This follows from [17,Prop. 9.2.1].
2. 2. 2 Notation, Terminology and Intuitions
Our view of a CLat⊓ -ﬁbration p : E → C isthat it equips objects of C with what we call indistinguishability structures. This suits our purpose,
since various bisimilarity-like notions are all about
degrees of indistinguishability between (the behav-{i, j} = {f, g}, and x′ ∈ X(x′ , y ′ , ε′ ) ∈ X 2 × [0, 1] such thati(x′ ) ≤ j(y ′ ), andε′ = j(y ′ ) − i(x′ )iors of) states of a system. We present examples
later in §2. 2. 3.
Notation 2.8 (indistinguishability predicate/order).
Let p : E → C be a CLat⊓ -ﬁbration. An object
P ∈ EX in the ﬁber category EX (i.e. an elementof the complete lattice EX ) is called an indistinguishability predicate over X. Our view is that P isan additional structure on X; therefore, as a convention, an object P ∈ EX shall also be denoted by(X, P ) ∈ EX .
Each ﬁber EX is a complete lattice; its order isdenoted by ⊑ and called the indistinguishability order over X. Intuitively, P ⊑ Q means that Q has agreater degree of indistinguishability than P —that
is, Q is coarser than P , and P is more discriminating than Q.
The supremum and inﬁmum with respect to the⊔indistinguishability order ⊑ are denoted byanddrespectively.
Deﬁnition 2.9 (decent map). Let p : E → C bea CLat⊓ -ﬁbration, f : X → Y be an arrow in C,(X, P ) ∈ EX and (Y, Q) ∈ EY be objects in theﬁbers. We say that f is decent (from P to Q) if
there exists a necessarily unique arrow f˙ : P → Q in

E such that pf˙ = f . We write f : (X, P ) →˙ (Y, Q)in this case. The following equivalences follow.
f : (X, P ) →˙ (Y, Q) ⇐⇒ P ⊑ f ∗ Q ⇐⇒ f∗ P ⊑ Q
We write f : (X, P ) ↛˙ (Y, Q) if f is not decent.
The notion of decency is a ﬁbered generalization of continuity, non-expansiveness, relationpreservation, etc. Decency f : (X, P ) →˙ (Y, Q)means f respects indistinguishability, carrying P indistinguishable elements to Q-indistinguishableones.
2. 2. 3 Examples
As shown in Table 5, various well-known categories can be seen as categories that equip sets withcertain indistinguishability structures. The evident
forgetful functors from the total categories (Top,Meas, etc.) to Set in Table 5 are all CLat⊓ ﬁbrations.
Speciﬁcally, Top is the category of topologicalspaces and continuous maps; Meas is that of measurable spaces and measurable maps; PMet1 isthat of 1-bounded pseudometric spaces (where apseudo-metric is a metric without the condition
d(x, y) = 0 ⇒ x = y) and non-expansive maps;
ERel is that of sets with endorelations (X, R ⊆X 2 ) and relation-preserving maps; Pre is that ofpreordered sets and monotone maps; and EqRel isthat of sets with equivalence relations and relationpreserving maps—see [29] for details.
Note that, in Top and Meas, the indistinguishability order is the opposite of the inclusion order.
Therefore the meet of a family of indistinguishability structures computed as the one generated fromthe union of the family.
Another class of examples is given as follows:
for any well-powered category B admitting small
limits, the subobject ﬁbration of B is a CLat⊓ ﬁbration. All the algebraic categories over Set andGrothendieck topoi fall into this class. On the other
hand, the forgetful functors from algebraic categories over Set are rarely (CLat⊓ -)ﬁbrations.

3 Codensity Bisimilarity
3 in Fig. 1) andWe introduce codensity lifting (○2 based on [29]. These
codensity bisimilarity (○)
turn out to subsume many bisimilarity-like notions in the literature. The material in §3. 1–3. 2is largely from [29]; §3. 3 is new, paving the way
to codensity bisimilarity games presented in later

sections.
3. 1 Codensity Lifting
Deﬁnition 3.1 (codensity lifting F Ω,τ [29]). Let
p : E → C be a CLat⊓ -ﬁbration, and F : C → C
be a functor. A parameter of codensity lifting of F
along p is a pair of• a C-arrow τ : F Ω → Ω (i.e. an F -algebra)
called modality [12, 16] and• an E-object Ω above Ω called observation domain.
The codensity lifting of F : C → C with parameter(Ω, τ ) is the endofunctor F Ω,τ : E → E deﬁned asfollows. On objects, l(())∗
F Ω,τ P =
τ ◦ F p(k) Ω.
k∈E(P,Ω)

Its action on arrows is as follows. It is not hard to
see that, for each arrow l : P → Q in E, the arrow
F (p(l)) is decent from F Ω,τ P to F Ω,τ Q. Then wedeﬁne F Ω,τ l : F Ω,τ P → F Ω,τ Q to be the uniquearrow in E above F (p(l)).
An alternative description is possible. When E
has powers ⋔ and p preserves them, F Ω,τ is characterized as the following pullback in the ﬁbration[E, p] : [E, E] → [E, C]:[E, E]

[E,p]/F Ω,τ _ _ _ _E(−,Ω) ⋔ Ω/E(−, Ω) ⋔ Ω[E, C]F ◦pαwhere αP = ⟨τ ◦ F (p(k))⟩k∈E(P,Ω) is the tupling.
A similar characterization of codensity liftings ofmonads is in [20].
Table 6 lists concrete examples of codensity liftings, with various ﬁbrations p, functors F , and parameters (Ω, τ ). Some of them coincide with known
notions. For example, the entry 5 of the table saysthat the functor (D≤1 )Ω,τ , with the designated Ωand τ , carries a metric space (X, d) to the set D≤1 X
equipped with the well-known Kantorovich metricK(d) induced by d—see (1).
Besides the functors listed in the table, there aresome natural ways to systematically lift polynomial
functors, by deﬁning τ : F Ω → Ω in an inductive
manner—see, e.g., [4].
Example 3.2. Let us closely look at the entry 4of Table 6. There we codensity-lift the covariant powerset functor P along the CLat⊓ -ﬁbration
EqRel → Set. We use the parameter ((2, Eq2 ), ⋄),where ⋄ : P2 → 2 is the modality given in §2.
We shall abbreviate (2, Eq2 ) by Eq2 —a nota-

Table 5

CLat⊓ -Fibrationsdfibrationindistinguishability structure

decent map

P v Q

Top → Set
Meas → Set
PMet1 → Set
ERel → Set
Pre → Set
EqRel → Set

topology
σ-field
pseudometric
endorelation
preorderequivalence relation

continuous func.
measurable func.
non-expansive func.
relation preserving func.
monotone func.
relation preserving func.

P ⊇ Q
P ⊇ Q
∀x, y. P (x, y) ≥ Q(x, y)
P ⊆ Q
P ⊆ Q
P ⊆ Q

Table 6Pi∪
generated fromP
∪ igenerated fromPi(x, y) 7→ supi Pi (x, y)
∩
Pi
∩
P
∩ i
Pi

Codensity Lifting of Functors

fibration p : E → C

functor F : C → C

obs. dom. Ωmodality τlifting F Ω,τ of F

1
2
3
4
5

Pre → Set
Pre → Set
ERel → Set
EqRel → Set
PMet1 → Set(2, ≤)(2, ≥)(2, Eq2 )(2, Eq2 )([0, 1], d[0,1] ) : P2 → 2
 : P2 → 2
 : P2 → 2
 : P2 → 2
e : D≤1 [0, 1] → [0, 1]

lower preorder [20]upper preorder [20](for bisimulation, see Ex. 3.3 )(for bisimulation, see Ex. 3.2 )Kantorovich metric

6

PMet1 → Set
U ∗ (PMet1 ) → Meas

powerset P
powerset P
powerset P
powerset P
subdistrib. D≤1

7
8†

9†
10†

powerset P([0, 1], d[0,1] )inf : P[0, 1] → [0, 1]

Hausdorff pseudometric (cf. [22, Appx. C])

sub-Giry G≤1([0, 1], d[0,1] )e : G≤1 [0, 1] → [0, 1]

Kantorovich metric

Pre → Set

powerset P(2, ≤), (2, ≥) : P2 → 2

convex preorder [20]EqRel → Set

subdistrib. D≤1
2 × ( )Σ(2, Eq2 )(τr : D≤1 2 → 2)r∈[0,1](for prob. bisim., see [22])Top → Set
Sierpinski space(see Ex. 6.5)
(for bisim. topology, see Ex. 6.5)
The fibration U ∗ (PMet1 ) → Meas is obtained as a change-of-base, pulling back PMet1 → Set along U : Meas → Set. d[0,1] denotes the
Euclidean metric on the unit interval [0, 1]. The modality  is introduced in the beginning of §2. The functions e : D≤1 [0, 1] → [0, 1] ande : G≤1 [0, 1] → [0, 1] both return expected values. The lower, upper and convex preorders are known for powerdomains; see e.g. [30]. The
function τr : D≤1 2 → 2 is defined by τr (p) = > if p(>) ≥ r, and τr (p) = ⊥ otherwise.
The examples marked with † involve multiple modalities and observation domains. The extension that allows such is described later in §6.

tional convention that is used throughout the paper.
Then P Eq2 ,⋄ (X, R) relates S, T ∈ PX if and onlyif∀k : X → 2. (∀(x, y) ∈ R. k(x) = k(y))
=⇒ (∃x ∈ S. k(x) = ⊤) ⇐⇒ (∃x ∈ T. k(x) = ⊤) .

Straightforward calculation shows that this isequivalent to(∀x ∈ S. ∃y ∈ T. (x, y) ∈ R)∧(∀y ∈ T. ∃x ∈ S. (x, y) ∈ R).

This lifting is the restriction of the standard relational lifting of P along ERel → Set, which is used
for the usual bisimulation notion for Kripke frames,
to EqRel.
Example 3.3. In the entry 3 of Table 6,
we codensity-lift P along the CLat⊓ -ﬁbration
ERel → Set (instead of EqRel → Set) with the()
parameter (2, Eq2 ), ⋄ .
The characterization of P Eq2 ,⋄ (X, R) is slightly
involved. Its relation part relates S, T ∈ PX if andonly if(∀x ∈ S. ∃y ∈ T. (x, y) ∈ Req ) ∧(∀y ∈ T. ∃x ∈ S. (x, y) ∈ Req ),eqwhere R denotes the equivalence closure of R.
It is not clear at this stage whether the codensity bisimilarities induced by the above liftings(Examples 3.2–3.3, i.e. the entries 4 & 3 of Table 6) coincide with the usual bisimilarity notion for
Kripke frames. This is because of the involvementof mandatory equivalence closures—speciﬁcally by
the use of EqRel in Example 3.2, and by the occurrence of ( )eq in Example 3.3.
Example 3.4. Here we follow [29, Example 3]

and show that codensity lifting generalizes the
Kantorovich lifting of functors introduced in [2].
Take PMet1 → Set as the CLat⊓ -ﬁbration p inDef. 3.1. As Ω, we take Ω = [0, 1] with the usual
Euclidean metric d[0,1] . There is freedom in the
choice of a modality τ : F Ω → Ω—this corresponds
to what is called an evaluation function in [2]. Thisway we recover the Kantorovich lifting in [2] asF Ω,τ .
3. 2 Codensity Bisimilarity
In [29], codensity bisimulation and bisimilarity
are introduced. Recall that a coalgebra c : X → F X
is a categorical presentation of state-based transition systems, such as automata, Markov chains,
etc.—see, e.g., [18, 27], and also §7.
Deﬁnition 3.5 (codensity bisimulation). Assume
the setting of Def. 3.1. Let c : X → F X bean F -coalgebra. An object P ∈ EX is a ((Ω, τ ))codensity bisimulation over c if c : (X, P ) →˙(F X, F Ω,τ P ); that is, c is decent with respect tothe designated indistinguishability structures on X
and F X.
We move on to the characterization of codensity bisimulations as (post-)ﬁxed points of suitablepredicate transformers.
Deﬁnition 3.6 (predicate transformer ΦΩ,τ ). Assume the setting of Def. 3.5. We deﬁne a predicate
transformer ΦΩ,τ: EX → EX with respect to c andcF Ω,τ by:ΦΩ,τ
P = c∗ (F Ω,τ P ), that is,
c

l

(
)∗
τ ◦F (p(k))◦c Ω.

k∈E(P,Ω)(2)
Theorem 3.7. Assume the setting of Def. 3.5. For
any P ∈ EX , the following are equivalent.
1. c : (X, P ) →˙ (F X, F Ω,τ P ); that is, P is a
codensity bisimulation over c (Def. 3.5).
2. P ⊑ ΦΩ,τP.
c
3. For each k ∈ C(X, Ω), k : (X, P ) →˙ (Ω, Ω)
implies τ ◦ F k ◦ c : (X, P ) →˙ (Ω, Ω).
The predicate transformer ΦΩ,τis a monotonecmap from the complete lattice EX to itself. Therefore, by the Knaster–Tarski theorem, the greatest
post-ﬁxed point of ΦΩ,τexists and it is the greatest
cﬁxed point of ΦΩ,τ.
c
Deﬁnition 3.8 (codensity bisimilarity νΦΩ,τ
).
cAssume the setting of Def. 3.5. The greatest codensity bisimulation, whose existence is guaranteed by
the above arguments, is called the codensity bisimilarity. It is denoted by νΦcΩ,τ .
Some bisimilarity notions, including bisimilarity
of deterministic automata (§7. 2), are accommodated in the generalized framework with multiple
observation domains—see §6.
Example 3.9 (bisimulation metric). Consider the
CLat⊓ -ﬁbration PMet1 → Set and the subdistribution functor D≤1 : Set → Set. Recall that∑D≤1 (X) = {p : X → [0, 1] | x∈X p(x) ≤ 1}. As aparameter of codensity lifting, we take (Ω, τ ) =(())[0, 1], d[0,1] , e : D≤1 [0, 1] → [0, 1] , where e is∑the expectation function e(p) = r∈[0,1] r · p(r) andd[0,1] is the Euclidean metric. Let c : X → D≤1 X
be a coalgebra, identiﬁed with a Markov chain.
The codensity bisimilarity in this setting coincides with bisimulation metric from [8] (seealso §1. 1. 3). This fact is not hard to check directly;
one can also derive the coincidence via Example 3.4
and the observations in [2].
3. 3 Joint Codensity Bisimulation
We introduce a notion of joint codensity bisimulation. This minor variation of codensity bisimulation becomes useful in the proof of soundness andcompleteness of our game notion (§4).
Deﬁnition 3.10 (joint codensity bisimulation).
Assume the setting of Def. 3.5. Let V ⊆ |EX |;⊔joins in EX are denoted by . We say that V is⊔a joint codensity bisimulation over c if P ∈V P is a

Table 7

Untrimmed Codensity Bisimilarity
Game

positionpl.

possible moves

P ∈ EXSk ∈ C(X, Ω)Dk ∈ C(X, Ω) s.t.
τ ◦ F k ◦ c : (X, P ) ↛˙ (Ω, Ω)
P ′ ∈ EX s.t. k : (X, P ′ ) ↛˙ (Ω, Ω)

Table 8Untrimmed Codensity Game for
Bisimulation Metricpositionpl.

possible movesd ∈ (PMet1 )XS

k ∈ Set(X, [0, 1]])Dk ∈ Set(X, [0, 1]) s.t.
e ◦ F k ◦ c ̸∈ PMet1 (d, d[0,1] )d′ ∈ (PMet1 )X s.t.
k ̸∈ PMet1 (d′ , d[0,1] )codensity bisimulation over c.
For instance, the set of all codensity bisimulations is a joint codensity bisimulation, because thejoin νΦΩ,τ
is the largest bisimulation (a consec
quence of the Knaster–Tarski theorem).
Lemma 3.11. In the setting of Def. 3.5, thedownset ↓(νΦΩ,τ
) is the largest joint codensitycbisimulation (with respect to the inclusion order).

4

Untrimmed Games for Codensity
Bisimilarity

As the ﬁrst main technical contribution, we introduce what we call the untrimmed version of codensity bisimilarity game. It is mathematically simple
but its game arenas can become much bigger thannecessary. The trimmed version of games—withsmaller arenas—will be introduced later in §5, after developing necessary categorical infrastructure.
Assume the setting of Def. 3.5 for the rest of thesection.
Deﬁnition 4.1 (untrimmed codensity bisimilarity
game). The untrimmed codensity bisimilarity gameis the safety game played by two players D and S,
shown in Table 7.
Lemma 4.2. Let V ⊆ |EX |. The following are
equivalent.
1. V is an invariant for Duplicator (Def. 2.3) inthe safety game in Table 7.
2. V is a joint codensity bisimulation over c.
Theorem 4.3. The following coincide.
1. The set of all winning positions for D.
2. The downset ↓(νΦΩ,τ
) of the codensity bisimc
ilarity.

Proof. On the one hand, the set of all winning
positions for D is the largest invariant for D,
by Prop. 2.4. On the other hand, the downset↓(νΦΩ,τ
) is the largest joint codensity bisimulaction over c. Thus, the statement follows from
Lem. 4.2.
We conclude that our game characterizes the codensity bisimilarity νΦΩ,τ
(Def. 3.8).
cCorollary 4.4 (soundness and completeness of
untrimmed codensity games). P ∈ EX is a winning position for D if and only if P ⊑ νΦΩ,τ
.
c
Example 4.5. Recall Example 3.9. Using theuntrimmed codensity bisimilarity game, we cancharacterize the bisimulation metric from [8]. Our
general deﬁnition (Def. 4.1) instantiates to the one
in Table 8, which is however more complicatedthan the game we exhibited in the introduction(Table 2). For example, in Table 8, Duplicator’s
move is a pseudometric d : X 2 → [0, 1] rather thana triple (x, y, ε).

5 Trimmed Codensity Games for Bisimilarity
Our previous untrimmed game (Table 7) is pleasantly simple from a theoretical point of view. However, as we saw in Example 4.5, its instances tend tohave a much bigger arena than some known gamenotions.
Here we push our theory a step further, andpresent a ﬁbrational construction that allows us totrim our games. We note that our construction still
remains on the ﬁbrational level of abstraction.
5. 1 Generating Sets and Fibered Separators in a Fibration
We start by building some ﬁbrational infrastructure. The following notion is a natural extension of
the corresponding lattice-theoretic one. Unlike inthe case of algebraic lattices, we do not assume thecompactness of elements in G.
Deﬁnition 5.1 (generating set). Let p : E → C bea CLat⊓ -ﬁbration and X ∈ C be an object. We
say that a set G ⊆ |EX | is a generating set of the
ﬁber EX if, for any P ∈ EX , there exists A ⊆ G⊔such that A = P .
Example 5.2. Consider the CLat⊓ -ﬁbration
EqRel → Set and X ∈ Set. For any x, y ∈ X,
we deﬁne the equivalence relation Ex,y to be theleast one equating x, y, that is, (z, w) ∈ Ex,y if
and only if (z = w ∨ {z, w} = {x, y}). Then the
set G = {Ex,y | x, y ∈ X} of elements of the ﬁber
EqRelX is a generating set.
Example 5.3. Recall Example 3.9. For x, y ∈ X(x ̸= y) and r ∈ [0, 1], the pseudometric dx,y,r over
X is deﬁned by
0 z = w
dx,y,r (z, w) = r {z, w} = {x, y}1otherwise.

Then the set of pseudometrics {dx,y,r | x, y ∈X, x ̸= y, r ∈ [0, 1]} is a generating set of the ﬁber
(PMet1 )X .
One natural question is how to ﬁnd such a generating set in the ﬁber over the state space. Below weshow that a generating set of the ﬁber of a special
object (called ﬁbered separator ) induces a generating set of each ﬁber by push-forward.
Deﬁnition 5.4 (ﬁbered separator). Let p : E → C
be a CLat⊓ -ﬁbration. We say that S ∈ C is aﬁbered separator if, for any X ∈ C and P, Q ∈ EX ,we have(∀f ∈ C(S, X). f ∗ P = f ∗ Q) =⇒ P = Q.
Theorem 5.5. Let S ∈ C be a ﬁbered separator ofa CLat⊓ -ﬁbration p : E → C, and G ⊆ |ES | be a
generating set of ES . For any X ∈ C, the following
set is a generating set of EX :{f∗ P | P ∈ G, f ∈ C(S, X)}.
Here f∗ denotes the pushforward along f (§2. 2).
In fact, it was Thm. 5.5 behind Examples 5.2–5.3:
in both cases, 2 ∈ Set turns out to be a ﬁbered separator for the ﬁbrations in question (EqRel → Set
and PMet1 → Set), and the presented generatingsets are obtained via push-forward.
5. 2 Trimmed Codensity Bisimilarity GamesThe above concepts lead to our second game notion.
Deﬁnition 5.6 (trimmed codensity bisimilarity
game). Assume the setting of Def. 3.5, and thatG ⊆ EX is a generating set. The codensity bisimilarity game is the safety game played by two players
D and S, shown in Table 9.
Assume the setting of Def. 5.6 for the rest of thesection.
Theorem 5.7. The following sets coincide.
1. The set of D-winning positions in the game in
Table 9.

Table 9

Trimmed Codensity Bisimilarity

Table 10Game

position

pl.

P ∈G

S

k ∈ C(X, Ω)D

Trimmed Codensity Bisimilarity

Game with Multiple Observations

possible moves

positionpl.

possible moves

k ∈ C(X, Ω) s.t.
τ ◦ F k ◦ c : (X, P ) ↛˙ (Ω, Ω)
P ′ ∈ G s.t.
k : (X, P ′ ) ↛˙ (Ω, Ω)P ∈GSA ∈ A andk ∈ C(X, ΩA )D

A ∈ A and k ∈ C(X, ΩA ) s.t.
τA ◦ F k ◦ c : (X, P ) ↛˙ (ΩA , ΩA )P ′ ∈ G s.t.
k : (X, P ′ ) ↛˙ (ΩA , ΩA )()
2. The intersection ↓(νΦΩ,τ
) ∩ G of thecdownset of the codensity bisimilarity over c andthe generating set G.
We conclude that our second game characterizes
the codensity bisimilarity νΦΩ,τ
(Def. 3.8) too.
c
Corollary 5.8 (soundness and completeness oftrimmed codensity games). In Def. 5.6, P ∈ G
is a winning position for Duplicator if and only if
P ⊑ νΦΩ,τ
.
cthat is,l()∗τA ◦ F (p(k)) (ΩA ).

A∈A,k∈E(P,ΩA )The rest of the theoretical development is completely parallel to the one in the previous sections.
Therefore we only present key deﬁnitions and themain result (Cor. 6.4). The omitted deﬁnitions
and results can be recovered from the ones in §3–
5, by replacing a single-parameter codensity lifting(Def. 3.1) by a multi-parameter one (Def. 6.1).
Deﬁnition 6.2 (codensity bisimulation). Assume
the setting of Def. 6.1. Let c : X → F X be an
F -coalgebra. An object P ∈ EX is a codensity
6 Multiple Observation Domains
bisimulation over c if c : (X, P ) →˙ (F X, F Ω,τ P );We extend the theory so far and accommodatethat is, c : X → F X is decent with respect to themultiple observation domains and modalities. This
designated indistinguishability structures.
extension is needed for some examples, such as
Deﬁnition 6.3 (codensity bisimilarity game). In
those marked with † in Table 6.
the setting of Def. 6.2, let G be a generating set of
We consider the class Lift(F, p) of liftings of an
EX . The codensity bisimilarity game is the safety
endofunctor F : C → C along a CLat⊓ -ﬁbration
game, played by two players D and S, shown in
p : E → C. It comes with a natural pointwise parTable 10.
tial order:
Corollary 6.4 (soundness and completeness of coG ⊑ H ⇐⇒ ∀X ∈ E. GX ⊑ HX (G, H ∈ Lift(F, p)),density games). Assume the setting of Def. 6.3.
(3)
P ∈ EX is a winning position for Duplicator if andand the partially ordered class Lift(F, p) admits
only if P ⊑ νΦΩ,τ
.
cmeets of arbitrary size. As done in the original coExample 6.5 (bisimulation topology for determindensity lifting of endofunctors in [29] (and monads
istic automata). Here we describe the topologicalin [20]), we extend the codensity lifting so that it
example in Table 5. Consider the CLat⊓ -ﬁbration
takes a family of parameters {(ΩA , τA )}A∈A , andTop → Set and the functor AΣ = 2×( )Σ : Set →returns the intersection of the codensity liftings ofSet, where Σ is a ﬁxed alphabet. Coalgebras for
F with these parameters.
this functor are deterministic automata over Σ; seeDeﬁnition 6.1 (codensity lifting of a functor withe.g. [18, 27].
multiple parameters [29]). Let F : C → C be a
We take the following data as a parameter of cofunctor, p : E → C be a CLat⊓ -ﬁbration, A be adensity lifting (cf. Def. 6.1): A = {ε} ∪ Σ, Ωα is theclass, and {(ΩA , τA )}A∈A be an A-indexed family of
Sierpinski space for each α ∈ A, and the modalities
parameters (of the codensity lifting of F along p),τε , τa : AΣ 2 → 2 (where a ∈ Σ) are deﬁned bywhich is denoted simply by (Ω, τ ). The (multipleτε (t, ρ) = t and τa (t, ρ) = ρ(a).
parameter) codensity lifting of F with (Ω, τ ) is the
Recall that the Sierpinski space is the set 2 =endofunctor F Ω,τ : E → E deﬁned by the intersec{⊥, ⊤} with the topology {∅, {⊤}, 2}; this observation of the lcodensity liftings:
tion domain models the situation where acceptanceF Ω,τ P =F ΩA ,τA P,
of a word is only semi-decidable.
A∈A
Let c : X → AΣ X be a deterministic automata.

The above choice of parameters leads to the foltional lifting of P to ERel (see [22]).
lowing codensity bisimilarity: the state space X is
Theorem 7.1. (x, y) is a D-winning position if
Eq ,⋄equipped with the topology generated by the foland only if (x, y) ∈ νΦc 2 , if and only if x and ylowing family of open sets.
are bisimilar.
{x ∈ X | w is accepted from x} ⊆ X, for each w ∈ Σ∗ Extension of this result to labeled transiOne can extract various information from thistion systems and Kripke models (with valuabisimulation topology via standard topological contions) is straightforward, using suitable choice ofstructs. For example, the specialization order of
endofunctors—see also §7. 2.
this topology coincides with the language inclusion
order.
7. 2 Deterministic Automata and Their
For illustration by comparison, consider changing
Language Equivalence
the observation domain from the Sierpinski space to
We use the functor AΣ : Set → Set from Exthe discrete 2-point set. The bisimulation topology
ample 6.5, for which a coalgebra is a determinover X is now generated by
istic automaton. Let us lift AΣ along the ﬁbra{x ∈ X | w is accepted from x} andtion EqRel → Set, with the same modalities{x ∈ X | w is not accepted from x}, for each w ∈ Σ∗τε. , τa : AΣ 2 → 2 as in Example 6.5 (where a ∈ Σ).
We can now observe rejection of a word, too, beOur observation domains are Ωα = (2, Eq2 ) for
cause {⊥} ⊆ 2 is open. The specialization order
all α ∈ {ε} ∪ Σ. The resulting codensity liftingof this topology is the language equivalence, and(AΣ )Ω,τ : EqRel → EqRel is concretely described
it satisﬁes the R0 separation axiom (while the last
as follows.
Sierpinski example does not).
Ω,τ (R) =
(A
()
 Σ

∀k : X → 2.
(t , ρ ), (t 1, ρ 1))
We take these examples of bisimulation topology(∀x, y ∈ X. (x, y) ∈ R ⇒ k(x) = k(y)) 
2
2
.
2


∈ (AΣ X)⇒ (t1 = t2 )∧as a process-semantical incarnation of the “observ(∀a ∈ Σ. (k ◦ ρ1 )(a) = (k ◦ ρ2 )(a))
ability via topology, computability via continuity”
Let c : X → AΣ X be a deterministic automaparadigm from domain theory. The deﬁnition of coton.
It is not hard to see that the codensity bisimdensity bisimulation (cf. Def. 3.1) ﬁts well with this
ilarityνΦΩ,τ
coincides with language equivalencecintuition, too: a continuous map k : (X, P ) →˙ Ωofdeterministic
automata. Our trimmed codensity
in Def. 3.1 is a “computable observation”; accordgame is shown in Table 12 (in a slightly optimized
ingly, an open set of the bisimulation topology is aform). The game therefore characterizes the lanproperty that is decided by ﬁnitely many of thoseguage equivalence (Cor. 6.4).
computable observations.

7 Examples
We list a few examples of pairs of a codensity
bisimilarity and the corresponding codensity game.
See the extended version [22] for a larger list of examples.
7. 1

Kripke Frames and (Conventional)
Bisimilarity
We consider EqRel → Set as an underlying
CLat⊓ -ﬁbration, and a Kripke frame c : X → PX
(as a P-coalgebra). We further use the codensity lifting P Eq2 ,⋄ (Example 3.2) and the generating set described in Example 5.2 to trim games;
the resulting game is shown in Table 11. The coEq ,⋄density bisimilarity νΦc 2 coincides with conventional bisimilarity on c using the standard rela-

7. 3 Deterministic Automata and theLanguage Topology
We introduced two versions of bisimulation topology for deterministic automata in Example 6.5.
They are in close correspondences with accepted
languages; therefore we call them language topologies.
For the ﬁrst topology in Example 6.5 (whereΩ is the Sierpinski space, capturing that acceptance is only semi-decidable), the corresponding(untrimmed) codensity game is shown in Table 13.
It follows from our general results that the gamenotion is sound and complete.
We have not yet found a good way (e.g. generating sets) of trimming the game arena; this is left as
future work.

Table 11

Table 12

Codensity Bisimilarity Game for Conventional Bisimilarity

positionpl.

possible moves(x, y) ∈ X × XSk ∈ Set(X, 2)

Dk ∈ Set(X, 2) s.t.
∃x′ ∈ c(x). k(x′ ) = ⊤̸⇔ ∃y ′ ∈ c(y). k(y ′ ) = ⊤′′(x , y ′′ ) s.t. k(x′′ ) ̸= k(y ′′ )Codensity Bisimilarity Game for Deterministic Automata and Their Language
Equivalence

Table 13

positionpl.

possible moves(x, y) ∈ X × X

Sa ∈ Σ andk ∈ Set(X, 2)

D

If π1 (x) ̸= π1 (y) then S winsIf π1 (x) = π1 (y) thena ∈ Σ and k ∈ Set(X, 2)
s.t. k(π2 (x)(a)) ̸= k(π2 (y)(a))(x′′ , y ′′ ) ∈ X × X s.t. k(x′′ ) ̸= k(y ′′ )Codensity Bisimilarity Game for Deterministic Automata and Bisimulation Topology

positionpl.

possible moves

O ∈ TopXS

a ∈ {ε} ∪ Σand k ∈ Set(X, 2)Da ∈ {ε} ∪ Σ and k ∈ Set(X, 2)
s.t. τa ◦ (AΣ k) ◦ c : (X, O) ↛˙ (2, Ωa )′O ∈ TopX
s.t. k : (X, O′ ) ↛˙ (2, Ωa )7. 4 Markov Chains and Bisimulation
MetricRecall Examples 3.9, 4.5, and 5.3. Markov chainsare D≤1 -coalgebras. We use the CLat⊓ -ﬁbration
PMet1 → Set, taking pseudometrics as a notion ofindistinguishability. With the lifting parameter we
described in Example 3.9, we get the bisimulation
metric as the codensity bisimilarity. We can use
the generating set described in Example 5.3 to obtain a trimmed codensity game; the resulting gameessentially coincides with the one in Table 2 in the
introduction. Therefore, Cor. 5.8 gives an abstract
proof for the correctness of the game.

8 Conclusions and Future Work
Motivated by some recent works [2,4,11,23], andespecially by the similarity of the two games (Tables 1 and 2), we introduced a ﬁbrational framework that uniformly describes the correspondence
between various bisimilarity notions and games.
The ﬁbrational abstraction allows us to accommodate some new examples, such as bisimulation
topology. Moreover, the structural theory developed in §6 provides new insights to the nature ofbisimilarity, we believe, identifying the crucial roleof observation maps (k : X → Ω in Def. 3.1) inbisimulation notions.
As future work, we intend to accommodate modal
logics as is done in [23]. We are also interested inusing games with more complex winning conditions(e.g. parity); they have been used for (bi)simulation
notions for Büchi and parity automata [10]. Finally, we will pursue the algorithmic use of the current results.
References[ 1 ] Adámek, J., Herrlich, H., and Strecker, G.: Abstract and Concrete Categories, Wiley-Interscience,
New York, NY, USA, 1990.
[ 2 ] Baldan, P., Bonchi, F., Kerstan, H., and König,
B.: Coalgebraic Behavioral Metrics, Logical Methods in Computer Science, Vol. 14, No. 3(2018).
[ 3 ] Beyene, T. A., Chaudhuri, S., Popeea, C.,
and Rybalchenko, A.: A constraint-based approach
to solving games on inﬁnite graphs, The 41st
Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’14,
San Diego, CA, USA, January 20-21, 2014, Jagannathan, S. and Sewell, P.(eds.), ACM, 2014,
pp. 221–234.

[ 4 ] Bonchi, F., König, B., and Petrisan, D.: UpTo Techniques for Behavioural Metrics via Fibrations, 29th International Conference on Concurrency Theory, CONCUR 2018, September 47, 2018, Beijing, China, Schewe, S. and Zhang,L.(eds.), LIPIcs, Vol. 118, Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2018, pp. 17:1–
17:17.
[ 5 ] Bonchi, F., Petrisan, D., Pous, D., and Rot,
J.: Coinduction up-to in a ﬁbrational setting, Joint
Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and theTwenty-Ninth Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS), CSL-LICS ’14,
Vienna, Austria, July 14 - 18, 2014, Henzinger,
T. A. and Miller, D.(eds.), ACM, 2014, pp. 20:1–
20:9.
[ 6 ] Cuijpers, P. J. L. and Reniers, M. A.: Topological (Bi-)Simulation, Electr. Notes Theor. Comput.
Sci., Vol. 100(2004), pp. 49–64.
[ 7 ] Desharnais, J., Laviolette, F., and Tracol, M.:
Approximate Analysis of Probabilistic Processes:
Logic, Simulation and Games, 2008 Fifth International Conference on Quantitative Evaluation of
Systems, Sep. 2008, pp. 264–273.
[ 8 ] Desharnais, J., Gupta, V., Jagadeesan, R., andPanangaden, P.: Metrics for labelled Markov processes, Theoretical Computer Science, Vol. 318,
No. 3(2004), pp. 323 – 354.
[ 9 ] Ehlers, R. and Moldovan, D.: Sparse Positional Strategies for Safety Games, Proceedings
First Workshop on Synthesis, SYNT 2012, Berkeley, California, USA, 7th and 8th July 2012., Peled,
D. A. and Schewe, S.(eds.), EPTCS, Vol. 84, 2012,
pp. 1–16.
[10] Etessami, K., Wilke, T., and Schuller, R. A.:
Fair Simulation Relations, Parity Games, and StateSpace Reduction for Büchi Automata, SIAM J.
Comput., Vol. 34, No. 5(2005), pp. 1159–1175.
[11] Fijalkow, N., Klin, B., and Panangaden, P.:
Expressiveness of Probabilistic Modal Logics, Revisited, Procs. ICALP 2017, Leibniz International
Proceedings in Informatics (LIPIcs), Vol. 80, 2017,
pp. 105:1–105:12.
[12] Hasuo, I.: Generic weakest precondition semantics from monads enriched with order, Theor. Comput. Sci., Vol. 604(2015), pp. 2–29.
[13] Hasuo, I., Kataoka, T., and Cho, K.: Coinductive predicates and ﬁnal sequences in a ﬁbration, Mathematical Structures in Computer Science, Vol. 28, No. 4(2018), pp. 562–611.
[14] Hermida, C. and Jacobs, B.: Structural Induction and Coinduction in a Fibrational Setting, Inf.
Comput., Vol. 145, No. 2(1998), pp. 107–152.
[15] Herrlich, H.: Topological functors, General
Topology and its Applications, Vol. 4, No. 2(1974),
pp. 125 – 142.
[16] Hino, W., Kobayashi, H., Hasuo, I., and Ja-

cobs, B.: Healthiness from Duality, Proceedings ofthe 31st Annual ACM/IEEE Symposium on Logicin Computer Science, LICS ’16, New York, NY,
USA, July 5-8, 2016, Grohe, M., Koskinen, E., andShankar, N.(eds.), ACM, 2016, pp. 682–691.
[17] Jacobs, B.: Categorical Logic and Type Theory,
North Holland, Amsterdam, 1999.
[18] Jacobs, B.: Introduction to Coalgebra: Towards
Mathematics of States and Observation, Cambridge
Tracts in Theoretical Computer Science, Vol. 59,
Cambridge University Press, 2016.
[19] Joyal, A., Nielsen, M., and Winskel, G.: Bisimulation from open maps, Inf. Comput., Vol. 127,
No. 2(1996), pp. 164–185.
[20] Katsumata, S., Sato, T., and Uustalu, T.: Codensity Lifting of Monads and its Dual, Logical
Methods in Computer Science, Vol. 14, No. 4(2018).
[21] Komorida, Y., Katsumata, S., Hu, N., Klin,
B., and Hasuo, I.: Codensity Games for Bisimilarity, 34th Annual ACM/IEEE Symposium on Logicin Computer Science, LICS 2019, Vancouver, BC,
Canada, June 24-27, 2019, IEEE, 2019, pp. 1–13.
[22] Komorida, Y., ya Katsumata, S., Hu, N., Klin,
B., and Hasuo, I.: Codensity Games for Bisimilarity,
2019. Extended version with appendices, available
at arXiv.org.
[23] König, B. and Mika-Michalski, C.: (Metric)
Bisimulation Games and Real-Valued Modal Logics for Coalgebras, 29th International Conference
on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, 2018, pp. 37:1–37:17.
[24] Larsen, K. G. and Skou, A.:
Bisimulation through Probabilistic Testing, Inf. Comput.,Vol. 94, No. 1(1991), pp. 1–28.
[25] Milner, R.: Communication and Concurrency,
Prentice-Hall, 1989.
[26] Park, D.: Concurrency and Automata on
Inﬁnite Sequences, Proceedings of the 5th GIConference on Theoretical Computer Science, London, UK, UK, Springer-Verlag, 1981, pp. 167–183.
[27] Rutten, J. J. M. M.:
Universal Coalgebra: a Theory of Systems, Theor. Comp. Sci.,
Vol. 249(2000), pp. 3–80.
[28] Sangiorgi, D. and Rutten, J.(eds.): Advanced
Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science,
Cambridge University Press, 2011.
[29] Sprunger, D., Katsumata, S., Dubut, J., and Hasuo, I.: Fibrational Bisimulations and Quantitative
Reasoning, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop,
CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected
Papers, Cı̂rstea, C.(ed.), Lecture Notes in Computer
Science, Vol. 11202, Springer, 2018, pp. 190–213.
[30] Tix, R., Keimel, K., and Plotkin, G.: Semantic Domains for Combining Probability and NonDeterminism, Electronic Notes in Theoretical Com-puter Science, Vol. 222(2009), pp. 3 – 99.
[31] van Breugel, F., Mislove, M. W., Ouaknine,J., and Worrell, J.: An Intrinsic Characterizationof Approximate Probabilistic Bisimilarity, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS
2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS
2003, Warsaw, Poland, April 7-11, 2003, Proceedings, Gordon, A. D.(ed.), Lecture Notes in Computer Science, Vol. 2620, Springer, 2003, pp. 200–

215.
[32] Wilke, T.: Alternating tree automata, parity
games, and modal µ-calculus, Bull. Belg. Math. Soc.
Simon Stevin, Vol. 8, No. 2(2001), pp. 359–391.
[33] Wißmann, T., Dubut, J., Katsumata, S., andHasuo, I.: Path Category for Free, Foundationsof Software Science and Computation Structures,
Bojańczyk, M. and Simpson, A.(eds.), Cham,
Springer International Publishing, 2019, pp. 523–
540.