The MSO+U Theory of (N,<) Is Undecidable

Authors Mikolaj Bojanczyk, Pawel Parys, Szymon Torunczyk

Thumbnail PDF


  • Filesize: 1.08 MB
  • 8 pages

Document Identifiers

Author Details

Mikolaj Bojanczyk
Pawel Parys
Szymon Torunczyk

Cite AsGet BibTex

Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U Theory of (N,<) Is Undecidable. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 21:1-21:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.
  • automata
  • logic
  • unbounding quantifier
  • bounds
  • undecidability


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Achim Blumensath, Olivier Carton, and Thomas Colcombet. Asymptotic monadic second-order logic. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 87-98. Springer, 2014. URL:
  2. Mikołaj Bojańczyk. A bounding quantifier. In Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, pages 41-55, 2004. URL:
  3. Mikołaj Bojańczyk. Weak MSO with the unbounding quantifier. Theory Comput. Syst., 48(3):554-576, 2011. URL:
  4. Mikołaj Bojańczyk. Weak MSO+U with path quantifiers over infinite trees. In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, pages 38-49, 2014. URL:
  5. Mikołaj Bojańczyk and Thomas Colcombet. Bounds in w-regularity. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 285-296, 2006. URL:
  6. Mikołaj Bojańczyk, Tomasz Gogacz, Henryk Michalewski, and Michał Skrzypczak. On the decidability of MSO+U on infinite trees. In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, pages 50-61, 2014. URL:
  7. Mikołaj Bojańczyk and Szymon Toruńczyk. Weak MSO+U over infinite trees. In 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, pages 648-660, 2012. URL:
  8. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, and Petr Novotný. Efficient controller synthesis for consumption games with multiple resource types. In CAV'12, pages 23-38, 2012. URL:
  9. Claudia Carapelle, Alexander Kartzow, and Markus Lohrey. Satisfiability of CTL* with constraints. In CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, pages 455-469, 2013. URL:
  10. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Automata, Languages and Programming, 36th International Colloquium, ICALP 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part II, pages 139-150, 2009. URL:
  11. Nathanaël Fijalkow and Martin Zimmermann. Cost-parity and cost-Streett games. In FSTTCS'12, pages 124-135, 2012. URL:
  12. Szczepan Hummel and Michał Skrzypczak. The topological complexity of MSO+U and related automata models. Fundam. Inform., 119(1):87-111, 2012. URL:
  13. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. From liveness to promptness. Formal Methods in System Design, 34(2):83-103, 2009. URL:
  14. Szymon Toruńczyk. Languages of profinite words and the limitedness problem. In Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II, pages 377-389, 2012. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail