This paper shows that over infinite trees, satisfiability is decidable for weak monadic second-order logic extended by the unbounding quantifier and quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while emptiness for the automaton model is decided using profinite trees. © 2014 Springer-Verlag.
CITATION STYLE
Bojańczyk, M. (2014). Weak MSO+U with path quantifiers over infinite trees. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8573 LNCS, pp. 38–49). Springer Verlag. https://doi.org/10.1007/978-3-662-43951-7_4
Mendeley helps you to discover research relevant for your work.