Results on the Propositional µ-Calculus
Dexter C. Kozen · DAIMI Report Series · 1982
We define a propositional version of the µ-calculus, and give an exponential-time decision procedure, small model property, and complete deductive system. We also show that it is strictly more expressive than PDL. Finally we give an algebraic semantics and prove a representation theorem.