摘要：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.
