Using coalgebras and the Giry monad for interpreting game logics— a tutorial

Abstract

The stochastic interpretation of Parikh’s game logic should not follow the usual pattern of Kripke models, which in turn are based on the Kleisli morphisms for the Giry monad, rather, a specific and more general approach to probabilistic nondeterminism is required.We outline this approach together with its probabilistic and measure theoretic basis, introducing in a leisurely pace the Giry monad and its Kleisli morphisms together with important techniques for manipulating them. Proof establishing specific techniques are given, and pointers to the extant literature are provided.

After working through this tutorial, the reader should find it easier to follow the original literature in this and related areas, and it should be possible for her or him to appreciate measure theoretic arguments for original work in the areas of Markov transition systems, and stochastic effectivity functions.

Keywords

coalgebras / modal logics / monads / Giry monad / upper closed monad / composition of monads / game logics

References

[1] RuttenJ J M M. Universal coalgebra: a theory of systems. Theoretical Computer Science, 2000, 249(1): 3–80

[2] VenemaY. 6 Algebras and co-algebras. Studies in Logic and Practical Reasoning, 2007, 3: 331–426

[3] JacobsB. Introduction to Coalgebra: Towards Mathematics of States and Observations. Cambridge: Cambridge University Press, 2016

[4] DoberkatE E. Special Topics in Mathematics for Computer Science: Sets, Categories, Topologies, Measures. Springer, 2015

[5] DoberkatE E. Algebraic properties of stochastic effectivity functions. Journal of Logical and Algebraic Methods in Programming, 2014, 83(3): 339–358

[6] DoberkatE E. A stochastic interpretation of game logic. 2016, arXiv: 1403.7765

[7] HennessyM, MilnerR. On observing nondeterminism and concurrency. In: Proceedings of the International Colloquium on Automata, Languages, and Programming. 1980, 299–309

[8] DoberkatE E. A note on the coalgebraic interpretation of game logic. Rend.istit.mat.univ.trieste, 2010, 42: 191–203

[9] DoberkatE E. Stochastic Coalgebraic Logic. Berlin: Springer-Verlag, 2009

[10] SrivastavaS M. A Course on Borel Sets (Graduate Texts in Mathematics). New York: Springer-Verlag, 1998

[11] TerrafP S. Unprovability of the logical characterization of bisimulation. Information and Computation, 2011, 209(7): 1048–1056

[12] DesharnaisJ, EdalatA, PanangadenP . Bisimulation of labelled Markov processes. Information and Computation, 2002, 179(2): 163–193

[13] EdalatA. Semi-pullbacks and bisimulations in categories of Markov processes. Mathematical Structures in Computer Science, 1999, 9(5): 523–543

[14] DoberkatE E. Semi-pullbacks for stochastic relations over analytic spaces. Mathematical Structures in Computer Science, 2005, 15(4): 647–670

[15] DoberkatE E. Semi-pullbacks and bisimulations in categories of stochastic relations. In: Proceedings of the International Colloquium on Automata, Languages, and Programming. 2003, 996–1007

[16] ParikhR.The logic of games and its applications. North-Holland Mathematics Studies, 1985, 102: 111–139

[17] PaulyM, ParikhR. Game logic—an overview. Studia Logica, 2003, 75(2): 165–182

[18] Van BenthemJ. Logic games are complete for game logics. Studia Logica, 2003, 75(2): 183–203

[19] PaulyM. Game Logic for Game Theorists.Centrum voor Wiskunde en Informatica, 2000

[20] GoldblattR. Deduction systems for coalgebras over measurable spaces. Journal of Logic and Computation, 2010, 20(5): 1069–1100

[21] MossL S. Coalgebraic logic. Annals of Pure and Applied Logic, 1999, 96(1): 277–317

[22] SchröderL. Expressivity of coalgebraic modal logic: the limits and beyond. Theoretical Computer Science, 2008, 390(2): 230–247

[23] D’argenioP R, Terraf P S, WolovickN . Bisimulations for nondeterministic labelled Markov processes. Mathematical Structures in Computer Science, 2012, 22(1): 43–68

[24] DoberkatE E, TerrafP S. Stochastic non-determinism and effectivity functions. Journal of Logic and Computation, doi: 10.1093/logcom/ exv049 (arxiv: 1405.7141), 2015

[25] JechT. Set Theory. 3rd ed. Berlin: Springer-Verlag, 2006

[26] HalmosP R. Measure Theory (Graduate Texts in Mathematics). Springer Science & Business Media, 2007

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg