Codensity Games for Bisimilarity

TL;DR

This paper introduces a categorical framework for bisimilarity games that unifies and extends game characterizations of bisimilarity and its quantitative variants across various system types.

Contribution

It provides a formal fibrational and coalgebraic framework that derives codensity bisimilarity games, covering known and new bisimilarity notions.

Findings

Unified categorical framework for bisimilarity games

Derivation of codensity bisimilarity games

Applicability to both classical and quantitative systems

Abstract

Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various 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; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive 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).

Tables

Table 1. TABLE I: The Game for Probabilistic Bisimilarity from  [ 13 ]

position	player	possible moves
$(x,y)\in X^2$	S	$Z\subseteq X\text{ s.t. }c\left(x\right)\left(Z\right)\ne c\left(y\right)\left(Z\right)$
$Z\subseteq X$	D	$(x^{\prime },y^{\prime })\in X^2\text{ s.t. }{x}^{\prime }\in Z\wedge y^{\prime }\notin Z$

Table 2. TABLE II: The Game for (Probabilistic) Bisimulation Metric, Adapting  [ 13 ]

position	P	possible moves
$(x,y,\epsilon )$	S	$f:X\to [0,1]$
$\in X^2\times [0,1]$		such that $\left|E_{c\left(x\right)}\left[f\right]-E_{c\left(y\right)}\left[f\right]\right|>\epsilon$
$f:X\to [0,1]$	D	$(x^{\prime },y^{\prime },{\epsilon }^{\prime })\in X^2\times [0,1]$
		such that $\left|f\left(x^{\prime }\right)-f\left(y^{\prime }\right)\right|>{\epsilon }^{\prime }$

Table 3. TABLE III: The Game for Probabilistic Bisimilarity, from  [ 16 ]

position	pl.	possible moves
$(x,y,\epsilon )\in X^2\times [0,1]$	S	$(s,t)\in X^2$ s.t. $\{s,t\}=\{x,y\}$,
		and $f:X\to [0,1]$
$(s,t,f,\epsilon )\in$	D	$g:X\to [0,1]$ such that
$X^2\times {[0,1]}^X\times [0,1]$		$\max \{0,E_{c\left(s\right)}\left[f\right]-E_{c\left(t\right)}\left[g\right]\}\le \epsilon$
$(f,g,\epsilon )\in {\left({[0,1]}^X\right)}^2$	S	$(i,j)\in {\left({[0,1]}^X\right)}^2$ such that
		$\{i,j\}=\{f,g\}$, and $x^{\prime }\in X$
$(x^{\prime },i,j,\epsilon )\in$	D	$(x^{\prime },y^{\prime },{\epsilon }^{\prime })\in X^2\times [0,1]$ such that
$X\times {\left({[0,1]}^X\right)}^2\times [0,1]$		$i\left(x^{\prime }\right)\le j\left(y^{\prime }\right)$, and
		${\epsilon }^{\prime }=j\left(y^{\prime }\right)-i\left(x^{\prime }\right)$

Table 4. TABLE V: 𝐂𝐋𝐚𝐭 ⊓ subscript 𝐂𝐋𝐚𝐭 square-intersection \mathbf{CLat}_{\sqcap} -Fibrations

fibration	indistinguishability structure	decent map	$P⊑Q$	$⨅P_i$
$\mathrm{𝐓𝐨𝐩}\to \mathrm{𝐒𝐞𝐭}$	topology	continuous func.	$P\supseteq Q$	generated from $\bigcup P_i$
$\mathrm{𝐌𝐞𝐚𝐬}\to \mathrm{𝐒𝐞𝐭}$	$\sigma$-field	measurable func.	$P\supseteq Q$	generated from $\bigcup P_i$
${\mathrm{𝐏𝐌𝐞𝐭}}_1\to \mathrm{𝐒𝐞𝐭}$	pseudometric	non-expansive func.	$\forall x,y.P(x,y)\ge Q(x,y)$	$(x,y)\mapsto {sup}_i{P}_i(x,y)$
$\mathrm{𝐄𝐑𝐞𝐥}\to \mathrm{𝐒𝐞𝐭}$	endorelation	relation preserving func.	$P\subseteq Q$	$\bigcap P_i$
$\mathrm{𝐏𝐫𝐞}\to \mathrm{𝐒𝐞𝐭}$	preorder	monotone func.	$P\subseteq Q$	$\bigcap P_i$
$\mathrm{𝐄𝐪𝐑𝐞𝐥}\to \mathrm{𝐒𝐞𝐭}$	equivalence relation	relation preserving func.	$P\subseteq Q$	$\bigcap P_i$

Table 5. TABLE VII: Untrimmed Codensity Bisimilarity Game

position	pl.	possible moves
$P\in {𝔼}_X$	S	$k\in ℂ(X,\Omega )$ s.t.
		$\tau \circ Fk\circ c:(X,P)\dot{\nrightarrow }(\Omega ,𝛀)$
$k\in ℂ(X,\Omega )$	D	$P^{\prime }\in {𝔼}_X$ s.t. $k:(X,P^{\prime })\dot{\nrightarrow }(\Omega ,𝛀)$

Table 6. TABLE IX: Trimmed Codensity Bisimilarity Game

position	pl.	possible moves
$P\in 𝒢$	S	$k\in ℂ(X,\Omega )$ s.t.
		$\tau \circ Fk\circ c:(X,P)\dot{\nrightarrow }(\Omega ,𝛀)$
$k\in ℂ(X,\Omega )$	D	$P^{\prime }\in 𝒢$ s.t.
		$k:(X,P^{\prime })\dot{\nrightarrow }(\Omega ,𝛀)$

Table 7. TABLE X: Trimmed Codensity Bisimilarity Game with Multiple Observations

position	pl.	possible moves
$P\in 𝒢$	S	$A\in 𝔸$ and $k\in ℂ(X,{\Omega }_A)$ s.t.
		${\tau }_A\circ Fk\circ c:(X,P)\dot{\nrightarrow }({\Omega }_A,{𝛀}_A)$
$A\in 𝔸$ and	D	$P^{\prime }\in 𝒢$ s.t.
$k\in ℂ(X,{\Omega }_A)$		$k:(X,P^{\prime })\dot{\nrightarrow }({\Omega }_A,{𝛀}_A)$

Table 8. TABLE XI: Codensity Bisimilarity Game for Conventional Bisimilarity

position	pl.	possible moves
$(x,y)\in X\times X$	S	$k\in \mathrm{𝐒𝐞𝐭}(X,2)$ s.t.
		$\exists x^{\prime }\in c\left(x\right).k\left(x^{\prime }\right)=\top$
		$\iff ̸\exists y^{\prime }\in c\left(y\right).k\left(y^{\prime }\right)=\top$
$k\in \mathrm{𝐒𝐞𝐭}(X,2)$	D	$(x^{\prime \prime },y^{\prime \prime })$ s.t. $k\left(x^{\prime \prime }\right)\ne k\left(y^{\prime \prime }\right)$

Equations

$$c\colon(X,\,d_{(X,c)})\longrightarrow\bigl{(}\,\mathcal{D}_{\leq 1}X,\,\mathcal{K}(d_{(X,c)})\,\bigr{)}$$

$$\mathcal{K}(d_{(X,c)})(\mu ,\nu )=\underset{f}{\sup }\left|E_{\mu }[f]-E_{\nu }[f]\right|,$$

$$f:(X,P)\dot{\to }(Y,Q)⟺P⊑f^{\ast }Q⟺f_{\ast }P⊑Q$$

$$F^{\mathbf{\Omega},\tau}P=\bigsqcap_{k\in\mathbb{E}(P,\mathbf{\Omega})}\bigl{(}\tau\circ F\bigl{(}p(k)\bigr{)}\bigr{)}^{\ast}\mathbf{\Omega}.$$

$$[\mathbb{E},\mathbb{E}]\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\displaystyle\begin{array}[]{l}\forall k\colon X\to 2.~{}\bigl{(}\,(\forall(x,y)\in R.~{}k(x)=k(y))\bigr{.}\\ \bigl{.}\implies\bigl{(}(\exists x\in S.~{}k(x)=\top)\iff(\exists x\in T.~{}k(x)=\top)\bigr{)}\,\bigr{)}.\end{array}$$

$$\displaystyle\small\begin{array}[]{l}(\forall x\in S.~{}\exists y\in T.~{}(x,y)\in R)\wedge(\forall y\in T.~{}\exists x\in S.~{}(x,y)\in R).\end{array}$$

$$(\forall x\in S.\exists y\in T.(x,y)\in R^{\mathrm{eq}})\wedge$$

$$(\forall y\in T.\exists x\in S.(x,y)\in R^{\mathrm{eq}}),$$

$$\Phi_{c}^{\mathbf{\Omega},\tau}P=c^{\ast}(F^{\mathbf{\Omega},\tau}P),\text{ that is, }\bigsqcap_{k\in\mathbb{E}(P,\mathbf{\Omega})}\bigl{(}\tau\circ F(p(k))\circ c\bigr{)}^{\ast}\mathbf{\Omega}.$$

