Search

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 work is a study of the class of non-deterministic automata on infinite trees that are unambiguous i.e. have at most one accepting run on every tree. The motivating question asks if the fact that an automaton is unambiguous implies some drop in the descriptive complexity of the language recognised by the automaton. As it turns out, such a drop occurs for the parity index and does not occur for the weak parity index.More precisely, given an unambiguous parity automaton [Formula: see text] of index [Formula: see text], we show how to construct an alternating automaton [Formula: see text] which accepts the same language, but is simpler in terms of the acceptance condition. In particular, if [Formula: see text] is a Büchi automaton ([Formula: see text]) then [Formula: see text] is a weak alternating automaton. In general, [Formula: see text] belongs to the class [Formula: see text], what implies that it is simultaneously of alternating index [Formula: see text] and of the dual index [Formula: see text]. The transformation algorithm is based on a separation procedure of Arnold and Santocanale (2005).In the case of non-deterministic automata with the weak parity condition, we provide a separation procedure analogous to the one used above. However, as illustrated by examples, this separation procedure cannot be used to prove a complexity drop in the weak case, as there is no such drop.

We consider the problem of computing the measure of a regular set of infinite binary trees. While the general case remains unsolved, we show that the measure of a language can be computed when the set is given in one of the following three formalisms: a first-order formula with no descendant relation; a Boolean combination of conjunctive queries (with descendant relation); or by a non-deterministic safety tree automaton. Additionally, in the first two cases the measure of the set is always rational, while in the third it is an algebraic number. Moreover, we provide an example of a first-order formula that uses descendant relation and defines a language of infinite trees having an irrational (but algebraic) measure.

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.

The paper presents a concept of a coloring - an extension of deterministic parity automata. A coloring K is a function A^@?->N [email protected]?"@a"@?"A"^"@wliminfn->~K(@[email protected]?"n) ~K(@[email protected]?"n)=0mod2}. We show that sets defined by colorings are exactly all @D"3^0 sets in the standard product topology on A^@w. Furthermore, when considering natural subfamilies of all colorings, we obtain families BC(@S"2^0), @D"2^0, and BC(@S"1^0). Therefore, colorings can be seen as a characterisation of all these classes with a uniform acceptance condition. Additionally, we analyse a similar definition of colorings where the limsup condition is used instead of liminf. It turns out that such colorings have smaller expressive power - they cannot define all @D"3^0 sets.

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.

An infinite binaryword can be identified with a branch in the full binary tree. We consider sets of branches definable in monadic second-order logic over the tree, where we allow some extra monadic predicates on the nodes. We show that this class equals to the Boolean combinations of sets in the Borel class Σ$^0_2$ over the Cantor discontinuum. Note that the last coincides with the Borel complexity of ω-regular languages.

mso logic is quite expressive, in particular it covers most of other logics used for specifying properties of computer systems. However, mso is not able to express quantitative properties of structures.

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.

As explained in Chap. 9, mso+u logic is an extension of mso that allows to express quantitative properties of structures. One of the consequences of the big expressive power of mso+u is that many decision problems about other quantitative formalisms can be reduced to mso+u. An example is the reduction [CL08] of the non-deterministic index problem to a certain boundedness problem that can be further reduced to mso+u on infinite trees. Therefore, decidability of mso+u would be a very desirable result.

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 this chapter, we study thin trees, which generalize both finite trees and \(\omega \)-words, but which are still simpler than arbitrary infinite trees. A tree is thin if it contains only countably many infinite branches. It turns out [BIS13] that some problems are more tractable on thin trees than in full generality. Therefore, thin trees can be seen as an intermediate step in understanding regular languages of general infinite trees.

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.

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.

We introduce a general method for proving measurability of topologically complex sets by establishing a correspondence between the notion of game tree languages from automata theory and the σ-algebra of \(\mathcal{R}\)-sets, introduced by A. Kolmogorov as a foundation for measure theory. We apply the method to answer positively to an open problem regarding the game interpretation of the probabilistic μ-calculus.

In this paper we show that {\omega}B- and {\omega}S-regular languages satisfy the following separation-type theorem If L1,L2 are disjoint languages of {\omega}-words both recognised by {\omega}B- (resp. {\omega}S)-automata then there exists an {\omega}-regular language Lsep that contains L1, and whose complement contains L2. In particular, if a language and its complement are recognised by {\omega}B- (resp. {\omega}S)-automata then the language is {\omega}-regular. The result is especially interesting because, as shown by Boja\'nczyk and Colcombet, {\omega}B-regular languages are complements of {\omega}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 {\omega}-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\'nczyk.

In the present study 5 grey seals (Halichoerus grypus), 3 common seals (Phoca vitulina) and 1 ringed seal (Pusa hispida) bycaught or stranded on the Polish Baltic Sea coast in years 2000-2006 were investigated for the infestation of parasitic anisakid nematodes. 749 of anisakids were found. The most common were: Contracaecum osculatum (59.3%) and Pseudoterranova decipiens (31.0%). There were also small numbers of Anisakis simplex (0.8%). After performing RFLP three sibling species were found. C. osculatum was identified as C. osculatum C, P decipiens was identified as P. decipiens sensu stricto and A. simplex — A. simplex sensu stricto. Nematodes found in seals were mostly in L4 and adult life stage — both of them were equal with some minor variations among the specimens. Sex ratio was also equal, but there was slight excess of males in some cases. There was a minority of L3 larvae belonging to A. simplex species (0.8%).

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.