We prove in this paper that the length of the Wadge hierarchy of omega context free languages is greater than the Cantor ordinal epsilon_omega, which is the omega-th fixed point of the ordinal exponentiation of base omega. The same result holds for the conciliating Wadge hierarchy, defined by J. Duparc, of infinitary context free languages, studied by D. Beauquier. We show also that there exist some omega context free languages which are Sigma^0_omega-complete Borel sets, improving previous results on omega context free languages and the Borel hierarchy.
We show that, from a topological point of view, considering the Borel and the Wadge hierarchies, 1-counter Büchi automata have the same accepting power than Turing machines equipped with a Büchi acceptance condition. In particular, for every non null recursive ordinal alpha, there exist some Sigma^0_alpha-complete and some Pi^0_alpha-complete omega context free languages accepted by 1-counter Büchi automata, and the supremum of the set of Borel ranks of context free omega languages is the ordinal gamma^1_2 which is strictly greater than the first non recursive ordinal. This very surprising res…
We show that, from the topological point of view, 2-tape Büchi automata have the same accepting power as Turing machines equipped with a Büchi acceptance condition. The Borel and the Wadge hierarchies of the class RAT_omega of infinitary rational relations accepted by 2-tape Büchi automata are equal to the Borel and the Wadge hierarchies of omega-languages accepted by real-time Büchi 1-counter automata or by Büchi Turing machines. In particular, for every non-null recursive ordinal $α$, there exist some $Σ^0_α$-complete and some $Π^0_α$-complete infinitary rational relations. And the supremum …
We provide a complete description of the Wadge hierarchy for deterministically recognisable sets of infinite trees. In particular we give an elementary procedure to decide if one deterministic tree language is continuously reducible to another. This extends Wagner's results on the hierarchy of omega-regular languages of words to the case of trees.
We define and study an effective version of the Wadge hierarchy in computable quasi-Polish spaces which include most spaces of interest for computable analysis. Along with hierarchies of sets we study hierarchies of k-partitions which are interesting on their own. We show that levels of such hierarchies are preserved by the computable effectively open surjections, that if the effective Hausdorff-Kuratowski theorem holds in the Baire space then it holds in every computable quasi-Polish space, and we extend the effective Hausdorff theorem to k-partitions.
We survey recent results on the topological complexity of context-free omega-languages which form the second level of the Chomsky hierarchy of languages of infinite words. In particular, we consider the Borel hierarchy and the Wadge hierarchy of non-deterministic or deterministic context-free omega-languages. We study also decision problems, the links with the notions of ambiguity and of degrees of ambiguity, and the special case of omega-powers.
We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Büchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. We show also that the determinacy of Wadge games between two players in charge of omega-languages accepted by 1-counter Büchi automata is equivalent to the (effective) analytic Wadge determinacy. Using some results of set theory we prove that one can effectively construct a 1-counter Büchi automaton A and a Büchi automaton B such that: (1) There exis…
We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Büchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. We show also that the determinacy of Wadge games between two players in charge of omega-languages accepted by 1-counter Büchi automata is equivalent to the (effective) analytic Wadge determinacy. Using some results of set theory we prove that one can effectively construct a 1-counter Büchi automaton A and a Büchi automaton B such that: (1) There exis…
We investigate the topological complexity of non Borel recognizable tree languages with regard to the difference hierarchy of analytic sets. We show that, for each integer $n \geq 1$, there is a $D_{ω^n}({\bf Σ}^1_1)$-complete tree language L_n accepted by a (non deterministic) Muller tree automaton. On the other hand, we prove that a tree language accepted by an unambiguous Büchi tree automaton must be Borel. Then we consider the game tree languages $W_{(i,k)}$, for Mostowski-Rabin indices $(i, k)$. We prove that the $D_{ω^n}({\bf Σ}^1_1)$-complete tree languages L_n are Wadge reducible to th…
We give in this paper additional answers to questions of Lescow and Thomas [Logical Specifications of Infinite Computations, In:"A Decade of Concurrency", Springer LNCS 803 (1994), 583-621], proving new topological properties of omega context free languages : there exist some omega-CFL which are non Borel sets. And one cannot decide whether an omega-CFL is a Borel set. We give also an answer to questions of Niwinski and Simonnet about omega powers of finitary languages, giving an example of a finitary context free language L such that L^omega is not a Borel set. Then we prove some recursive an…
The classic approaches to synthesize a reactive system from a linear temporal logic (LTL) specification first translate the given LTL formula to an equivalent omega-automaton and then compute a winning strategy for the corresponding omega-regular game. To this end, the obtained omega-automata have to be (pseudo)-determinized where typically a variant of Safra's determinization procedure is used. In this paper, we show that this determinization step can be significantly improved for tool implementations by replacing Safra's determinization by simpler determinization procedures. In particular, w…
We show that many classical decision problems about 1-counter omega-languages, context free omega-languages, or infinitary rational relations, are $Π_2^1$-complete, hence located at the second level of the analytical hierarchy, and "highly undecidable". In particular, the universality problem, the inclusion problem, the equivalence problem, the determinizability problem, the complementability problem, and the unambiguity problem are all $Π_2^1$-complete for context-free omega-languages or for infinitary rational relations. Topological and arithmetical properties of 1-counter omega-languages, c…
This paper is a continuation of the study of topological properties of omega context free languages (omega-CFL). We proved before that the class of omega-CFL exhausts the hierarchy of Borel sets of finite rank, and that there exist some omega-CFL which are analytic but non Borel sets. We prove here that there exist some omega context free languages which are Borel sets of infinite (but not finite) rank, giving additional answer to questions of Lescow and Thomas [Logical Specifications of Infinite Computations, In:"A Decade of Concurrency", Springer LNCS 803 (1994), 583-621].
It was noticed by Harel in [Har86] that "one can define $Σ_1^1$-complete versions of the well-known Post Correspondence Problem". We first give a complete proof of this result, showing that the infinite Post Correspondence Problem in a regular $ω$-language is $Σ_1^1$-complete, hence located beyond the arithmetical hierarchy and highly undecidable. We infer from this result that it is $Π_1^1$-complete to determine whether two given infinitary rational relations are disjoint. Then we prove that there is an amazing gap between two decision problems about $ω$-rational functions realized by finite …
We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with …
We prove that some fairly basic questions on automata reading infinite words depend on the models of the axiomatic system ZFC. It is known that there are only three possibilities for the cardinality of the complement of an omega-language $L(A)$ accepted by a Büchi 1-counter automaton $A$. We prove the following surprising result: there exists a 1-counter Büchi automaton $A$ such that the cardinality of the complement $L(A)^-$ of the omega-language $L(A)$ is not determined by ZFC: (1). There is a model $V_1$ of ZFC in which $L(A)^-$ is countable. (2). There is a model $V_2$ of ZFC in which $L(A…
We consider the two-variable fragment FO^2[<] of first-order logic over finite words. Numerous characterizations of this class are known. Thérien and Wilke have shown that it is decidable whether a given regular language is definable in FO^2[<]. From a practical point of view, as shown by Weis, FO^2[<] is interesting since its satisfiability problem is in NP. Restricting the number of quantifier alternations yields an infinite hierarchy inside the class of FO^2[<]-definable languages. We show that each level of this hierarchy is decidable. For this purpose, we relate each level of the hierarch…
We prove that the injectively omega-tree-automatic ordinals are the ordinals smaller than $ω^{ω^ω}$. Then we show that the injectively $ω^n$-automatic ordinals, where $n>0$ is an integer, are the ordinals smaller than $ω^{ω^n}$. This strengthens a recent result of Schlicht and Stephan who considered in [Schlicht-Stephan11] the subclasses of finite word $ω^n$-automatic ordinals. As a by-product we obtain that the hierarchy of injectively $ω^n$-automatic structures, n>0, which was considered in [Finkel-Todorcevic12], is strict.
