The Decidability of Guarded Fixed Point Logic

Erich Grädel

Erich Grädel
Mathematische Grundlagen der Informatik
RWTH Aachen
D-52056 Aachen
graedel@informatik.rwth-aachen.de
http://www-mgi.informatik.rwth-aachen.de/index.html

Abstract

Guarded fixed point logics are obtained by adding least and greatest fixed points to the guarded fragments of first-order logic that were recently introduced by Andréka, van Benthem and Németi. Guarded fixed point logics can also be viewed as the natural common extensions of the modal mu-calculus and the guarded fragments. In a joint paper with Igor Walukiewicz, we proved recently that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time. That proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. We present here an elementary proof for the decidability of guarded fixed point logics which is based on guarded bisimulations, a tree model property for guarded logics and an interpretation into the monadic second-order theory of countable trees.

Dvi-file
PS-File
PDF-File
Bibtex Entry