$$d_{x,y,r}(z,w)=\{\begin{array}{ll}0& z=w\\ r& \{z,w\}=\{x,y\}\\ 1& \text{otherwise.}\end{array}$$

$$(\forall f\in \mathbb{C}(S,X).f^{\ast }P=f^{\ast }Q)⟹P=Q.$$

$$\{f_{\ast }P|P\in \mathcal{G},f\in \mathbb{C}(S,X)\}.$$

$$G⊑H⟺\forall X\in \mathbb{E}.GX⊑HX(G,H\in \mathbf{Lift}(F,p)),$$

$$F^{\mathbf{\Omega },\tau }P$$

$$\displaystyle\text{that is, }\bigsqcap_{A\in\mathbb{A},k\in\mathbb{E}(P,\mathbf{\Omega}_{A})}\bigl{(}\tau_{A}\circ F(p(k))\bigr{)}^{\ast}(\mathbf{\Omega}_{A}).$$

$${\tau }_{\epsilon }(t,\rho )=t\text{and}{\tau }_a(t,\rho )=\rho (a).$$

$$\{x\in X\mid \text{w is accepted from x}\}\subseteq X,\text{for each }w\in {\Sigma }^{\ast }$$

$$\begin{array}[]{l}\{x\in X\mid\text{$w$ is accepted from $x$}\}\text{ and }\\ \{x\in X\mid\text{$w$ is not accepted from $x$}\},\quad\text{for each }w\in\Sigma^{*}.\end{array}$$

$$\mathbb{E}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\mathbf{EqRel}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{array}[]{rclll}\dot{\mathcal{P}}_{2}&=&\mathcal{P}^{\mathrm{Eq}_{2},\diamond}&:\mathbf{EqRel}\mathrel{\rightarrow}\mathbf{EqRel}&\text{(Example~{}\ref{ex:eqrelpowlift})},\\ \dot{\mathcal{P}}_{3}&=&\mathcal{P}^{\mathrm{Eq}_{2},\diamond}&:\mathbf{ERel}\mathrel{\rightarrow}\mathbf{ERel}&\text{(Example~{}\ref{ex:erelpowlift})}\end{array}$$

$$\displaystyle\small\begin{array}[]{rcl}(S,T)\in\dot{\mathcal{P}}_{1}(R)&\Longleftrightarrow&(\forall x\in S.~{}\exists y\in T.~{}(x,y)\in R)~{}\wedge\\ &&(\forall y\in T.~{}\exists x\in S.~{}(x,y)\in R).\end{array}$$

$$\displaystyle\footnotesize\begin{array}[]{ll}&(A_{\Sigma})^{\mathbf{\Omega},\tau}(R)=\\ &\left\{\begin{array}[]{l|l}\big{(}(t_{1},\rho_{1}),&\forall k\colon X\to 2.{}\\ (t_{2},\rho_{2})\big{)}&(\forall x,y\in X.~{}(x,y)\in R\Rightarrow k(x)=k(y))\\ \in(A_{\Sigma}X)^{2}&\Rightarrow(t_{1}=t_{2})\wedge\\ &(\forall a\in\Sigma.~{}(k\mathbin{\circ}\rho_{1})(a)=(k\mathbin{\circ}\rho_{2})(a))\end{array}\right\}.\end{array}$$

$${\mathbf{\Omega }}_{\epsilon }={\mathbf{\Omega }}_a={\mathrm{Eq}}_2,{\tau }_{\epsilon }(t,\rho )=t,{\tau }_a(t,\rho )=\diamond (\rho (a)).$$

$$\displaystyle\footnotesize\begin{array}[]{ll}&(N_{\Sigma})^{\mathbf{\Omega},\tau}(R)=\\ &\left\{\begin{array}[]{l|l}\big{(}(t_{1},\rho_{1}),&\forall k\colon X\to 2.{}\\ (t_{2},\rho_{2})\big{)}&(\forall x,y\in X.~{}(x,y)\in R\Rightarrow k(x)=k(y))\\ \in(N_{\Sigma}X)^{2}&\Rightarrow(t_{1}=t_{2})\wedge\\ &\qquad\big{(}\forall a\in\Sigma.~{}\top\in(k\mathbin{\circ}\rho_{1})(a)\\ &\qquad\quad\Leftrightarrow\top\in(k\mathbin{\circ}\rho_{2})(a)\big{)}\end{array}\right\}.\end{array}$$

$$\displaystyle\small\forall r\in[0,1].~{}\forall k\colon X\to 2.~{}\bigl{(}(\forall(x,y)\in R.~{}k(x)=k(y))\bigr{.}$$

$$\displaystyle\small\textstyle\qquad\bigl{.}\implies\bigl{(}\sum_{x\in k^{-1}(\top)}p(x)\geq r\Leftrightarrow\sum_{x\in k^{-1}(\top)}q(x)\geq r\bigr{)}\bigr{)}.$$

$$\bar{Z}=\{w\in X\mid \exists v\in Z\text{mbox}s.t.DuplicatorwinsTable\text{ref}table:probabilisticBisimGameIntroFKPfrom(v,w)\}.$$

$$\tau (x,Z)\le \tau (x,\bar{Z})\text{mbox}and\tau (y,Z)\le \tau (y,\bar{Z}).$$

$$\tau (x,\bar{Z})=\tau (y,\bar{Z}).$$

$$\tau (x,Z)\le \tau (y,\bar{Z})\text{mbox}and\tau (y,Z)\le \tau (x,\bar{Z}),$$

Full text

In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive 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).

††publicationid: pubid: 978-1-7281-3608-0/19/$31.00 ©2019 IEEE

I Introduction

I-A Bisimilarity Notions and Games

Since the seminal works by Park and Milner [1, 2], 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 observation-oriented view on process semantics. Bisimilarity is usually defined as the largest bisimulation, which is a binary relation that satisfies a suitable mimicking condition. In fact, a bisimulation $R$ can be characterized as a post-fixed point $R\subseteq\Phi(R)$ using a suitable relation transformer $\Phi$; from this we obtain that bisimilarity is the greatest fixed point of $\Phi$ by the Knaster–Tarski theorem. This order-theoretic foundation is the basis of a variety of advanced techniques for reasoning about (or using) bisimilarity, such as bisimulation up-to—see, e.g., [3].

Bisimilarity is conventionally defined for state-based 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 been energetically sought in the literature. One notable example is the bisimulation notion for probabilistic systems in [4]: 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 [5]. It replaces a relation with a metric that is induced by the probabilistic transition structure.

There is a body of literature (including [6, 7, 8, 9, 10, 11, 12]) that aims to identify the mathematical essences that are shared by this variety of bisimilarity, and express the identified essences in a rigorous manner using category theory. Our particular interest is in the correspondence between bisimilarity notions and (safety) games; three examples of which are given below. This interest in bisimilarity games is shared by the recent work [10], and the comparison is discussed in §I-D.

I-A1 Bisimilarity Games

It is well-known that the following game characterizes the conventional notion of bisimilarity between Kripke frames. Let $(X,{\to})$ be a Kripke frame where ${\to}\subseteq X^{2}$; the game is played between Duplicator (D) and Spoiler (S). In a position $(x_{1},x_{2})$, Spoiler challenges Duplicator’s claim that $x_{1}$ and $x_{2}$ are bisimilar, by choosing one of the states (say $x_{1}$) and further choosing a transition $x_{1}\to x_{1}^{\prime}$. Duplicator responds by choosing a transition $x_{2}\to x_{2}^{\prime}$ from the other state, and the game is continued from $(x_{1}^{\prime},x_{2}^{\prime})$. Duplicator wins if Spoiler gets stuck, or the game continues infinitely long, and this witnesses that $x_{1}$ and $x_{2}$ are bisimilar.

I-A2 Games for Probabilistic Bisimilarity

A recent step forward in the topic of bisimilarity and games is the characterization of probabilistic bisimulation introduced in [13]. 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\colon X\to\mathcal{D}_{\leq 1}X$ is a transition kernel that assigns to each state $x\in X$ a probability subdistribution $c(x)\in\mathcal{D}_{\leq 1}X$. Here $\mathcal{D}_{\leq 1}X=\{d\colon X\to[0,1]\mid\sum_{x\in X}d(x)\leq 1\}$ denotes the set of probability subdistributions over $X$. For $Z\subseteq X$, let $c(x)(Z)$ denote the probability with which a successor of $x$ is chosen from $Z$; that is, $c(x)(Z)=\sum_{x^{\prime}\in Z}c(x)(x^{\prime})$. Since $c(x)$ is only a sub-distribution over $X$, the probability $c(x)(X)$ is $\leq 1$ rather than $=1$. The remaining probability $1-c(x)(X)$ can be thought of as the probability of $x$ getting stuck.

Recall from [4] that an equivalence relation $R\subseteq X^{2}$ is a (probabilistic) bisimulation if, for any $(x,y)\in R$ and each $R$-closed subset $Z\subseteq X$, $c(x)(Z)=c(y)(Z)$ holds.

The game introduced in [13] is in Table I. It is shown in [13] that Duplicator is winning in the game at $(x,y)$ if and only if $x$ and $y$ are bisimilar, in the sense of [4] (recalled above). It is not hard to find an intuitive correspondence between the game in Table I and the definition of bisimulation [4]: 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 by claiming that $Z$ is in fact not bisimilarity-closed, exhibiting a pair of states $(x^{\prime},y^{\prime})$ that Duplicator claims are bisimilar.

I-A3 Games for Probabilistic Bisimulation Metric

Our following observation marked the beginning of the current work: the game for (qualitative) bisimilarity for probabilistic systems (from [13], Table I) can be almost literally adapted to (quantitative) bisimulation metric for probabilistic systems. This metric was first introduced in [5].

For simplicity we focus on the discrete setting; we also 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)}\colon X^{2}\to[0,1]$ is defined to be the smallest pseudometric (with respect to the pointwise order) that makes the transition kernel

[TABLE]

non-expansive with respect to the specified pseudometrics. Here $\mathcal{K}(d_{(X,c)})$ is the so-called Kantorovich metric over $\mathcal{D}_{\leq 1}X$ induced by the pseudometric $d_{(X,c)}$ over $X$. It is defined as follows. For $\mu,\nu\in\mathcal{D}_{\leq 1}X$,

[TABLE]

where in the above sup, $f$ ranges over all non-expansive functions from $(X,d_{(X,c)})$ to \bigl{(}[0,1],d_{[0,1]}\bigr{)}, $d_{[0,1]}$ denotes the usual Euclidean metric, and $E_{\mu}[f]$ is the expectation $\sum_{x\in X}f(x)\cdot\mu(x)$ of $f$ with respect to $\mu$.

Our observation is that the bisimulation metric $d_{(X,c)}$ is characterized by the game in Table II: Duplicator is winning at $(x,y,\varepsilon)$ if and only if $d_{(X,c)}(x,y)\leq\varepsilon$.

The game seems to be new, although its intuition is similar to the one for Table I. Note that the formula (1) appears in the condition of Spoiler’s moves. Spoiler challenges by exhibiting a “predicate” $f$ that suggests violation of the non-expansiveness of $c$; and Duplicator makes a counterargument that $f$ is in fact not non-expansive and thus invalid.

I-A4 Towards a Unifying Framework

