文章基本信息

标题：Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction
本地全文：下载
作者：Karoliina Lehtinen ; Sandra Quickert
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：41
页码：457-471
DOI：10.4230/LIPIcs.CSL.2015.457
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We construct, for any sentence of the modal mu calculus Psi, derived sentences in the modal fragment and the fragment without least fixpoints of the modal mu calculus such that Psi is equivalent to a formula in these fragments if and only if it is equivalent to these formulas. The formula without greatest fixpoints that Psi is equivalent to if and only if it is equivalent to any formula without greatest fixpoint is obtained by duality. This yields a constructive proof of decidability of the first levels of the modal mu alternation hierarchy. The blow-up incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed sub-exponentially more efficiently with the use of fixpoints. For the fragments with only greatest or least fixpoints however, as long as formulas are in disjunctive form, the transformation into a formula syntactically in these fragments does not increase the size of the formula.
关键词：modal mu calculus; fixpoint logic; alternation hierarchy