A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation

We consider nested fixed-point expressions like µz.νy.µx.f(x,y,z) evaluated over a finite lattice, and ask how many queries to a function f are needed to find the value. Following a recent development for parity games, we show that a quasi-polynomial number of queries is sufficient, namely n^{lg(d/lg n)+O(1)} for a monotone function f of arity d over the lattice {0,1}^n. The algorithm is an abstract version of several algorithms proposed recently by a number of authors, which involve (implicitly or explicitly) the structure of a universal tree. We also show a quasi-polynomial lower bound for the number of queries used by the algorithms in consideration. This is joint work with André Arnold and Damian Niwiński. Link to the paper: https://www.mimuw.edu.pl/~parys/publications/2020-mu-calculus-quasipolynomial.pdf