Universitätsbibliothek Wien

Improved algorithms and conditional lower bounds for problems in formal verification and reactive synthesis

Loitzenbauer, Veronika (2016) Improved algorithms and conditional lower bounds for problems in formal verification and reactive synthesis.
Dissertation, University of Vienna. Fakultät für Informatik
BetreuerIn: Henzinger, Monika

[img] PDF-File
Alle Rechte vorbehalten / All rights reserved

Download (1052Kb)
DOI: 10.25365/thesis.45415
URN: urn:nbn:at:at-ubw:1-25688.63983.143761-9

Link zu u:search

Abstract in English

Model checking is a fully automated approach in formal verification to either prove a system's correctness or find an error. It is an essential and widely-used component in the iterative design of systems such as microprocessors. In contrast to iterative design, Church's synthesis problem asks to automatically generate a correct system from its specification. Reactive synthesis is the synthesis of reactive systems that are systems that repeatedly interact with their environment. For formal verification and synthesis mathematical models of systems and their behaviors are needed. Directed graphs are a fundamental model of systems. Markov decision processes (MDPs) additionally incorporate probabilistic behavior of, for example, randomized concurrent systems or communication protocols. A model for reactive systems are game graphs, where the vertices of the graph are partitioned between two players and one player represents controllable inputs and the other uncontrollable inputs. The automata-theoretic approach to model-checking and synthesis is a canonical way to formally specify the desired behaviors of a system using omega-regular objectives such as Büchi, parity, and Streett objectives. Additionally, mean-payoff objectives allow for expressing quantitative properties of systems such as resource consumption. In this thesis we develop algorithms with improved worst-case running times for several problems on graphs, MDPs, and game graphs with omega-regular and mean-payoff objectives. Additionally, we show the first super-linear conditional lower bounds for polynomial-time problems in this area. In particular we present the following results: * For mean-payoff objectives on graphs the first approximation algorithm that improves for dense graphs upon the long-standing running time bounds for exact algorithms. * For Streett objectives the first sub-quadratic time algorithm for MDPs and a faster algorithm for dense MDPs and graphs. * For parity games the first sub-cubic time algorithm for three priorities and improved symbolic algorithms for the general case. * New algorithms and super-linear conditional lower bounds for conjunctions and disjunctions of basic omega-regular objectives. These results show for the first time that, under popular assumptions, there exist problems with strictly higher running times on MDPs than on graphs (``model separation'') and that for each graph and MDPs there exist objectives with strictly higher running times compared to closely related objectives (``objective separation''). * For generalized Büchi games a new upper and tight conditional lower bounds that imply a model separation between MDPs and game graphs, and a faster algorithm for dense GR(1) games.

Schlagwörter in Englisch

theoretical computer science / efficient algorithms / conditional lower bounds / fine-grained complexity / graph algorithms / formal verification / reactive synthesis / graph games / Markov Decision Processes / omega-regular objectives / mean-payoff objectives

Abstract in German

