The quantitative µ-calculus

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

Aachen / Publikationsserver der RWTH Aachen University (2013) [Doktorarbeit]

Seite(n): XII, 126 S. : graph. Darst.

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.

Identifikationsnummern

  • URN: urn:nbn:de:hbz:82-opus-46199
  • REPORT NUMBER: RWTH-CONV-144745