Guarded fixed point logic
- 1 January 1999
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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.Keywords
This publication has 11 references indexed in Scilit:
- Tree automata, mu-calculus and determinacyPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On the Restraining Power of GuardsThe Journal of Symbolic Logic, 1999
- On logics with two variablesTheoretical Computer Science, 1999
- On Preservation Theorems for Two‐Variable LogicMathematical Logic Quarterly, 1999
- Modal Languages and Bounded Fragments of Predicate LogicJournal of Philosophical Logic, 1998
- Infinite games on finitely coloured graphs with applications to automata on infinite treesTheoretical Computer Science, 1998
- Reasoning about the past with two-way automataPublished by Springer Nature ,1998
- On the Decision Problem for Two-Variable First-Order LogicBulletin of Symbolic Logic, 1997
- An automata theoretic decision procedure for the propositional mu-calculusInformation and Computation, 1989
- On languages with two variablesMathematical Logic Quarterly, 1975