In this talk, we will see how the main idea behind Calude et al.'s breakthrough quasipolynomial time algorithm for solving parity games extends to the computation of nested fixpoints of arbitrary set-functions. This result can alternatively be phrased as a fixpoint theorem stating that the iterative computation of nested fixpoints by approximation stabilizes after a quasipolynomial number of iterations. Furthermore we show that the problem of computing nested fixpoints is contained in both NP and Co-NP. Time admitting, we will also see how Zielonka's algorithm for parity games can be used to compute nested fixpoints of arbitrary set-functions.
These results find application in solving generalized parity games as well as model checking and satisfiability checking for extensions of the mu-calculus (e.g. graded, probabilistic or alternating-time), and prospectively in the computation of fair bisimulations and type checking for inductive-coinductive types.
The main message of all this is that many results and algorithms for solving parity games naturally generalize to the computation of nested fixpoints, pointing to a close relation between the two problems. |