The last two games (Table I from [13] and Table II 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 ($Z$ and $f$ respectively), and the predicates usable in those observations are subject to certain preservation properties (bisimilarity-closedness in the former, and non-expansiveness in the latter).

I-B A Codensity-Based Framework for Bisimilarity and Games

The main contribution of the current paper is a categorical framework that derives a variety of bisimilarity notions and corresponding game notions. The correspondence is proved once and for all on the categorical level of generality. It covers the three examples introduced earlier in §I-A, much like the recent categorical framework in [10] does. However, our fibration-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 [14] and [15]. In [14] a general construction called codensity lifting is introduced: given a fibration $p:\mathbb{E}\rightarrow\mathbb{C}$ and parameters $(\mathbf{\Omega},\tau)$ that embody the kind of observations we can make, a functor $F\colon\mathbb{C}\to\mathbb{C}$ is lifted to $F^{\mathbf{\Omega},\tau}\colon\mathbb{E}\to\mathbb{E}$. In [15], codensity lifting is used to introduce a generic family of bisimulation notions called codensity bisimilarity—see \small2⃝. In this paper, we extend these previous results by

• •

introducing the notion of codensity bisimilarity game (\small1⃝) that comes in two variants (untrimmed (§IV) and trimmed (§V)),

• •

establishing the correspondence between codensity bisimulations (\small2⃝) and games (\small1⃝) on a fibrational level of generality, and

• •

working out several concrete examples (\small4⃝, \small5⃝).

In general, devising a game notion (\small4⃝) directly from a bisimilarity notion (\small5⃝) is far from trivial. Indeed, doing so for an individual bisimilarity notion has itself been deemed a scientific novelty [16, 13]. Our codensity-based framework (in the left half of Fig. 1) can automate part of this process in the following precise sense.

We derive concrete notions of bisimilarity (\small5⃝) and bisimilarity game (\small4⃝) as instances; then the correspondence between the two is guaranteed by the categorical general result between \small1⃝ and \small2⃝.

We note, however, that this is no panacea. When one starts with a given concrete notion of bisimilarity (\small5⃝), their next task would be to identify the right choice of the parameters $\mathbb{E}\xrightarrow{p}\mathbb{C},\mathbf{\Omega},\tau$ for the codensity lifting (\small3⃝). This task is not easy in general: we needed to get our hands dirty working out the examples in this paper, [14], and [15]. Nevertheless, we believe that the required passage from \small5⃝ to \small3⃝ is much easier than the direct derivation from \small5⃝ to \small4⃝, with our categorical framework providing templates of bisimilarity games (see Tables VIII, IX and X). After all, our framework identifies which part of the path from \small5⃝ to \small4⃝ can be automated, and which part remains to be done individually. This is much like what many other categorical frameworks offer, as meta-level theories.

As an additional benefit, our categorical framework can be used to discover new bisimilarity notions (\small5⃝), starting from (choices of parameters for) \small3⃝. We believe those derived new bisimilarity notions are useful, since our categorical theory embodies sound intuitions about observation, predicate transformation, and indistinguishability—see e.g. §II-B.

I-C Contributions

Our main technical contributions are as follows.

• •

We introduce a categorical framework that uniformly describes various bisimulation notions (including metrics, preorders and topologies) and the corresponding game notions (Fig. 1). The framework is based on coalgebras, fibrations, and codensity liftings in particular [14]. Our general game notion comes in two variants.

• –

The first (the untrimmed codensity game: §IV) arises naturally in a fibration, using its objects and arrows as possible moves. The untrimmed game is theoretically clean, but it tends to have a huge arena.

• –

We therefore introduce a method that restricts these arenas, leading to the (trimmed) codensity bisimilarity game (§V). The reduction method is also described in general fibrational terms, specifically using fibered separators and generating sets.

• •

From the general framework, we derive several concrete examples of bisimilarity and its related notions (\small4⃝ and \small5⃝ in Fig. 1). They are listed in Table VI. Among them, a few bisimilarity notions seem new (especially the bisimulation topology examples), and several game notions also seem new.

• •

We discuss the transfer of codensity bisimilarity by suitable fibered functors (§VII). As an example usage, we give an abstract proof of the fact that (usual) bisimilarity for Kripke frames is necessarily an equivalence (Example VII.2).

• •

Additionally, we conduct investigations of the game notion in [13] (Table I) in concrete, non-categorical terms. For one, we obtain its variation for bisimulation metric (as we showed in Table II). We also give a direct proof of the equivalence to another game notion for probabilistic bisimilarity, previously introduced in [16], by exhibiting a mutual translation of winning strategies (Appendix -A).

I-D Related Work

Besides the one in [13], another game characterization of probabilistic bisimulation has been given in [16]. It is described later in §II (Table IV). The latter game has a bigger arena than the one in [13]: in [16] both players have to play a subset $Z\subseteq X$, while in [13] only Spoiler does so.

The work that is the closest to ours is the recent work [10] that studies bisimilarity games in a categorical setting. Their formalization uses (co)algebras (following the (co)algebraic generalization of the Kantorovich metric introduced in [8]), and therefore embraces a variety of different branching types. The major differences between the two works are as follows.

• •

Our current work is fibration-based (in particular $\mathbf{CLat}_{\sqcap}$-fibrations), while [10] is not. As a consequence, ours accommodates an additional dimension of generality by changing fibrations, which correspond to different indistinguishability notions (relation, metric, topology, preorder, measurable structures, etc.). In contrast, the works [10] and [8] deal exclusively with two settings: binary relations and pseudometrics.

• •

A relationship to modal logic is beautifully established in [10], while it is not done in this work. We expect our fibrational framework can accommodate modal logic too: fibrations have been used for categorical modeling of logics [17]. We leave this aspect to future work.

• •

The categorical generalization [10] is based on the game notion in [16], while ours is based on that in [13]. Therefore, for some bisimulation notions (including the bisimulation metric), we obtain a game notion with a smaller arena. Compare Table II (an instance of ours) and Table IV (an instance of [10]).

There are a number of categorical studies of bisimilarity notions; notable mentions include open map-based approaches [18] and coalgebraic ones [19, 20]. The fibrational approach we adopt also uses coalgebras; it was initiated in [6] and pursued, e.g., in [11, 7, 9], and [15]. For example, in the recent work [11], fibrational generality is exploited to study up-to techniques for bisimilarity metric. They use the Wasserstein lifting of functors introduced in [8] instead of the codensity lifting that we use (it generalizes the Kantorovich lifting in [8], see Example III.4). It is known [8] that the Wasserstein and Kantorovich liftings can differ in general, while they coincide for some specific functors such as the distribution functor.

Some of our new examples are topological: we derive what we call bisimulation topology and a game notion that characterizes it. The relation between these notions and the existing works on bisimulation and topology (including [21, 22]) is left as future work.

I-E Organization

In §II, we present preliminaries on a general theory of games (we can restrict to safety games), and on fibrations. For the latter, we focus on a class called $\mathbf{CLat}_{\sqcap}$-fibrations, and argue that they offer an appropriate categorical abstraction of sets equipped with indistinguishability structures. In §III, we present codensity lifting and codensity bisimilarity (\small2⃝, \small3⃝ in Fig. 1). The material is based on [15], but we introduce some auxiliary notions needed for the correspondence with games. Our first game notion (the untrimmed one) is introduced in §IV; in §V, we cut down the arenas and obtain trimmed codensity bisimilarity game. The theory is further extended in §VI–VII: in §VI we accommodate multiple observation domains, and in §VII we discuss the transfer of codensity bisimilarities by full-faithful fibered functors preserving meets. These categorical observations give rise to the concrete examples in §VIII.

Some proofs and details are deferred to Appendix -A.

II Preliminaries

We write $\mathcal{P}\colon\mathbf{Set}\to\mathbf{Set}$ for the covariant powerset functor, and $2$ for the two-point set $2=\{\bot,\top\}$. We define the function $\diamond:\mathcal{P}2\mathrel{\rightarrow}2$ called may-modality by $\diamond S=\top$ if and only if $\top\in S$. We write $\mathrm{Eq}_{I}$ for the diagonal (equality) relation over a set $I$.

II-A 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 infinite play is won by the same player (namely Duplicator). This winning condition reflects the characterization of bisimilarity-like notions by suitable greatest fixed points; the correspondence generalizes, for example, to the one between parity games and nested alternating fixed points—see [23]. The term “safety game” occurs, e.g., in [24, 25].

Safety games are played between two players; in this paper, they are called Duplicator (D) and Spoiler (S). We restrict to those games in which Duplicator and Spoiler alternate turns.

Definition II.1** (safety game).**

A (safety game) arena is a triple $\mathcal{G}=(Q_{\text{D}},Q_{\text{S}},E)$ of a set $Q_{\text{D}}$ of Duplicator’s positions, a set $Q_{\text{S}}$ of Spoiler’s positions, and a transition relation $E\subseteq(Q_{\text{D}}\times Q_{\text{S}})\cup(Q_{\text{S}}\times Q_{\text{D}})$. Hence $\mathcal{G}$ is a bipartite graph. We require that $Q_{\text{D}}$ and $Q_{\text{S}}$ are disjoint, and that $Q_{\text{D}}\cup Q_{\text{S}}\neq\emptyset$. We write $Q=Q_{\text{D}}\cup Q_{\text{S}}$.

For a position $q\in Q$, the elements of the set $\{q^{\prime}\in Q\mid(q,q^{\prime})\in E\}$ are called the possible moves at $q$. Unlike some works, we allow positions that have no possible moves at them.

A play in an arena $\mathcal{G}=(Q_{\text{D}},Q_{\text{S}},E)$ is a (finite or infinite) sequence of positions $q_{0}q_{1}\dotsc$, such that $(q_{i-1},q_{i})\in E$ so long as $q_{i}$ belongs to the sequence.

A play in $\mathcal{G}$ is won by either player, according to the following conditions: 1) a finite play $q_{0}\dotsc q_{n}$ is won by Spoiler (or by Duplicator) if $q_{n}\in Q_{\text{D}}$ (or $q_{n}\in Q_{\text{S}}$ respectively); and 2) every infinite play $q_{0}q_{1}\dotsc$ is won by Duplicator.

Definition II.2** (strategy, winning position).**

In an arena $\mathcal{G}=(Q_{\text{D}},Q_{\text{S}},E)$, a strategy of Duplicator is a partial function $\sigma_{\text{D}}\colon Q^{*}\times Q_{\text{D}}\rightharpoonup Q_{\text{S}}$; we require that $\sigma_{\text{D}}(\vec{q}q)=q^{\prime}$ implies $(q,q^{\prime})\in E$. A strategy of Spoiler is defined similarly, as a partial function $\sigma_{\text{S}}\colon Q^{*}\times Q_{\text{S}}\rightharpoonup Q_{\text{D}}$ that returns a possible move at the last position in the history.

Given an initial position $q\in Q$ and two strategies $\sigma_{\text{D}}$ and $\sigma_{\text{S}}$ for Duplicator and Spoiler respectively, the play from $q$ induced by $(\sigma_{\text{D}},\sigma_{\text{S}})$ is defined in a natural inductive manner. The induced play is denoted by $\pi^{\sigma_{\text{D}},\sigma_{\text{S}}}(q)$.

A position $q\in Q$ is said to be winning for Duplicator if there exists a strategy $\sigma_{\text{D}}$ of Duplicator such that, for any strategy $\sigma_{\text{S}}$ of Spoiler, the induced play $\pi^{\sigma_{\text{D}},\sigma_{\text{S}}}(q)$ is won by Duplicator.

In what follows, for simplicity, we restrict the initial position $q$ of a play $\pi^{\sigma_{\text{D}},\sigma_{\text{S}}}(q)$ to be in $Q_{\text{S}}$. (Note that Spoiler’s position can be winning for Duplicator.)

Winning positions of safety games are witnessed by invariants (Prop. II.4), which is a well-known fact.

Definition II.3** (invariant).**

Let $\mathcal{G}=(Q_{\text{D}},Q_{\text{S}},E)$ be an arena. A subset $P\subseteq Q_{\text{S}}$ is called an invariant for Duplicator if, for each $q\in P$ and any possible move $q^{\prime}\in Q_{\text{D}}$ at $q$, there exists a possible move $q^{\prime\prime}$ at $q^{\prime}$ that is in $P$. That is, \forall q\in P.\,\forall q^{\prime}\in Q_{\text{D}}.\,\bigl{(}\,(q,q^{\prime})\in E\;\Rightarrow\;\exists q^{\prime\prime}\in Q_{\text{S}}.\,\,(q^{\prime},q^{\prime\prime})\in E\land q^{\prime\prime}\in P\,\bigr{)}.

Proposition II.4**.**

Any position $q\in P$ in an invariant $P$ for Duplicator is winning for Duplicator. 2. 2.

Invariants are closed under arbitrary union. Therefore, there exists a largest invariant for Duplicator. 3. 3.

The largest invariant for Duplicator coincides with the set of winning positions for Duplicator in $Q_{\text{S}}$. ∎

Examples of safety games have been given in Tables I–II. We present two other examples (Tables IV–IV).

Example II.5** (alternative games for probabilistic bisimilarity and bisimulation metric).**

In [16], a game notion that characterizes (qualitative) probabilistic bisimilarity is presented. It is in Table IV, presented in a slightly adapted form.

This game notion is categorically generalized in [10]; the generalization has freedom in the choice of coalgebra functors (i.e. branching types), as well as in the choice between relations and metrics. The instance of this general game notion for bisimulation metric is shown in Table IV.

The two games (Tables IV–IV) characterize the same bisimilarity-like notions as the games in Tables I–II, 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 for probabilistic bisimilarity. See Appendix -A.

We note that the game in Table II (an instance of our current framework) is simpler than Table IV (an instance of [10]). Table II is not only structurally simpler (it has fewer rows), but its set of moves are smaller too, asking for functions $X\to[0,1]$ only at one place.

Our categorical framework based on codensity liftings (presented in later sections) covers Tables I–II but not Tables IV–IV. Accommodation of the latter two is future work.

II-B *

$\mathbf{CLat}_{\sqcap}$-fibrations *

II-B1 Definition and Properties

Here we sketch a basic theory of fibrations—see, e.g., [17] for a comprehensive account. In particular, we focus on a class of poset fibrations called $\mathbf{CLat}_{\sqcap}$-fibrations. We observe that the simple axiomatics of the class adequately capture all the examples of interest—and hence the mathematical essences of the logical phenomena that we wish to model.

Our exposition here is largely based on that in [15]. However, in this paper we introduce new notation and terminology (such as indistinguishability order and decent map)—see §II-B2. They help to further clarify the intuitions.

