Erschienen: 08.03.2017 Abbildung von Dittmann | Parity games, separations, and the modal µ-calculus | 1. Auflage | 2017 | beck-shop.de

Dittmann

Parity games, separations, and the modal µ-calculus

lieferbar, ca. 10 Tage

Buch. Softcover

2017

In englischer Sprache

Universitätsverlag TU Ber. ISBN 978-3-7983-2887-7

Format (B x L): 14.9 x 21 cm

Gewicht: 547 g

Das Werk ist Teil der Reihe: Foundations of Computing

Produktbeschreibung

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.

Top-Produkte dieser Kategorie

Autoren

  • Rezensionen

    Dieses Set enthält folgende Produkte:
      Auch in folgendem Set erhältlich:
      • nach oben

        Ihre Daten werden geladen ...