LIPIcs.STACS.2016.21.pdf
- Filesize: 1.08 MB
- 8 pages
Document
The MSO+U Theory of (N,<) Is Undecidable
Authors
-
Part of:
Volume:
33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2016-02-16
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)
https://doi.org/10.4230/LIPIcs.STACS.2016.21
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.
Keywords
- automata
- logic
- unbounding quantifier
- bounds
- undecidability
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.