Game Semantics for Probabilistic mu-Calculi

In this talk I will consider (a family of) probabilistic (or quantitative) variants of Kozen's Modal mu-Calculus, designed for expressing properties of probabilistic-nondeterministic transition systems. Two type of semantics can be defined for these logics: one denotational and one based on a novel kind of games, called Tree Games, which I will introduce. I will discuss some of the ideas behind the main result of my PhD thesis: the equivalence of the two semantics (proved in ZFC set theory extended with Martin’s Axiom at the first uncountable cardinal).