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 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 study two-player games with counters, where the objective of the first player is that the counter values remain bounded. We investigate the existence of a trade-off between the size of the memory and the bound achieved on the counters, which has been conjectured by Colcombet and Loeding. We show that unfortunately this conjecture does not hold: there is no trade-off between bounds and memory, even for finite arenas. On the positive side, we prove the existence of a trade-off for the special case of thin tree arenas. This allows to extend the theory of regular cost functions over thin trees, and obtain as a corollary the decidability of cost monadic second-order logic over thin trees., Conference version: ICALP'15

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.

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.

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.

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.

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%).

An infinite tree is called thin if it contains only countably many infinite branches. Thin trees can be seen as intermediate structures between infinite words and infinite trees. In this work we investigate properties of regular languages of thin trees. Our main tool is an algebra suitable for thin trees. Using this framework we characterize various classes of regular languages: commutative, open in the standard topology, closed under two variants of bisimulational equivalence, and definable in WMSO logic among all trees. We also show that in various meanings thin trees are not as rich as all infinite trees. In particular we observe a parity index collapse to level (1,3) and a topological complexity collapse to co-analytic sets. Moreover, a gap property is shown: a regular language of thin trees is either WMSO-definable among all trees or co-analytic-complete.

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.