The μ-calculus alternation hierarchy collapses over structures with restricted connectivity

Julian Gutierrez, Felix Klaedtke, Martin Lange

Research output: Contribution to journalArticleOtherpeer-review

3 Citations (Scopus)

Abstract

The alternation hierarchy of least and greatest fixpoint operators in the μ-calculus is strict. However, the strictness of the hierarchy does not necessarily carry over when considering restricted classes of structures. For instance, over the class of infinite words the alternation-free fragment of the μ-calculus is already as expressive as the full logic. Our current understanding of when and why the μ-calculus alternation hierarchy is (and is not) strict is limited. This article makes progress in answering these questions by showing that the alternation hierarchy of the μ-calculus collapses to the alternation-free fragment over some classes of structures, including infinite nested words and finite graphs with feedback vertex sets of a bounded size. Common to these classes is that the connectivity between the components in a structure from such a class is restricted in the sense that the removal of certain vertices from the structure's graph decomposes it into graphs in which all paths are of finite length. The collapse results herein are obtained in an automata-theoretic setting. They subsume, generalize, and strengthen several prior results on the expressivity of the μ-calculus over restricted classes of structures.

Original languageEnglish
Pages (from-to)292-306
Number of pages15
JournalTheoretical Computer Science
Volume560
Issue numberP3
DOIs
Publication statusPublished - 4 Dec 2014
Externally publishedYes

Keywords

  • Alternation hierarchy
  • Fixpoints
  • Modal μ-calculus
  • Parity automata

Cite this