Detailansicht
Leveraging the power of graph algorithms
efficient algorithms for computer-aided verification
Alexander Svozil
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 (DissG: Informatik)
Betreuer*in
Monika Henzinger
DOI
10.25365/thesis.69895
URN
urn:nbn:at:at-ubw:1-11136.21566.930899-5
Link zu u:search
(Print-Exemplar eventuell in Bibliothek verfügbar)
Abstracts
Abstract
(Deutsch)
Ein Modellprüfer kontrolliert ob ein gegebenes Modell eines Systems
eine Anforderung erfüllt. In der reaktiven Synthese ist die Eingabe eine Anforderung und
das Ziel ist ein korrektes reaktives System zu erzeugen.
Wir betrachten folgende Modelle: (Zustand-Transition) Graphen wo Knoten die Zustände des Systems darstellen und Kanten die Transitionen von einem Zustand zum Nächsten sind.
Markow-Entscheidungsprozesse (MEPs) erweitern Graphen
um probabilistische Systeme modellieren zu können, z.B. randomisierte Protokolle.
Spielgraphen erweitern Graphen um Interaktionen mit der Umwelt zu
modellieren und sind ein zentrales Werkzeug für die reaktive Synthese.
Zielvorgaben sind Mengen von Abläufen in einem Modell und
repräsentieren die Anforderungen. Die Klasse der omega-regulären
Zielvorgaben drückt alle üblichen funktionalen
Anforderungen für reaktive Systeme in der Modellprüfung
und in der Synthese aus. Beispiele für mega-reguläre Zielvorgaben die wir betrachten sind Erreichbarkeits-, Büchi-, eingeschränkte Büchi-,
Streett- und Paritäts-Zielvorgaben.
Um funktionale und effiziente reaktive Systeme zu modellieren benutzen wir die
Kombination von quantitativen (Mittelwert-) Zielvorgaben und omega-regulären Zielvorgaben.
Für die Prüfung von MEPs mit omega-regulären Zielvorgaben betrachten wir die Berechnung von der maximalen Schluss-Komponenten (MSK) Dekomposition eines MEPs.
Das Ziel der Arbeit ist es schnelle
Graphalgorithmen und moderne algorithmische Techniken für
Probleme in der Modellprüfung und Synthese in Graphen, MEPs und
Spielgraphen wirksam einzusetzen.
Unter den Resultate sind auch symbolische Algorithmen,
eine bekannte Klasse von Algorithmen in der Modellprüfung die einen
begrenzten Zugang zum Eingabemodell für eine effiziente
Repräsentation eintauschen. Wir stellen folgende Ergebnisse vor:
Algorithmen für Spielgraphen mit Mittelwert-Büchi-Zielvorgaben und Mittelwert-coBüchi-Zielvorgaben
die einem der schnellsten Algorithmen für Mittelwert-Zielvorgaben in der Laufzeit gleichziehen.
Ein randomisierter Algorithmus für Streett-Zielvorgaben in Graphen und MEPs in fast linearer Laufzeit.
Ein Algorithmus für eingeschränkte Büchi Zielvorgaben in sub-kubischer Laufzeit für Graphen und kubischer Laufzeit in Spielgraphen.
Konditionale untere Schranken für Anfragen von
Erreichbarkeits-Zielvorgaben in Spielgraphen und MEPs.
Algorithmen für sequenzielle Erreichbarkeits-Zielvorgaben in
Graphen und MEPs in jeweils linearer Zeit und fast linearer Zeit.
Der erste symbolische Algorithmus für
Paritäts-Zielvorgaben in quasi-polynomieller Zeit.
Wir durchbrechen eine langstehende Laufzeitschranke für die MSK Dekomposition
von den 90er-Jahren indem wir einen symbolischen Algorithmus in sub-quadratischer Laufzeit präsentieren.
Abstract
(Englisch)
Model checking verifies whether a given model of a system ensures a specification.
In reactive synthesis the input is a specification and the goal is to construct a
correct reactive system.
We consider a variety of models:
(state-transition) graphs where vertices represent the
states of a system and edges are the transitions from one state to the next.
Markov Decision Processes (MDPs) extend graphs to model probabilistic systems, e.g., randomized
protocols.
Game graphs extend graphs to model interactions with the environment and are a central tool
for reactive synthesis.
Objectives are sets of traces in the model and represent the specification.
The class of omega-regular objectives} expresses all commonly used functional specifications for reactive systems in model checking and
synthesis. Examples for omega-regular objectives we consider are reachability objectives,
Büchi objectives, bounded Büchi objectives, Streett objectives, and
parity objectives. To model functional and efficient reactive systems we use the combination of quantitative (mean-payoff) objectives and omega-regular objectives.
For the verification of MDPs with omega-regular objectives, we consider computing the
maximal end-component (MEC) decomposition of MDPs.
The goal of the thesis is to leverage fast graph algorithms
and modern algorithmic techniques for problems in model checking and synthesis on graphs, MDPs, and game graphs.
The results include symbolic algorithms, a well-known class of algorithms in model checking
that trades limited access to the input model for an efficient representation.
In particular, we present the following results:
Algorithms for game graphs with
mean-payoff Büchi objectives and mean-payoff coBüchi objectives
which match one of the best
running time bounds for mean-payoff objectives.
A near-linear time randomized algorithm for Streett objectives in graphs and MDPs.
A sub-cubic time algorithm for bounded Büchi objectives in graphs and a cubic time algorithm for game graphs.
Conditional lower bounds for queries of reachability objectives in game graphs and MDPs. Linear and near-linear time algorithms for sequential reachability objectives in graphs and MDPs respectively.
The first quasi-polynomial time symbolic algorithm for parity objectives in game graphs.
We break a long-standing running time bound for MEC decomposition from the '90s
by providing a sub-quadratic time symbolic algorithm.
Schlagwörter
Schlagwörter
(Englisch)
omega-regular objectives formal verification reactive synthesis games on graphs MDPs efficient algorithms
Schlagwörter
(Deutsch)
omega-reguläre Zielvorgaben formale Verifikation reaktive Synthese Spiele auf Graphen Markow-Entscheidungsprozesse effiziente Algorithmen
Autor*innen
Alexander Svozil
Haupttitel (Englisch)
Leveraging the power of graph algorithms
Hauptuntertitel (Englisch)
efficient algorithms for computer-aided verification
Paralleltitel (Deutsch)
Wirksame Nutzung der Leistungsfähigkeit von Graph-Algorithmen
Paralleluntertitel (Deutsch)
effiziente Algorithmen für die Computergestützte Verifizierung
Publikationsjahr
2021
Umfangsangabe
xiii, 175 Seiten : Diagramme
Sprache
Englisch
Beurteiler*innen
Christel Baier ,
Véronique Bruyère
Klassifikation
54 Informatik > 54.10 Theoretische Informatik
AC Nummer
AC16449375
Utheses ID
59563
Studienkennzahl
UA | 786 | 880 | |