License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2017.107
URN: urn:nbn:de:0030-drops-74062
URL: http://drops.dagstuhl.de/opus/volltexte/2017/7406/
Go to the corresponding LIPIcs Volume Portal


Benedikt, Michael ; Bourhis, Pierre ; Vanden Boom, Michael

Characterizing Definability in Decidable Fixpoint Logics

pdf-format:
LIPIcs-ICALP-2017-107.pdf (0.5 MB)


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.

BibTeX - Entry

@InProceedings{benedikt_et_al:LIPIcs:2017:7406,
  author =	{Michael Benedikt and Pierre Bourhis and Michael Vanden Boom},
  title =	{{Characterizing Definability in Decidable Fixpoint Logics}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{107:1--107:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7406},
  URN =		{urn:nbn:de:0030-drops-74062},
  doi =		{10.4230/LIPIcs.ICALP.2017.107},
  annote =	{Keywords: Guarded logics, bisimulation, definability, automata}
}

Keywords: Guarded logics, bisimulation, definability, automata
Seminar: 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Issue Date: 2017
Date of publication: 06.07.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI