Back and forth between guarded and modal logics

Guarded fixed point logic μGF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal μ-calculus plays within the modal domain. We provide a semantic characterisation of μGF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterisation of the modal μ-calculus, due to D. Janin and I. Walukiewicz (1999), is lifted from the modal to the guarded domain by means of model theoretic translations. At the methodological level, these translations make the intuitive analogy between modal and guarded logics available as a tool in the analysis of the guarded domain