2026-07-20T09:01:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7406 2024-03-06T10:40:30Z ddc:004 open_access

Characterizing Definability in Decidable Fixpoint Logics Benedikt, Michael Bourhis, Pierre Vanden Boom, Michael Guarded logics bisimulation definability automata 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michael Benedikt and Pierre Bourhis and Michael Vanden Boom 2017 Is Part Of LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2017.107 urn:nbn:de:0030-drops-74062 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.107 eng https://creativecommons.org/licenses/by/3.0/legalcode