Document Open Access Logo

On a Fragment of AMSO and Tiling Systems

Authors Achim Blumensath, Thomas Colcombet, Pawel Parys

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2016.19.pdf
  • Filesize: 0.64 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • monadic second-order logic
  • boundedness
  • tiling problems

Metrics

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

Abstract

We prove that satisfiability over infinite words is decidable for a fragment of asymptotic monadic second-order logic. In this fragment we only allow formulae of the form "exists t forall s exists r: phi(r,s,t)", where phi does not use quantifiers over number variables, and variables r and s can be only used simultaneously, in subformulae of the form s < f(x) <= r.

Cite As Get BibTex

Achim Blumensath, Thomas Colcombet, and Pawel Parys. On a Fragment of AMSO and Tiling Systems. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.STACS.2016.19

Author Details

Achim Blumensath
Thomas Colcombet
Pawel Parys

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. The finite graph problem for two-way alternating automata. Theor. Comput. Sci., 3(298):511-528, 2003. URL: http://dx.doi.org/10.1016/S0304-3975(02)00866-6.
  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 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. IEEE Computer Society, 2006. URL: http://dx.doi.org/10.1109/LICS.2006.17.
  5. Mikołaj Bojańczyk, Paweł Parys, and Szymon Toruńczyk. The MSO+U Theory of (N,<) Is Undecidable. In Nicolas Ollinger and Heribert Vollmer, editors, 33rd International Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France, volume 47 of LIPIcs, pages 21:1-21:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2016.21.
  6. Mikołaj Bojańczyk and Szymon Toruńczyk. Weak MSO+U over infinite trees. In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 648-660. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2012.648.
  7. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, and Petr Novotný. Efficient controller synthesis for consumption games with multiple resource types. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 23-38. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31424-7_8.
  8. J. Richard Büchi. On a decision method in a restricted second order arithmetic. In Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.), pages 1-11, Stanford, Calif., 1962. Stanford Univ. Press. Google Scholar
  9. Claudia Carapelle, Alexander Kartzow, and Markus Lohrey. Satisfiability of CTL* with constraints. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 455-469. Springer, 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 Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas, editors, Automata, Languages and Programming, 36th Internatilonal Collogquium, ICALP 2009, Rhodes, greece, July 5-12, 2009, Proceedings, Part II, volume 5556 of Lecture Notes in Computer Science, pages 139-150. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02930-1_12.
  11. Thomas Colcombet. Regular cost functions, part I: logic and algebra over words. Logical Methods in Computer Science, 9(3), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(3:3)2013.
  12. Nathanaël Fijalkow and Martin Zimmermann. Cost-parity and cost-streett games. Logical Methods in Computer Science, 10(2), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(2:14)2014.
  13. Szczepan Hummel and Michal Skrzypczak. The topological complexity of MSO+U and related automata models. Fundam. Inform., 119(1):87-111, 2012. Google Scholar
  14. Daniel Kirsten. Distance desert automata and the star height problem. ITA, 39(3):455-509, 2005. URL: http://dx.doi.org/10.1051/ita:2005027.
  15. 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.
  16. Imre Simon. Factorization forests of finite height. Theor. Comput. Sci., 72(1):65-94, 1990. URL: http://dx.doi.org/10.1016/0304-3975(90)90047-L.
  17. Szymon Toruńczyk. Languages of profinite words and the limitedness problem. PhD thesis, Warsaw University, 2011. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact