Lehtinen, Karoliina ;
Quickert, Sandra
Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction
Abstract
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 blowup incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed subexponentially 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.
BibTeX  Entry
@InProceedings{lehtinen_et_al:LIPIcs:2015:5431,
author = {Karoliina Lehtinen and Sandra Quickert},
title = {{Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {457471},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897903},
ISSN = {18688969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5431},
URN = {urn:nbn:de:0030drops54316},
doi = {10.4230/LIPIcs.CSL.2015.457},
annote = {Keywords: modal mu calculus, fixpoint logic, alternation hierarchy}
}
07.09.2015
Keywords: 

modal mu calculus, fixpoint logic, alternation hierarchy 
Seminar: 

24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Issue date: 

2015 
Date of publication: 

07.09.2015 