Finite satisfiability for guarded fixpoint logic

The finite satisfiability problem for guarded fixpoint logic is decidable and complete for 2ExpTime (resp. ExpTime for formulas of bounded width).

► We prove that the finite satisfiability problem for guarded fixpoint logic is decidable.
► The complexity is shown to be the same as for satisfiability: 2ExpTime-complete.
► We exploit the connection between guarded fixpoint logic and alternating automata.
► We reuse the algorithm for finite emptiness of alternating automata on undirected graphs.
► Correctness is based on a recent development in the finite model theory of guarded logics.