A formal definition is as follows. (See Appendix -B for a rather gentle introduction to $\mathbf{CLat}_{\sqcap}$-fibration.)

Definition II.6** ($\mathbf{CLat}_{\sqcap}$-fibration).**

A $\mathbf{CLat}_{\sqcap}$-fibration is a fibration $p:\mathbb{E}\rightarrow\mathbb{C}$ such that each fiber $\mathbb{E}_{X}$ (for each $X\in\mathbb{C}$) is a complete lattice, and each pullback functor $f^{*}\colon\mathbb{E}_{Y}\to\mathbb{E}_{X}$ (for each $f\colon X\to Y$ in $\mathbb{C}$) preserves all meets $\bigsqcap$.

Via the Grothendieck construction, a $\mathbf{CLat}_{\sqcap}$-fibration is in a bijective correspondence with a functor $F_{\mathbb{E}}\colon\mathbb{C}^{\mathrm{op}}\to\mathbf{CLat}_{\sqcap}$, where $\mathbf{CLat}_{\sqcap}$ is the category of complete lattices and functions preserving all meets—see [17] and [7], as well as Appendix -B. The functor $F_{\mathbb{E}}$ assigns

• •

a complete lattice $\mathbb{E}_{X}$ (called the fiber over $X$) to each $X\in\mathbb{C}$, and

• •

a function $f^{*}\colon\mathbb{E}_{Y}\to\mathbb{E}_{X}$ preserving all meets to each $f\colon X\to Y$ in $\mathbb{C}$. The map $f^{*}$ is called a pullback; it is also called a pullback functor since, in the general theory of fibrations, a fiber $\mathbb{E}_{X}$ is a category rather than a poset.

Although the indexed category presentation $F_{\mathbb{E}}\colon\mathbb{C}^{\mathrm{op}}\to\mathbf{CLat}_{\sqcap}$ may be more intuitive at first, we shall stick to the fibration presentation $p:\mathbb{E}\rightarrow\mathbb{C}$ since we will eventually need some global structures in the total category $\mathbb{E}$. It turns out that $\mathbf{CLat}_{\sqcap}$-fibrations are special kinds of topological functor [26] such that each fiber category is a poset. Topological functors are a well-studied topic, and many examples and results are available; a good summary is found in [27].

The use of poset fibrations is common in categorical modeling of logics [7, 9]. $\mathbf{CLat}_{\sqcap}$-fibrations additionally require fibered small meets; this simple assumption turns out to be a mathematically powerful one.

Proposition II.7**.**

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration.

$p$* is split, and faithful as a functor.* 2. 2.

Each arrow $f\colon X\to Y$ has its pushforward $f_{*}\colon\mathbb{E}_{X}\to\mathbb{E}_{Y}$, so that an adjunction $f_{*}\dashv f^{*}$ is formed. This is a consequence of Freyd’s adjoint functor theorem; it makes $p$ a bifibration **[17]**. 3. 3.

$p^{\mathrm{op}}\colon\mathbb{E}^{\mathrm{op}}\to\mathbb{C}^{\mathrm{op}}$* is also a $\mathbf{CLat}_{\sqcap}$-fibration.* 4. 4.

The change-of-base **[17, Lemma 1.5.1]** of $p$ along any functor $H:\mathbb{D}\mathrel{\rightarrow}\mathbb{C}$ is also a $\mathbf{CLat}_{\sqcap}$-fibration. 5. 5.

If $\mathbb{C}$ is (co)complete, then the total category $\mathbb{E}$ is also (co)complete. This follows from **[17, Prop. 9.2.1]**.∎

II-B2 Notation, Terminology and Intuitions

Our view of a $\mathbf{CLat}_{\sqcap}$-fibration $p:\mathbb{E}\rightarrow\mathbb{C}$ is that it equips objects of $\mathbb{C}$ with what we call indistinguishability structures. This suits our purpose, since various bisimilarity-like notions are all about degrees of indistinguishability between (the behaviors of) states of a system. We present examples later in §II-B3.

Notation II.8** (indistinguishability predicate/order).**

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration. An object $P\in\mathbb{E}_{X}$ in the fiber category $\mathbb{E}_{X}$ (i.e. an element of the complete lattice $\mathbb{E}_{X}$) is called an indistinguishability predicate over $X$. Our view is that $P$ is an additional structure on $X$; therefore, as a convention, an object $P\in\mathbb{E}_{X}$ shall also be denoted by $(X,P)\in\mathbb{E}_{X}$.

Each fiber $\mathbb{E}_{X}$ is a complete lattice; its order is denoted by $\sqsubseteq$ and called the indistinguishability order over $X$. Intuitively, $P\sqsubseteq Q$ means that $Q$ has a greater degree of indistinguishability than $P$—that is, $Q$ is coarser than $P$, and $P$ is more discriminating than $Q$.

The supremum and infimum with respect to the indistinguishability order $\sqsubseteq$ are denoted by $\bigsqcup$ and $\bigsqcap$ respectively.

Definition II.9** (decent map).**

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration, $f\colon X\to Y$ be an arrow in $\mathbb{C}$, $(X,P)\in\mathbb{E}_{X}$ and $(Y,Q)\in\mathbb{E}_{Y}$ be objects in the fibers. We say that $f$ is decent (from $P$ to $Q$) if there exists a necessarily unique arrow $\dot{f}\colon P\mathrel{\rightarrow}Q$ in $\mathbb{E}$ such that $p\dot{f}=f$. We write $f\colon(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}(Y,Q)$ in this case. The following equivalences follow.

[TABLE]

We write $f\colon(X,P)\mathrel{\dot{\nrightarrow}}(Y,Q)$ if $f$ is not decent.

The notion of decency is a fibered generalization of continuity, non-expansiveness, relation-preservation, etc. Decency $f\colon(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}(Y,Q)$ means $f$ respects indistinguishability, carrying $P$-indistinguishable elements to $Q$-indistinguishable ones.

II-B3 Examples

As shown in Table VI, various well-known categories can be seen as categories that equip sets with certain indistinguishability structures. The evident forgetful functors from the total categories ($\mathbf{Top}$, $\mathbf{Meas}$, etc.) to $\mathbf{Set}$ in Table VI are all $\mathbf{CLat}_{\sqcap}$-fibrations.

Specifically, $\mathbf{Top}$ is the category of topological spaces and continuous maps; $\mathbf{Meas}$ is that of measurable spaces and measurable maps; $\mathbf{PMet}_{1}$ is that of $1$-bounded pseudometric spaces (where a pseudo-metric is a metric without the condition $d(x,y)=0\Rightarrow x=y$) and non-expansive maps; $\mathbf{ERel}$ is that of sets with endorelations $(X,R\subseteq X^{2})$ and relation-preserving maps; $\mathbf{Pre}$ is that of preordered sets and monotone maps; and $\mathbf{EqRel}$ is that of sets with equivalence relations and relation-preserving maps—see [15] for details.

