17 Search Results for "Skrzypczak, Michał"

Document
DOI: 10.4230/DagRep.11.10.57
Unambiguity in Automata Theory (Dagstuhl Seminar 21452)

Authors: Thomas Colcombet, Karin Quaas, and Michał Skrzypczak

Published in: Dagstuhl Reports, Volume 11, Issue 10 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21452 "Unambiguity in Automata Theory". The aim of the seminar was to improve the understanding of the notion of unambiguity in automata theory, especially with respect to questions related to the expressive power, succinctness, and the tractability of unambiguous devices. The main motivation behind these studies is the hope that unambiguous machines can provide a golden balance between efficiency - sometimes not worse than for deterministic devices - and expressibility / succinctness, which often is similar to the general nondeterministic machines. These trade-offs become especially important in the models where the expressiveness or the decidability status of unambiguous machines is different from that of nondeterministic ones, as it is the case, e.g., for register automata.
Cite as

Thomas Colcombet, Karin Quaas, and Michał Skrzypczak. Unambiguity in Automata Theory (Dagstuhl Seminar 21452). In Dagstuhl Reports, Volume 11, Issue 10, pp. 57-71, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{colcombet_et_al:DagRep.11.10.57,
  author =	{Colcombet, Thomas and Quaas, Karin and Skrzypczak, Micha{\l}},
  title =	{{Unambiguity in Automata Theory (Dagstuhl Seminar 21452)}},
  pages =	{57--71},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{10},
  editor =	{Colcombet, Thomas and Quaas, Karin and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.10.57},
  URN =		{urn:nbn:de:0030-drops-159282},
  doi =		{10.4230/DagRep.11.10.57},
  annote =	{Keywords: Unambiguity in Automata Theory, Dagstuhl Seminar}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.81
On Guidable Index of Tree Automata

Authors: Damian Niwiński and Michał Skrzypczak

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We study guidable parity automata over infinite trees introduced by Colcombet and Löding, which form an expressively complete subclass of all non-deterministic tree automata. We show that, for any non-deterministic automaton, an equivalent guidable automaton with the smallest possible index can be effectively found. Moreover, if an input automaton is of a special kind, i.e. it is deterministic or game automaton then a guidable automaton with an optimal index can be deterministic (respectively game) automaton as well. Recall that the problem whether an equivalent non-deterministic automaton with the smallest possible index can be effectively found is open, and a positive answer is known only in the case when an input automaton is a deterministic, or more generally, a game automaton.
Cite as

Damian Niwiński and Michał Skrzypczak. On Guidable Index of Tree Automata. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 81:1-81:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{niwinski_et_al:LIPIcs.MFCS.2021.81,
  author =	{Niwi\'{n}ski, Damian and Skrzypczak, Micha{\l}},
  title =	{{On Guidable Index of Tree Automata}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{81:1--81:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.81},
  URN =		{urn:nbn:de:0030-drops-145214},
  doi =		{10.4230/LIPIcs.MFCS.2021.81},
  annote =	{Keywords: guidable automata, index problem, \omega-regular games}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.126
Deterministic and Game Separability for Regular Languages of Infinite Trees

Authors: Lorenzo Clemente and Michał Skrzypczak

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

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 our results by reducing to infinite duration games with ω-regular winning conditions and applying the finite-memory determinacy theorem of Büchi and Landweber.
Cite as

Lorenzo Clemente and Michał Skrzypczak. Deterministic and Game Separability for Regular Languages of Infinite Trees. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 126:1-126:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.ICALP.2021.126,
  author =	{Clemente, Lorenzo and Skrzypczak, Micha{\l}},
  title =	{{Deterministic and Game Separability for Regular Languages of Infinite Trees}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{126:1--126:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.126},
  URN =		{urn:nbn:de:0030-drops-141952},
  doi =		{10.4230/LIPIcs.ICALP.2021.126},
  annote =	{Keywords: separation, infinite trees, regular languages, deterministic automata, game automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.36
Degrees of Ambiguity for Parity Tree Automata

Authors: Alexander Rabinovich and Doron Tiferet

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is boundedly ambiguous if there is k ∈ ℕ, such that for every input it has at most k accepting computations. We consider Parity Tree Automata (PTA) and prove that the problem whether a PTA is not unambiguous (respectively, is not boundedly ambiguous, not finitely ambiguous) is co-NP complete, and the problem whether a PTA is not countably ambiguous is co-NP hard.
Cite as

Alexander Rabinovich and Doron Tiferet. Degrees of Ambiguity for Parity Tree Automata. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 36:1-36:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{rabinovich_et_al:LIPIcs.CSL.2021.36,
  author =	{Rabinovich, Alexander and Tiferet, Doron},
  title =	{{Degrees of Ambiguity for Parity Tree Automata}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.36},
  URN =		{urn:nbn:de:0030-drops-134709},
  doi =		{10.4230/LIPIcs.CSL.2021.36},
  annote =	{Keywords: automata on infinite trees, degree of ambiguity, omega word automata, parity automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.41
On the Succinctness of Alternating Parity Good-For-Games Automata

Authors: Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

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 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.
Cite as

Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On the Succinctness of Alternating Parity Good-For-Games Automata. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 41:1-41:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2020.41,
  author =	{Boker, Udi and Kuperberg, Denis and Lehtinen, Karoliina and Skrzypczak, Micha{\l}},
  title =	{{On the Succinctness of Alternating Parity Good-For-Games Automata}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{41:1--41:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.41},
  URN =		{urn:nbn:de:0030-drops-132825},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.41},
  annote =	{Keywords: Good for games, history-determinism, alternation}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.69
Regular Choice Functions and Uniformisations For countable Domains

Authors: Vincent Michielini and Michał Skrzypczak

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We view languages of words over a product alphabet A x B as relations between words over A and words over B. This leads to the notion of regular relations - relations given by a regular language. We ask when it is possible to find regular uniformisations of regular relations. The answer depends on the structure or shape of the underlying model: it is true e.g. for ω-words, while false for words over ℤ or for infinite trees. In this paper we focus on countable orders. Our main result characterises, which countable linear orders D have the property that every regular relation between words over D has a regular uniformisation. As it turns out, the only obstacle for uniformisability is the one displayed in the case of ℤ - non-trivial automorphisms of the given structure. Thus, we show that either all regular relations over D have regular uniformisations, or there is a non-trivial automorphism of D and even the simple relation of choice cannot be uniformised. Moreover, this dichotomy is effective.
Cite as

Vincent Michielini and Michał Skrzypczak. Regular Choice Functions and Uniformisations For countable Domains. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 69:1-69:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{michielini_et_al:LIPIcs.MFCS.2020.69,
  author =	{Michielini, Vincent and Skrzypczak, Micha{\l}},
  title =	{{Regular Choice Functions and Uniformisations For countable Domains}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{69:1--69:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.69},
  URN =		{urn:nbn:de:0030-drops-127386},
  doi =		{10.4230/LIPIcs.MFCS.2020.69},
  annote =	{Keywords: Uniformisation, Monadic Second-order logic, Countable words}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.80
Ambiguity Hierarchy of Regular Infinite Tree Languages

Authors: Alexander Rabinovich and Doron Tiferet

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is k-ambiguous (for k > 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if there is k ∈ ℕ, such that for every input it has at most k accepting computations. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous) automaton. Over finite words every regular language is accepted by a deterministic automaton. Over finite trees every regular language is accepted by an unambiguous automaton. Over ω-words every regular language is accepted by an unambiguous Büchi automaton [Arnold, 1983] and by a deterministic parity automaton. Over infinite trees there are ambiguous languages [Carayol et al., 2010]. We show that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages which are not k-1 ambiguous; there are finitely (respectively countably, uncountably) ambiguous languages which are not boundedly (respectively finitely, countably) ambiguous.
Cite as

Alexander Rabinovich and Doron Tiferet. Ambiguity Hierarchy of Regular Infinite Tree Languages. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 80:1-80:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{rabinovich_et_al:LIPIcs.MFCS.2020.80,
  author =	{Rabinovich, Alexander and Tiferet, Doron},
  title =	{{Ambiguity Hierarchy of Regular Infinite Tree Languages}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{80:1--80:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.80},
  URN =		{urn:nbn:de:0030-drops-127495},
  doi =		{10.4230/LIPIcs.MFCS.2020.80},
  annote =	{Keywords: automata on infinite trees, ambiguous automata, monadic second-order logic}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.136
Computing Measures of Weak-MSO Definable Sets of Trees

Authors: Damian Niwiński, Marcin Przybyłko, and Michał Skrzypczak

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
This 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 μ-calculus or in temporal logic CTL. Thus, the new algorithm may enhance the toolbox of probabilistic model checking.
Cite as

Damian Niwiński, Marcin Przybyłko, and Michał Skrzypczak. Computing Measures of Weak-MSO Definable Sets of Trees. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 136:1-136:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{niwinski_et_al:LIPIcs.ICALP.2020.136,
  author =	{Niwi\'{n}ski, Damian and Przyby{\l}ko, Marcin and Skrzypczak, Micha{\l}},
  title =	{{Computing Measures of Weak-MSO Definable Sets of Trees}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{136:1--136:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.136},
  URN =		{urn:nbn:de:0030-drops-125430},
  doi =		{10.4230/LIPIcs.ICALP.2020.136},
  annote =	{Keywords: infinite trees, weak alternating automata, coin-flipping measure}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.61
Uniformisation Gives the Full Strength of Regular Languages

Authors: Nathan Lhote, Vincent Michielini, and Michał Skrzypczak

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
Given R a binary relation between words (which we treat as a language over a product alphabet AxB), a uniformisation of it is another relation L included in R which chooses a single word over B, for each word over A whenever there exists one. It is known that MSO, the full class of regular languages, is strong enough to define a uniformisation for each of its relations. The quest of this work is to see which other formalisms, weaker than MSO, also have this property. In this paper, we solve this problem for pseudo-varieties of semigroups: we show that no nonempty pseudo-variety weaker than MSO can provide uniformisations for its relations.
Cite as

Nathan Lhote, Vincent Michielini, and Michał Skrzypczak. Uniformisation Gives the Full Strength of Regular Languages. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 61:1-61:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lhote_et_al:LIPIcs.MFCS.2019.61,
  author =	{Lhote, Nathan and Michielini, Vincent and Skrzypczak, Micha{\l}},
  title =	{{Uniformisation Gives the Full Strength of Regular Languages}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{61:1--61:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.61},
  URN =		{urn:nbn:de:0030-drops-110053},
  doi =		{10.4230/LIPIcs.MFCS.2019.61},
  annote =	{Keywords: pseudo-variety, finite word, semigroup, uniformisation, regular language}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.140
Unambiguous Languages Exhaust the Index Hierarchy

Authors: Michal Skrzypczak

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

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 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 the cannot be recognised by any alternating parity tree automata of bounded range of priorities. Hardness of the examples is based on the theory of signatures, previously studied by Walukiewicz. The technical core of the article is a definition of the canonical signatures together with a parity game that compares signatures of a given pair of parity games (of the same index).
Cite as

Michal Skrzypczak. Unambiguous Languages Exhaust the Index Hierarchy. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 140:1-140:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{skrzypczak:LIPIcs.ICALP.2018.140,
  author =	{Skrzypczak, Michal},
  title =	{{Unambiguous Languages Exhaust the Index Hierarchy}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{140:1--140:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.140},
  URN =		{urn:nbn:de:0030-drops-91442},
  doi =		{10.4230/LIPIcs.ICALP.2018.140},
  annote =	{Keywords: unambiguous automata, parity games, infinite trees, index hierarchy}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.18
How Deterministic are Good-For-Games Automata?

Authors: Udi Boker, Orna Kupferman, and Michal Skrzypczak

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
In good for games (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 Büchi and co-Büchi 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 Büchi or co-Büchi 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.
Cite as

Udi Boker, Orna Kupferman, and Michal Skrzypczak. How Deterministic are Good-For-Games Automata?. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 18:1-18:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2017.18,
  author =	{Boker, Udi and Kupferman, Orna and Skrzypczak, Michal},
  title =	{{How Deterministic are Good-For-Games Automata?}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{18:1--18:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.18},
  URN =		{urn:nbn:de:0030-drops-83776},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.18},
  annote =	{Keywords: finite automata on infinite words, determinism, good-for-games}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.56
A Characterisation of Pi^0_2 Regular Tree Languages

Authors: Filippo Cavallari, Henryk Michalewski, and Michal Skrzypczak

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We show an algorithm that for a given regular tree language L decides if L is in Pi^0_2, that is if L belongs to the second level of Borel Hierarchy. Moreover, if L is in Pi^0_2, then we construct a weak alternating automaton of index (0, 2) which recognises L. We also prove that for a given language L, L is recognisable by a weak alternating (1, 3)-automaton if and only if it is recognisable by a weak non-deterministic (1, 3)-automaton.
Cite as

Filippo Cavallari, Henryk Michalewski, and Michal Skrzypczak. A Characterisation of Pi^0_2 Regular Tree Languages. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 56:1-56:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cavallari_et_al:LIPIcs.MFCS.2017.56,
  author =	{Cavallari, Filippo and Michalewski, Henryk and Skrzypczak, Michal},
  title =	{{A Characterisation of Pi^0\underline2 Regular Tree Languages}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{56:1--56:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.56},
  URN =		{urn:nbn:de:0030-drops-80683},
  doi =		{10.4230/LIPIcs.MFCS.2017.56},
  annote =	{Keywords: infinite trees, Rabin-Mostowski hierarchy, regular languages}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.36
The Logical Strength of Büchi's Decidability Theorem

Authors: Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

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, less_or_equal). We prove that the following are equivalent over the weak second-order arithmetic theory RCA: 1. Büchi's complementation theorem for nondeterministic automata on infinite words, 2. the decidability of the depth-n fragment of the MSO theory of (N, less_or_equal), for each n greater than 5, 3. the induction scheme for Sigma^0_2 formulae of arithmetic. Moreover, each of (1)-(3) is equivalent to the additive version of Ramsey's Theorem for pairs, often used in proofs of (1); each of (1)-(3) implies McNaughton's determinisation theorem for automata on infinite words; and each of (1)-(3) implies the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem.
Cite as

Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. The Logical Strength of Büchi's Decidability Theorem. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 36:1-36:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kolodziejczyk_et_al:LIPIcs.CSL.2016.36,
  author =	{Kolodziejczyk, Leszek Aleksander and Michalewski, Henryk and Pradic, Pierre and Skrzypczak, Michal},
  title =	{{The Logical Strength of B\"{u}chi's Decidability Theorem}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{36:1--36:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.36},
  URN =		{urn:nbn:de:0030-drops-65765},
  doi =		{10.4230/LIPIcs.CSL.2016.36},
  annote =	{Keywords: nondeterministic automata, monadic second-order logic, B\"{u}chi's theorem, additive Ramsey's theorem, reverse mathematics}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.99
Deciding the Topological Complexity of Büchi Languages

Authors: Michal Skrzypczak and Igor Walukiewicz

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We study the topological complexity of languages of Büchi automata on infinite binary trees. We show that such a language is either Borel and WMSO-definable, or Sigma_1^1-complete and not WMSO-definable; moreover it can be algorithmically decided which of the two cases holds. The proof relies on a direct reduction to deciding the winner in a finite game with a regular winning condition.
Cite as

Michal Skrzypczak and Igor Walukiewicz. Deciding the Topological Complexity of Büchi Languages. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 99:1-99:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{skrzypczak_et_al:LIPIcs.ICALP.2016.99,
  author =	{Skrzypczak, Michal and Walukiewicz, Igor},
  title =	{{Deciding the Topological Complexity of B\"{u}chi Languages}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{99:1--99:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.99},
  URN =		{urn:nbn:de:0030-drops-62346},
  doi =		{10.4230/LIPIcs.ICALP.2016.99},
  annote =	{Keywords: tree automata, non-determinism, Borel sets, topological complexity, decidability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.78
On the Complexity of Branching Games with Regular Conditions

Authors: Marcin Przybylko and Michal Skrzypczak

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
Infinite duration games with regular conditions are one of the crucial tools in the areas of verification and synthesis. In this paper we consider a branching variant of such games - the game contains branching vertices that split the play into two independent sub-games. Thus, a play has the form of~an~infinite tree. The winner of the play is determined by a winning condition specified as a set of infinite trees. Games of this kind were used by Mio to provide a game semantics for the probabilistic mu-calculus. He used winning conditions defined in terms of parity games on trees. In this work we consider a more general class of winning conditions, namely those definable by finite automata on infinite trees. Our games can be seen as a branching-time variant of the stochastic games on graphs. We address the question of determinacy of a branching game and the problem of computing the optimal game value for each of the players. We consider both the stochastic and non-stochastic variants of the games. The questions under consideration are parametrised by the family of strategies we allow: either mixed, behavioural, or pure. We prove that in general, branching games are not determined under mixed strategies. This holds even for topologically simple winning conditions (differences of two open sets) and non-stochastic arenas. Nevertheless, we show that the games become determined under mixed strategies if we restrict the winning conditions to open sets of trees. We prove that the problem of comparing the game value to a rational threshold is undecidable for branching games with regular conditions in all non-trivial stochastic cases. In the non-stochastic cases we provide exact bounds on the complexity of the problem. The only case left open is the 0-player stochastic case, i.e. the problem of computing the measure of a given regular language of infinite trees.
Cite as

Marcin Przybylko and Michal Skrzypczak. On the Complexity of Branching Games with Regular Conditions. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 78:1-78:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{przybylko_et_al:LIPIcs.MFCS.2016.78,
  author =	{Przybylko, Marcin and Skrzypczak, Michal},
  title =	{{On the Complexity of Branching Games with Regular Conditions}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{78:1--78:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.78},
  URN =		{urn:nbn:de:0030-drops-64865},
  doi =		{10.4230/LIPIcs.MFCS.2016.78},
  annote =	{Keywords: stochastic games, meta-parity games, infinite trees, regular languages, parity automata}
}
  • Refine by Author
  • 8 Skrzypczak, Michał
  • 7 Skrzypczak, Michal
  • 2 Boker, Udi
  • 2 Michalewski, Henryk
  • 2 Michielini, Vincent
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Automata over infinite objects
  • 3 Theory of computation → Regular languages
  • 3 Theory of computation → Tree languages
  • 1 Mathematics of computing → Markov processes
  • 1 Theory of computation → Algebraic language theory
  • Show More...

  • Refine by Keyword
  • 7 infinite trees
  • 4 regular languages
  • 2 automata on infinite trees
  • 2 monadic second-order logic
  • 2 nondeterministic automata
  • Show More...

  • Refine by Type
  • 17 document

  • Refine by Publication Year
  • 4 2020
  • 3 2016
  • 3 2021
  • 2 2013
  • 2 2018
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact