Characterizing definability in decidable fixpoint logics

Michael Benedikt, Pierre Bourhis, Michael Vanden Boom

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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 languageEnglish
Title of host publication44th International Colloquium on Automata, Languages, and Programming, ICALP 2017
EditorsAnca Muscholl, Piotr Indyk, Fabian Kuhn, Ioannis Chatzigiannakis
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770415
DOIs
Publication statusPublished - 1 Jul 2017
Externally publishedYes
Event44th International Colloquium on Automata, Languages, and Programming, ICALP 2017 - Warsaw, Poland
Duration: 10 Jul 201714 Jul 2017

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume80
ISSN (Print)1868-8969

Conference

Conference44th International Colloquium on Automata, Languages, and Programming, ICALP 2017
Country/TerritoryPoland
CityWarsaw
Period10/07/1714/07/17

Keywords

  • Automata
  • Bisimulation
  • Definability
  • Guarded logics

Fingerprint

Dive into the research topics of 'Characterizing definability in decidable fixpoint logics'. Together they form a unique fingerprint.

Cite this