Note that, in $\mathbf{Top}$ and $\mathbf{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 from the union of the family.

Another class of examples is given as follows: for any well-powered category $\mathbb{B}$ admitting small limits, the subobject fibration of $\mathbb{B}$ is a $\mathbf{CLat}_{\sqcap}$-fibration. All the algebraic categories over $\mathbf{Set}$ and Grothendieck topoi fall into this class. On the other hand, the forgetful functors from algebraic categories over $\mathbf{Set}$ are rarely ($\mathbf{CLat}_{\sqcap}$-)fibrations.

III Codensity Bisimilarity

We introduce codensity lifting (\small3⃝ in Fig. 1) and codensity bisimilarity (\small2⃝) based on [15]. These turn out to subsume many bisimilarity-like notions in the literature. The material in §III-A–III-B is largely from [15]; §III-C is new, paving the way to codensity bisimilarity games presented in later sections.

III-A Codensity Lifting

Definition III.1** **(codensity lifting $F^{\mathbf{\Omega},\tau}$

[15]).

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration, and $F:\mathbb{C}\rightarrow\mathbb{C}$ be a functor. A parameter of codensity lifting of $F$ along $p$ is a pair of

• •

a $\mathbb{C}$-arrow $\tau:F\Omega\rightarrow\Omega$ (i.e. an $F$-algebra) called modality [29, 30] and

• •

an $\mathbb{E}$-object $\mathbf{\Omega}$ above $\Omega$ called observation domain.

The codensity lifting of $F\colon\mathbb{C}\rightarrow\mathbb{C}$ with parameter $(\mathbf{\Omega},\tau)$ is the endofunctor $F^{\mathbf{\Omega},\tau}:\mathbb{E}\mathrel{\rightarrow}\mathbb{E}$ defined as follows. On objects,

[TABLE]

Its action on arrows is as follows. It is not hard to see that, for each arrow $l:P\mathrel{\rightarrow}Q$ in $\mathbb{E}$, the arrow $F(p(l))$ is decent from $F^{\mathbf{\Omega},\tau}P$ to $F^{\mathbf{\Omega},\tau}Q$. Then we define $F^{\mathbf{\Omega},\tau}l\colon F^{\mathbf{\Omega},\tau}P\to F^{\mathbf{\Omega},\tau}Q$ to be the unique arrow in $\mathbb{E}$ above $F(p(l))$.

An alternative description is possible. When $\mathbb{E}$ has powers $\pitchfork$ and $p$ preserves them, $F^{\mathbf{\Omega},\tau}$ is characterized as the following pullback in the fibration $[\mathbb{E},p]:[\mathbb{E},\mathbb{E}]\rightarrow[\mathbb{E},\mathbb{C}]$:

[TABLE]

where $\alpha_{P}=\langle\tau\circ F(p(k))\rangle_{k\in\mathbb{E}(P,\mathbf{\Omega})}$ is the tupling. A similar characterization of codensity liftings of monads is in [14].

Table VI lists concrete examples of codensity liftings, with various fibrations $p$, functors $F$, and parameters $(\mathbf{\Omega},\tau)$. Some of them coincide with known notions. For example, the entry VI of the table says that the functor $(\mathcal{D}_{\leq 1})^{\mathbf{\Omega},\tau}$, with the designated $\mathbf{\Omega}$ and $\tau$, carries a metric space $(X,d)$ to the set $\mathcal{D}_{\leq 1}X$ equipped with the well-known Kantorovich metric $\mathcal{K}(d)$ induced by $d$—see (1).

Besides the functors listed in the table, there are some natural ways to systematically lift polynomial functors, by defining $\tau\colon F\Omega\to\Omega$ in an inductive manner—see, e.g., [11].

Example III.2**.**

Let us closely look at the entry VI of Table VI. There we codensity-lift the covariant powerset functor $\mathcal{P}$ along the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{EqRel}\rightarrow\mathbf{Set}$. We use the parameter $((2,\mathrm{Eq}_{2}),\diamond)$, where $\diamond:\mathcal{P}2\mathrel{\rightarrow}2$ is the modality given in §II.

We shall abbreviate $(2,\mathrm{Eq}_{2})$ by $\mathrm{Eq}_{2}$—a notational convention that is used throughout the paper.

Then $\mathcal{P}^{\mathrm{Eq}_{2},\diamond}(X,R)$ relates $S,T\in\mathcal{P}X$ if and only if

[TABLE]

Straightforward calculation shows that this is equivalent to

[TABLE]

This lifting is the restriction of the standard relational lifting of $\mathcal{P}$ along $\mathbf{ERel}\rightarrow\mathbf{Set}$, which is used for the usual bisimulation notion for Kripke frames, to $\mathbf{EqRel}$.

Example III.3**.**

In the entry VI of Table VI, we codensity-lift $\mathcal{P}$ along the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{ERel}\rightarrow\mathbf{Set}$ (instead of $\mathbf{EqRel}\rightarrow\mathbf{Set}$) with the parameter \bigl{(}(2,\mathrm{Eq}_{2}),\diamond\bigr{)}.

The characterization of $\mathcal{P}^{\mathrm{Eq}_{2},\diamond}(X,R)$ is slightly involved. Its relation part relates $S,T\in\mathcal{P}X$ if and only if

[TABLE]

where $R^{\mathrm{eq}}$ denotes the equivalence closure of $R$.

It is not clear at this stage whether the codensity bisimilarities induced by the above liftings (Examples III.2–III.3, i.e. the entries VI & VI of Table VI) coincide with the usual bisimilarity notion for Kripke frames. This is because of the involvement of mandatory equivalence closures—specifically by the use of $\mathbf{EqRel}$ in Example III.2, and by the occurrence of $(\underline{\phantom{n}}\,)^{\mathrm{eq}}$ in Example III.3. Later, in VII.2, we prove that both of the codensity bisimilarities indeed coincide with the usual bisimilarity notion. The proof relies crucially on transfer of codensity liftings via fibered functors.

Example III.4**.**

Here we follow [15, Example 3] and show that codensity lifting generalizes the Kantorovich lifting of functors introduced in [8]. Take $\mathbf{PMet}_{1}\rightarrow\mathbf{Set}$ as the $\mathbf{CLat}_{\sqcap}$-fibration $p$ in Def. III.1. As $\mathbf{\Omega}$, we take $\Omega=[0,1]$ with the usual Euclidean metric $d_{[0,1]}$. There is freedom in the choice of a modality $\tau\colon F\Omega\to\Omega$—this corresponds to what is called an evaluation function in [8]. This way we recover the Kantorovich lifting in [8] as $F^{\mathbf{\Omega},\tau}$.

III-B Codensity Bisimilarity

In [15], codensity bisimulation and bisimilarity are introduced. Recall that a coalgebra $c\colon X\to FX$ is a categorical presentation of state-based transition systems, such as automata, Markov chains, etc.—see, e.g., [20, 19], and also §VIII.

Definition III.5** **(codensity

bisimulation).

Assume the setting of Def. III.1. Let $c:X\to FX$ be an $F$-coalgebra. An object $P\in\mathbb{E}_{X}$ is a ($(\mathbf{\Omega},\tau)$-)codensity bisimulation over $c$ if $c:(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}(FX,F^{\mathbf{\Omega},\tau}P)$; that is, $c$ is decent with respect to the designated indistinguishability structures on $X$ and $FX$.

We move on to the characterization of codensity bisimulations as (post-)fixed points of suitable predicate transformers.

Definition III.6** (predicate transformer $\Phi^{\mathbf{\Omega},\tau}$).**

Assume the setting of Def. III.5. We define a predicate transformer $\Phi_{c}^{\mathbf{\Omega},\tau}:\mathbb{E}_{X}\rightarrow\mathbb{E}_{X}$ with respect to $c$ and $F^{\mathbf{\Omega},\tau}$ by:

[TABLE]

Theorem III.7**.**

Assume the setting of Def. III.5. For any $P\in\mathbb{E}_{X}$, the following are equivalent.

$c:(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}(FX,F^{\mathbf{\Omega},\tau}P)$; that is, $P$ is a codensity bisimulation over $c$ (Def. III.5). 2. 2.

$P\sqsubseteq\Phi_{c}^{\mathbf{\Omega},\tau}P$. 3. 3.

For each $k\in\mathbb{C}(X,\Omega)$, $k:(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}(\Omega,\mathbf{\Omega})$ implies $\tau\circ Fk\circ c:(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}(\Omega,\mathbf{\Omega})$. ∎

The predicate transformer $\Phi_{c}^{\mathbf{\Omega},\tau}$ is a monotone map from the complete lattice $\mathbb{E}_{X}$ to itself. Therefore, by the Knaster–Tarski theorem, the greatest post-fixed point of $\Phi_{c}^{\mathbf{\Omega},\tau}$ exists and it is the greatest fixed point of $\Phi_{c}^{\mathbf{\Omega},\tau}$.

Definition III.8** (codensity bisimilarity $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$).**

Assume the setting of Def. III.5. The greatest codensity bisimulation, whose existence is guaranteed by the above arguments, is called the codensity bisimilarity. It is denoted by $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$.

Some bisimilarity notions, including bisimilarity of deterministic automata (§VIII-B), are accommodated in the generalized framework with multiple observation domains—see §VI.

Example III.9** (bisimulation metric).**

Consider the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{PMet}_{1}\rightarrow\mathbf{Set}$ and the subdistribution functor $\mathcal{D}_{\leq 1}\colon\mathbf{Set}\to\mathbf{Set}$. Recall that $\textstyle\mathcal{D}_{\leq 1}(X)=\{p\colon X\to[0,1]\mid\sum_{x\in X}p(x)\leq 1\}.$ As a parameter of codensity lifting, we take (\mathbf{\Omega},\tau)=\bigl{(}\,\bigl{(}[0,1],d_{[0,1]}\bigr{)},\,e\colon\mathcal{D}_{\leq 1}[0,1]\to[0,1]\,\bigr{)}, where $e$ is the expectation function $e(p)=\sum_{r\in[0,1]}r\cdot p(r)$ and $d_{[0,1]}$ is the Euclidean metric. Let $c\colon X\to\mathcal{D}_{\leq 1}X$ be a coalgebra, identified with a Markov chain.

The codensity bisimilarity in this setting coincides with bisimulation metric from [5] (see also §I-A3). This fact is not hard to check directly; one can also derive the coincidence via III.4 and the observations in [8].

III-C Joint Codensity Bisimulation

We introduce a notion of joint codensity bisimulation. This minor variation of codensity bisimulation becomes useful in the proof of soundness and completeness of our game notion (§IV).

Definition III.10** **(joint codensity

bisimulation).

Assume the setting of Def. III.5. Let $\mathcal{V}\subseteq|\mathbb{E}_{X}|$; joins in $\mathbb{E}_{X}$ are denoted by $\bigsqcup$. We say that $\mathcal{V}$ is a joint codensity bisimulation over $c$ if $\bigsqcup_{P\in\mathcal{V}}P$ is a codensity bisimulation over $c$.

For instance, the set of all codensity bisimulations is a joint codensity bisimulation, because the join $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$ is the largest bisimulation (a consequence of the Knaster–Tarski theorem).

Lemma III.11**.**

In the setting of Def. III.5, the downset $\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})$ is the largest joint codensity bisimulation (with respect to the inclusion order). ∎

IV

Untrimmed Games for Codensity Bisimilarity

As the first 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 than necessary. The trimmed version of games—with smaller arenas—will be introduced later in §V, after developing necessary categorical infrastructure.

Assume the setting of Def. III.5 for the rest of the section.

Definition IV.1** (untrimmed codensity bisimilarity game).**

The untrimmed codensity bisimilarity game is the safety game played by two players D and S, shown in Table VIII.

Lemma IV.2**.**

Let $\mathcal{V}\subseteq|\mathbb{E}_{X}|$. The following are equivalent.

$\mathcal{V}$* is an invariant for Duplicator (Def. II.3) in the safety game in Table VIII.* 2. 2.

$\mathcal{V}$* is a joint codensity bisimulation over $c$. ∎*

Theorem IV.3**.**

The following coincide.

The set of all winning positions for D. 2. 2.

The downset $\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})$ of the codensity bisimilarity.

Proof*.*

On the one hand, the set of all winning positions for D is the largest invariant for D, by Prop. II.4. On the other hand, the downset $\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})$ is the largest joint codensity bisimulation over $c$. Thus, the statement follows from Lem. IV.2.∎

We conclude that our game characterizes the codensity bisimilarity $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$ (Def. III.8).

Corollary IV.4** **(soundness and completeness of untrimmed codensity

games).

$P\in\mathbb{E}_{X}$* is a winning position for D if and only if $P\sqsubseteq\nu\Phi_{c}^{\mathbf{\Omega},\tau}$. ∎*

Example IV.5**.**

Recall Example III.9. Using the untrimmed codensity bisimilarity game, we can characterize the bisimulation metric from [5]. Our general definition (Def. IV.1) instantiates to the one in Table VIII, which is however more complicated than the game we exhibited in the introduction (Table II). For example, in Table VIII, Duplicator’s move is a pseudometric $d\colon X^{2}\to[0,1]$ rather than a triple $(x,y,\varepsilon)$.

V Trimmed Codensity Games for Bisimilarity

Our previous untrimmed game (Table VIII) is pleasantly simple from a theoretical point of view. However, as we saw in Example IV.5, its instances tend to have a much bigger arena than some known game notions.

Here we push our theory a step further, and present a fibrational construction that allows us to trim our games. We note that our construction still remains on the fibrational level of abstraction.

V-A Generating Sets and Fibered Separators in a Fibration

We start by building some fibrational infrastructure. The following notion is a natural extension of the corresponding lattice-theoretic one. Unlike in the case of algebraic lattices, we do not assume the compactness of elements in $\mathcal{G}$.

Definition V.1** (generating set).**

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration and $X\in\mathbb{C}$ be an object. We say that a set $\mathcal{G}\subseteq|\mathbb{E}_{X}|$ is a generating set of the fiber $\mathbb{E}_{X}$ if, for any $P\in\mathbb{E}_{X}$, there exists $\mathcal{A}\subseteq\mathcal{G}$ such that $\bigsqcup\mathcal{A}=P$.

Example V.2**.**

Consider the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{EqRel}\rightarrow\mathbf{Set}$ and $X\in\mathbf{Set}$. For any $x,y\in X$, we define the equivalence relation $E_{x,y}$ to be the least one equating $x,y$, that is, $(z,w)\in E_{x,y}$ if and only if $(z=w\vee\{z,w\}=\{x,y\})$. Then the set $\mathcal{G}=\{E_{x,y}~{}|~{}x,y\in X\}$ of elements of the fiber $\mathbf{EqRel}_{X}$ is a generating set.

Example V.3**.**

Recall Example III.9. For $x,y\in X$ ($x\neq y$) and $r\in[0,1]$, the pseudometric $d_{x,y,r}$ over $X$ is defined by

[TABLE]

Then the set of pseudometrics $\{d_{x,y,r}~{}|~{}x,y\in X,x\neq y,r\in[0,1]\}$ is a generating set of the fiber $(\mathbf{PMet}_{1})_{X}$.

One natural question is how to find such a generating set in the fiber over the state space. Below we show that a generating set of the fiber of a special object (called fibered separator) induces a generating set of each fiber by push-forward.

Definition V.4** (fibered separator).**

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration. We say that $S\in\mathbb{C}$ is a fibered separator if, for any $X\in\mathbb{C}$ and $P,Q\in\mathbb{E}_{X}$, we have

[TABLE]

Theorem V.5**.**

Let $S\in\mathbb{C}$ be a fibered separator of a $\mathbf{CLat}_{\sqcap}$-fibration $p:\mathbb{E}\rightarrow\mathbb{C}$, and $\mathcal{G}\subseteq|\mathbb{E}_{S}|$ be a generating set of $\mathbb{E}_{S}$. For any $X\in\mathbb{C}$, the following set is a generating set of $\mathbb{E}_{X}$:

[TABLE]

Here $f_{*}$ denotes the pushforward along $f$ (§II-B). ∎

In fact, it was Thm. V.5 behind Examples V.2–V.3: in both cases, $2\in\mathbf{Set}$ turns out to be a fibered separator for the fibrations in question ($\mathbf{EqRel}\rightarrow\mathbf{Set}$ and $\mathbf{PMet}_{1}\rightarrow\mathbf{Set}$), and the presented generating sets are obtained via push-forward.

