The study of various decision problems for logic fragments has a long history in computer science. This paper is on the membership problem for a fragment of first-order logic over infinite words; the membership problem asks for a given language whether it is definable in some fixed fragment. The alphabetic topology was introduced as part of an effective characterization of the fragment ∑_2 over infinite words. Here, ∑_2 consists of the first-order formulas with two blocks of quantifiers, starting with an existential quantifier. Its Boolean closure is B∑_2. Our first main result is an effective characterization of the Boolean closure of the alphabetic topology, that is, given an ω-regular language L, it is decidable whether L is a Boolean combination of open sets in the alphabetic topology. This is then used for transferring Place and Zeitoun's recent decidability result for B∑_2 from finite to infinite words.
展开▼
