Decision procedures for guarded logics

Abstract

Different variants of guarded logics (a powerful generaliza­tion of modal logics) are surveyed and the recent decidability result for guarded fixed point logic (obtained in joint work with I. Walukiewicz) is explained. 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, different methods for reasoning with guarded fixed point sentences are presented: (1) reduction to the monadic theory of countable trees (SωS); (2) reduction to the μ-calculus with backwards modalities; (3) the automata theoretic method (which gives theoretically optimal complexity results).