The following result is useful in finding fibered separators—see §VIII-F.

Proposition V.6** (change-of-base and fibered separators).**

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration, $R\colon\mathbb{D}\to\mathbb{C}$ be a functor with a left adjoint $L\colon\mathbb{C}\to\mathbb{D}$, and $S\in\mathbb{C}$ be a fibered separator for $p$. Then $LS\in\mathbb{D}$ is a fibered separator of the change-of-base fibration $R^{*}p$. ∎

V-B $\mathcal{G}$-Joint Codensity Bisimulation

We use generating sets to restrict moves in codensity games.

Definition V.7**.**

In the setting of Def. III.5, let $\mathcal{G}$ be a generating set of $\mathbb{E}_{X}$. A $\mathcal{G}$-joint codensity bisimulation over $c:X\to FX$ is a joint codensity bisimulation $\mathcal{V}$ over $c$ such that $\mathcal{V}\subseteq\mathcal{G}$.

Lemma V.8** (key lemma).**

Assume the setting of Def. III.5, and let $\mathcal{G}$ be a generating set of $\mathbb{E}_{X}$. The intersection \bigl{(}\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})\bigr{)}\cap\mathcal{G} of the downset $\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})$ and the generating set $\mathcal{G}$ is the largest $\mathcal{G}$-joint codensity bisimulation.

Proof*.*

Since $\mathcal{G}$ is a generating set, the union of all elements of $\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})\cap\mathcal{G}$ is equal to $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$. Thus, $\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})\cap\mathcal{G}$ is a $\mathcal{G}$-joint codensity bisimulation.

For any $\mathcal{G}$-joint codensity bisimulation $\mathcal{V}$, we have already shown $\mathcal{V}\subseteq\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})$. We also have $\mathcal{V}\subseteq\mathcal{G}$ by definition. These imply $\mathcal{V}\subseteq\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})\cap\mathcal{G}$.∎

V-C Trimmed Codensity Bisimilarity Games

The above structural results lead to our second game notion.

Definition V.9** **(trimmed codensity bisimilarity

game).

Assume the setting of Def. III.5, and that $\mathcal{G}\subseteq\mathbb{E}_{X}$ is a generating set. The codensity bisimilarity game is the safety game played by two players D and S, shown in Table IX.

Assume the setting of Def. V.9 for the rest of the section.

Lemma V.10**.**

Let $\mathcal{V}\subseteq|\mathbb{E}_{X}|$. The following are equivalent:

$\mathcal{V}$* is an invariant for D (Def. II.3) in the game in Table IX.* 2. 2.

$\mathcal{V}$* is a $\mathcal{G}$-joint codensity bisimulation over $c$. ∎*

Theorem V.11**.**

The following sets coincide.

The set of D-winning positions in the game in Table IX. 2. 2.

The intersection \bigl{(}\mathop{\downarrow}(\nu\Phi_{c}^{\mathbf{\Omega},\tau})\bigr{)}\cap\mathcal{G} of the downset of the codensity bisimilarity over $c$ and the generating set $\mathcal{G}$. ∎

We conclude that our second game characterizes the codensity bisimilarity $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$ (Def. III.8) too.

Corollary V.12** **(soundness and completeness of trimmed codensity

games).

In Def. V.9, $P\in\mathcal{G}$ is a winning position for Duplicator if and only if $P\sqsubseteq\nu\Phi_{c}^{\mathbf{\Omega},\tau}$. ∎

VI Multiple Observation Domains

We extend the theory so far and accommodate multiple observation domains and modalities. This extension is needed for some examples, such as those marked with $\dagger$ in Table VI.

We consider the class ${\bf Lift}(F,p)$ of liftings of an endofunctor $F:\mathbb{C}\mathrel{\rightarrow}\mathbb{C}$ along a $\mathbf{CLat}_{\sqcap}$-fibration $p:\mathbb{E}\rightarrow\mathbb{C}$. It comes with a natural pointwise partial order:

[TABLE]

and the partially ordered class ${\bf Lift}(F,p)$ admits meets of arbitrary size. As done in the original codensity lifting of endofunctors in [15] (and monads in [14]), we extend the codensity lifting so that it takes a family of parameters $\{(\mathbf{\Omega}_{A},\tau_{A})\}_{A\in\mathbb{A}}$, and returns the intersection of the codensity liftings of $F$ with these parameters.

Definition VI.1** **(codensity lifting of a

functor with multiple parameters [15]).

Let $F:\mathbb{C}\mathrel{\rightarrow}\mathbb{C}$ be a functor, $p:\mathbb{E}\rightarrow\mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration, $\mathbb{A}$ be a class, and $\{(\mathbf{\Omega}_{A},\tau_{A})\}_{A\in\mathbb{A}}$ be an $\mathbb{A}$-indexed family of parameters (of the codensity lifting of $F$ along $p$), which is denoted simply by $(\mathbf{\Omega},\tau)$. The (multiple-parameter) codensity lifting of $F$ with $(\mathbf{\Omega},\tau)$ is the endofunctor $F^{\mathbf{\Omega},\tau}:\mathbb{E}\mathrel{\rightarrow}\mathbb{E}$ defined by the intersection of the codensity liftings:

[TABLE]

The rest of the theoretical development is completely parallel to the one in the previous sections. Therefore we only present key definitions and the main result (Cor. VI.4). The omitted definitions and results can be recovered from the ones in §III–V, by replacing a single-parameter codensity lifting (Def. III.1) by a multi-parameter one (Def. VI.1).

Definition VI.2** (codensity bisimulation).**

Assume the setting of Def. VI.1. Let $c:X\to FX$ be an $F$-coalgebra. An object $P\in\mathbb{E}_{X}$ is a codensity bisimulation over $c$ if $c:(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}(FX,F^{\mathbf{\Omega},\tau}P)$; that is, $c\colon X\to FX$ is decent with respect to the designated indistinguishability structures.

Definition VI.3** (codensity bisimilarity game).**

In the setting of Def. VI.2, let $\mathcal{G}$ be a generating set of $\mathbb{E}_{X}$. The codensity bisimilarity game is the safety game, played by two players D and S, shown in Table X.

Corollary VI.4** (soundness and completeness of codensity games).**

Assume the setting of Def. VI.3. $P\in\mathbb{E}_{X}$ is a winning position for Duplicator if and only if $P\sqsubseteq\nu\Phi_{c}^{\mathbf{\Omega},\tau}$. ∎

Example VI.5** (bisimulation topology for deterministic automata).**

Here we describe the topological example in Table VI. Consider the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{Top}\rightarrow\mathbf{Set}$ and the functor $A_{\Sigma}=2\times(\underline{\phantom{n}}\,)^{\Sigma}\colon\mathbf{Set}\to\mathbf{Set}$, where $\Sigma$ is a fixed alphabet. Coalgebras for this functor are deterministic automata over $\Sigma$; see e.g. [20, 19].

We take the following data as a parameter of codensity lifting (cf. Def. VI.1): $\mathbb{A}=\{\varepsilon\}\cup\Sigma$, $\mathbf{\Omega}_{\alpha}$ is the Sierpinski space for each $\alpha\in\mathbb{A}$, and the modalities $\tau_{\varepsilon},\tau_{a}\colon A_{\Sigma}2\to 2$ (where $a\in\Sigma$) are defined by

[TABLE]

Recall that the Sierpinski space is the set $2=\{\bot,\top\}$ with the topology $\{\emptyset,\{\top\},2\}$; this observation domain models the situation where acceptance of a word is only semi-decidable.

Let $c\colon X\to A_{\Sigma}X$ be a deterministic automata. The above choice of parameters leads to the following codensity bisimilarity: the state space $X$ is equipped with the topology generated by the following family of open sets.

[TABLE]

One can extract various information from this bisimulation topology via standard topological constructs. For example, the specialization order of this topology coincides with the language inclusion order.

For illustration by comparison, consider changing the observation domain from the Sierpinski space to the discrete 2-point set. The bisimulation topology over $X$ is now generated by

[TABLE]

We can now observe rejection of a word, too, because $\{\bot\}\subseteq 2$ is open. The specialization order of this topology is the language equivalence, and it satisfies the R0 separation axiom (while the last Sierpinski example does not).

We take these examples of bisimulation topology as a process-semantical incarnation of the “observability via topology, computability via continuity” paradigm from domain theory. The definition of codensity bisimulation (cf. Def. III.1) fits well with this intuition, too: a continuous map $k\colon(X,P)\mathrel{\dot{\mathrel{\rightarrow}}}\mathbf{\Omega}$ in Def. III.1 is a “computable observation”; accordingly, an open set of the bisimulation topology is a property that is decided by finitely many of those computable observations.

VII Transfer of Codensity Bisimilarities

In our formulation, for the same endofunctor $F\colon\mathbb{C}\to\mathbb{C}$, we can use various $\mathbf{CLat}_{\sqcap}$-fibrations and parameters $(\mathbf{\Omega},\tau)$ to equip $F$-coalgebras with different bisimilarity-like notions. Some relations among those codensity bisimilarities can be categorically captured by the following theorem.

Theorem VII.1** (transfer of codensity bisimilarity).**

Let $p:\mathbb{E}\rightarrow\mathbb{C}$ and $q:\mathbb{F}\rightarrow\mathbb{C}$ be $\mathbf{CLat}_{\sqcap}$-fibrations, $F\colon\mathbb{C}\to\mathbb{C}$ be an endofunctor, $c\colon X\to FX$ be an $F$-coalgebra, $T\colon\mathbb{E}\to\mathbb{F}$ be a full and faithful fibered functor from $p$ to $q$ preserving fibered meets, and $\{(\mathbf{\Omega}_{A},\tau_{A})\}_{A\in\mathbb{A}}$ be an $\mathbb{A}$-indexed family of parameters for codensity lifting of $F$ along $p$.

[TABLE]

In this setting, $\{(T\mathbf{\Omega}_{A},\tau_{A})\}_{A\in\mathbb{A}}$ is an $\mathbb{A}$-indexed family of parameters for codensity lifting of $F$ along $q$, and we have $\nu\Phi_{c}^{T\mathbf{\Omega},\tau}=T(\nu\Phi_{c}^{\mathbf{\Omega},\tau})$. ∎

Example VII.2**.**

We show that the codensity bisimilarities in Examples III.2 & III.3 are indeed the usual bisimilarity notions for Kripke frames. Recall that they are build on the two $\mathbf{CLat}_{\sqcap}$-fibrations $\mathbf{EqRel}\rightarrow\mathbf{Set}$ and $\mathbf{ERel}\rightarrow\mathbf{Set}$.

We first note that the inclusion functor $i\colon\mathbf{EqRel}\to\mathbf{ERel}$ is a reflection, having the equivalence closure $(\underline{\phantom{n}}\,)^{\mathrm{eq}}\colon\mathbf{ERel}\to\mathbf{EqRel}$ as the left adjoint. It follows that $i$ is meet-preserving. Moreover, $i$ is fibered.

[TABLE]

We introduce shorthands $\dot{\mathcal{P}}_{2},\dot{\mathcal{P}}_{3}$ for the liftings in Examples III.2 & III.3:

[TABLE]

Now, for the sake of our proof, let us introduce a relational lifting $\dot{\mathcal{P}}_{1}:\mathbf{ERel}\mathrel{\rightarrow}\mathbf{ERel}$ of $\mathcal{P}$ along $\mathbf{ERel}\rightarrow\mathbf{Set}$, for which it is obvious that the corresponding bisimilarity notion is the usual bisimilarity for Kripke frames. We do so in concrete terms, instead of as a codensity lifting:

[TABLE]

