Codensity Games for Bisimilarity

Bartek Klin; Ichiro Hasuo; Nick Hu; Shin-ya Katsumata; Yuichi Komorida

arxiv: 1907.09634 · v1 · pith:PPAQ4QLDnew · submitted 2019-07-22 · 💻 cs.LO

Codensity Games for Bisimilarity

Yuichi Komorida , Shin-ya Katsumata , Nick Hu , Bartek Klin , Ichiro Hasuo This is my paper

Pith reviewed 2026-05-24 17:27 UTC · model grok-4.3

classification 💻 cs.LO

keywords bisimilaritycodensity gamesfibrationscoalgebrasbisimulation metricpredicate transformersbisimulation topologygame characterizations

0 comments

The pith

Fibrational predicate transformers derive codensity games that characterize bisimilarity uniformly.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out a categorical framework that uses fibrations and coalgebras to produce game characterizations of bisimilarity and its quantitative extensions. It shows that predicate transformers defined in a fibration yield codensity bisimilarity games, which serve as the uniform game description. A sympathetic reader cares because the same construction recovers both ordinary bisimilarity and quantitative versions such as bisimulation metrics, as well as new notions like bisimulation topology, without separate ad-hoc arguments for each system model.

Core claim

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.

What carries the argument

Fibrational predicate transformers on coalgebras, which convert coalgebra morphisms into relations or distances inside the fibration and thereby produce the codensity games.

Load-bearing premise

The fibrational predicate transformer construction exactly recovers the intended bisimilarity or metric when instantiated on the appropriate fibration and coalgebra.

What would settle it

A concrete system model together with its standard bisimilarity definition where the equivalence classes produced by the codensity game differ from those of the usual definition.

Figures

Figures reproduced from arXiv: 1907.09634 by Bartek Klin, Ichiro Hasuo, Nick Hu, Shin-ya Katsumata, Yuichi Komorida.

**Figure 2.** Figure 2: The Grothendieck construction uniquely via a vertical arrow. That is, there exists unique g 0 such that g = f(Q) ◦ g 0 and pg0 = idX. E p Q =⇒ f ∗Q f(Q) /Q P g 99 g 0 OO C X f /Y X f /Y • The correspondences ( ) ∗ and ( ) are functorial: id∗ Y Q = Q , (g ◦ f) ∗ (Q) = f ∗ (g ∗Q), idY (Q) = idQ , g ◦ f(Q) = gQ ◦ f(g ∗Q). The last equality can be depicted as follows. E p f ∗ (g ∗Q) f(g ∗Q) /g ∗Q gQ /Q (… view at source ↗

read the original 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).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper supplies a uniform fibrational construction that derives codensity games for bisimilarity and its quantitative extensions, recovering known cases while adding new ones like bisimulation topology.

read the letter

The core contribution is a categorical route, via fibrations and predicate transformers, that produces game characterizations for bisimilarity in one go instead of case by case. They use codensity to get the games and show how the same setup covers both ordinary bisimilarity and things like bisimulation metrics, plus a new notion they call bisimulation topology. That unification is the actual advance; prior work had separate games for each quantitative variant, so a single derivation that hits several of them is useful for the subfield. The presentation is clean on the abstract level and the coalgebraic language is handled competently. The main open question is how much tuning is required when you instantiate the framework on a concrete model. The stress-test concern is real: if each target equivalence needs its own fibration or extra structure chosen by hand, then the uniformity is weaker than the abstract suggests, even if the internal categorical steps are correct. The paper claims exact recovery for the bisimulation metric, so the referee would need to see the concrete derivations and check that no ad-hoc adjustments slipped in. No circularity or invented parameters appear in the claims. This is specialist material for people already working in coalgebra or categorical process theory; a general reader in concurrency would find the game part interesting but would need the full details to judge the payoff. It is coherent on its own terms and the central construction is new, so it should go to peer review rather than desk rejection. A referee can verify the instantiations and assess whether the framework actually dictates the right fibrations or still requires per-model choices.

Referee Report

2 major / 1 minor

Summary. The paper presents a categorical framework using fibrations and coalgebras to give a uniform game-theoretic characterization of bisimilarity-like notions. It derives codensity bisimilarity games from fibrational predicate transformers and claims that the resulting framework covers both established quantitative notions such as bisimulation metrics and new ones such as bisimulation topology.

Significance. A verified uniform categorical derivation that recovers standard bisimilarity games and metrics exactly would constitute a significant unification, allowing systematic extension of game characterizations from qualitative to quantitative systems and the principled introduction of new notions. The fibrational approach itself is a conceptual strength when the recovery property holds.

major comments (2)

