Skip to Main content Skip to Navigation
Conference papers

Characterizing Definability in Decidable Fixpoint Logics

Michael Benedikt 1 Pierre Bourhis 2, 3 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 : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01639015
Contributor : Pierre Bourhis Connect in order to contact the contributor
Submitted on : Monday, November 20, 2017 - 11:51:57 AM
Last modification on : Wednesday, September 7, 2022 - 8:14:05 AM
Long-term archiving on: : Wednesday, February 21, 2018 - 1:30:10 PM

File

LIPIcs-ICALP-2017-107.pdf
Files produced by the author(s)

Identifiers

Citation

Michael Benedikt, Pierre Bourhis, Michael Vanden Boom. Characterizing Definability in Decidable Fixpoint Logics . ICALP 2017 - 44th International Colloquium on Automata, Languages, and Programming, Jul 2017, Varsovie, Poland. pp.14, ⟨10.4230/LIPIcs.ICALP.2017.107⟩. ⟨hal-01639015⟩

Share

Metrics

Record views

319

Files downloads

42