The \(\mu\)-calculus alternation hierarchy collapses over structures with restricted connectivity (Q477204)

The paper considers modal \(\mu\)-calculus, an extension of modal logic with least and greatest fixpoints of monotone operators. As shown by \textit{J. C. Bradfield} [ibid. 195, No. 2, 133--153 (1998; Zbl 0915.03017)], the hierarchy of formulas given by the number of alternations between least and greatest fixpoints is infinite in arbitrary graphs. This leaves open the question of the infinity of the hierarchy over restricted classes of graphs. The paper focuses on the classes \(\mathrm{BDAG}_{\leq w}\) of bottleneck directed acyclic graphs of width at most \(w\), which are directed acyclic graphs subdivided into layers, where every infinite path must meet infinitely often some layers (bottlenecks) of size at most \(w\). As a main result, the authors show that the alternation hierarchy of the \(\mu\)-calculus over \(\mathrm{BDAG}_{\leq w}\) is finite: actually alternation free formulas suffice, that is, formulas obtained by composing subformulas with only least or only greatest fixpoints.