Skip to Main content Skip to Navigation
Conference papers

Characterizing Definability in Decidable Fixpoint Logics

Michael Benedikt 1 Pierre Bourhis 2, 3 Michael Boom 1
2 LINKS - Linking Dynamic Data
CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189, Inria Lille - Nord Europe
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 <>
Submitted on : Monday, November 20, 2017 - 11:51:57 AM
Last modification on : Friday, December 11, 2020 - 6:44:06 PM
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

Collections

Citation

Michael Benedikt, Pierre Bourhis, Michael 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

326

Files downloads

70