License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.457
URN: urn:nbn:de:0030-drops-54316
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5431/
Go to the corresponding LIPIcs Volume Portal

Lehtinen, Karoliina ; Quickert, Sandra

Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction

pdf-format:
28.pdf (0.5 MB)

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 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.

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 =	{457--471},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5431},
  URN =		{urn:nbn:de:0030-drops-54316},
  doi =		{10.4230/LIPIcs.CSL.2015.457},
  annote =	{Keywords: modal mu calculus, fixpoint logic, alternation hierarchy}
}

Keywords: modal mu calculus, fixpoint logic, alternation hierarchy
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI