Article ID Journal Published Year Pages File Type
427746 Information Processing Letters 2012 5 Pages PDF
Abstract

The finite satisfiability problem for guarded fixpoint logic is decidable and complete for 2ExpTime (resp. ExpTime for formulas of bounded width).

► We prove that the finite satisfiability problem for guarded fixpoint logic is decidable. ► The complexity is shown to be the same as for satisfiability: 2ExpTime-complete. ► We exploit the connection between guarded fixpoint logic and alternating automata. ► We reuse the algorithm for finite emptiness of alternating automata on undirected graphs. ► Correctness is based on a recent development in the finite model theory of guarded logics.

Keywords
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, ,