Document Open Access Logo

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

Authors Mikolaj Bojanczyk, Pawel Parys, Szymon Torunczyk

PDF
Thumbnail PDF

File

LIPIcs.STACS.2016.21.pdf
  • Filesize: 1.08 MB
  • 8 pages

Document Identifiers

Author Details

Mikolaj Bojanczyk
Pawel Parys
Szymon Torunczyk

Cite As Get 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) https://doi.org/10.4230/LIPIcs.STACS.2016.21

Abstract

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.

Subject Classification

Keywords
  • automata
  • logic
  • unbounding quantifier
  • bounds
  • undecidability

Metrics

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

References

  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: http://dx.doi.org/10.1007/978-3-662-44522-8_8.
  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: http://dx.doi.org/10.1007/978-3-540-30124-0_7.
  3. Mikołaj Bojańczyk. Weak MSO with the unbounding quantifier. Theory Comput. Syst., 48(3):554-576, 2011. URL: http://dx.doi.org/10.1007/s00224-010-9279-2.
  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: http://dx.doi.org/10.1007/978-3-662-43951-7_4.
  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: http://dx.doi.org/10.1109/LICS.2006.17.
  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: http://dx.doi.org/10.1007/978-3-662-43951-7_5.
  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: http://dx.doi.org/10.4230/LIPIcs.STACS.2012.648.
  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: http://dx.doi.org/10.1007/978-3-642-31424-7_8.
  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: http://dx.doi.org/10.1007/978-3-642-40184-8_32.
  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: http://dx.doi.org/10.1007/978-3-642-02930-1_12.
  11. Nathanaël Fijalkow and Martin Zimmermann. Cost-parity and cost-Streett games. In FSTTCS'12, pages 124-135, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.124.
  12. Szczepan Hummel and Michał Skrzypczak. The topological complexity of MSO+U and related automata models. Fundam. Inform., 119(1):87-111, 2012. URL: http://dx.doi.org/10.3233/FI-2012-728.
  13. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. From liveness to promptness. Formal Methods in System Design, 34(2):83-103, 2009. URL: http://dx.doi.org/10.1007/s10703-009-0067-z.
  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: http://dx.doi.org/10.1007/978-3-642-31585-5_35.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact