10.4230/LIPICS.STACS.2012.648
Bojanczyk, Mikolaj
Mikolaj
Bojanczyk
Torunczyk, Szymon
Szymon
Torunczyk
Weak MSO+U over infinite trees
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2012
Article
Infinite trees
distance automata
MSO+U
profinite words
Dürr, Christoph
Christoph
Dürr
Wilke, Thomas
Thomas
Wilke
2012
2012-02-24
2012-02-24
2012-02-24
en
urn:nbn:de:0030-drops-34279
10.4230/LIPIcs.STACS.2012
978-3-939897-35-4
1868-8969
10.4230/LIPIcs.STACS.2012
LIPIcs, Volume 14, STACS 2012
29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)
2013
14
58
648
660
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dürr, Christoph
Christoph
Dürr
Wilke, Thomas
Thomas
Wilke
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2012
14
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
13 pages
1736842 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012), pages 648-660