Skip to Main content Skip to Navigation
Conference papers

A Step Up in Expressiveness of Decidable Fixpoint Logics

Michael Benedikt 1 Pierre Bourhis 2 Michael Vanden Boom 1
2 LINKS - Linking Dynamic Data
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189
Abstract : Guardedness restrictions are one of the principal means to obtain decidable logics — operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Inria Links <>
Submitted on : Sunday, April 9, 2017 - 8:26:00 PM
Last modification on : Friday, December 11, 2020 - 6:44:06 PM
Long-term archiving on: : Monday, July 10, 2017 - 12:20:49 PM


Files produced by the author(s)


  • HAL Id : hal-01413890, version 1



Michael Benedikt, Pierre Bourhis, Michael Vanden Boom. A Step Up in Expressiveness of Decidable Fixpoint Logics. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2016, New York, United States. ⟨hal-01413890⟩



Record views


Files downloads