Please use this identifier to cite or link to this item: doi:10.22028/D291-27756
Title: Optimality and resilience in parity games
Authors: Weinert, Alexander Dominik
Language: English
Issue Date: 2018
DDC groups: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: Modeling reactive systems as infinite games has yielded a multitude of results in the fields of program verification and program synthesis. The canonical parity condition, however, neither suffices to express non-functional requirements on the modeled system, nor to capture malfunctions of the deployed system. We address these issues by investigating quantitative games in which the above characteristics can be expressed. Parity games with costs are a variant of parity games in which traversing an edge incurs some nonnegative cost. The cost of a play is the limit superior of the cost incurred between answering odd colors by larger even ones. We extend that model by using integer costs, obtaining parity games with weights, and show that the problem of solving such games is in the intersection of NP and coNP and that it is PTIME-equivalent to the problem of solving energy parity games. We moreover show that Player 0 requires exponential memory to implement a winning strategy in parity games with weights. Further, we show that the problem of determining whether Player 0 can keep the cost of a play below a given bound is EXPTIME-complete for parity games with weights and PSPACE-complete for the special cases of parity games with costs and finitary parity games, i.e., it is harder than solving the game. Thus, optimality comes at a price even in finitary parity games. We further determine the complexity of computing strategies in parity games that are resilient against malfunctions. We show that such strategies can be effectively computed and that this is as hard as solving the game without disturbances. Finally, we combine all these aspects and show that Player 0 can trade memory, cost, and resilience for one another. Furthermore, we show how to compute the possible tradeoffs for a given game.
Die Modellierung von reaktiven Systemen durch unendliche Spiele ermöglichte zahlreiche Fortschritte in der Programmverifikation und der Programmsynthese. Die häufig genutzte Paritätsbedingung kann jedoch weder nichtfunktionale Anforderungen ausdrücken, noch Fehlfunktionen des Systems modellieren. Wir betrachten quantitative Spiele in denen diese Merkmale ausgedrückt werden können. Paritätsspiele mit Kosten (PSK) sind eine Variante der Paritätsspiele in denen die Benutzung einer Kante nichtnegative Kosten verursacht. Die Kosten einer Partie sind der Limes Superior der Kosten zwischen ungeraden und den jeweils nächsten größeren geraden Farben. Wir erweitern dieses Modell durch ganzzahlige Kosten zu Paritätsspielen mit Gewichten (PSG). Wir zeigen, dass das Lösen dieser Spiele im Schnitt von NP und coNP liegt, dass es PTIME-äquivalent dazu ist, Energieparitätsspiele zu lösen und dass Spieler 0 exponentiellen Speicher benötigt, um zu gewinnen. Ferner zeigen wir, dass das Problem, zu entscheiden, ob Spieler 0 die Kosten eines Spiels unter einer gegebenen Schranke halten kann, EXPTIME-vollständig für PSG ist, sowie dass es PSPACE-vollständig für die Spezialfälle PSK und finitäre Paritätsspiele (FPS) ist. Optimalität ist also selbst in FPS nicht kostenlos. Außerdem bestimmen wir die Komplexität davon, Strategien in Paritätsspielen zu berechnen, die robust gegenüber Fehlfunktionen sind, zeigen, dass solche Strategien effektiv berechnet werden können und beweisen, dass dies nur linearen Mehraufwand bedeutet. Darüberhinaus kombinieren wir die oben genannten Aspekte, zeigen, dass Spieler 0 Speicher, Kosten und Robustheit gegeneinander eintauschen kann und berechnen die möglichen Kompromisse.
URI: urn:nbn:de:bsz:291--ds-277563
hdl:20.500.11880/27380
http://dx.doi.org/10.22028/D291-27756
Advisor: Zimmermann, Martin
Date of oral examination: 14-Dec-2018
Date issued: 9-Apr-2019
Faculty: MI - Fakultät für Mathematik und Informatik
Institute: MI - Informatik
Appears in Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files in This Item:
File Description SizeFormat 
main.pdfDissertation1,01 MBAdobe PDFView/Open


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