Automata for Guarded Fixed Point Logics

Abstract

The guarded fixed point logics μGF and μCGF introduced in the previous chapter extend the guarded fragments of first-order logic GF and CGF on the one hand and the modal μ-calculus on the other hand. Thereby, the expressive power of the underlying formalisms is increased considerably. On transition systems, for instance, μGF already subsumes the μ-calculus with backwards modalities. Hence, the question arises, whether these logics are still manageable algorithmically. In this chapter we will study the complexity of their satisfiability problems.