# Matteo Mio

*The probabilistic modal mu calculus and its semantics*

The probabilistic modal mu-calculus, introduced in [1, 2, 3], is a generalization of the standard modal mu-calculus, designed for expressing properties of probabilistic transitions systems. Two semantics have been proposed for this logic: one denotational [1,3] (in the style of Kozen) and one based on two player stochastic games [2] (in the style of Stirling). The problem of proving that the two semantics coincide on every (infinite) model was left open in [2]. In this lab lunch talk, I will introduce the two semantics and state that they indeed coincide on every model.

[1] L. de Alfaro and R. Majumdar. Quantitative solution of omega-regular games. 2004 [2] A. McIver and C. Morgan. Results on the quantitative mu-calculus qmu. 2003 [3] Michael Huth and Marta Kwiatkowska. Quantitative analysis and model checking 1997