Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-5700
Main Title: Parity games, separations, and the modal μ-calculus
Translated Title: Paritätsspiele, Separationen und der modale μ-Kalkül
Author(s): Dittmann, Christoph
Referee(s): Kreutzer, Stephan
Grädel, Erich
Nestmann, Uwe
Granting Institution: Technische Universität Berlin
Type: Doctoral Thesis
Language Code: en
Abstract: The topics of this thesis are the modal μ-calculus and parity games. The modal μ-calculus is a common logic for model-checking in computer science. The model-checking problem of the modal μ-calculus is polynomial time equivalent to solving parity games, a 2-player game on labeled directed graphs. We present the first FPT algorithms (fixed-parameter tractable) for the model-checking problem of the modal μ-calculus on restricted classes of graphs, specifically on classes of bounded Kelly-width or bounded DAG-width. In this process we also prove a general decomposition theorem for the modal μ-calculus and define a useful notion of type for this logic. Then, assuming a class of parity games has a polynomial time algorithm solving it, we consider the problem of extending this algorithm to larger classes of parity games. In particular, we show that joining games, pasting games, or adding single vertices preserves polynomial-time solvability. It follows that parity games can be solved in polynomial time if their underlying undirected graph is a tournament, a complete bipartite graph, or a block graph. In the last chapter we present the first non-trivial formal proof about parity games. We explain a formal proof of positional determinacy of parity games in the proof assistant Isabelle/HOL.
Die Themen dieser Dissertation sind der modale μ-Kalkül und Paritätsspiele. Der modale μ-Kalkül ist eine häufig eingesetzte Logik im Bereich des Model-Checkings in der Informatik. Das Model-Checking-Problem des modalen μ-Kalküls ist polynomialzeitäquivalent zum Lösen von Paritätsspielen, einem 2-Spielerspiel auf beschrifteten, gerichteten Graphen. Wir präsentieren die ersten FPT-Algorithmen (fixed-parameter tractable) für das Model-Checking-Problem des modalen μ-Kalküls auf Klassen von Graphen mit beschränkter Kelly-Weite oder beschränkter DAG-Weite. Für diesen Zweck beweisen wir einen allgemeineren Zerlegungssatz für den modalen μ-Kalkül und stellen eine nützliche Definition von Typen für diese Logik vor. Angenommen, eine Klasse von Paritätsspielen hat einen Polynomialzeit-Lösungs-Algorithmus, betrachten wir danach das Problem, diese Klassen zu erweitern auf eine Weise, sodass Polynomialzeit-Lösbarkeit erhalten bleibt. Wir zeigen, dass dies beim Join von Paritätsspielen, beim Pasting und beim Hinzufügen einzelner Knoten der Fall ist. Wir folgern daraus, dass das Lösen von Paritätsspielen in Polynomialzeit möglich ist, falls der unterliegende ungerichtete Graph ein Tournament, ein vollständiger bipartiter Graph oder ein Blockgraph ist. Im letzten Kapitel präsentieren wir den ersten nicht-trivialen formalen Beweis über Paritätsspiele. Wir stellen einen formalen Beweis für die positionale Determiniertheit von Paritätsspielen im Beweis-Assistenten Isabelle/HOL vor.
URI: http://depositonce.tu-berlin.de/handle/11303/6135
http://dx.doi.org/10.14279/depositonce-5700
Exam Date: 20-Jan-2017
Issue Date: 2017
Date Available: 27-Feb-2017
DDC Class: DDC::000 Informatik, Informationswissenschaft, allgemeine Werke::000 Informatik, Wissen, Systeme::000 Informatik, Informationswissenschaft, allgemeine Werke
Subject(s): modal logic
graph theory
decompositions
parity games
formal proofs
Modallogik
Graphentheorie
Zerlegungen
Paritätsspiele
formale Beweise
Creative Commons License: https://creativecommons.org/licenses/by/4.0/
Series: Foundations of computing
Series Number: 9
EISSN: 2199-5257
ISBN: 978-3-7983-2888-4
Notes: Published in print by Universitätsverlag der TU Berlin, ISBN 978-3-7983-2887-7 (ISSN 2199-5249)
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Publications

Files in This Item:
File Description SizeFormat 
dittmann_christoph.pdf1.81 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.