Quantification over Noetherian Subsets and the Alternation-Free μ-Calculus
Yde Venema

The modal μ-calculus is the extension of basic modal logic with explicit least and greatest fixpoint operators. As an extension of van Benthem's bisimulation invariance result on modal and first-order logic, Janin and Walukiewicz proved that the modal mu-calculus has the same expressive power as monadic second-order logic, when it comes to bisimulation-invariant properties. In this talk we look at some variations of the latter result. As our most pertinent result we show that the alternation-free fragment of the modal mu-calculus corresponds to the bisimulation-invariant fragment of the version of second-order logic where the second- order quantifiers range over so-called noetherian subsets of the Kripke model. Here we call a subset noetherian if it is the union of a bundle of finite paths, all starting from the same root.