[Abstract] Abstract: the claim that the framework covers bisimulation metric is unsupported; no derivation or instantiation is supplied showing that the codensity game obtained from the fibrational predicate transformer coincides with the standard bisimulation metric on any concrete coalgebra.
[Abstract] Abstract and framework sections: the central claim that the construction recovers intended bisimilarities (including new notions such as bisimulation topology) without case-by-case ad-hoc adjustments remains unverified; no example is given in which the choice of fibration and coalgebra is dictated by the general theory and the resulting game is shown to match the target equivalence exactly.

minor comments (1)

The high-level presentation of the codensity construction would benefit from an explicit comparison table relating the new games to at least one classical bisimilarity game (e.g., the standard bisimulation game).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive report. The major comments correctly identify that the submitted manuscript asserts coverage of bisimulation metrics and exact recovery of intended equivalences (including the new bisimulation topology) but does not supply the explicit derivations or worked examples needed to verify those claims. We will revise the paper to include them.

read point-by-point responses

Referee: [Abstract] Abstract: the claim that the framework covers bisimulation metric is unsupported; no derivation or instantiation is supplied showing that the codensity game obtained from the fibrational predicate transformer coincides with the standard bisimulation metric on any concrete coalgebra.

Authors: We agree that the current text does not contain an explicit derivation showing that the codensity game for the metric fibration coincides exactly with the standard bisimulation metric on a concrete coalgebra. The general construction is given, but the concrete verification step is missing. In the revision we will add a subsection that instantiates the fibrational predicate transformer for the metric case, derives the corresponding codensity game, and proves coincidence with the standard definition. revision: yes
Referee: [Abstract] Abstract and framework sections: the central claim that the construction recovers intended bisimilarities (including new notions such as bisimulation topology) without case-by-case ad-hoc adjustments remains unverified; no example is given in which the choice of fibration and coalgebra is dictated by the general theory and the resulting game is shown to match the target equivalence exactly.

Authors: We acknowledge that the manuscript does not provide a fully worked example in which the fibration is selected according to the general theory and the resulting game is shown to match a target equivalence exactly, including for the newly introduced bisimulation topology. The framework is designed so that the fibration encodes the desired notion, but the verification is not carried out in detail. We will add a concrete example section that specifies the fibration and coalgebra dictated by the theory and proves exact recovery of the intended equivalence. revision: yes

Circularity Check

0 steps flagged

No significant circularity; categorical derivation is self-contained.

full rationale

The paper introduces a fibrational predicate transformer construction to derive codensity bisimilarity games from coalgebras. The abstract and provided text present this as a uniform categorical framework that recovers known notions like bisimulation metrics via appropriate instantiations, without any quoted equations, fitted parameters, or self-citations that reduce the central result to its inputs by construction. No load-bearing steps match the enumerated circularity patterns; the derivation chain relies on standard categorical machinery rather than renaming or self-referential definitions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The framework rests on standard category-theoretic background (fibrations, coalgebras, predicate transformers, codensity monads) rather than new free parameters or invented physical entities. No numerical fitting occurs.

axioms (1)

standard math Standard axioms of category theory and fibrations suffice to model state-based systems and their properties.
Invoked throughout the abstract as the setting in which the predicate transformers and codensity games are defined.

invented entities (1)

codensity bisimilarity games no independent evidence
purpose: General categorical game characterization of bisimilarity
Introduced as the derived object of the framework; no independent falsifiable prediction outside the categorical construction is stated.

pith-pipeline@v0.9.0 · 5697 in / 1433 out tokens · 30368 ms · 2026-05-24T17:27:03.209069+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages · 1 internal anchor

[1]

Concurrency and automata on inﬁnite sequences,

D. Park, “Concurrency and automata on inﬁnite sequences,” in Proceedings of the 5th GI-Conference on Theoretical Computer Science. London, UK, UK: Springer-Verlag, 1981, pp. 167–183. [Online]. Available: http://dl.acm.org/citation.cfm?id=647210.720030

work page arXiv 1981
[2]

Milner, Communication and Concurrency

R. Milner, Communication and Concurrency . Prentice-Hall, 1989

work page 1989
[3]

Sangiorgi and J

D. Sangiorgi and J. Rutten, Eds., Advanced Topics in Bisimulation and Coinduction, ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2011. 12

work page 2011
[4]

Bisimulation through probabilistic testing,

K. G. Larsen and A. Skou, “Bisimulation through probabilistic testing,” Inf. Comput., vol. 94, no. 1, pp. 1–28, 1991

work page 1991
[5]

Metrics for labelled markov processes,

J. Desharnais, V . Gupta, R. Jagadeesan, and P. Panangaden, “Metrics for labelled markov processes,” Theoretical Computer Science , vol. 318, no. 3, pp. 323 – 354, 2004. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S0304397503006042

