The complexity of solving parity games is an important open problem in verification, automata theory, and complexity theory. In this paper we develop an abstract setting for studying parity games and related problems, based on function optimization over certain discrete structures. We introduce new classes of completely local-global (CLG) and recursively local-global (RLG) functions, and show that strategy evaluation functions for parity games belong to these classes. We also establish a relation to the previously well-studied completely unimodal (CU) and local-global functions. A number of nice properties of CLG-functions are proved.
In this setting, we survey several randomized optimization algorithms appropriate for CU-, CLG-, and RLG-functions. We show that the subexponential algorithms for linear programming by Kalai and Matousek, Sharir, and Welzl, can be adapted to optimizing the functions we study, with preserved subexponential expected running time. We examine the relations to two other abstract frameworks for subexponential optimization, the LP-type problems of Matousek, Sharir, and Welzl, and the abstract optimization problems of Gärtner. The applicability of our abstract optimization approach to parity games builds upon a discrete strategy evaluation measure.
We also consider local search type algorithms, and settle two nontrivial, but still exponential, upper bounds. As applications we address some complexity-theoretic issues including non-PLS-completeness of the problems studied.
Download BibTeX entry.