Die Modellprüfung ist ein vollautomatisches Verfahren zur formalen Verifikation, die entweder die Korrektheit eines Systems zeigt oder einen Fehler findet. Sie ist ein essentieller und oft verwendeter Bestandteil im schrittweisen Design von Systemen, wie zum Beispiel von Mikroprozessoren. Im Gegensatz zu schrittweisem Design verlangt das Syntheseproblem von Church die automatische Generierung eines korrekten Systems aus einer vorgegebenen Spezifikation. Reaktive Sythese ist die Synthese von reaktiven Systemen, welche laufend mit ihrer Umgebung interagieren. Für die formale Verifikation und Synthese werden mathematische Modelle von Systemen und ihrem Verhalten benötigt. Gerichtete Graphen sind ein grundlegendes Modell von Systemen. Markow-Entscheidungsprozesse (MEPs) können zusätzlich zufallsgesteuertes Verhalten abbilden, zum Beispiel von randomisierten parallelen Systemen und von Kommunikationsprotokollen. Ein Modell für reaktive Systeme sind Spielgraphen, bei denen die Knoten des Graphens zwischen einer Spielerin, die die kontrollierbaren Eingaben repräsentiert, und ihrem Gegenspieler, der die unkontrollierbaren Eingaben repräsentiert, aufgeteilt sind. Der Automaten-basierte Ansatz zur Modellprüfung und Synthese ist eine anerkannte Methode um das erwünschte Verhalten von Systemen mit Hilfe von omega-regulären Zielvorgaben wie Büchi-, Paritäts- oder Streett-Zielvorgaben formal zu beschreiben. Zusätzlich können quantitative Eigenschaften wie Ressourcenverbrauch durch Mittelwerts-Zielvorgaben ausgedrückt werden. In dieser Arbeit entwickeln wir Algorithmen mit verbesserter Laufzeit für mehrere Probleme auf Graphen, MEPs, und Spielgraphen mit omega-regulären Zielvorgaben und Mittelwerts-Zielvorgaben. Zusätzlich zeigen wir die ersten super-linearen bedingten unteren Schranken für Polynomialzeitprobleme in diesem Gebiet. Konkret präsentieren wir die folgenden Ergebnisse: * Für Mittelwerts-Zielvorgaben auf Graphen den ersten Approximationsalgorithmus, der für dichte Graphen die lange bekannten Laufzeitschranken für exakte Algorithmen durchbricht. * Für Streett-Zielvorgaben den ersten Algorithmus mit weniger als quadratischer Laufzeit sowie verbesserte Algorithmen für dichte MEPs und Graphen. * Für Paritätsspiele den ersten sub-kubischen Algorithmus für drei Prioritäten sowie verbesserte symbolische Algorithmen für den allgemeinen Fall. * Neue Algorithmen und super-lineare bedingte untere Schranken für Konjunktionen und Disjunktionen von einfachen omega-regulären Zielvorgaben. Diese Ergebnisse zeigen zum ersten Mal, dass es unter weitverbreiteten Annahmen für MEPs strikt höhere Laufzeitschranken als für Graphen (``Modell-Separierung'') und für manche Zielvorgaben strikt höhere Laufzeitschranken als für nah verwandte Zielvorgaben (``Zielvorgaben-Separierung'') gibt. * Für verallgemeinerte Büchi Spiele einen neuen Algorithmus und passende bedingte untere Schranken, die eine Modellseparierung zwischen MEPs und Spielgraphen implizieren, sowie für GR(1) Spiele einen schnelleren Algorithmus auf dichten Graphen.

Schlagwörter in Deutsch

theoretische Informatik / effiziente Algorithmen / bedingte untere Schranken / Graphalgorithmen / formale Verifikation / reaktive Synthese / Spiele auf Graphen / Markow-Entscheidungsprozesse / omega-reguläre Zielvorgaben / Mittelwerts-Zielvorgaben

Item Type: Hochschulschrift (Dissertation)
Author: Loitzenbauer, Veronika
Title: Improved algorithms and conditional lower bounds for problems in formal verification and reactive synthesis
Umfangsangabe: xii, 211 Seiten : Diagramme
Institution: University of Vienna
Faculty: Fakultät für Informatik
Studiumsbezeichnung bzw.
Universitätslehrgang (ULG):
Dr.-Studium der technischen Wissenschaften (Dissertationsgebiet: Informatik)
Publication year: 2016
Language: eng ... Englisch
Supervisor: Henzinger, Monika
Assessor: Raskin, Jean-François
2. Assessor: Sankowski, Piotr
Classification: 54 Informatik > 54.10 Theoretische Informatik
AC Number: AC13456184
Item ID: 45415
(Das PDF-Layout ist ident mit der Druckausgabe der Hochschulschrift.)

Urheberrechtshinweis: Für Dokumente, die in elektronischer Form über Datennetze angeboten werden, gilt uneingeschränkt das österreichische Urheberrechtsgesetz; insbesondere sind gemäß § 42 UrhG Kopien und Vervielfältigungen nur zum eigenen und privaten Gebrauch gestattet. Details siehe Gesetzestext.

Edit item (Administrators only) Edit item (Administrators only)