Finite Satisfiability for Guarded Fixpoint Logic
Vince B\'ar\'any, Miko{\l}aj Boja\'nczyk
TL;DR
This paper proves that determining finite satisfiability in guarded fixpoint logic is a decidable problem with complexity bounds of 2ExpTime in general and ExpTime for bounded width formulas.
Contribution
It establishes the decidability and exact complexity of the finite satisfiability problem for guarded fixpoint logic.
Findings
Decidability of finite satisfiability for guarded fixpoint logic.
Complexity bounds of 2ExpTime for general formulas.
Complexity bounds of ExpTime for formulas of bounded width.
Abstract
The finite satisfiability problem for guarded fixpoint logic is decidable and complete for 2ExpTime (resp. ExpTime for formulas of bounded width).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Logic, Reasoning, and Knowledge