1 Search Results for "Quickert, Sandra"

Document

DOI: 10.4230/LIPIcs.CSL.2015.457

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

Authors: Karoliina Lehtinen and Sandra Quickert

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

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.

Cite as

Karoliina Lehtinen and Sandra Quickert. Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 457-471, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{lehtinen_et_al:LIPIcs.CSL.2015.457,
  author =	{Lehtinen, Karoliina and Quickert, Sandra},
  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 =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.457},
  URN =		{urn:nbn:de:0030-drops-54316},
  doi =		{10.4230/LIPIcs.CSL.2015.457},
  annote =	{Keywords: modal mu calculus, fixpoint logic, alternation hierarchy}
}

Refine by Author
1 Lehtinen, Karoliina
1 Quickert, Sandra

Refine by Classification

Refine by Keyword
1 alternation hierarchy
1 fixpoint logic
1 modal mu calculus

Refine by Type
1 document

Refine by Publication Year
1 2015

1 Search Results for "Quickert, Sandra"

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

Abstract

Cite as

Thanks for your feedback!

Could not send message