D. Janin and I. Walukiewicz, “Automata for the mu-calculus and Related Results”, BRICS, vol. 2, no. 27, Jan. 1995.