On a Fragment of AMSO and Tiling Systems
Achim Blumensath, Thomas Colcombet, Paweł Parys · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2016
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.