文章基本信息

标题：Characterizing Definability in Decidable Fixpoint Logics
本地全文：下载
作者：Michael Benedikt ; Pierre Bourhis ; Michael Vanden Boom 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：80
页码：107:1-107:14
DOI：10.4230/LIPIcs.ICALP.2017.107
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Guarded logics; bisimulation; definability; automata