License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2012.648
URN: urn:nbn:de:0030-drops-34279
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3427/
Go to the corresponding LIPIcs Volume Portal

Bojanczyk, Mikolaj ; Torunczyk, Szymon

Weak MSO+U over infinite trees

pdf-format:
43.pdf (2 MB)

Abstract

We prove that, over infinite trees, satisfiability is decidable for Weak Monadic Second-Order Logic extended by the unbounding quantifier U. We develop an automaton model, prove that it is effectively equivalent to the logic, and that the automaton model has decidable emptiness.

BibTeX - Entry

@InProceedings{bojanczyk_et_al:LIPIcs:2012:3427,
  author =	{Mikolaj Bojanczyk and Szymon Torunczyk},
  title =	{{Weak MSO+U over infinite trees}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{648--660},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{Christoph D{\"u}rr and Thomas Wilke},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3427},
  URN =		{urn:nbn:de:0030-drops-34279},
  doi =		{10.4230/LIPIcs.STACS.2012.648},
  annote =	{Keywords: Infinite trees, distance automata, MSO+U, profinite words}
}

Keywords: Infinite trees, distance automata, MSO+U, profinite words
Collection: 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)
Issue Date: 2012
Date of publication: 24.02.2012

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