| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 427746 | Information Processing Letters | 2012 | 5 Pages |
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
Vince Bárány, Mikołaj Bojańczyk,