An automata theoretic decision procedure for the propositional mu- calculus (Q1119630)

A decision procedure of elementary complexity is presented for the propositional mu-calculus. This calculus was introduced by D. Kozen as a powerful generalization of propositional dynamic logic, in which, in particular, Streett's infinite repeating construction \(\Delta\) \(a\) can be expressed. The proof is based on using tree automata and strengthens a result by D. Kozen and R. Parikh on (non-elementary) decidability of the mu-calculus obtained by reduction to the monadic second order theory of many successors.