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 (CRIStAL) - 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.
Type de document :
Communication dans un congrès
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2016, New York, United States
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01413890
Contributeur : Inria Links <>
Soumis le : dimanche 9 avril 2017 - 20:26:00
Dernière modification le : mardi 3 juillet 2018 - 11:37:07
Document(s) archivé(s) le : lundi 10 juillet 2017 - 12:20:49

Fichier

LICS16-gnfpup-long.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01413890, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

160

Téléchargements de fichiers

51