Search

We prove that $\omega$-languages of (non-deterministic) Petri nets and $\omega$-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of $\omega$-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of $\omega$-languages of (non-deterministic) Turing machines. We also show that it is highly undecidable to determine the topological complexity of a Petri net $\omega$-language. Moreover, we infer from the proofs of the above results that the equivalence and the inclusion problems for $\omega$-languages of Petri nets are $\Pi_2^1$-complete, hence also highly undecidable. Additionally, we show that the situation is quite the opposite when considering unambiguous Petri nets, which have the semantic property that at most one accepting run exists on every input. We provide a procedure of determinising them into deterministic Muller counter machines with counter copying. As a consequence, we entail that the $\omega$-languages recognisable by unambiguous Petri nets are $\Delta^0_3$ sets., Comment: arXiv admin note: substantial text overlap with arXiv:1712.07945

We consider the problem of deciding whether a given mso-definable relation over bi-infinite words contains an mso-definable function with the same domain. We prove that this problem is decidable. There are two obstacles to the existence of such uniformisations: the first is related to the existence of non-trivial automorphisms of bi-infinite words, whereas the second, more subtle obstacle, is related to the existence of finite, discrete dynamical systems, where no trajectory can be selected by an mso formula.

This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying “almost surely a branch $\pi \in\{0,1\}^{\omega}$ satisfies a formula $\varphi(\pi)$ ”, This logic was introduced by Michalewski and Mio; we call it $\mathrm{MSO}+\nabla$ following notation of Shelah and Lehmann. The logic $\mathrm{Mso}+\nabla$ subsumes many qualitative probabilistic formalisms, including qualitative probabilistic $check$ , probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of $\mathrm{MSO}+\nabla$ is true in the full binary tree11Independently and in parallel another proof of this result was given employing different techniques in [3]..

This paper exhibits an example of a \(\mathbf {\Sigma }^{1}_{1}\)-complete \(\omega \)-language that can be recognised by a Buchi automaton with one partially blind counter (or equivalently a Buchi VASS with only one place). It follows as a corollary that there is no equivalent model of deterministic automata, even if we allow much richer data structures than just counters. The same holds for weaker forms of determinism, like for unambiguous or countably-unambiguous machines. This shows that even in the one counter case, non-determinism of Buchi VASS is inherent.

We show that there are @S"3^0-complete languages of infinite words accepted by non-deterministic Petri nets with Buchi acceptance condition, or equivalently by Buchi blind counter automata. This shows that @w-languages accepted by non-deterministic Petri nets are topologically more complex than those accepted by deterministic Petri nets.

This work is about studying reasons for (un)decidability of variants of Monadic Second-order (mso) logic over infinite structures. Thus, it focuses on connecting the fact that a given theory is (un)decidable with certain measures of complexity of that theory.

A natural class in-between deterministic and non-deterministic automata is the class of unambiguous ones — an automaton is unambiguous if it has at most one accepting run on every tree. It seems that an unambiguous automaton represents the structure of the recognised language in a more rigid way than a general non-deterministic automaton. However, as shown in [NW96], there are ambiguous regular tree languages — languages that are not recognised by any unambiguous automaton.

In this chapter we study the classes of \(\omega \mathrm {B}\)- and \(\omega \mathrm {S}\)-regular languages, introduced by Bojanczyk and Colcombet in [BC06]. These languages of \(\omega \)-words are defined as those that can be recognised by a certain model of counter automata with asymptotic acceptance condition. Both these classes are strictly contained in the class of mso+u-definable languages, the advantage of these classes is that they admit effective constructions.

As the axiom of choice implies, for every relation \(R\subseteq X\times Y\) there exists a graph of a total function \(f:\pi _X(R) \rightarrow Y\) that is contained in R (such a graph is called a uniformization of R). A natural question asks in which cases such a function f is definable. A particular instance of this problem is, when R is an mso-definable set of pairs of trees and we ask about mso-definable f. This question is known as Rabin’s uniformization question. The negative answer to this question was given by Gurevich and Shelah [GS83] (see [CL07] for a simplified proof). They proved that there is no mso formula \(\psi (x,X)\) that chooses from every non-empty subset X of the complete binary tree a unique element x of X. This result is known as undefinability of a choice function on the complete binary tree. On the other hand, the formula saying that x is the \(\le \)-minimal element of X is a choice formula on \(\omega \)-words. In [Sie75, LS98, Rab07] it is proved that any mso-definable relation on \(\omega \)-words admits an mso-definable uniformization.

In both cases of finite words and \(\omega \)-words the class of regular languages can be equivalently defined as the class of languages recognisable by homomorphisms to appropriate finite algebras (monoids and \(\omega \)-semigroups respectively, see Sect. 1.5, page 10).

A non-deterministic automaton on infinite trees is unambiguous if it has at most one accepting run on every tree. For a given unambiguous parity automaton $$\mathcal {A} $$ of index i,i¾?2j we construct an alternating automaton $$\textsc {Transformation}\mathcal {A}$$ which accepts the same language, but is simpler in terms of alternating hierarchy of automata. If $$\mathcal {A} $$ is a Buchi automaton $$i=0, j=1$$, then $$\textsc {Transformation}\mathcal {A}$$ is a weak alternating automaton. In general, $$\textsc {Transformation}\mathcal {A}$$ belongs to the class $$\mathrm {Comp}{i}+1,2{j}$$, in particular it is simultaneously of alternating index i,i¾?2j and of the dual index $$i+1,2j+1$$. The main theorem of this paper is a correctness proof of the algorithm $$\textsc {Transformation}$$. The transformation algorithm is based on a separation algorithm of Arnold and Santocanale 2005 and extends results of Finkel and Simonnet 2009.

