Weak MSO+U over infinite trees

Authors Mikolaj Bojanczyk, Szymon Torunczyk



PDF
Thumbnail PDF

File

LIPIcs.STACS.2012.648.pdf
  • Filesize: 1.65 MB
  • 13 pages

Document Identifiers

Author Details

Mikolaj Bojanczyk
Szymon Torunczyk

Cite AsGet BibTex

Mikolaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 648-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/LIPIcs.STACS.2012.648

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.
Keywords
  • Infinite trees
  • distance automata
  • MSO+U
  • profinite words

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail