Preservation and reflection of bisimilarity via invertible steps. (English) Zbl 07770344
Kupferman, Orna (ed.) et al., Foundations of software science and computation structures. 26th international conference, FOSSACS 2023, held as part of the European joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22–27, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13992, 328-348 (2023).
Summary: In the theory of coalgebras, distributive laws give a general perspective on determinisation and other automata constructions. This perspective has recently been extended to include so-called weak distributive laws, covering several constructions on state-based systems that are not captured by regular distributive laws, such as the construction of a belief-state transformer from a probabilistic automaton, and ultrafilter extensions of Kripke frames.
In this paper we first observe that weak distributive laws give rise to the more general notion of what we call an invertible step: a pair of natural transformations that allows to move coalgebras along an adjunction. Our main result is that part of the construction induced by an invertible step preserves and reflects bisimilarity. This covers results that have previously been shown by hand for the instances of ultrafilter extensions and belief-state transformers.
For the entire collection see [Zbl 1524.68006].
In this paper we first observe that weak distributive laws give rise to the more general notion of what we call an invertible step: a pair of natural transformations that allows to move coalgebras along an adjunction. Our main result is that part of the construction induced by an invertible step preserves and reflects bisimilarity. This covers results that have previously been shown by hand for the instances of ultrafilter extensions and belief-state transformers.
For the entire collection see [Zbl 1524.68006].
References:
| [1] | Aczel, P., Mendler, N.P.: A final coalgebra theorem. In: Category Theory and Computer Science. Lecture Notes in Computer Science, vol. 389, pp. 357-365. Springer (1989) · Zbl 1496.03206 |
| [2] | Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and Concrete Categories - The Joy of Cats. Dover Publications (2009) · Zbl 0695.18001 |
| [3] | Bartels, F., Sokolova, A., de Vink, E.P.: A hierarchy of probabilistic system types. Theor. Comput. Sci. 327(1-2), 3-22 (2004) · Zbl 1071.68071 |
| [4] | van Benthem, J.: Canonical modal logics and ultrafilter extensions. The Journal of Symbolic Logic 44(1), 1-8 (1979), publisher: Cambridge University Press · Zbl 0405.03011 |
| [5] | Bezhanishvili, N., Fontaine, G., Venema, Y.: Vietoris bisimulations. J. Log. Comput. 20(5), 1017-1040 (2010) · Zbl 1266.03029 |
| [6] | Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001) · Zbl 0988.03006 |
| [7] | Bonchi, F., Bonsangue, M.M., Boreale, M., Rutten, J.J.M.M., Silva, A.: A coalgebraic perspective on linear weighted automata. Inf. Comput. 211, 77-105 (2012) · Zbl 1279.68235 |
| [8] | Bonchi, F., Bonsangue, M.M., Caltais, G., Rutten, J., Silva, A.: A coalgebraic view on decorated traces. Math. Struct. Comput. Sci. 26(7), 1234-1268 (2016) · Zbl 1364.68276 |
| [9] | Bonchi, F., Petrisan, D., Pous, D., Rot, J.: A general account of coinduction up-to. Acta Informatica 54(2), 127-190 (2017) · Zbl 1371.68186 |
| [10] | Bonchi, F., Santamaria, A.: Combining semilattices and semimodules. In: FoSSaCS. Lecture Notes in Computer Science, vol. 12650, pp. 102-123. Springer (2021) · Zbl 07410421 |
| [11] | Bonchi, F., Silva, A., Sokolova, A.: The power of convex algebras. In: CONCUR. LIPIcs, vol. 85, pp. 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017) · Zbl 1442.68085 |
| [12] | Bonchi, F., Silva, A., Sokolova, A.: Distribution bisimilarity via the power of convex algebras. Log. Methods Comput. Sci. 17(3) (2021) · Zbl 1480.18005 |
| [13] | Bonsangue, M.M., Hansen, H.H., Kurz, A., Rot, J.: Presenting distributive laws. Log. Methods Comput. Sci. 11(3) (2015) · Zbl 1448.68324 |
| [14] | Bonsangue, M.M., Kurz, A.: Duality for logics of transition systems. In: FoSSaCS. Lecture Notes in Computer Science, vol. 3441, pp. 455-469. Springer (2005) · Zbl 1119.03021 |
| [15] | Bonsangue, M.M., Milius, S., Silva, A.: Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log. 14(1), 7:1-7:52 (2013) · Zbl 1353.68186 |
| [16] | Borceux, F.: Handbook of categorical algebra: volume 1, Basic category theory, vol. 1. Cambridge University Press (1994) · Zbl 0911.18001 |
| [17] | Chen, L., Jung, A.: On a categorical framework for coalgebraic modal logic. In: MFPS. Electronic Notes in Theoretical Computer Science, vol. 308, pp. 109-128. Elsevier (2014) · Zbl 1337.03091 |
| [18] | Enqvist, S., Sourabh, S.: Bisimulations for coalgebras on Stone spaces. J. Log. Comput. 28(6), 991-1010 (2018) · Zbl 1444.03186 |
| [19] | Garner, R.: The Vietoris monad and weak distributive laws. Appl. Categorical Struct. 28(2), 339-354 (2020) · Zbl 1442.18010 |
| [20] | Goldblatt, R.I.: Metamathematics of modal logic. Bulletin of the Australian Mathematical Society 10(3), 479-480 (1974), publisher: Cambridge University Press · Zbl 0273.02016 |
| [21] | Goy, A.: On the compositionality of monads via weak distributive laws. (Compositionnalité des monades par lois de distributivité faibles). Ph.D. thesis, University of Paris-Saclay, France (2021) |
| [22] | Goy, A., Petrisan, D.: Combining probabilistic and non-deterministic choice via weak distributive laws. In: LICS. pp. 454-464. ACM (2020) · Zbl 1502.68171 |
| [23] | Goy, A., Petrisan, D., Aiguier, M.: Powerset-like monads weakly distribute over themselves in toposes and compact Hausdorff spaces. In: ICALP. LIPIcs, vol. 198, pp. 132:1-132:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021) |
| [24] | Gumm, H.P., Taheri, M.: Saturated Kripke structures as Vietoris coalgebras. In: CMCS. Lecture Notes in Computer Science, vol. 13225, pp. 88-109. Springer (2022) · Zbl 07628068 |
| [25] | Hasuo, I., Kataoka, T., Cho, K.: Coinductive predicates and final sequences in a fibration. Math. Struct. Comput. Sci. 28(4), 562-611 (2018) · Zbl 1386.68103 |
| [26] | Hermida, C.: On fibred adjunctions and completeness for fibred categories. In: COMPASS/ADT. Lecture Notes in Computer Science, vol. 785, pp. 235-251. Springer (1992) · Zbl 0941.18501 |
| [27] | Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107-152 (1998) · Zbl 0941.18006 |
| [28] | Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation, Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press (2016) · Zbl 1364.68001 |
| [29] | Jacobs, B., Silva, A., Sokolova, A.: Trace semantics via determinization. J. Comput. Syst. Sci. 81(5), 859-879 (2015) · Zbl 1327.68158 |
| [30] | Jacobs, B.P.F.: Categorical Logic and Type Theory, Studies in logic and the foundations of mathematics, vol. 141. North-Holland (2001) · Zbl 0911.03001 |
| [31] | Kelly, G.M., Street, R.: Review of the elements of 2-categories. In: Kelly, G.M. (ed.) Category Seminar: Proceedings Sydney Category Seminar 1972/1973. No. 420 in Lecture Notes in Mathematics, Springer-Verlag (1974) · Zbl 0334.18016 |
| [32] | Klin, B.: Coalgebraic modal logic beyond sets. In: MFPS. Electronic Notes in Theoretical Computer Science, vol. 173, pp. 177-201. Elsevier (2007) · Zbl 1316.03017 |
| [33] | Klin, B.: Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci. 412(38), 5043-5069 (2011) · Zbl 1246.68150 |
| [34] | Klin, B., Salamanca, J.: Iterated covariant powerset is not a monad. In: MFPS. Electronic Notes in Theoretical Computer Science, vol. 341, pp. 261-276. Elsevier (2018) · Zbl 1528.18007 |
| [35] | Kupke, C., Kurz, A., Pattinson, D.: Algebraic semantics for coalgebraic logics. In: CMCS. Electronic Notes in Theoretical Computer Science, vol. 106, pp. 219-241. Elsevier (2004) · Zbl 1271.03031 |
| [36] | Kupke, C., Kurz, A., Pattinson, D.: Ultrafilter extensions for coalgebras. In: CALCO. Lecture Notes in Computer Science, vol. 3629, pp. 263-277. Springer (2005) · Zbl 1151.03357 |
| [37] | Leinster, T.: Higher Operads, Higher Categories, London Mathematical Society Lecture Notes, vol. 298. Cambridge University Press (2004) · Zbl 1160.18001 |
| [38] | Levy, P.B.: Final coalgebras from corecursive algebras. In: CALCO. LIPIcs, vol. 35, pp. 221-237. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015) · Zbl 1366.03244 |
| [39] | Manes, E.: A triple theoretic construction of compact algebras. In: Seminar on triples and categorical homology theory. pp. 91-118. Springer (1969) · Zbl 0186.02901 |
| [40] | Pavlovic, D., Mislove, M.W., Worrell, J.: Testing semantics: Connecting processes and process logics. In: AMAST. Lecture Notes in Computer Science, vol. 4019, pp. 308-322. Springer (2006) · Zbl 1236.68065 |
| [41] | Rot, J., Jacobs, B., Levy, P.B.: Steps and traces. J. Log. Comput. 31(6), 1482-1525 (2021) · Zbl 1509.18003 |
| [42] | Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3-80 (2000) · Zbl 0951.68038 |
| [43] | Silva, A., Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M.: Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci. 9(1) (2013) · Zbl 1262.18002 |
| [44] | Staton, S.: Relating coalgebraic notions of bisimulation. Log. Methods Comput. Sci. 7(1) (2011) · Zbl 1247.68192 |
| [45] | Turi, D., Plotkin, G.D.: Towards a mathematical operational semantics. In: LICS. pp. 280-291. IEEE Computer Society (1997) |
| [46] | Varacca, D.: Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. Ph.D. thesis, University of Aarhus (2003) |
| [47] | Zwart, M., Marsden, D.: No-go theorems for distributive laws. Log. Methods Comput. Sci. 18(1) (2022) · Zbl 07471702 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
