Characterizing Definability in Decidable Fixpoint Logics

Michael Benedikt 1 Pierre Bourhis 2, 3 Michael 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 : We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back-and-forth between relational logics and logics over trees.
Type de document :
Communication dans un congrès
Ioannis Chatzigiannakis; Piotr Indyk; Fabian Kuhn; Anca Muscholl. ICALP 2017 - 44th International Colloquium on Automata, Languages, and Programming, Jul 2017, Varsovie, Poland. 107, pp.14, 〈10.4230/LIPIcs.ICALP.2017.107〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01639015
Contributeur : Pierre Bourhis <>
Soumis le : lundi 20 novembre 2017 - 11:51:57
Dernière modification le : mercredi 25 avril 2018 - 15:42:54
Document(s) archivé(s) le : mercredi 21 février 2018 - 13:30:10

Fichier

LIPIcs-ICALP-2017-107.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Michael Benedikt, Pierre Bourhis, Michael Boom. Characterizing Definability in Decidable Fixpoint Logics . Ioannis Chatzigiannakis; Piotr Indyk; Fabian Kuhn; Anca Muscholl. ICALP 2017 - 44th International Colloquium on Automata, Languages, and Programming, Jul 2017, Varsovie, Poland. 107, pp.14, 〈10.4230/LIPIcs.ICALP.2017.107〉. 〈hal-01639015〉

Partager

Métriques

Consultations de la notice

168

Téléchargements de fichiers

16