The quantitative µ-calculus

Fischer, Diana; Grädel, Erich

doi:4619

The quantitative µ-calculus = Der Quantitative µ-Kalkül

Fischer, Diana (Author)

2013

Verantwortlichkeitsangabevorgelegt von Diana Fischer

ImpressumAachen : Publikationsserver der RWTH Aachen University 2013

UmfangXII, 126 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2013

Zsfassung in dt. und engl. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2013-04-23

Online
URN: urn:nbn:de:hbz:82-opus-46199
URL: https://publications.rwth-aachen.de/record/229869/files/4619.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Mathematische Logik (Genormte SW) ; Spieltheorie (Genormte SW) ; Model Checking (Genormte SW) ; Modallogik (Genormte SW) ; Informatik (frei) ; Quantitative Logik (frei) ; µ-Kalkül (frei) ; Bisimulation (frei) ; µ-calculus (frei) ; mathematical logics (frei) ; quantitative logics (frei) ; games (frei) ; game theory (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.4.1

Kurzfassung
Diese Dissertation behandelt eine Verallgemeinerung des modalen µ-Kalküls, einer wichtigen Spezifikationssprache in der formalen Verifikation. Die quantitative Erweiterung ist dergestalt, dass Formeln nicht länger nur zu wahr oder falsch ausgewertet werden können, sondern zu beliebigen reellen Zahlen. Wir werten diese Logik zunächst auf einer quantitativen Erweiterung von Transitionssystemen aus, in der jedem Knoten durch quantitative Prädikate reelle Werte zugewiesen werden. Anschließend untersuchen wir, welche klassischen Resultate für den µ-Kalkül sich sinnvoll in diesen quantitativen Rahmen übertragen lassen. Eines dieser Resultate ist die enge Verbindung zwischen dem µ-Kalkül und der Bisimulation, einer Art von Verhaltensäquivalenz für Transitionssysteme. Wir führen quantitative Bisimulation als einen Abstand zwischen Transitionssystemen ein und zeigen, dass für Systeme, die einen festen Abstand haben, auch der Unterschied in der Auswertung von Formeln durch diesen Abstand begrenzt wird. Dies ist eine quantitative Version des klassischen Resultats, dass der modale µ-Kalkül invariant unter Bisimulation ist. Die Rückrichtung dieses Satzes gilt nicht für beliebige Systeme, aber wie im klassischen Fall zeigen wir, dass für endlich verzweigte Systeme diese Richtung bereits für die quantitative Modallogik gilt. Somit charakterisiert quantitative Modallogik quantitative Bisimulation für endlich verzweigte Systeme. Weiterhin betrachten wir das Model-Checking-Problem, d.h. die Frage ob für ein gegebenes System und eine Formel gilt, dass das System Modell der Formel ist. Für den quantitativen Fall lässt sich dies übersetzen in die Berechnung der Auswertungsfunktion einer Formel für ein gegebenes System. Im klassischen Fall kann dies durch die Übersetzung in Paritätsspiele gelöst werden, einer Klasse von unendlichen Graphspielen. In dieser Arbeit führen wir eine quantitative Erweiterung dieser Spiele ein und zeigen, dass diese die geeigneten Model-Checking-Spiele für den quantitativen µ-Kalkül sind. Schließlich beschäftigen wir uns mit Anwendungsszenarien für den quantitativen µ-Kalkül, wobei wir zuerst eine entsprechend erweiterte Logik auf discounted systems betrachten. Dies sind quantitative Systeme in denen auch die Kanten mit reellen Werten beschriftet sind. Die Definition eines geeigneten Negationsoperators - welcher entscheidend für den spielbasierten Zugang zum Model-Checking-Problem ist - ist in diesem Fall nicht offensichtlich. Wir zeigen, dass es nur eine sinnvolle Art gibt diesen zu definieren. Wie bereits zuvor führen wir eine passende Erweiterung von Paritätsspielen ein und zeigen, dass sie die geeigneten Model-Checking-Spiele für diesen Fall sind. Anschließend zeigen wir, wie sich diese Spiele algorithmisch lösen lassen. Im letzten Kapitel werten wir den quantitativen µ-Kalkül auf einer einfachen Klasse von hybriden Systemen aus. Wir zeigen, dass der Wert einer quantitativen µ-Kalkül-Formel mit beliebiger Präzision auf diesen Systemen berechnet werden kann. Dazu nutzen wir wieder die Beschreibung durch entsprechende Paritätsspiele aus, sowie die Resultate aus den vorherigen Kapiteln. Die Berechnung läuft in mehreren Reduktionsschritten ab. Wir führen eine detaillierte mathematische Analyse dieser Spiele durch. Insbesondere definieren wir eine neue Klasse von Strategien, die uns erlaubt, die Spiele zu vereinfachen und ihre Werte zu berechnen.

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.

Fulltext:
PDF