Optimality and Resilience in Parity Games
Alexander Weinert
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.
PhD Thesis.