Working Seminar on Formal Models, Discrete Structures, and Algorithms

The Quantitative mu-Calculus

Diana Fischer (RWTH Aachen)

When: November 26, 1pm

Where: room G2.91b


In this talk, we present a quantitative extension of the modal mu-calculus and give an overview over the results obtained for this logic. In the quantitative mu-calculus, formulae cannot just evaluate to true or false but to arbitrary real values. The semantics is given by quantitative transition systems, i.e. directed graphs where the nodes are labelled with real values. The connection to games is a fundamental aspect of logics, so we study the question whether this connection can be lifted from the qualitative logics to their quantitative counterparts. For the modal mu-calculus, model checking is described by parity games. We show a similar correspondence in the quantitative setting for an appropriate quantitative extension of parity games. Furthermore, we discuss a quantitative notion of bisimulation and present quantitative versions of the invariance theorem for the mu-calculus, and the characterisation theorem for modal logic on finitely-branching systems. Towards practical applications, we show how to model-check the quantitative mu-calculus on discounted systems, i.e. graphs where also the edges are labelled with real values, and on a simple class of hybrid systems, again using a game-based approach.