Optimality and resilience in parity games

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.