On a Fragment of AMSO and Tiling Systems

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 ∃t∀s∃r ϕ(r, s, t), where ϕ 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. 1998 ACM Subject Classification F.4.1 Mathematical Logic Keywords and phrases monadic second-order logic, boundedness, tiling problems Digital Object Identifier 10.4230/LIPIcs.STACS.2016.19

• Type: Journal
• Year: 2016
• Where: STACS
• Authors: Achim Blumensath, Thomas Colcombet, Pawel Parys
• Keywords: STACS 2016, Theoretical Computer Science