Paper detail

Separation Property for wB- and wS-regular Languages

In this paper we show that ωB- and ωS-regular languages satisfy the following separation-type theorem If L1,L2 are disjoint languages of ω-words both recognised by ωB- (resp. ωS)-automata then there exists an ω-regular language Lsep that contains L1, and whose complement contains L2. In particular, if a language and its complement are recognised by ωB- (resp. ωS)-automata then the language is ω-regular. The result is especially interesting because, as shown by Bojańczyk and Colcombet, ωB-regular languages are complements of ωS-regular languages. Therefore, the above theorem shows that these are two mutually dual classes that both have the separation property. Usually (e.g. in descriptive set theory or recursion theory) exactly one class from a pair C, Cc has the separation property. The proof technique reduces the separation property for ω-word languages to profinite languages using Ramsey's theorem and topological methods. After that reduction, the analysis of the separation property in the profinite monoid is relatively simple. The whole construction is technically not complicated, moreover it seems to be quite extensible. The paper uses a framework for the analysis of B- and S-regular languages in the context of the profinite monoid that was proposed by Toruńczyk.