work page 2004
[6]

Structural induction and coinduction in a ﬁbrational setting,

C. Hermida and B. Jacobs, “Structural induction and coinduction in a ﬁbrational setting,” Inf. Comput. , vol. 145, no. 2, pp. 107–152, 1998. [Online]. Available: https://doi.org/10.1006/inco.1998.2725

work page doi:10.1006/inco.1998.2725 1998
[7]

Coinductive predicates and ﬁnal sequences in a ﬁbration,

I. Hasuo, T. Kataoka, and K. Cho, “Coinductive predicates and ﬁnal sequences in a ﬁbration,” Mathematical Structures in Computer Science, vol. 28, no. 4, pp. 562–611, 2018. [Online]. Available: https://doi.org/10.1017/S0960129517000056

work page doi:10.1017/s0960129517000056 2018
[8]

Coalgebraic behavioral metrics,

P. Baldan, F. Bonchi, H. Kerstan, and B. K ¨onig, “Coalgebraic behavioral metrics,” Logical Methods in Computer Science , vol. 14, no. 3, 2018. [Online]. Available: https://doi.org/10.23638/LMCS-14(3:20)2018

work page doi:10.23638/lmcs-14(3:20)2018 2018
[9]

Coinduction up-to in a ﬁbrational setting,

F. Bonchi, D. Petrisan, D. Pous, and J. Rot, “Coinduction up-to in a ﬁbrational setting,” in Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014 , T. A. Henzinger and D. Miller, Eds. AC...

work page doi:10.1145/2603088.2603149 2014
[10]

(Metric) bisimulation games and real- valued modal logics for coalgebras,

B. K ¨onig and C. Mika-Michalski, “(Metric) bisimulation games and real- valued modal logics for coalgebras,” in 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, 2018, pp. 37:1–37:17

work page 2018
[11]

Up-to techniques for behavioural metrics via ﬁbrations,

F. Bonchi, B. K ¨onig, and D. Petrisan, “Up-to techniques for behavioural metrics via ﬁbrations,” in 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China , ser. LIPIcs, S. Schewe and L. Zhang, Eds., vol. 118. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018, pp. 17:1–17:17. [Online]. Available: http...

work page doi:10.4230/lipics.concur.2018.17 2018
[12]

Path category for free - Open morphisms from coalgebras with non-deterministic branching

T. Wißmann, J. Dubut, S. Katsumata, and I. Hasuo, “Path category for free—open morphisms from coalgebras with non-deterministic branching,” CoRR, vol. abs/1811.12294, 2018, to appear in Proc. FoSSaCS 2019. [Online]. Available: http://arxiv.org/abs/1811.12294

work page internal anchor Pith review Pith/arXiv arXiv 2018
[13]

Expressiveness of Proba- bilistic Modal Logics, Revisited,

N. Fijalkow, B. Klin, and P. Panangaden, “Expressiveness of Proba- bilistic Modal Logics, Revisited,” in Procs. ICALP 2017 , ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, 2017, pp. 105:1–105:12

work page 2017
[14]

Codensity lifting of monads and its dual,

S. Katsumata, T. Sato, and T. Uustalu, “Codensity lifting of monads and its dual,” Logical Methods in Computer Science , vol. 14, no. 4,

work page
[15]

Available: https://doi.org/10.23638/LMCS-14(4:6)2018

[Online]. Available: https://doi.org/10.23638/LMCS-14(4:6)2018

work page doi:10.23638/lmcs-14(4:6)2018 2018
[16]

Fibrational bisimulations and quantitative reasoning,

D. Sprunger, S. Katsumata, J. Dubut, and I. Hasuo, “Fibrational bisimulations and quantitative reasoning,” in 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, ser. Lecture Notes in Computer Science, C. C ˆırstea, Ed., v...

work page doi:10.1007/978-3-030-00389-0 2018
[17]

Approximate analysis of probabilistic processes: Logic, simulation and games,

J. Desharnais, F. Laviolette, and M. Tracol, “Approximate analysis of probabilistic processes: Logic, simulation and games,” in 2008 Fifth International Conference on Quantitative Evaluation of Systems , Sep. 2008, pp. 264–273

work page 2008
[18]

Jacobs, Categorical Logic and Type Theory

B. Jacobs, Categorical Logic and Type Theory . Amsterdam: North Holland, 1999

work page 1999
[19]

Bisimulation from open maps,

A. Joyal, M. Nielsen, and G. Winskel, “Bisimulation from open maps,” Inf. Comput., vol. 127, no. 2, pp. 164–185, 1996

work page 1996
[20]

