Modal correspondence and fixpoints

Modal correspondence theory is the comparative study of expressiveness of modal languages and classical languages, like first order logic (FO) and monadic second order logic (MSO).
The two main results in this context are van Benthem and Janin-Walukiewicz characterization theorems.
The former states that modal logic is the bisimulation invariant fragment of FO, while the latter states that the modal mu-calculus is the bisimulation invariant fragment of MSO. Such characterization theorems can thence be seen as solutions for the equation:

x / bis = y (over M)

where x ranges over FO, MSO, WMSO etc, y ranges over fragments of the modal mu-calculus, and M ranges over subclasses of Kripke models. Thus for instance van Benthem's theorem says that the equation holds when x=FO, y=modal logic and M=the class of all Kripke models.
In this talk I will discuss the case when x is WMSO (weak monadic second order logic) and y is the alternation free fragment of the modal mu-calculus.
This is an ongoing joint research with Yde Venema (ILLC) and Fabio Zanasi (ENS Lyon).