Logic in Computer Science (LICS 1999)

Paper: Guarded Fixed Point Logic (at LICS 1999)

Authors: Erich Grädel Igor Walukiewicz

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. We prove that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time. For guarded fixed point sentences of bounded width, the most important case for applications, the satisfiability problem is EXPTIME-complete.

BibTeX

  @InProceedings{GrdelWalukiewicz-GuardedFixedPointLo,
    author = 	 {Erich Grädel and Igor Walukiewicz},
    title = 	 {Guarded Fixed Point Logic},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {45--54},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }