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

摘要

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.