The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics
By: Leonardo Pacheco
Potential Business Impact:
Makes computer logic more powerful and complex.
The modal mu-calculus is obtained by adding least and greatest fixed-point operators to modal logic. Its alternation hierarchy classifies the mu-formulas by their alternation depth: a measure of the codependence of their least and greatest fixed-point operators. The mu-calculus' alternation hierarchy is strict over the class of all Kripke frames: for all n, there is a mu-formula with alternation depth n+1 which is not equivalent to any formula with alternation depth n. This does not always happen if we restrict the semantics. For example, every mu-formula is equivalent to a formula without fixed-point operators over S5 frames. We show that the multimodal mu-calculus' alternation hierarchy is strict over non-trivial fusions of modal logics. We also comment on two examples of multimodal logics where the mu-calculus collapses to modal logic.
Similar Papers
Cut-elimination for the alternation-free modal mu-calculus
Logic in Computer Science
Makes computer logic proofs shorter and faster.
On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
Logic in Computer Science
Makes computer logic proofs simpler and stronger.
Higher-order Kripke models for intuitionistic and non-classical modal logics
Logic in Computer Science
Shows new ways to think about logic.