Searcharxiv⌕ Search

arXiv subjects

Michał Skrzypczak

Publications and source records attributed to Michał Skrzypczak.

26 records · Page 2Linked to original sources
arXiv2017

How Deterministic are Good-For-Games Automata?

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.

cs.FL↗
arXiv2017

Trading Bounds for Memory in Games with Counters

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.

cs.FL↗
arXiv2016

Index problems for game automata

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.

cs.FL↗
arXiv2016

Unambiguous Buchi is weak

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.

cs.FL↗
arXiv2014

Separation Property for wB- and wS-regular Languages

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.

cs.FL↗
arXiv2014

On the Topological Complexity of omega-Languages of Non-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.

cs.LO↗
arXiv2011

Equational theories of profinite structures

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.

cs.FL↗