Quantitative Logic and Games

In this talk, we investigate quantitative variants of modal logic and its fixpoint extension, the modal mu-calculus. We study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts.

It turns out that the model checking problem for the quantitative mu-calculus can indeed be characterised by a quantitative variant of parity games, provided that the quantitative mu-calculus is defined in an appropriate way respecting the duality properties between the logical operators.

These games, however, although a natural generalisation of parity games, have quite different properties than their qualitative counterparts, in particular they are, in general, not positionally determined.

We also briefly discuss the problems that arose in previous definitions of quantitative logics and show how the game-theoretical approach further helps in understanding and defining the semantics of quantitative logics.