Alternation hierarchies and fragments of modal $mu$-calculus (Proof theory and proving)

Modal $mu$-calculus, the logic obtained by adding (non-first-order) least and greatest fixpoint operators to the modal logic, has attracted great interests from computer science and mathematical logic. It is natural to classify the formulas of modal $mu$-calculus by the number of alternating blocks of fixpoint operators, which is called the alternation hierarchy. A fundamental issue is the strictness of such alternation hierarchies. We review the historical and latest studies on the (semantical) strictness of alternation hierarchy with respect to various transition systems. We also introduce the variable hierarchy and observe that, the simple alternation hierarchy of the one-variable fragment of modal $mu$-calculus is strict over finitely branching transition systems