Guarded fixed point logics and the monadic theory of countable trees

AbstractDifferent variants of guarded logics (a powerful generalization of modal logics) are surveyed and an elementary proof for the decidability of guarded fixed point logics is presented. In a joint paper with Igor Walukiewicz, we proved that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time (E. Grädel and I. Walukiewicz, Proc. 14th IEEE Symp. on Logic in Computer Science, 1999, pp. 45–54). That proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. The exposition given here emphasizes the tree model property of guarded logics: every satisfiable sentence has a model of bounded tree width. Based on the tree model property, we show that the satisfiability problem for guarded fixed point formulae can be reduced to the monadic theory of countable trees (SωS), or to the μ-calculus with backwards modalities