Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics

Leonardo Pacheco

TL;DR

This work analyzes the mu-calculus' alternation hierarchy in multimodal settings, proving that the hierarchy remains strict over non-trivial fusions of modal logics. central to the argument is a reduction of mu-calculus evaluation to parity games, plus the construction of winning-region formulas W_n that witness the separations between alternation depths. The authors adapt parity-to-Kripke encodings and define refined modalities to handle fused frame classes, extending Bradfield’s and Alberucci–Facchini’s earlier results to multimodal logics. They also discuss cases where the mu-calculus collapses to modal logic (e.g., GLP and IS5 under certain restrictions), illustrating that fixed-point expressivity can vanish with strong inter-modal constraints. Overall, the paper advances understanding of when fixed-point alternation yields genuine expressive gain in fusion logics and lays groundwork for further study of collapse phenomena in multimodal frameworks.

Abstract

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.

The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics

TL;DR

This work analyzes the mu-calculus' alternation hierarchy in multimodal settings, proving that the hierarchy remains strict over non-trivial fusions of modal logics. central to the argument is a reduction of mu-calculus evaluation to parity games, plus the construction of winning-region formulas W_n that witness the separations between alternation depths. The authors adapt parity-to-Kripke encodings and define refined modalities to handle fused frame classes, extending Bradfield’s and Alberucci–Facchini’s earlier results to multimodal logics. They also discuss cases where the mu-calculus collapses to modal logic (e.g., GLP and IS5 under certain restrictions), illustrating that fixed-point expressivity can vanish with strong inter-modal constraints. Overall, the paper advances understanding of when fixed-point alternation yields genuine expressive gain in fusion logics and lays groundwork for further study of collapse phenomena in multimodal frameworks.

Abstract

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.

Paper Structure

This paper contains 15 sections, 7 theorems, 12 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Outline
  3. Preliminaries
  4. The $\mu$-calculus
  5. Fusions
  6. Alternation Hierarchy
  7. Game Semantics
  8. Parity games
  9. Evaluation games as parity games
  10. Winning region formulas
  11. Strictness
  12. Finishing the proof of the Main Theorem
  13. Case studies on the collapse over multimodal logics
  14. Provability Logic
  15. Intuitionistic Modal Logic

Key Result

Corollary 1

Let $\{\mathsf{L}_0,\mathsf{L}_1\} \subseteq \{\mathsf{K}, \mathsf{K4}, \mathsf{S4}, \mathsf{KD45}, \mathsf{S5}, \mathsf{GL}\}$, then the $\mu$-calculus' alternation hierarchy is strict over $\mathsf{L}_0\otimes\mathsf{L}_1$.

Figures (1)

  • Figure 1: Example of a parity game $\mathcal{P}$ and the corresponding bimodal model $\mathcal{P}^K$. The model $\mathcal{P}^K$ is built using copies of $\mathsf{S5}$ models.

Theorems & Definitions (15)

  • Corollary
  • Conjecture
  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • Proposition 3
  • proof
  • Proposition 4
  • proof
  • ...and 5 more