We note that $\dot{\mathcal{P}}_{2}$ is the restriction of $\dot{\mathcal{P}}_{1}$ from $\mathbf{ERel}$ to $\mathbf{EqRel}$ along $i$. Note also that $\dot{\mathcal{P}}_{3}=\dot{\mathcal{P}}_{1}\circ i\circ(\underline{\phantom{n}}\,)^{\mathrm{eq}}$.

Let $c:X\mathrel{\rightarrow}\mathcal{P}X$ be a Kripke frame and $\Phi_{i}=c^{*}\circ\dot{\mathcal{P}}_{i}$ ($i=1,2,3$) be the predicate transformer corresponding to each lifting. Theorem VII.1 states that $\nu\Phi_{3}=i(\nu\Phi_{2})$.

Furthermore, by $\dot{\mathcal{P}}_{1}\sqsubseteq\dot{\mathcal{P}}_{3}$ (where $\sqsubseteq$ is the order in (3)), we have $\nu\Phi_{1}\sqsubseteq\nu\Phi_{3}$. From $i\circ\dot{\mathcal{P}}_{2}=\dot{\mathcal{P}}_{1}\circ i$ and fiberedness of $c$, we can see that $i(\nu\Phi_{2})$ is a fixed point of $\Phi_{1}$, which yields $i(\nu\Phi_{2})\sqsubseteq\nu\Phi_{1}$ by the Knaster–Tarski theorem. The three (in)equalities so far allow us to conclude $\nu\Phi_{3}=i(\nu\Phi_{2})=\nu\Phi_{1}$, stating that the conventional bisimilarity $\nu\Phi_{1}$ is equal to the codensity bisimilarities in Examples III.2 & III.3. As a consequence, the conventional bisimilarity $\nu\Phi_{1}$ is necessarily an equivalence relation.

VIII Examples

VIII-A * Kripke Frames and (Conventional) Bisimilarity*

We consider $\mathbf{EqRel}\rightarrow\mathbf{Set}$ as an underlying $\mathbf{CLat}_{\sqcap}$-fibration, and a Kripke frame $c:X\mathrel{\rightarrow}\mathcal{P}X$ (as a $\mathcal{P}$-coalgebra). We further use the codensity lifting $\mathcal{P}^{\mathrm{Eq}_{2},\diamond}$ (Example III.2) and the generating set described in Example V.2 to trim games; the resulting game is shown in Table XV. As shown in Example VII.2, the codensity bisimilarity $\nu\Phi_{c}^{\mathrm{Eq}_{2},\diamond}$ (which is $\nu\Phi_{2}$ in VII.2) coincides with conventional bisimilarity on $c$ using the standard relational lifting of $\mathcal{P}$ to $\mathbf{ERel}$.

Theorem VIII.1**.**

$(x,y)$* is a D-winning position if and only if $(x,y)\in\nu\Phi_{c}^{\mathrm{Eq}_{2},\diamond}$, if and only if $x$ and $y$ are bisimilar. ∎*

Extension of this result to labeled transition systems and Kripke models (with valuations) is straightforward, using suitable choice of endofunctors—see also §VIII-B.

VIII-B *Deterministic Automata and Their Language

Equivalence*

We use the functor $A_{\Sigma}\colon\mathbf{Set}\to\mathbf{Set}$ from Example VI.5, for which a coalgebra is a deterministic automaton. Let us lift $A_{\Sigma}$ along the fibration $\mathbf{EqRel}\rightarrow\mathbf{Set}$, with the same modalities $\tau_{\varepsilon},\tau_{a}\colon A_{\Sigma}2\to 2$ as in Example VI.5 (where $a\in\Sigma$). Our observation domains are $\mathbf{\Omega}_{\alpha}=(2,\mathrm{Eq}_{2})$ for all $\alpha\in\{\varepsilon\}\cup\Sigma$. The resulting codensity lifting $(A_{\Sigma})^{\mathbf{\Omega},\tau}\colon\mathbf{EqRel}\to\mathbf{EqRel}$ is concretely described as follows.

[TABLE]

Let $c\colon X\to A_{\Sigma}X$ be a deterministic automaton. It is not hard to see that the codensity bisimilarity $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$ coincides with language equivalence of deterministic automata. Our trimmed codensity game is shown in Table XV (in a slightly optimized form). The game therefore characterizes the language equivalence (Cor. VI.4).

VIII-C Deterministic Automata and the Language Topology

We introduced two versions of bisimulation topology for deterministic automata in Example VI.5. They are in close correspondences with accepted languages; therefore we call them language topologies.

For the first topology in Example VI.5 (where $\mathbf{\Omega}$ is the Sierpinski space, capturing that acceptance is only semi-decidable), the corresponding (untrimmed) codensity game is shown in Table XV. It follows from our general results that the game notion 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.

VIII-D Nondeterministic Automata and Bisimilarity

Let us now turn to nondeterministic automata, that is, $N_{\Sigma}$-coalgebras for the functor $N_{\Sigma}=2\times(\mathcal{P}\underline{\phantom{n}}\,)^{\Sigma}$. Much like the situation for DFAs, we lift this functor along the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{EqRel}\rightarrow\mathbf{Set}$ by codensity lifting with multiple observation domains, as follows. Let $\mathbb{A}$ be the set $\{\varepsilon\}\cup\Sigma$. We set the parameter of codensity lifting as follows, where $a\in\Sigma$.

[TABLE]

The resulting codensity lifting $(N_{\Sigma})^{\mathbf{\Omega},\tau}\colon\mathbf{EqRel}\to\mathbf{EqRel}$ is concretely described as

[TABLE]

Let $c\colon X\to N_{\Sigma}X$ be a nondeterministic automaton. It is again not hard to see that the codensity bisimilarity $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$ is the usual notion of bisimilarity of nondeterministic automata. Our trimmed codensity game is shown in Table XV, in a slightly optimized form, and it captures bisimilarity.

A topological variant of the above story is possible, much like in §VIII-C.

VIII-E Markov Chains and Bisimulation Metric

Recall Examples III.9, IV.5, and V.3. Markov chains are $\mathcal{D}_{\leq 1}$-coalgebras. We use the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{PMet}_{1}\rightarrow\mathbf{Set}$, taking pseudometrics as a notion of indistinguishability. With the lifting parameter we described in Example III.9, we get the bisimulation metric as the codensity bisimilarity. We can use the generating set described in Example V.3 to obtain a trimmed codensity game; the resulting game essentially coincides with the one in Table II in the introduction. Therefore, Cor. V.12 gives an abstract proof for the correctness of the game.

VIII-F Continuous State Markov Chains and Bisimulation Metric

In order to accommodate continuous state Markov chains (for which measurable structures are essential), we consider an example that involves $\mathbf{Meas}$. Continuing §VIII-E, by the change-of-base along the forgetful functor $U\colon\mathbf{Meas}\to\mathbf{Set}$, we get another $\mathbf{CLat}_{\sqcap}$-fibration $U^{*}(\mathbf{PMet}_{1})\rightarrow\mathbf{Meas}$. A continuous state Markov chain is a coalgebra $X\to\mathcal{G}_{\leq 1}X$ of the so-called sub-Giry functor over $\mathbf{Meas}$—see, e.g., [29].

Since the forgetful functor $\mathbf{Meas}\to\mathbf{Set}$ has a left adjoint, Prop. V.6 gives us a fibered separator for $U^{*}(\mathbf{PMet}_{1})\to\mathbf{Meas}$. This gives us a game notion similar to that in §VIII-E.

VIII-G *Markov Chains and Probabilistic Bisimilarity *

In order to define bisimilarity-like equivalence relation on Markov chains, we first lift $\mathcal{D}_{\leq 1}$ along the $\mathbf{CLat}_{\sqcap}$-fibration $\mathbf{EqRel}\rightarrow\mathbf{Set}$. For that purpose, here we use the following multiple lifting parameters. The index set is $\mathbb{A}=[0,1]$. For each $r\in\mathbb{A}$, we set $\mathbf{\Omega}_{r}=(2,\mathrm{Eq}_{2})$, and define a threshold modality $\tau_{r}\colon\mathcal{D}_{\leq 1}2\to 2$ by $\tau_{r}(p)=\top$ if and only if $p(\top)\geq r$. Then for any $R\in\mathbf{EqRel}_{X}$, the relation part of the codensity lifting $\mathcal{D}_{\leq 1}^{\mathbf{\Omega},\tau}(X,R)$ relates $p,q\in\mathcal{D}_{\leq 1}(X)$ if and only if

[TABLE]

Let us fix a Markov chain $c\colon X\to\mathcal{D}_{\leq 1}X$. All these data give rise to $\mathcal{D}_{\leq 1}^{\mathbf{\Omega},\tau}$ and $\nu\Phi_{c}^{\mathbf{\Omega},\tau}$ as in Definitions VI.2 and III.8. It is not hard to see that the resulting codensity bisimilarity coincides with probabilistic bisimilarity in [4]. Note, for example, that a relation-preserving map $k\colon(X,R)\mathrel{\dot{\mathrel{\rightarrow}}}(2,\mathrm{Eq}_{2})$ coincides with an $R$-closed subset of $X$. The resulting trimmed codensity game is in Table XV. It is essentially the same as Table I (arising from [13]). The difference is that $r$ is additionally present in Table XV; it is easy to realize that $r$ plays no role in the game.

IX Conclusions and Future Work

Motivated by some recent works [13, 10, 11, 8], and especially by the similarity of the two games (Tables I and II), we introduced a fibrational framework that uniformly describes the correspondence between various bisimilarity notions and games. The fibrational abstraction allows us to accommodate some new examples, such as bisimulation topology. Moreover, the structural theory developed in §VI–VII provides new insights to the nature of bisimilarity, we believe, identifying the crucial role of observation maps ($k\colon X\to\Omega$ in Def. III.1) in bisimulation notions.

As future work, we intend to accommodate modal logics as is done in [10]. We are also interested in using games with more complex winning conditions (e.g. parity); they have been used for (bi)simulation notions for Büchi and parity automata [31]. Finally, we will pursue the algorithmic use of the current results.

-A Direct Proof of Equivalence of the Two Game Notions Characterizing Probabilistic Bisimilarity (Tables I, IV)

-A1 Table IV $\leadsto$

Table I

Assume that Duplicator wins Table IV from $(x,y)$, and let Spoiler play some $Z$ in Table I . There are two cases to consider which are essentially identical, but we write them down separately just to make sure.

• •

If $\tau(x,Z)>\tau(y,Z)$ then make Spoiler select $s=x$ and play $Z$ in Table IV. To this Duplicator responds with some $Z^{\prime}\supseteq Z$ such that $\tau(x,Z)\leq\tau(y,Z^{\prime})$, which implies that $Z^{\prime}\neq Z$. Pick any $y^{\prime}\in Z^{\prime}\setminus Z$ and play it as Spoiler in Table IV; when Duplicator responds with some $x^{\prime}\in Z$, play the pair $x^{\prime}$ and $y^{\prime}$ as Duplicator in Table I.

• •

If $\tau(x,Z)<\tau(y,Z)$ then make Spoiler select $s=y$ and play $Z$ in Table IV. To this Duplicator responds with some $Z^{\prime}\supseteq Z$ such that $\tau(y,Z)\leq\tau(x,Z^{\prime})$, which implies that $Z^{\prime}\neq Z$. Pick any $y^{\prime}\in Z^{\prime}\setminus Z$ and play it as Spoiler in Table IV; when Duplicator responds with some $x^{\prime}\in Z$, play the pair $x^{\prime}$ and $y^{\prime}$ as Duplicator in Table I.

-A2

Table I $\leadsto$ Table IV

This is a less straightforward implication. A winning strategy for Duplicator in Table IV is built not from a single strategy in Table I, but rather from an entire collection of winning positions.

