Locally threshold testable languages of infinite words
Two versions of local threshold testability for languages of infinite words (omega-languages) are compared: It is proved that an omega-language is finitely locally threshold testable iff it is locally threshold testable and belongs to the intersection of the Borel classes Fsigma and Gdelta. As a consequence we obtain a result on the definability of infinite word structures in the signature of the successor function: It is decidable whether a given monadic second order formula has the same set of infinite word models as some first order formula. For biinfinite word models the corresponding problem was raised by Jean Eric Pin. The major tool in the proofs is the analysis of De Bruijn graphs.