nach oben

New Generation Computing

Erschienen in:

03.08.2022

Codensity Games for Bisimilarity

verfasst von: Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Samuel Humeau, Clovis Eberhart, Ichiro Hasuo

Erschienen in: New Generation Computing | Ausgabe 2/2022

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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, such as 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 what we call codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric and bisimulation seminorm) as well as new ones (including what we call bisimulation topology).

Vorheriger Artikel Preface to Hagiya-sensei’s 26-th Birthday Special Issue

Nächster Artikel Making Programs Reversible with Minimal Extra Data

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

Park, D.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science, pp. 167–183. Springer, London (1981). http://dl.acm.org/citation.cfm?id=647210.720030

Milner, R.: Communication and Concurrency. Prentice-Hall, Hoboken (1989)MATH

Sangiorgi, D., Rutten, J. (eds.): Advanced Topics in Bisimulation and Coinduction. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2011). https://doi.org/10.1017/CBO9780511792588CrossRef

Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)MathSciNetCrossRef

Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004). https://doi.org/10.1016/j.tcs.2003.09.013MathSciNetCrossRefMATH

Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107–152 (1998). https://doi.org/10.1006/inco.1998.2725MathSciNetCrossRefMATH

Hasuo, I., Kataoka, T., Cho, K.: Coinductive predicates and final sequences in a fibration. Math. Struct. Comput. Sci. 28(4), 562–611 (2018). https://doi.org/10.1017/S0960129517000056MathSciNetCrossRefMATH

Baldan, P., Bonchi, F., Kerstan, H., König, B.: Coalgebraic behavioral metrics. Log. Methods Comput. Sci. (2018). https://doi.org/10.23638/LMCS-14(3:20)2018MathSciNetCrossRefMATH

Bonchi, F., Petrisan, D., Pous, D., Rot, J.: Coinduction up-to in a fibrational setting. In: Henzinger, T.A., Miller, D. (eds.) 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, pp. 20–1209. ACM (2014). https://doi.org/10.1145/2603088.2603149

10.

König, B., Mika-Michalski, C.: (Metric) bisimulation games and real-valued modal logics for coalgebras. In: 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, pp. 37–13717. Beijing, China (2018)

11.

Bonchi, F., König, B., Petrisan, D.: Up-to techniques for behavioural metrics via fibrations. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, vol. 118, pp. 17–11717. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.17

12.

Wißmann, T., Dubut, J., Katsumata, S., Hasuo, I.: Path category for free—open morphisms from coalgebras with non-deterministic branching. CoRR (2018). arXiv:1811.12294 (To appear in Proc. FoSSaCS 2019)

13.

Fijalkow, N., Klin, B., Panangaden, P.: Expressiveness of probabilistic modal logics, Revisited. In: Procs. ICALP 2017. Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, pp. 105–110512 (2017)

14.

Katsumata, S., Sato, T., Uustalu, T.: Codensity lifting of monads and its dual. Log. Methods Comput. Sci. (2018). https://doi.org/10.23638/LMCS-14(4:6)2018MathSciNetCrossRefMATH

15.

Sprunger, D., Katsumata, S., Dubut, J., Hasuo, I.: Fibrational bisimulations and quantitative reasoning. In: Cîrstea, C. (ed.) 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. Lecture Notes in Computer Science, vol. 11202, pp. 190–213. Springer (2018). https://doi.org/10.1007/978-3-030-00389-0_11

16.

Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: Logic, simulation and games. In: 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp. 264–273 (2008). https://doi.org/10.1109/QEST.2008.42

17.

Komorida, Y., Katsumata, S., Hu, N., Klin, B., Hasuo, I.: Codensity games for bisimilarity. In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pp. 1–13. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785691

18.

Staton, S.: Relating coalgebraic notions of bisimulation. Log. Methods Comput. Sci. (2011). https://doi.org/10.2168/LMCS-7(1:13)2011MathSciNetCrossRefMATH

19.

Bakhtiari, Z., Hansen, H.H.: Bisimulation for weakly expressive coalgebraic modal logics. In: Bonchi, F., König, B. (eds.) 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 72, pp. 4–1416. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2017). https://doi.org/10.4230/LIPIcs.CALCO.2017.4. http://drops.dagstuhl.de/opus/volltexte/2017/8050

20.

Balle, B., Gourdeau, P., Panangaden, P.: Bisimulation Metrics for Weighted Automata. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl, A. (eds.) 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, pp. 103–110314. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2017). https://doi.org/10.4230/LIPIcs.ICALP.2017.103. http://drops.dagstuhl.de/opus/volltexte/2017/7395

21.

Komorida, Y., Katsumata, S.-y., Kupke, C., Rot, J., Hasuo, I.: Expressivity of quantitative modal logics : Categorical foundations via codensity and approximation. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–14 (2021). https://doi.org/10.1109/LICS52264.2021.9470656

22.

Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Inf. Comput. 127(2), 164–185 (1996)MathSciNetCrossRef

23.

Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3–80 (2000)MathSciNetCrossRef

24.

Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press, Cambridge (2016). https://doi.org/10.1017/CBO9781316823187CrossRef

25.

van Breugel, F., Mislove, M.W., Ouaknine, J., Worrell, J.: An intrinsic characterization of approximate probabilistic bisimilarity. In: Gordon, A.D. (ed.) Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2620, pp. 200–215. Springer (2003). https://doi.org/10.1007/3-540-36576-1_13

26.

Cuijpers, P.J.L., Reniers, M.A.: Topological (bi-)simulation. Electr. Notes Theor. Comput. Sci. 100, 49–64 (2004). https://doi.org/10.1016/j.entcs.2004.08.017CrossRefMATH

27.

Baldan, P., König, B., Mika-Michalski, C., Padoan, T.: Fixpoint games on continuous lattices. Proc. ACM Program. Lang. (2019). https://doi.org/10.1145/3290339CrossRef

28.

Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)MathSciNetCrossRef

29.

Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pac. J. Math. 82(1), 43–57 (1979)MathSciNetCrossRef

30.

Wilke, T.: Alternating tree automata, parity games, and modal \(\mu\)-calculus. Bull. Belg. Math. Soc. Simon Stevin 8(2), 359–391 (2001)MathSciNetCrossRef

31.

Ehlers, R., Moldovan, D.: Sparse positional strategies for safety games. In: Peled, D.A., Schewe, S. (eds.) Proceedings First Workshop on Synthesis, SYNT 2012, Berkeley, California, USA, 7th and 8th July 2012. EPTCS, vol. 84, pp. 1–16 (2012). https://doi.org/10.4204/EPTCS.84.1

32.

Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pp. 221–234. ACM (2014). https://doi.org/10.1145/2535838.2535860

33.

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

34.

Herrlich, H.: Topological functors. Gen. Topol. Appl. 4(2), 125–142 (1974). https://doi.org/10.1016/0016-660X(74)90016-6MathSciNetCrossRefMATH

35.

Adámek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories. Wiley-Interscience, New York (1990)MATH

36.

Tix, R., Keimel, K., Plotkin, G.: Semantic domains for combining probability and non-determinism. Electron. Notes Theor. Comput. Sci. 222, 3–99 (2009). https://doi.org/10.1016/j.entcs.2009.01.002CrossRefMATH

37.

Hasuo, I.: Generic weakest precondition semantics from monads enriched with order. Theor. Comput. Sci. 604, 2–29 (2015). https://doi.org/10.1016/j.tcs.2015.03.047MathSciNetCrossRefMATH

38.

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

39.

MacLane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5, 2nd edn. Springer, Berlin (1998)

40.

Blackburn, P., Rijke, M.D., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001). https://doi.org/10.1017/CBO9781107050884CrossRefMATH

41.

Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002). https://doi.org/10.1017/CBO9780511809088CrossRefMATH

42.

Vickers, S.: Topology Via Logic Tracts in Theoretical Computer Science, vol. 5. Cambridge University Press, Cambridge (1989)

43.

Schröder, L.: Expressivity of coalgebraic modal logic: the limits and beyond. Theor. Comput. Sci. 390(2–3), 230–247 (2008). https://doi.org/10.1016/j.tcs.2007.09.023MathSciNetCrossRefMATH

44.

Klin, B.: The least fibred lifting and the expressivity of coalgebraic modal logic. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J.J.M.M. (eds.) Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3629, pp. 247–262. Springer (2005). https://doi.org/10.1007/11548133_16

45.

Adámek, J., Gumm, H.P., Trnková, V.: Presentation of set functors: a coalgebraic perspective. J. Log. Comput. 20(5), 991–1015 (2010). https://doi.org/10.1093/logcom/exn090MathSciNetCrossRefMATH

46.

Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log. 45(1), 19–33 (2004). https://doi.org/10.1305/ndjfl/1094155277MathSciNetCrossRefMATH

47.

Boreale, M.: Weighted bisimulation in linear algebraic form. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009-Concurrency Theory, pp. 163–177. Springer, Berlin (2009)CrossRef

48.

Conway, J.B.: A Course in Functional Analysis. Graduate Texts in Mathematics, vol. 96, 2nd edn. Springer, Berlin (2007)CrossRef

49.

Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005)MathSciNetCrossRef

Titel: Codensity Games for Bisimilarity
verfasst von: Yuichi Komorida
Shin-ya Katsumata
Nick Hu
Bartek Klin
Samuel Humeau
Clovis Eberhart
Ichiro Hasuo
Publikationsdatum: 03.08.2022
Verlag: Ohmsha
Erschienen in: New Generation Computing / Ausgabe 2/2022
Print ISSN: 0288-3635
Elektronische ISSN: 1882-7055
DOI: https://doi.org/10.1007/s00354-022-00186-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2022

Making Programs Reversible with Minimal Extra Data

Toggling Between Two Limit Cycles in a Molecular Ecosystem

The Weak Universality of Two-Dimensional Five-State von Neumann Neighborhood Number-Conserving Cellular Automaton

Preface to Hagiya-sensei’s 26-th Birthday Special Issue

Monotone Control of R Systems

Autonomous and Programmable Strand Generator Implemented as DNA and Enzymatic Chemical Reaction Cascade

Premium Partner