Computing Nested Fixpoints in Quasipolynomial Time
share
It is well known that the winning region of a parity game with n nodes and k priorities can be computed as a k-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires n^k/2+1 iterations of the function. The recent parity game solving algorithm by Calude et al. runs in quasipolynomial time and essentially shows how to compute the same fixpoint using only a quasipolynomial number of iterations. We show that their central idea naturally generalizes to the computation of k-nested fixpoints of any set-valued function; hence k-nested fixpoints of set functions that can be computed in quasipolynomial time can be computed in quasipolynomial time as well. While this result is of clear interest in itself, we focus in particular on applications to modal fixpoint logics beyond relational semantics. For instance, the model checking problems for the graded and the (two-valued) probabilistic μ-calculus -- with numbers coded in binary -- can be solved by computing nested fixpoints of functions that differ from the function for parity game solving, but still can be computed in quasipolynomial time; our result hence implies that model checking for these μ-calculi is in QP. A second implication of our result lies in satisfiability checking for generalized μ-calculi, including the graded, probabilistic and alternating-time variants; in a general setting that covers all the mentioned cases, our result immediately improves the upper time bound for satisfiability checking for fixpoint formulas of size n with alternation-depth k from 2^O(n^2k^2 n) to 2^O(nk n).
READ FULL TEXT