Matteo Mio: The probabilistic modal mu-calculus win independent product

Matteo Mio
University of Edinburgh

Abstract: The modal µ-calculus (Lµ) is the logic obtained by extending standard propositional modal logic with least and greatest fixed points operators. This logic was intensively studied in the last 20 years, as it allows the expression of many interesting properties of labeled transition systems.

The probabilistic modal µ-calculus (pLµ) is a generalization of Lµ, designed for expressing properties of probabilistic labeled transition systems.

In this talk I will discuss an extension of pLµ, called probabilistic modal µ-calculus with independent product, which can express more complex properties of practical interest. We provide two semantics for this extended logic: one denotational and one based on a new class of games which we call tree games. The main result is the equivalence of the two semantics. The proof is carried out in ZFC set theory extended with Martin’s Axiom at the first uncountable cardinal.

Vabljeni!