License
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://drops.dagstuhl.de/opus/volltexte/2012/3427/
Go to the corresponding Portal


Bojanczyk, Mikolaj ; Torunczyk, Szymon

Weak MSO+U over infinite trees

pdf-format:
Document 1.pdf (1,696 KB)


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 =		{http://dx.doi.org/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
Seminar: 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 Published by LZI