Abstract
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.

This publication has 0 references indexed in Scilit: