Using Coalgebras and the Giry Monad for Interpreting Game Logics --- A Tutorial

TL;DR

This tutorial introduces a measure-theoretic approach using coalgebras and the Giry monad for interpreting stochastic game logics, emphasizing probabilistic nondeterminism beyond traditional Kripke models.

Contribution

It provides a comprehensive, accessible introduction to the Giry monad and coalgebraic techniques for probabilistic game logic interpretation, bridging measure theory and categorical methods.

Findings

Clarifies the use of the Giry monad in probabilistic semantics

Provides techniques for manipulating Kleisli morphisms

Facilitates understanding of measure-theoretic foundations in stochastic systems

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 their 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.