Universal coalgebra: a theory of systems,

J. J. M. M. Rutten, “Universal coalgebra: a theory of systems,” Theor. Comp. Sci., vol. 249, pp. 3–80, 2000

work page 2000
[21]

Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observation , ser

B. Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observation , ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016, vol. 59. [Online]. Available: https://doi.org/10.1017/CBO9781316823187

work page doi:10.1017/cbo9781316823187 2016
[22]

An intrinsic characterization of approximate probabilistic bisimilarity,

F. van Breugel, M. W. Mislove, J. Ouaknine, and J. Worrell, “An intrinsic characterization of approximate probabilistic bisimilarity,” in 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, Apri...

work page doi:10.1007/3-540-36576-1 2003
[23]

Topological (bi-)simulation,

P. J. L. Cuijpers and M. A. Reniers, “Topological (bi-)simulation,” Electr. Notes Theor. Comput. Sci. , vol. 100, pp. 49–64, 2004. [Online]. Available: https://doi.org/10.1016/j.entcs.2004.08.017

work page doi:10.1016/j.entcs.2004.08.017 2004
[24]

Alternating tree automata, parity games, and modal µ- calculus,

T. Wilke, “Alternating tree automata, parity games, and modal µ- calculus,” Bull. Belg. Math. Soc. Simon Stevin, vol. 8, no. 2, pp. 359–391, 2001

work page 2001
[25]

Sparse positional strategies for safety games,

R. Ehlers and D. Moldovan, “Sparse positional strategies for safety games,” in Proceedings First Workshop on Synthesis, SYNT 2012, Berkeley, California, USA, 7th and 8th July 2012. , ser. EPTCS, D. A. Peled and S. Schewe, Eds., vol. 84, 2012, pp. 1–16. [Online]. Available: https://doi.org/10.4204/EPTCS.84.1

work page doi:10.4204/eptcs.84.1 2012
[26]

In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, ACM, pp

T. A. Beyene, S. Chaudhuri, C. Popeea, and A. Rybalchenko, “A constraint-based approach to solving games on inﬁnite graphs,” in The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 , S. Jagannathan and P. Sewell, Eds. ACM, 2014, pp. 221–234. [Online]. Available: https://doi....

work page doi:10.1145/2535838.2535860 2014
[27]

Topological functors,

H. Herrlich, “Topological functors,” General Topology and its Applications, vol. 4, no. 2, pp. 125 – 142, 1974. [Online]. Available: http://www.sciencedirect.com/science/article/pii/0016660X74900166

work page arXiv 1974
[28]

Ad ´amek, H

J. Ad ´amek, H. Herrlich, and G. Strecker, Abstract and Concrete Cate- gories. New York, NY , USA: Wiley-Interscience, 1990

work page 1990
[29]

Semantic domains for combining probability and non-determinism,

R. Tix, K. Keimel, and G. Plotkin, “Semantic domains for combining probability and non-determinism,” Electronic Notes in Theoretical Computer Science , vol. 222, pp. 3 – 99, 2009. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S1571066109000036

work page 2009
[30]

Generic weakest precondition semantics from monads enriched with order,

I. Hasuo, “Generic weakest precondition semantics from monads enriched with order,” Theor. Comput. Sci. , vol. 604, pp. 2–29, 2015. [Online]. Available: http://dx.doi.org/10.1016/j.tcs.2015.03.047

work page doi:10.1016/j.tcs.2015.03.047 2015
[31]

Healthiness from duality,

W. Hino, H. Kobayashi, I. Hasuo, and B. Jacobs, “Healthiness from duality,” in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, M. Grohe, E. Koskinen, and N. Shankar, Eds. ACM, 2016, pp. 682–691

work page 2016
[32]

Fair simulation relations, parity games, and state space reduction for B ¨uchi automata,

K. Etessami, T. Wilke, and R. A. Schuller, “Fair simulation relations, parity games, and state space reduction for B ¨uchi automata,” SIAM J. Comput., vol. 34, no. 5, pp. 1159–1175, 2005. 13 APPENDIX A. Direct Proof of Equivalence of the Two Game Notions Characterizing Probabilistic Bisimilarity (Tables I, III)

work page 2005
[33]

There are two cases to consider which are essentially identical, but we write them down separately just to make sure

Table III ⇝ Table I : Assume that Duplicator wins Table III 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 τ(x,Z ) > τ(y,Z ) then make Spoiler select s = x and play Z in Table III. To this Duplicator responds with some Z′ ⊇Z su...

work page
[34]

A winning strategy for Duplicator in Table III is built not from a single strategy in Table I, but rather from an entire collection of winning positions

Table I ⇝ Table III : This is a less straightforward implication. A winning strategy for Duplicator in Table III 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 chooses ∈ {x,y } and play someZ in Table III. Deﬁne ¯Z = {w ∈X...

work page
[35]

patch up

The Grothendieck Construction: In general, the equiva- lence between index categories Cop → Cat and ﬁbrations is well-known. Here we sketch the Grothendieck construction from the former to the latter, focusing the special case of Cop → CLat⊓ and CLat⊓-ﬁbrations. Its idea is to “patch up” the family ( FEX ) X∈C of complete lattices, and form a big category...

work page
[36]

patch up

Formal Deﬁnition of CLat⊓-Fibration: We axiomatize those structures which arise in the way described above. Deﬁnition A.2 (CLat⊓-ﬁbration). A CLat⊓-ﬁbration p : E → C consists of two categories E, C and a functor p: E → C, that satisfy the following properties. • Each ﬁber EX is a complete lattice. Here the ﬁber EX for X ∈ C is the subcategory of E consis...

work page
[37]

III.11: Proof

Proof of Lem. III.11: Proof. The downset ↓(νΦΩ,τ) is a joint codensity bisimula- tion, because the union of all elements of ↓(νΦΩ,τ) is equal to a codensity bisimulation νΦΩ,τ . Let V be a joint codensity bisimulation. Then for any P ∈ V, we haveP ⊑νΦΩ,τ , becauseP ⊑ ⨆ Q∈VQ ⊑νΦΩ,τ

work page
[38]

IV .2: Proof

Proof of Lem. IV .2: Proof. We follow the following logical equivalence

work page
[39]

τ◦Fk◦c̸∈ E(P, Ω) =⇒ ∃P′∈V

⇐ ⇒ (∀P∈V ,k∈ C(X, Ω). τ◦Fk◦c̸∈ E(P, Ω) =⇒ ∃P′∈V . k̸∈ E(P′, Ω) ) ⇐ ⇒ ( ∀P∈V ,k∈ C(X, Ω). (∀P′∈V . k∈ E(P′, Ω)) =⇒ τ◦Fk◦c∈ E(P, Ω) ) ⇐ ⇒ ( ∀k∈ C(X, Ω). (k∈ E(⨆ P′∈VP′, Ω)) =⇒ τ◦Fk◦c∈ E(⨆ P∈VP, Ω) ) ⇐ ⇒⨆ P∈VP ⊑ ΦΩ,τ(⨆ P′∈VP′), where the last equivalence is by Thm. III.7

work page
[40]

V .6: Proof

Proof of Prop. V .6: Proof. For any X ∈ D, the bijection D(LS,X ) ∼= C(S,RX ) exists. Thus, naturally identifying (R∗E)X and ERX, we have the following for any P,Q ∈ (R∗E)X. ∀f∈ D(LS,X ). f∗P =f∗Q =⇒ ∀f∈ D(LS,X ). (Rf)∗P = (Rf)∗Q =⇒ ∀f∈ D(LS,X ). (Rf◦ηS)∗P = (Rf◦ηS)∗Q =⇒ ∀g∈ C(S,RX ). g∗P =g∗Q =⇒ P =Q

work page
[41]

VII.1: Proof

Proof of Prop. VII.1: Proof. We haveT ΦΩ,τ = ΦTΩ,τT because, for any P ∈ FX, T ΦΩ,τP =T   l A∈A l k∈F(P,Ω(A)) (τA ◦F (rk) ◦c)∗Ω(A)   = l A∈A l k∈F(P,Ω(A)) (τA ◦F (rk) ◦c)∗TΩ(A) = l A∈A l k∈F(P,Ω(A)) (τA ◦F (rk) ◦c)∗TΩ(A) = l A∈A l k∈F(P,Ω(A)) (τA ◦F (p(Tk )) ◦c)∗TΩ(A) = l A∈A l l∈E(TP,T Ω(A)) (τA ◦F (pl) ◦c)∗TΩ(A) = ΦTΩ,τTP holds. Considering this and...

work page

[1] [1]

Concurrency and automata on inﬁnite sequences,

D. Park, “Concurrency and automata on inﬁnite sequences,” in Proceedings of the 5th GI-Conference on Theoretical Computer Science. London, UK, UK: Springer-Verlag, 1981, pp. 167–183. [Online]. Available: http://dl.acm.org/citation.cfm?id=647210.720030

work page arXiv 1981

[2] [2]

Milner, Communication and Concurrency

R. Milner, Communication and Concurrency . Prentice-Hall, 1989

work page 1989

[3] [3]

Sangiorgi and J

D. Sangiorgi and J. Rutten, Eds., Advanced Topics in Bisimulation and Coinduction, ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2011. 12

work page 2011

[4] [4]

Bisimulation through probabilistic testing,

K. G. Larsen and A. Skou, “Bisimulation through probabilistic testing,” Inf. Comput., vol. 94, no. 1, pp. 1–28, 1991

work page 1991

[5] [5]

Metrics for labelled markov processes,

J. Desharnais, V . Gupta, R. Jagadeesan, and P. Panangaden, “Metrics for labelled markov processes,” Theoretical Computer Science , vol. 318, no. 3, pp. 323 – 354, 2004. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S0304397503006042

work page 2004

[6] [6]

Structural induction and coinduction in a ﬁbrational setting,

C. Hermida and B. Jacobs, “Structural induction and coinduction in a ﬁbrational setting,” Inf. Comput. , vol. 145, no. 2, pp. 107–152, 1998. [Online]. Available: https://doi.org/10.1006/inco.1998.2725

work page doi:10.1006/inco.1998.2725 1998

[7] [7]

Coinductive predicates and ﬁnal sequences in a ﬁbration,

I. Hasuo, T. Kataoka, and K. Cho, “Coinductive predicates and ﬁnal sequences in a ﬁbration,” Mathematical Structures in Computer Science, vol. 28, no. 4, pp. 562–611, 2018. [Online]. Available: https://doi.org/10.1017/S0960129517000056

work page doi:10.1017/s0960129517000056 2018

[8] [8]

Coalgebraic behavioral metrics,

P. Baldan, F. Bonchi, H. Kerstan, and B. K ¨onig, “Coalgebraic behavioral metrics,” Logical Methods in Computer Science , vol. 14, no. 3, 2018. [Online]. Available: https://doi.org/10.23638/LMCS-14(3:20)2018

work page doi:10.23638/lmcs-14(3:20)2018 2018

[9] [9]

Coinduction up-to in a ﬁbrational setting,

F. Bonchi, D. Petrisan, D. Pous, and J. Rot, “Coinduction up-to in a ﬁbrational setting,” in Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014 , T. A. Henzinger and D. Miller, Eds. AC...

work page doi:10.1145/2603088.2603149 2014

[10] [10]

(Metric) bisimulation games and real- valued modal logics for coalgebras,

B. K ¨onig and C. Mika-Michalski, “(Metric) bisimulation games and real- valued modal logics for coalgebras,” in 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, 2018, pp. 37:1–37:17

work page 2018

[11] [11]

Up-to techniques for behavioural metrics via ﬁbrations,

F. Bonchi, B. K ¨onig, and D. Petrisan, “Up-to techniques for behavioural metrics via ﬁbrations,” in 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China , ser. LIPIcs, S. Schewe and L. Zhang, Eds., vol. 118. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018, pp. 17:1–17:17. [Online]. Available: http...

work page doi:10.4230/lipics.concur.2018.17 2018

[12] [12]

Path category for free - Open morphisms from coalgebras with non-deterministic branching

T. Wißmann, J. Dubut, S. Katsumata, and I. Hasuo, “Path category for free—open morphisms from coalgebras with non-deterministic branching,” CoRR, vol. abs/1811.12294, 2018, to appear in Proc. FoSSaCS 2019. [Online]. Available: http://arxiv.org/abs/1811.12294

work page internal anchor Pith review Pith/arXiv arXiv 2018

[13] [13]

Expressiveness of Proba- bilistic Modal Logics, Revisited,

N. Fijalkow, B. Klin, and P. Panangaden, “Expressiveness of Proba- bilistic Modal Logics, Revisited,” in Procs. ICALP 2017 , ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, 2017, pp. 105:1–105:12

work page 2017

[14] [14]

Codensity lifting of monads and its dual,

S. Katsumata, T. Sato, and T. Uustalu, “Codensity lifting of monads and its dual,” Logical Methods in Computer Science , vol. 14, no. 4,

work page

[15] [15]

Available: https://doi.org/10.23638/LMCS-14(4:6)2018

[Online]. Available: https://doi.org/10.23638/LMCS-14(4:6)2018

work page doi:10.23638/lmcs-14(4:6)2018 2018

[16] [16]

Fibrational bisimulations and quantitative reasoning,

D. Sprunger, S. Katsumata, J. Dubut, and I. Hasuo, “Fibrational bisimulations and quantitative reasoning,” in 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, ser. Lecture Notes in Computer Science, C. C ˆırstea, Ed., v...

work page doi:10.1007/978-3-030-00389-0 2018

[17] [17]

Approximate analysis of probabilistic processes: Logic, simulation and games,

J. Desharnais, F. Laviolette, and M. Tracol, “Approximate analysis of probabilistic processes: Logic, simulation and games,” in 2008 Fifth International Conference on Quantitative Evaluation of Systems , Sep. 2008, pp. 264–273

work page 2008

[18] [18]

Jacobs, Categorical Logic and Type Theory

B. Jacobs, Categorical Logic and Type Theory . Amsterdam: North Holland, 1999

work page 1999

[19] [19]

Bisimulation from open maps,

A. Joyal, M. Nielsen, and G. Winskel, “Bisimulation from open maps,” Inf. Comput., vol. 127, no. 2, pp. 164–185, 1996

work page 1996

[20] [20]

Universal coalgebra: a theory of systems,

J. J. M. M. Rutten, “Universal coalgebra: a theory of systems,” Theor. Comp. Sci., vol. 249, pp. 3–80, 2000

work page 2000

[21] [21]

Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observation , ser

B. Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observation , ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016, vol. 59. [Online]. Available: https://doi.org/10.1017/CBO9781316823187

work page doi:10.1017/cbo9781316823187 2016

[22] [22]

An intrinsic characterization of approximate probabilistic bisimilarity,

F. van Breugel, M. W. Mislove, J. Ouaknine, and J. Worrell, “An intrinsic characterization of approximate probabilistic bisimilarity,” in 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, Apri...

work page doi:10.1007/3-540-36576-1 2003

[23] [23]

Topological (bi-)simulation,

P. J. L. Cuijpers and M. A. Reniers, “Topological (bi-)simulation,” Electr. Notes Theor. Comput. Sci. , vol. 100, pp. 49–64, 2004. [Online]. Available: https://doi.org/10.1016/j.entcs.2004.08.017

work page doi:10.1016/j.entcs.2004.08.017 2004

[24] [24]

Alternating tree automata, parity games, and modal µ- calculus,

T. Wilke, “Alternating tree automata, parity games, and modal µ- calculus,” Bull. Belg. Math. Soc. Simon Stevin, vol. 8, no. 2, pp. 359–391, 2001

work page 2001

[25] [25]

Sparse positional strategies for safety games,

R. Ehlers and D. Moldovan, “Sparse positional strategies for safety games,” in Proceedings First Workshop on Synthesis, SYNT 2012, Berkeley, California, USA, 7th and 8th July 2012. , ser. EPTCS, D. A. Peled and S. Schewe, Eds., vol. 84, 2012, pp. 1–16. [Online]. Available: https://doi.org/10.4204/EPTCS.84.1

work page doi:10.4204/eptcs.84.1 2012

[26] [26]

In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, ACM, pp

T. A. Beyene, S. Chaudhuri, C. Popeea, and A. Rybalchenko, “A constraint-based approach to solving games on inﬁnite graphs,” in The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 , S. Jagannathan and P. Sewell, Eds. ACM, 2014, pp. 221–234. [Online]. Available: https://doi....

work page doi:10.1145/2535838.2535860 2014

[27] [27]

Topological functors,

H. Herrlich, “Topological functors,” General Topology and its Applications, vol. 4, no. 2, pp. 125 – 142, 1974. [Online]. Available: http://www.sciencedirect.com/science/article/pii/0016660X74900166

work page arXiv 1974

[28] [28]

Ad ´amek, H

J. Ad ´amek, H. Herrlich, and G. Strecker, Abstract and Concrete Cate- gories. New York, NY , USA: Wiley-Interscience, 1990

work page 1990

[29] [29]

Semantic domains for combining probability and non-determinism,

R. Tix, K. Keimel, and G. Plotkin, “Semantic domains for combining probability and non-determinism,” Electronic Notes in Theoretical Computer Science , vol. 222, pp. 3 – 99, 2009. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S1571066109000036

work page 2009

[30] [30]

Generic weakest precondition semantics from monads enriched with order,

I. Hasuo, “Generic weakest precondition semantics from monads enriched with order,” Theor. Comput. Sci. , vol. 604, pp. 2–29, 2015. [Online]. Available: http://dx.doi.org/10.1016/j.tcs.2015.03.047

work page doi:10.1016/j.tcs.2015.03.047 2015

[31] [31]

Healthiness from duality,

W. Hino, H. Kobayashi, I. Hasuo, and B. Jacobs, “Healthiness from duality,” in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, M. Grohe, E. Koskinen, and N. Shankar, Eds. ACM, 2016, pp. 682–691

work page 2016

[32] [32]

Fair simulation relations, parity games, and state space reduction for B ¨uchi automata,

K. Etessami, T. Wilke, and R. A. Schuller, “Fair simulation relations, parity games, and state space reduction for B ¨uchi automata,” SIAM J. Comput., vol. 34, no. 5, pp. 1159–1175, 2005. 13 APPENDIX A. Direct Proof of Equivalence of the Two Game Notions Characterizing Probabilistic Bisimilarity (Tables I, III)

work page 2005

[33] [33]

There are two cases to consider which are essentially identical, but we write them down separately just to make sure

Table III ⇝ Table I : Assume that Duplicator wins Table III 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 τ(x,Z ) > τ(y,Z ) then make Spoiler select s = x and play Z in Table III. To this Duplicator responds with some Z′ ⊇Z su...

work page

[34] [34]

A winning strategy for Duplicator in Table III is built not from a single strategy in Table I, but rather from an entire collection of winning positions

Table I ⇝ Table III : This is a less straightforward implication. A winning strategy for Duplicator in Table III 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 chooses ∈ {x,y } and play someZ in Table III. Deﬁne ¯Z = {w ∈X...

work page

[35] [35]

patch up

The Grothendieck Construction: In general, the equiva- lence between index categories Cop → Cat and ﬁbrations is well-known. Here we sketch the Grothendieck construction from the former to the latter, focusing the special case of Cop → CLat⊓ and CLat⊓-ﬁbrations. Its idea is to “patch up” the family ( FEX ) X∈C of complete lattices, and form a big category...

work page

[36] [36]

patch up

Formal Deﬁnition of CLat⊓-Fibration: We axiomatize those structures which arise in the way described above. Deﬁnition A.2 (CLat⊓-ﬁbration). A CLat⊓-ﬁbration p : E → C consists of two categories E, C and a functor p: E → C, that satisfy the following properties. • Each ﬁber EX is a complete lattice. Here the ﬁber EX for X ∈ C is the subcategory of E consis...

work page

[37] [37]

III.11: Proof

Proof of Lem. III.11: Proof. The downset ↓(νΦΩ,τ) is a joint codensity bisimula- tion, because the union of all elements of ↓(νΦΩ,τ) is equal to a codensity bisimulation νΦΩ,τ . Let V be a joint codensity bisimulation. Then for any P ∈ V, we haveP ⊑νΦΩ,τ , becauseP ⊑ ⨆ Q∈VQ ⊑νΦΩ,τ

work page

[38] [38]

IV .2: Proof

Proof of Lem. IV .2: Proof. We follow the following logical equivalence

work page

[39] [39]

τ◦Fk◦c̸∈ E(P, Ω) =⇒ ∃P′∈V

⇐ ⇒ (∀P∈V ,k∈ C(X, Ω). τ◦Fk◦c̸∈ E(P, Ω) =⇒ ∃P′∈V . k̸∈ E(P′, Ω) ) ⇐ ⇒ ( ∀P∈V ,k∈ C(X, Ω). (∀P′∈V . k∈ E(P′, Ω)) =⇒ τ◦Fk◦c∈ E(P, Ω) ) ⇐ ⇒ ( ∀k∈ C(X, Ω). (k∈ E(⨆ P′∈VP′, Ω)) =⇒ τ◦Fk◦c∈ E(⨆ P∈VP, Ω) ) ⇐ ⇒⨆ P∈VP ⊑ ΦΩ,τ(⨆ P′∈VP′), where the last equivalence is by Thm. III.7

work page

[40] [40]

V .6: Proof

Proof of Prop. V .6: Proof. For any X ∈ D, the bijection D(LS,X ) ∼= C(S,RX ) exists. Thus, naturally identifying (R∗E)X and ERX, we have the following for any P,Q ∈ (R∗E)X. ∀f∈ D(LS,X ). f∗P =f∗Q =⇒ ∀f∈ D(LS,X ). (Rf)∗P = (Rf)∗Q =⇒ ∀f∈ D(LS,X ). (Rf◦ηS)∗P = (Rf◦ηS)∗Q =⇒ ∀g∈ C(S,RX ). g∗P =g∗Q =⇒ P =Q

work page

[41] [41]

VII.1: Proof

Proof of Prop. VII.1: Proof. We haveT ΦΩ,τ = ΦTΩ,τT because, for any P ∈ FX, T ΦΩ,τP =T   l A∈A l k∈F(P,Ω(A)) (τA ◦F (rk) ◦c)∗Ω(A)   = l A∈A l k∈F(P,Ω(A)) (τA ◦F (rk) ◦c)∗TΩ(A) = l A∈A l k∈F(P,Ω(A)) (τA ◦F (rk) ◦c)∗TΩ(A) = l A∈A l k∈F(P,Ω(A)) (τA ◦F (p(Tk )) ◦c)∗TΩ(A) = l A∈A l l∈E(TP,T Ω(A)) (τA ◦F (pl) ◦c)∗TΩ(A) = ΦTΩ,τTP holds. Considering this and...

work page