Deciding the First Level of the $\mu$-calculus Alternation Hierarchy
Ralf Kuesters and Thomas Wilke
-------------------------------------------------------------------------------
We show that the following problem is decidable and complete for deterministic exponential time. Given a formula of modal mu-calculus, determine if the formula is equivalent to a formula without greatest fixed point operators. In other words, we show that the first level of the mu-calculus fixed point alternation hierarchy is decidable in deterministic exponential time.