Definability and interpolation within decidable fixpoint logics

Michael Benedikt; Pierre Bourhis; Michael Vanden Boom

doi:10.23638/LMCS-15(3:29)2019

Definability and interpolation within decidable fixpoint logics

Michael Benedikt
, Pierre Bourhis
, Michael Vanden Boom

University of Oxford
Université de Lille

Research output: Contribution to journal › Article › peer-review

8 Citations (Scopus)

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.

Original language	English
Article number	29
Journal	Logical Methods in Computer Science
Volume	15
Issue number	3
DOIs	https://doi.org/10.23638/LMCS-15(3:29)2019
Publication status	Published - 1 Jan 2019
Externally published	Yes

Keywords

Automata
Bisimulation
Characterizations
Guarded logics
Uniform interpolation

Access to Document

10.23638/LMCS-15(3:29)2019

Cite this

@article{c6efef6d39684f4db6053fdf146aff45,

title = "Definability and interpolation within decidable fixpoint logics",

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.",

keywords = "Automata, Bisimulation, Characterizations, Guarded logics, Uniform interpolation",

author = "Michael Benedikt and Pierre Bourhis and Boom, \{Michael Vanden\}",

note = "Publisher Copyright: {\textcopyright} M. Benedikt, P. Bourhis, and M. Vanden Boom.",

year = "2019",

month = jan,

day = "1",

doi = "10.23638/LMCS-15(3:29)2019",

language = "English",

volume = "15",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Logical Methods in Computer Science",

number = "3",

}

TY - JOUR

T1 - Definability and interpolation within decidable fixpoint logics

AU - Benedikt, Michael

AU - Bourhis, Pierre

AU - Boom, Michael Vanden

N1 - Publisher Copyright: © M. Benedikt, P. Bourhis, and M. Vanden Boom.

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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.

AB - 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.

KW - Automata

KW - Bisimulation

KW - Characterizations

KW - Guarded logics

KW - Uniform interpolation

U2 - 10.23638/LMCS-15(3:29)2019

DO - 10.23638/LMCS-15(3:29)2019

M3 - Article

AN - SCOPUS:85074128025

SN - 1860-5974

VL - 15

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 3

M1 - 29

ER -

Definability and interpolation within decidable fixpoint logics

Abstract

Keywords

Access to Document

Fingerprint

Cite this