Detailansicht
Improved algorithms and conditional lower bounds for problems in formal verification and reactive synthesis
Veronika Loitzenbauer
Art der Arbeit
Dissertation
Universität
Universität Wien
Fakultät
Fakultät für Informatik
Studiumsbezeichnung bzw. Universitätlehrgang (ULG)
Dr.-Studium der technischen Wissenschaften (Dissertationsgebiet: Informatik)
Betreuer*in
Monika Henzinger
DOI
10.25365/thesis.45415
URN
urn:nbn:at:at-ubw:1-25688.63983.143761-9
Link zu u:search
(Print-Exemplar eventuell in Bibliothek verfügbar)
Abstracts
Abstract
(Deutsch)
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.
Abstract
(Englisch)
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
Schlagwörter
(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
Schlagwörter
(Deutsch)
theoretische Informatik effiziente Algorithmen bedingte untere Schranken Graphalgorithmen formale Verifikation reaktive Synthese Spiele auf Graphen Markow-Entscheidungsprozesse omega-reguläre Zielvorgaben Mittelwerts-Zielvorgaben
Autor*innen
Veronika Loitzenbauer
Haupttitel (Englisch)
Improved algorithms and conditional lower bounds for problems in formal verification and reactive synthesis
Paralleltitel (Deutsch)
Verbesserte Algorithmen und Bedingte Untere Schranken für Probleme in Formaler Verifikation und Reaktiver Synthese
Publikationsjahr
2016
Umfangsangabe
xii, 211 Seiten : Diagramme
Sprache
Englisch
Beurteiler*innen
Jean-François Raskin ,
Piotr Sankowski
Klassifikation
54 Informatik > 54.10 Theoretische Informatik
AC Nummer
AC13456184
Utheses ID
40185
Studienkennzahl
UA | 786 | 880 | |