First Talk: Game Semantics for Probabilistic mu-Calculi
In this talk I will consider several 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 which I call Tree games. I will discuss 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). I will also present some more recent results (joint work with Alex Simpson).