In this work we study Good-For-Games GFG automata over $$\omega $$ -words: non-deterministic automata where the non-determinism can be resolved by a strategy depending only on the prefix of the $$\omega $$ -word read so far. These automata retain some advantages of determinism: they can be composed with games and trees in a sound way, and inclusion $$\mathrm {L} \mathcal {A}\supseteq \mathrm {L} \mathcal {B}$$ can be reduced to a parity game over $$\mathcal {A} \times \mathcal {B} $$ if $$\mathcal {A} $$ is GFG. Therefore, they could be used to some advantage in verification, for instance as solutions to the synthesis problem. The main results of this work answer the question whether parity GFG automata actually present an improvement in terms of state-complexity the number of states compared to the deterministic ones. We show that a frontier lies between the Buchi condition, where GFG automata can be determinised with only quadratic blow-up in state-complexity; and the co-Buchi condition, where GFG automata can be exponentially smaller than any deterministic automaton for the same language. We also study the complexity of deciding whether a given automaton is GFG.

We consider probabilistic automata over finite words. Such an automaton defines the language consisting of the set of words accepted with probability greater than a given threshold. We show the existence of a universally non-regular probabilistic automaton, i.e. an automaton such that the language it defines is non-regular for every threshold. As a corollary, we obtain an alternative and very simple proof of the undecidability of determining whether such a language is regular.

Game automata are known to recognise languages arbitrarily high in both the non-deterministic and alternating Rabin–Mostowski index hierarchies. Recently it was shown that for this class both hierarchies are decidable. Here we complete the picture by showing that the weak index hierarchy is decidable as well. We also provide a procedure computing for a game automaton an equivalent weak alternating automaton with the minimal index and a quadratic number of states. As a by-product we obtain that, as for deterministic automata, the weak index and the Borel rank coincide.

For a given regular language of infinite trees, one can ask about the minimal number of priorities needed to recognize this language with a nondeterministic, alternating, or weak alternating parity automaton. These questions are known as, respectively, the nondeterministic, alternating, and weak Rabin-Mostowski index problems. Whether they can be answered effectively is a long-standing open problem, solved so far only for languages recognizable by deterministic automata (the alternating variant trivializes). We investigate a wider class of regular languages, recognizable by so-called game automata, which can be seen as the closure of deterministic ones under complementation and composition. Game automata are known to recognize languages arbitrarily high in the alternating Rabin-Mostowski index hierarchy; that is, the alternating index problem does not trivialize anymore. Our main contribution is that all three index problems are decidable for languages recognizable by game automata. Additionally, we show that it is decidable whether a given regular language can be recognized by a game automaton.

This paper is about MSO+U, an extension of monadic second-order logic, which has a quantifier that can express that a property of sets is true for arbitrarily large sets. We conjecture that the MSO+U theory of the complete binary tree is undecidable. We prove a weaker statement: there is no algorithm which decides this theory and has a correctness proof in zfc. This is because the theory is undecidable, under a set-theoretic assumption consistent with zfc, namely that there exists of projective well-ordering of 2 ω of type ω 1. We use Shelah’s undecidability proof of the MSO theory of the real numbers.

For a given regular language of infinite trees, one can ask about the minimal number of priorities needed to recognise this language with a non-deterministic or alternating parity automaton. These questions are known as, respectively, the non-deterministic and the alternating Rabin-Mostowski index problems. Whether they can be answered effectively is a long-standing open problem, solved so far only for languages recognisable by deterministic automata (the alternating variant trivialises). We investigate a wider class of regular languages, recognisable by so-called game automata, which can be seen as the closure of deterministic ones under complementation and composition. Game automata are known to recognise languages arbitrarily high in the alternating Rabin-Mostowski index hierarchy, i.e., the alternating index problem does not trivialise any more. Our main contribution is that both index problems are decidable for languages recognisable by game automata. Additionally, we show that it is decidable whether a given regular language can be recognised by a game automaton.

International audience; Choices made by nondeterministic word automata depend on both the past (the prefix of the word read so far) and the future (the suffix yet to be read). In several applications, most notably synthesis, the future is diverse or unknown, leading to algorithms that are based on deterministic automata. Hoping to retain some of the advantages of nondeterministic automata, researchers have studied restricted classes of nondeterministic automata. Three such classes are nondeterministic automata that are good for trees (GFT; i.e., ones that can be expanded to tree automata accepting the derived tree languages, thus whose choices should satisfy diverse futures), good for games (GFG; i.e., ones whose choices depend only on the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent deterministic automata). The theoretical properties and relative merits of the different classes are still open, having vagueness on whether they really differ from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also open is the possible succinctness of GFG and GFT automata compared to deterministic automata. We study these problems for ω-regular automata with all common acceptance conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction for GFG automata.

This work shows that for each i ∈ ω there exists a $\Sigma ^1_i$-hard ω-word language definable in Monadic Second Order Logic extended with the unbounding quantifier (MSO+U). This quantifier was introduced by Bojanczyk to express some asymptotic properties. Since it is not hard to see that each language expressible in MSO+U is projective, our finding solves the topological complexity of MSO+U. The result can immediately be transferred from ω-words to infinite labelled trees. As a consequence of the topological hardness we note that no alternating automaton with a Borel acceptance condition — or even with an acceptance condition of a bounded projective complexity — can capture all of MSO+U. The same holds for deterministic and nondeterministic automata since they are special cases of alternating ones. We also give exact topological complexities of related classes of languages recognized by nondeterministic ωB-, ωS- and ωBS-automata studied by Bojanczyk and Colcombet. Furthermore, we show that corresponding alternating automata have higher topological complexity than nondeterministic ones — they inhabit all finite levels of the Borel hierarchy. The paper is an extended journal version of [8]. The main theorem of that article is strengthened here.