Level Two of the Quantifier Alternation Hierarchy over Infinite Words

From MaRDI portal



Abstract: 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 Sigma2 over infinite words. Here, Sigma2 consists of the first-order formulas with two blocks of quantifiers, starting with an existential quantifier. Its Boolean closure is mathbbBSigma2. Our first main result is an effective characterization of the Boolean closure of the alphabetic topology, that is, given an omega-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 mathbbBSigma2 from finite to infinite words.











This page was built for publication: Level Two of the Quantifier Alternation Hierarchy over Infinite Words

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740188)