Formally, assume that Duplicator wins Table I from $(x,y)$, and let Spoiler choose $s\in\{x,y\}$ and play some $Z$ in Table IV. Define

[TABLE]

One basic observation is that $Z\subseteq\bar{Z}$, since Duplicator wins from all positions of the form $(w,w)$. As a result:

[TABLE]

Another observation is that Spoiler wins Table I from the position $\bar{Z}$. To see this, consider any Duplicator’s response $x^{\prime}\in\bar{Z}$, $y^{\prime}\not\in\bar{Z}$. Then there is some $v\in Z$ such that Duplicator wins Table I from $(v,x^{\prime})$. If Duplicator could win Table I from $(x^{\prime},y^{\prime})$ then she could win from $(v,y^{\prime})$ as well, which contradicts the assumption that $y^{\prime}\not\in\bar{Z}$.

Since we assume that Duplicator wins Table I from $(x,y)$, $\bar{Z}$ cannot be a legal move for Spoiler from $(x,y)$, hence

[TABLE]

Together with (4) this implies that

[TABLE]

so $Z^{\prime}=\bar{Z}$ is a legal move for Duplicator in stage (ii) of Table IV, no matter if Spoiler chose $s=x$ or $s=y$ in stage (i). To this, in stage (iii) replies with some $y^{\prime}\in\bar{Z}\setminus Z$. By definition of $\bar{Z}$, there is some $v\in Z$ such that Duplicator wins Table I from $(v,y^{\prime})$, so Duplicator can respond with $x^{\prime}=v$.

-B Introduction to $\mathbf{CLat}_{\sqcap}$-Fibration

We present an introduction to ($\mathbf{CLat}_{\sqcap}$-)fibrations, starting from a functor $F_{\mathbb{E}}\colon\mathbb{C}^{\mathrm{op}}\to\mathbf{CLat}_{\sqcap}$. The relevance of the latter is explained in §II-B. For details, readers are referred to [17].

-B1 The Grothendieck Construction

In general, the equivalence between index categories $\mathbb{C}^{\mathrm{op}}\to\mathbf{Cat}$ and fibrations is well-known. Here we sketch the Grothendieck construction from the former to the latter, focusing the special case of $\mathbb{C}^{\mathrm{op}}\to\mathbf{CLat}_{\sqcap}$ and $\mathbf{CLat}_{\sqcap}$-fibrations. Its idea is to “patch up” the family \bigl{(}F_{\mathbb{E}}X\bigr{)}_{X\in\mathbb{C}} of complete lattices, and form a big category $\mathbb{E}$, as shown in Fig. 2.

On the right-hand side in Fig. 2, we add some arrows (denoted by $\dashrightarrow$) so that we have an arrow $(F_{\mathbb{E}}f)(Q)\to Q$ in $\mathbb{E}$ for each $Q\in F_{\mathbb{E}}Y$. (On the left-hand side, the correspondence \raisebox{0.3pt}{\shortmid}\!\joinrel\dashrightarrow depicts the action of the map $F_{\mathbb{E}}f$.) The diagram in $\mathbb{E}$ in Fig. 2 should be understood as a Hasse diagram: those arrows which arise from composition are not depicted.

Definition .1** (The Grothendieck construction).**

Given $F_{\mathbb{E}}\colon\mathbb{C}^{\mathrm{op}}\to\mathbf{CLat}_{\sqcap}$, we define the category $\mathbb{E}$ by

• •

its objects: a pair $(X,P)$ of an object $X\in\mathbb{C}$ and an element $P$ of the poset $F_{\mathbb{E}}X$; and

• •

its arrows: $f\colon(X,P)\to(Y,Q)$ is an arrow $f\colon X\to Y$ in $\mathbb{C}$ such that

[TABLE]

Here $\sqsubseteq$ refers to the order of $F_{\mathbb{E}}X$.

Thus arises a category $\mathbb{E}$ that incorporates:

• •

the order structure of each of the posets $(F_{\mathbb{E}}X)_{X\in\mathbb{C}}$, and

• •

the pullback structure by (F_{\mathbb{E}}f)_{f\colon\text{\mathbb{C}-arrow}}.

For fixed $X\in\mathbb{C}$, the objects of the form $(X,P)$ and the arrows $\mathrm{id}_{X}$ between them form a subcategory of $\mathbb{E}$. This is denoted by $\mathbb{E}_{X}$ and called the fiber over $X$. It is obvious that $\mathbb{E}_{X}$ is a poset that is isomorphic to $F_{\mathbb{E}}X$.

Moreover, there is a canonical projection functor $p\colon\mathbb{E}\to\mathbb{C}$ that carries $(X,P)$ to $X$.

-B2 Formal Definition of $\mathbf{CLat}_{\sqcap}$-Fibration

We axiomatize those structures which arise in the way described above.

Definition .2** ($\mathbf{CLat}_{\sqcap}$-fibration).**

A $\mathbf{CLat}_{\sqcap}$-fibration $p:\mathbb{E}\rightarrow\mathbb{C}$ consists of two categories $\mathbb{E},\mathbb{C}$ and a functor $p\colon\mathbb{E}\to\mathbb{C}$, that satisfy the following properties.

• •

Each fiber $\mathbb{E}_{X}$ is a complete lattice. Here the fiber $\mathbb{E}_{X}$ for $X\in\mathbb{C}$ is the subcategory of $\mathbb{E}$ consisting of the following data: objects $P\in\mathbb{E}$ such that $pP=X$; and arrows $f\colon P\to Q$ such that $pf=\mathrm{id}_{X}$ (such arrows are said to be vertical).

• •

Given $f\colon X\to Y$ in $\mathbb{C}$ and $Q\in\mathbb{E}_{Y}$, there is an object $f^{*}Q\in\mathbb{E}_{X}$ and an $\mathbb{E}$-arrow $\overline{f}Q\colon f^{*}Q\to Q$ with the following universal property. For any $P\in\mathbb{E}_{X}$ and $g\colon P\to Q$ in $\mathbb{E}$, if $pg=f$ then $g$ factors through $\overline{f}(Q)$ uniquely via a vertical arrow. That is, there exists unique $g^{\prime}$ such that $g=\overline{f}(Q)\mathbin{\circ}g^{\prime}$ and $pg^{\prime}=\mathrm{id}_{X}$.

[TABLE]

• •

The correspondences $(\underline{\phantom{n}}\,)^{*}$ and $\overline{(\underline{\phantom{n}}\,)}$ are functorial:

[TABLE]

The last equality can be depicted as follows.

[TABLE]

The category $\mathbb{E}$ is called the total category of the fibration; $\mathbb{C}$ is the base category. The arrow $\overline{f}Q\colon f^{*}Q\to Q$ is called the Cartesian lifting of $f$ and $Q$. An arrow in $\mathbb{E}$ is Cartesian (or reindexing) if it coincides with $\overline{f}Q$ for some $f$ and $Q$.

In the case where $p:\mathbb{E}\rightarrow\mathbb{C}$ is induced by an indexed category $F_{\mathbb{E}}\colon\mathbb{C}^{\mathrm{op}}\to\mathbf{CLat}_{\sqcap}$ via Def. .1, a Cartesian lifting is given by $f^{*}(Q)=(F_{\mathbb{E}}f)(Q)$.

In the current paper we focus on $\mathbf{CLat}_{\sqcap}$-fibrations. In a (general) fibration, a fiber $\mathbb{E}_{X}$ is not just a preorder but a category, and this elicits a lot of technical subtleties. Nevertheless, it should not be hard to generalize the current paper’s observations to general, not necessarily $\mathbf{CLat}_{\sqcap}$-, fibrations (especially to the split ones). We shall often denote a vertical arrow in $\mathbb{E}$ (i.e. an arrow inside a fiber) by $\sqsubseteq$.

-C Codensity Characterization of Hausdorff pseudometric

Proposition .3**.**

Let $(X,d)$ be a pseudometric space. For any $S,T\subseteq X$, we define two functions

[TABLE]

and

[TABLE]

The values of two functions coincide.

Proof*.*

First, we show $d_{c}(S,T)\geq d_{H}(S,T)$ by contradiction.

Suppose it doesn’t hold. Then, by definition, at least one of

[TABLE]

and

[TABLE]

is greater than $d_{c}(S,T)$. We can assume the former is greater than $d_{c}(S,T)$ w.l.o.g.

Therefore, for some $x_{0}\in S$,

[TABLE]

holds.

Now, since $d(x_{0},\underline{\phantom{n}}\,)$ is a non-expansive function by the triangle inequality, we have

[TABLE]

However, since $\inf_{x\in S}d(x_{0},x)=0$, we have $d_{c}(S,T)\geq\inf_{y\in T}d(x_{0},y)$, which is a contradiction.

Next, we show $d_{c}(S,T)\leq d_{H}(S,T)$ by contradiction.

Suppose $d_{c}(S,T)>d_{H}(S,T)+\varepsilon$ for some $\varepsilon>0$. Then, for some non-expansive $k\colon X\to[0,1]$,

[TABLE]

holds.

W.l.o.g. we can assume $\inf_{x\in S}k(x)\leq\inf_{y\in T}k(y)$.

Thus, for some $x_{0}\in S$ and $y_{0}\in T$ satisfying $k(x_{0})\leq\inf_{x\in S}k(x)+\varepsilon/5$ and $k(y_{0})\leq\inf_{y\in T}k(y)+\varepsilon/5$,

[TABLE]

holds. Since

[TABLE]

there exists some $y_{1}\in T$ satisfying

[TABLE]

However, we have $k(x_{0})\leq k(y_{0})+\varepsilon/5\leq k(y_{1})+2\varepsilon/5$, so

[TABLE]

and

[TABLE]

holds.

Then,

[TABLE]

holds, which is a contradiction.∎

-D Omitted Proofs

-D1 Proof of Lem. III.11

Proof*.*

The downset $\mathop{\downarrow}(\nu\Phi^{\mathbf{\Omega},\tau})$ is a joint codensity bisimulation, because the union of all elements of $\mathop{\downarrow}(\nu\Phi^{\mathbf{\Omega},\tau})$ is equal to a codensity bisimulation $\nu\Phi^{\mathbf{\Omega},\tau}$.

Let $\mathcal{V}$ be a joint codensity bisimulation. Then for any $P\in\mathcal{V}$, we have $P\sqsubseteq\nu\Phi^{\mathbf{\Omega},\tau}$, because $P\sqsubseteq\bigsqcup_{Q\in\mathcal{V}}Q\sqsubseteq\nu\Phi^{\mathbf{\Omega},\tau}$.∎

-D2 Proof of Lem. IV.2

Proof*.*

We follow the following logical equivalence.

[TABLE]

where the last equivalence is by Thm. III.7.

-D3 Proof of Prop. V.6

Proof*.*

For any $X\in\mathbb{D}$, the bijection $\mathbb{D}(LS,X)\cong\mathbb{C}(S,RX)$ exists. Thus, naturally identifying $(R^{*}\mathbb{E})_{X}$ and $\mathbb{E}_{RX}$, we have the following for any $P,Q\in(R^{*}\mathbb{E})_{X}$.

[TABLE]

∎

-D4 Proof of Prop. VII.1

Proof*.*

We have $T\Phi^{\mathbf{\Omega},\tau}=\Phi^{T\mathbf{\Omega},\tau}T$ because, for any $P\in\mathbb{F}_{X}$,

[TABLE]

holds.

Considering this and the fact that $T$ preserves meets, [15, Lemma 20] implies $T(\nu\Phi^{\mathbf{\Omega},\tau})=\nu\Phi^{T\mathbf{\Omega},\tau}$.∎