The quantitative µ-calculus

• Der Quantitative µ-Kalkül

Fischer, Diana; Grädel, Erich (Thesis advisor)

Aachen : Publikationsserver der RWTH Aachen University (2013)
Dissertation / PhD Thesis

Aachen, Techn. Hochsch., Diss., 2013

Abstract

This thesis studies a generalisation of the modal µ-calculus, a modal fixed-point logic that is an important specification language in formal verification. We define a quantitative generalisation of this logic, meaning that formulae do not evaluate to just true or false anymore but instead to arbitrary real values. First, this logic is evaluated on a quantitative extension of transition systems equipped with quantitative predicates that assign real values to the nodes of the system. Having fixed a quantitative semantics, we investigate which of the classical theorems established for the modal µ-calculus can be lifted to this quantitative setting. The modal µ-calculus is connected to bisimulation, a notion of behavioural equivalence for transition systems. We define a quantitative notion of bisimulation as a distance between systems. First, we show that for systems that have a fixed maximal distance, the evaluation of formulae also differs by at most this distance, thus providing a quantitative version of the classical result that the modal µ-calculus is invariant under bisimulation. The converse direction does not hold for Qµ on arbitrary systems. However, as in the classical case, on finitely-branching systems the converse can be shown for the modal fragment and thus already quantitative modal logic characterises quantitative bisimulation on finitely-branching systems. Next, we consider the model-checking problem which, given a system and a formula, is to decide whether the system is a model of the formula. In the quantitative world, this translates to computing the numerical value of a formula at a given node of the system. The model-checking problem for the modal µ-calculus can be solved by parity games, a class of infinite zero-sum graph games. We introduce a quantitative extension of these games and show that they are the corresponding model-checking games for our logic. After establishing bisimulation invariance and developing model-checking games, we move to systems that are closer to the scenarios arising in practical applications. First, we consider discounted systems, i.e. systems where additionally the edges are labelled with quantities. It is not straightforward to define a negation operator in this setting that allows for the duality properties needed for a game-based approach to model checking. We show that in this setting there is only one reasonable way to define it. Again, we define an appropriate extension of parity games and show that they correctly describe the evaluation of a discounted quantitative µ-calculus formula. Finally, we provide an algorithm for solving these games, thus also for model checking the quantitative µ-calculus on discounted systems. In the final chapter, we go even further towards practical applications and evaluate the quantitative µ-calculus on a simple class of hybrid systems, namely initialised linear hybrid systems. We show how to approximate the value of a quantitative µ-calculus formula with arbitrary precision on such systems. We define a corresponding version of parity games and use the previously obtained results to prove that they are the correct model-checking games. Then we show how to simplify these games in several steps. We provide a detailed mathematical analysis of these games. In particular we introduce a new class of almost discrete strategies that permit us to simplify the games and to compute their values.

Institutions

• Department of Mathematics [110000]
• Mathematical Fundamentals of Computer Science (Logic and Complexity) Teaching and Research Area [117220]