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.
@InProceedings{blumensath_et_al:LIPIcs.STACS.2016.19, author = {Blumensath, Achim and Colcombet, Thomas and Parys, Pawel}, title = {{On a Fragment of AMSO and Tiling Systems}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {19:1--19:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.19}, URN = {urn:nbn:de:0030-drops-57202}, doi = {10.4230/LIPIcs.STACS.2016.19}, annote = {Keywords: monadic second-order logic, boundedness, tiling problems} }
Feedback for Dagstuhl Publishing