-
Infinite lexicographic products of positional objectives
Authors:
Antonio Casares,
Pierre Ohlmann,
Michał Skrzypczak,
Igor Walukiewicz
Abstract:
This paper contributes to the study of positional determinacy of infinite duration games played on potentially infinite graphs. Recently, [Ohlmann, TheoretiCS 2023] established that positionality of prefix-independent objectives is preserved by finite lexicographic products. We propose two different notions of infinite lexicographic products indexed by arbitrary ordinals, and extend Ohlmann's resu…
▽ More
This paper contributes to the study of positional determinacy of infinite duration games played on potentially infinite graphs. Recently, [Ohlmann, TheoretiCS 2023] established that positionality of prefix-independent objectives is preserved by finite lexicographic products. We propose two different notions of infinite lexicographic products indexed by arbitrary ordinals, and extend Ohlmann's result by proving that they also preserve positionality. In the context of one-player positionality, this extends positional determinacy results of [Grädel and Walukiewicz, Logical Methods in Computer Science 2006] to edge-labelled games and arbitrarily many priorities for both Max-Parity and Min-Parity. Moreover, we show that the Max-Parity objectives over countable ordinals are complete for the infinite levels of the difference hierarchy over $Σ^0_2$ and that Min-Parity is complete for the class $Σ^0_3$. We obtain therefore positional languages that are complete for all those levels, as well as new insights about closure under unions and neutral letters.
△ Less
Submitted 17 June, 2025;
originally announced June 2025.
-
A Dichotomy Theorem for Ordinal Ranks in MSO
Authors:
Damian Niwiński,
Paweł Parys,
Michał Skrzypczak
Abstract:
We focus on formulae $\exists X.\, \varphi (\vec{Y}, X) $ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank} (X) < ω_1$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $\varphi$. Let…
▽ More
We focus on formulae $\exists X.\, \varphi (\vec{Y}, X) $ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank} (X) < ω_1$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $\varphi$. Let $η_{\varphi}$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank} (X) \leq η_{\varphi}$. Then $η_{\varphi}$ is either strictly smaller than $ω^2$ or it reaches the maximal possible value $ω_1$. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.
△ Less
Submitted 9 January, 2025;
originally announced January 2025.
-
Computing measures of weak-MSO definable sets of trees
Authors:
Damian Niwiński,
Marcin Przybyłko,
Michał Skrzypczak
Abstract:
his work addresses the problem of computing measures of recognisable sets of infinite trees. An algorithm is provided to compute the probability measure of a tree language recognisable by a weak alternating automaton, or equivalently definable in weak monadic second-order logic. The measure is the uniform coin-flipping measure or more generally it is generated by a~branching stochastic process. Th…
▽ More
his work addresses the problem of computing measures of recognisable sets of infinite trees. An algorithm is provided to compute the probability measure of a tree language recognisable by a weak alternating automaton, or equivalently definable in weak monadic second-order logic. The measure is the uniform coin-flipping measure or more generally it is generated by a~branching stochastic process. The class of tree languages in consideration, although smaller than all regular tree languages, comprises in particular the languages definable in the alternation-free mu-calculus or in temporal logic CTL. Thus, the new algorithm may enhance the toolbox of probabilistic model checking.
△ Less
Submitted 17 October, 2024;
originally announced October 2024.
-
Positionality in Σ_0^2 and a completeness result
Authors:
Pierre Ohlmann,
Michał Skrzypczak
Abstract:
We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in Σ_0^2 which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Büchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyńs…
▽ More
We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in Σ_0^2 which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Büchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023].
We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective W which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective W' which is equivalent to W over finite game graphs and positional over arbitrary game graphs.
△ Less
Submitted 11 June, 2025; v1 submitted 29 September, 2023;
originally announced September 2023.
-
On the Computability of Measures of Regular Sets of Infinite Trees
Authors:
Damian Niwiński,
Paweł Parys,
Michał Skrzypczak
Abstract:
The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where simila…
▽ More
The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where similar results were shown for formalisms weaker than the full monadic second-order logic.
△ Less
Submitted 21 November, 2024; v1 submitted 24 April, 2023;
originally announced April 2023.
-
Languages given by Finite Automata over the Unary Alphabet
Authors:
Wojciech Czerwiński,
Maciej Dębski,
Tomasz Gogasz,
Gordon Hoi,
Sanjay Jain,
Michał Skrzypczak,
Frank Stephan,
Christopher Tan
Abstract:
This paper studies the complexity of operations on finite automata and the complexity of their decision problems when the alphabet is unary. Let $n$ denote the maximum of the number of states of the input finite automata considered in the corresponding results. The following main results are obtained:
(1) Given two unary NFAs recognising $L$ and $H$, respectively, one can decide whether…
▽ More
This paper studies the complexity of operations on finite automata and the complexity of their decision problems when the alphabet is unary. Let $n$ denote the maximum of the number of states of the input finite automata considered in the corresponding results. The following main results are obtained:
(1) Given two unary NFAs recognising $L$ and $H$, respectively, one can decide whether $L \subseteq H$ as well as whether $L = H$ in time $2^{O((n \log n)^{1/3})}$. The previous upper bound on time was $2^{O((n \log n)^{1/2})}$ as given by Chrobak (1986), and this bound was not significantly improved since then.
(2) Given two unary UFAs (unambiguous finite automata) recognising $L$ and $H$, respectively, one can determine a UFA recognising $L \cup H$ and a UFA recognising complement of $L$, where these output UFAs have the number of states bounded by a quasipolynomial in $n$. However, in the worst case, a UFA for recognising concatenation of languages recognised by two $n$-state UFAs, uses $2^{Θ((n \log^2 n)^{1/3})}$ states.
(3) Given a unary language $L$, if $L$ contains the word of length $k$, then let $L(k)=1$ else let $L(k)=0$. Let $ω_L$ be the $ω$-word $L(0)L(1)\ldots$ and let $\cal L$ be a fixed $ω$-regular language. The last section studies how difficult it is to decide, given an $n$-state UFA or NFA
△ Less
Submitted 13 December, 2024; v1 submitted 13 February, 2023;
originally announced February 2023.
-
On the expressive power of non-deterministic and unambiguous Petri nets over infinite words
Authors:
Olivier Finkel,
Michał Skrzypczak
Abstract:
We prove that $ω$-languages of (non-deterministic) Petri nets and $ω$-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of $ω$-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of $ω$-languages of (non-deterministic) Turing machines. We also show that it is highly u…
▽ More
We prove that $ω$-languages of (non-deterministic) Petri nets and $ω$-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of $ω$-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of $ω$-languages of (non-deterministic) Turing machines. We also show that it is highly undecidable to determine the topological complexity of a Petri net $ω$-language. Moreover, we infer from the proofs of the above results that the equivalence and the inclusion problems for $ω$-languages of Petri nets are $Π_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 $ω$-languages recognisable by unambiguous Petri nets are $Δ^0_3$ sets.
△ Less
Submitted 14 December, 2021; v1 submitted 8 July, 2021;
originally announced July 2021.
-
Deterministic and game separability for regular languages of infinite trees
Authors:
Lorenzo Clemente,
Michał Skrzypczak
Abstract:
We show that it is decidable whether two regular languages of infinite trees are separable by a deterministic language, resp., a game language. We consider two variants of separability, depending on whether the set of priorities of the separator is fixed, or not. In each case, we show that separability can be decided in EXPTIME, and that separating automata of exponential size suffice. We obtain o…
▽ More
We show that it is decidable whether two regular languages of infinite trees are separable by a deterministic language, resp., a game language. We consider two variants of separability, depending on whether the set of priorities of the separator is fixed, or not. In each case, we show that separability can be decided in EXPTIME, and that separating automata of exponential size suffice. We obtain our results by reducing to infinite duration games with ω-regular winning conditions and applying the finite-memory determinacy theorem of Büchi and Landweber.
△ Less
Submitted 3 May, 2021;
originally announced May 2021.
-
On the Succinctness of Alternating Parity Good-for-Games Automata
Authors:
Udi Boker,
Denis Kuperberg,
Karoliina Lehtinen,
Michał Skrzypczak
Abstract:
We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read.
We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single expone…
▽ More
We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read.
We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG. We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is PSpace-hard already for alternating automata on finite words.
△ Less
Submitted 29 September, 2020;
originally announced September 2020.
-
On Succinctness and Recognisability of Alternating Good-for-Games Automata
Authors:
Udi Boker,
Denis Kuperberg,
Karoliina Lehtinen,
Michał Skrzypczak
Abstract:
We study alternating good-for-games (GFG) automata, i.e., alternating automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we lift many results from nondeterministic…
▽ More
We study alternating good-for-games (GFG) automata, i.e., alternating automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we lift many results from nondeterministic parity GFG automata to alternating ones: a single exponential determinisation procedure, an Exptime upper bound to the GFGness problem, a PTime algorithm for the GFGness problem of weak automata, and a reduction from a positive solution to the $G_2$ conjecture to a PTime algorithm for the GFGness problem of parity automata with a fixed index. The $G_2$ conjecture states that a nondeterministic parity automaton A is GFG if and only if a token game, known as the $G_2$ game, played on A is won by the first player. So far, it had only been proved for Büchi automata; we provide further evidence for it by proving it for coBüchi automata. We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is strictly more difficult than GFGness check, already for alternating automata on finite words.
△ Less
Submitted 17 February, 2020;
originally announced February 2020.
-
The Uniform Measure of Simple Regular Sets of Infinite Trees
Authors:
Marcin Przybyłko,
Michał Skrzypczak
Abstract:
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-deterministi…
▽ More
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.
△ Less
Submitted 30 January, 2020;
originally announced January 2020.
-
MSO+nabla is undecidable
Authors:
Mikołaj Bojańczyk,
Edon Kelmendi,
Michał Skrzypczak
Abstract:
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 π \in {0, 1}^w satisfies a formula φ(π)''. This logic was introduced by Michalewski and Mio; we call it MSO+nabla following notation of Shelah and Lehmann. The logic MSO+nabla subsumes many qualitative probabilistic formalisms, including qualitative proba…
▽ More
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 π \in {0, 1}^w satisfies a formula φ(π)''. This logic was introduced by Michalewski and Mio; we call it MSO+nabla following notation of Shelah and Lehmann. The logic MSO+nabla subsumes many qualitative probabilistic formalisms, including qualitative probabilistic CTL, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+nabla is true in the full binary tree.
△ Less
Submitted 29 April, 2019; v1 submitted 21 January, 2019;
originally announced January 2019.
-
Regular tree languages in low levels of the Wadge Hierarchy
Authors:
Mikołaj Bojańczyk,
Filippo Cavallari,
Thomas Place,
Michał Skrzypczak
Abstract:
In this article we provide effective characterisations of regular languages of infinite trees that belong to the low levels of the Wadge hierarchy. More precisely we prove decidability for each of the finite levels of the hierarchy; for the class of the Boolean combinations of open sets $BC(Σ_1^0)$ (i.e. the union of the first $ω$ levels); and for the Borel class $Δ_2^0$ (i.e. for the union of the…
▽ More
In this article we provide effective characterisations of regular languages of infinite trees that belong to the low levels of the Wadge hierarchy. More precisely we prove decidability for each of the finite levels of the hierarchy; for the class of the Boolean combinations of open sets $BC(Σ_1^0)$ (i.e. the union of the first $ω$ levels); and for the Borel class $Δ_2^0$ (i.e. for the union of the first $ω_1$ levels).
△ Less
Submitted 2 September, 2019; v1 submitted 6 June, 2018;
originally announced June 2018.
-
Unambiguous languages exhaust the index hierarchy
Authors:
Michał Skrzypczak
Abstract:
This work is a study of the expressive power of unambiguity in the case of automata over infinite trees. An automaton is called unambiguous if it has at most one accepting run on every input, the language of such an automaton is called an unambiguous language. It is known that not every regular language of infinite trees is unambiguous. Except that, very little is known about which regular tree la…
▽ More
This work is a study of the expressive power of unambiguity in the case of automata over infinite trees. An automaton is called unambiguous if it has at most one accepting run on every input, the language of such an automaton is called an unambiguous language. It is known that not every regular language of infinite trees is unambiguous. Except that, very little is known about which regular tree languages are unambiguous.
This paper answers the question whether unambiguous languages are of bounded complexity among all regular tree languages. The notion of complexity is the canonical one, called the (parity or Rabin-Mostowski) index hierarchy. The answer is negative, as exhibited by a family of examples of unambiguous languages that cannot be recognised by any alternating parity tree automata of bounded range of priorities.
Hardness of the given examples is based on the theory of signatures in parity games, previously studied by Walukiewicz. This theory is further developed here to construct canonical signatures. The technical core of the article is a parity game that compares signatures of a given pair of parity games (without an increase in the index).
△ Less
Submitted 20 April, 2018; v1 submitted 16 March, 2018;
originally announced March 2018.
-
How Deterministic are Good-For-Games Automata?
Authors:
Udi Boker,
Orna Kupferman,
Michał Skrzypczak
Abstract:
In GFG automata, it is possible to resolve nondeterminism in a way that only depends on the past and still accepts all the words in the language. The motivation for GFG automata comes from their adequacy for games and synthesis, wherein general nondeterminism is inappropriate. We continue the ongoing effort of studying the power of nondeterminism in GFG automata. Initial indications have hinted th…
▽ More
In GFG automata, it is possible to resolve nondeterminism in a way that only depends on the past and still accepts all the words in the language. The motivation for GFG automata comes from their adequacy for games and synthesis, wherein general nondeterminism is inappropriate. We continue the ongoing effort of studying the power of nondeterminism in GFG automata. Initial indications have hinted that every GFG automaton embodies a deterministic one. Today we know that this is not the case, and in fact GFG automata may be exponentially more succinct than deterministic ones.
We focus on the typeness question, namely the question of whether a GFG automaton with a certain acceptance condition has an equivalent GFG automaton with a weaker acceptance condition on the same structure. Beyond the theoretical interest in studying typeness, its existence implies efficient translations among different acceptance conditions. This practical issue is of special interest in the context of games, where the Buchi and co-Buchi conditions admit memoryless strategies for both players. Typeness is known to hold for deterministic automata and not to hold for general nondeterministic automata.
We show that GFG automata enjoy the benefits of typeness, similarly to the case of deterministic automata. In particular, when Rabin or Streett GFG automata have equivalent Buchi or co-Buchi GFG automata, respectively, then such equivalent automata can be defined on a substructure of the original automata. Using our typeness results, we further study the place of GFG automata in between deterministic and nondeterministic ones. Specifically, considering automata complementation, we show that GFG automata lean toward nondeterministic ones, admitting an exponential state blow-up in the complementation of a Streett automaton into a Rabin automaton, as opposed to the constant blow-up in the deterministic case.
△ Less
Submitted 11 October, 2017;
originally announced October 2017.
-
Trading Bounds for Memory in Games with Counters
Authors:
Nathanaël Fijalkow,
Florian Horn,
Denis Kuperberg,
Michał Skrzypczak
Abstract:
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,…
▽ More
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.
△ Less
Submitted 10 September, 2017;
originally announced September 2017.
-
Büchi VASS recognise w-languages that are Sigma^1_1 - complete
Authors:
Michał Skrzypczak
Abstract:
This short note exhibits an example of a Sigma^1_1-complete language that can be recognised by a one blind counter Büchi automaton (or equivalently a Büchi VASS with only one place).
This short note exhibits an example of a Sigma^1_1-complete language that can be recognised by a one blind counter Büchi automaton (or equivalently a Büchi VASS with only one place).
△ Less
Submitted 9 October, 2017; v1 submitted 31 August, 2017;
originally announced August 2017.
-
Monadic Second Order Logic with Measure and Category Quantifiers
Authors:
Matteo Mio,
Michał Skrzypczak,
Henryk Michalewski
Abstract:
We investigate the extension of Monadic Second Order logic, interpreted over infinite words and trees, with generalized "for almost all" quantifiers interpreted using the notions of Baire category and Lebesgue measure.
We investigate the extension of Monadic Second Order logic, interpreted over infinite words and trees, with generalized "for almost all" quantifiers interpreted using the notions of Baire category and Lebesgue measure.
△ Less
Submitted 9 April, 2018; v1 submitted 15 February, 2017;
originally announced February 2017.
-
The logical strength of Büchi's decidability theorem
Authors:
Leszek Kołodziejczyk,
Henryk Michalewski,
Cécilia Pradic,
Michał Skrzypczak
Abstract:
We study the strength of axioms needed to prove various results related to automata on infinite words and Büchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $RCA_0$:
(1) the induction scheme for $Σ^0_2$ formulae of arithmetic,
(2) a variant of Ramsey's Theorem for pairs restricted to so-…
▽ More
We study the strength of axioms needed to prove various results related to automata on infinite words and Büchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $RCA_0$:
(1) the induction scheme for $Σ^0_2$ formulae of arithmetic,
(2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings,
(3) Büchi's complementation theorem for nondeterministic automata on infinite words,
(4) the decidability of the depth-$n$ fragment of the MSO theory of $(N, {\le})$, for each $n \ge 5$.
Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem.
△ Less
Submitted 22 May, 2019; v1 submitted 26 August, 2016;
originally announced August 2016.
-
Index problems for game automata
Authors:
Alessandro Facchini,
Filip Murlak,
Michał Skrzypczak
Abstract:
For a given regular language of infinite trees, one can ask about the minimal number of priorities needed to recognize this language with a non-deterministic, alternating, or weak alternating parity automaton. These questions are known as, respectively, the non-deterministic, alternating, and weak Rabin-Mostowski index problems. Whether they can be answered effectively is a long-standing open prob…
▽ More
For a given regular language of infinite trees, one can ask about the minimal number of priorities needed to recognize this language with a non-deterministic, alternating, or weak alternating parity automaton. These questions are known as, respectively, the non-deterministic, 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 any more.
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.
△ Less
Submitted 31 May, 2016; v1 submitted 6 June, 2015;
originally announced June 2015.
-
On the Topological Complexity of omega-Languages of Non-Deterministic Petri Nets
Authors:
Olivier Finkel,
Michał Skrzypczak
Abstract:
We show that there are $Σ_3^0$-complete languages of infinite words accepted by non-deterministic Petri nets with Büchi acceptance condition, or equivalently by Büchi blind counter automata. This shows that omega-languages accepted by non-deterministic Petri nets are topologically more complex than those accepted by deterministic Petri nets.
We show that there are $Σ_3^0$-complete languages of infinite words accepted by non-deterministic Petri nets with Büchi acceptance condition, or equivalently by Büchi blind counter automata. This shows that omega-languages accepted by non-deterministic Petri nets are topologically more complex than those accepted by deterministic Petri nets.
△ Less
Submitted 27 January, 2014;
originally announced January 2014.
-
Unambiguous Buchi is weak
Authors:
Henryk Michalewski,
Michał Skrzypczak
Abstract:
A non-deterministic automaton running on infinite trees is unambiguous if it has at most one accepting run on every tree. The class of languages recognisable by unambiguous tree automata is still not well-understood. In particular, decidability of the problem whether a given language is recognisable by some unambiguous automaton is open. Moreover, there are no known upper bounds on the descriptive…
▽ More
A non-deterministic automaton running on infinite trees is unambiguous if it has at most one accepting run on every tree. The class of languages recognisable by unambiguous tree automata is still not well-understood. In particular, decidability of the problem whether a given language is recognisable by some unambiguous automaton is open. Moreover, there are no known upper bounds on the descriptive complexity of unambiguous languages among all regular tree languages.
In this paper we show the following complexity collapse: if a non-deterministic parity tree automaton $A$ is unambiguous and its priorities are between $i$ and $2n$ then the language recognised by $A$ is in the class $Comp(i+1,2n)$. A particular case of this theorem is for $i=n=1$: if $A$ is an unambiguous Buchi tree automaton then $L(A)$ is recognisable by a weak alternating automaton (or equivalently definable in weak MSO). The main motivation for this result is a theorem by Finkel and Simonnet stating that every unambiguous Buchi automaton recognises a Borel language.
The assumptions of the presented theorem are syntactic (we require one automaton to be both unambiguous and of particular parity index). However, to the authors' best knowledge this is the first theorem showing a collapse of the parity index that exploits the fact that a given automaton is unambiguous.
△ Less
Submitted 9 May, 2016; v1 submitted 16 January, 2014;
originally announced January 2014.
-
Separation Property for wB- and wS-regular Languages
Authors:
Michał Skrzypczak
Abstract:
In this paper we show that ωB- and ωS-regular languages satisfy the following separation-type theorem If L1,L2 are disjoint languages of ω-words both recognised by ωB- (resp. ωS)-automata then there exists an ω-regular language Lsep that contains L1, and whose complement contains L2. In particular, if a language and its complement are recognised by ωB- (resp. ωS)-automata then the language is ω-re…
▽ More
In this paper we show that ωB- and ωS-regular languages satisfy the following separation-type theorem If L1,L2 are disjoint languages of ω-words both recognised by ωB- (resp. ωS)-automata then there exists an ω-regular language Lsep that contains L1, and whose complement contains L2. In particular, if a language and its complement are recognised by ωB- (resp. ωS)-automata then the language is ω-regular. The result is especially interesting because, as shown by Bojańczyk and Colcombet, ωB-regular languages are complements of ω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 ω-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ńczyk.
△ Less
Submitted 10 February, 2014; v1 submitted 14 January, 2014;
originally announced January 2014.
-
Equational theories of profinite structures
Authors:
Michał Skrzypczak
Abstract:
In this paper we consider a general way of constructing profinite struc- tures based on a given framework - a countable family of objects and a countable family of recognisers (e.g. formulas). The main theorem states:
A subset of a family of recognisable sets is a lattice if and only if it is definable by a family of profinite equations.
This result extends Theorem 5.2 from [GGEP08] expressed…
▽ More
In this paper we consider a general way of constructing profinite struc- tures based on a given framework - a countable family of objects and a countable family of recognisers (e.g. formulas). The main theorem states:
A subset of a family of recognisable sets is a lattice if and only if it is definable by a family of profinite equations.
This result extends Theorem 5.2 from [GGEP08] expressed only for finite words and morphisms to finite monoids. One of the applications of our theorem is the situation where objects are finite relational structures and recognisers are first order sentences. In that setting a simple characterisation of lattices of first order formulas arise.
△ Less
Submitted 2 November, 2011;
originally announced November 2011.
