Model Checking Games for the Quantitative µ-Calculus

Abstract

We investigate quantitative extensions of modal logic and the modal
   $mu$-calculus, and 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, if the
   quantitative $mu$-calculus is defined in an appropriate way
   respecting the duality properties between the logical operators,
   then its model checking problem can indeed be characterised by a
   quantitative variant of parity games.  However, these quantitative
   games have quite different properties than their classical
   counterparts, in particular they are, in general, not positionally
   determined.  The correspondence between the logic and the games
   goes both ways: the value of a formula on a quantitative transition
   system coincides with the value of the associated quantitative
   game, and conversely, the values of quantitative parity games are
   definable in the quantitative $mu$-calculus.