11 Search Results for "Michalewski, Henryk"

Document
DOI: 10.4230/LIPIcs.STACS.2026.63
Generalised Quantifiers Based on Rabin-Mostowski Index

Authors: Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
In this work we introduce new generalised quantifiers which allow us to express the Rabin-Mostowski index of automata. Our main results study expressive power and decidability of the monadic second-order (MSO) logic extended with these quantifiers. We study these problems in the realm of both ω-words and infinite trees. As it turns out, the pictures in these two cases are very different. In the case of ω-words the new quantifiers can be effectively expressed in pure MSO logic. In contrast, in the case of infinite trees, addition of these quantifiers leads to an undecidable formalism. To realise index-quantifier elimination, we consider the extension of MSO by game quantifiers. As a tool, we provide a specific quantifier-elimination procedure for them. Moreover, we introduce a novel construction of transducers realising strategies in ω-regular games with monadic parameters.
Cite as

Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak. Generalised Quantifiers Based on Rabin-Mostowski Index. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 63:1-63:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.STACS.2026.63,
  author =	{Kuperberg, Denis and Niwi\'{n}ski, Damian and Parys, Pawe{\l} and Skrzypczak, Micha{\l}},
  title =	{{Generalised Quantifiers Based on Rabin-Mostowski Index}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{63:1--63:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.63},
  URN =		{urn:nbn:de:0030-drops-255526},
  doi =		{10.4230/LIPIcs.STACS.2026.63},
  annote =	{Keywords: monadic quantifiers, decidability, quantifier elimination, parity automata, game quantifier, Rabin-Mostowski index}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.15
Cyclic Proof Theory of Generalised Inductive Definitions

Authors: Gianluca Curzi and Lukas Melgaard

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We study cyclic proof systems for μPA, an extension of Peano arithmetic by generalised inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic Π^1_2-CA₀ by Möllerfeld. The main result of this paper is that cyclic and inductive μPA have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam’s systems for first-order μ-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within Π^1_2-CA₀, leveraging Möllerfeld’s conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem. As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and "plain" cyclic proofs for μPA prove the same theorems. This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson’s Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.
Cite as

Gianluca Curzi and Lukas Melgaard. Cyclic Proof Theory of Generalised Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{curzi_et_al:LIPIcs.CSL.2026.15,
  author =	{Curzi, Gianluca and Melgaard, Lukas},
  title =	{{Cyclic Proof Theory of Generalised Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.15},
  URN =		{urn:nbn:de:0030-drops-254399},
  doi =		{10.4230/LIPIcs.CSL.2026.15},
  annote =	{Keywords: cyclic proofs, positive inductive definitions, arithmetic, fixed points, proof theory, reset proof systems}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.24
Well-Founded Coalgebras Meet Kőnig’s Lemma

Authors: Henning Urbat and Thorsten Wißmann

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category ℂ, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ℂ and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space - in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.
Cite as

Henning Urbat and Thorsten Wißmann. Well-Founded Coalgebras Meet Kőnig’s Lemma. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.CSL.2026.24,
  author =	{Urbat, Henning and Wi{\ss}mann, Thorsten},
  title =	{{Well-Founded Coalgebras Meet K\H{o}nig’s Lemma}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.24},
  URN =		{urn:nbn:de:0030-drops-254485},
  doi =		{10.4230/LIPIcs.CSL.2026.24},
  annote =	{Keywords: K\H{o}nig’s Lemma, Well-Foundedness, Coalgebra}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.35
Chain of Grounded Objectives: Concise Goal-Oriented Prompting for Code Generation

Authors: Sangyeop Yeo, Seung-Won Hwang, and Yu-Seung Ma

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
The use of Large Language Models (LLMs) for code generation has gained significant attention in recent years. Existing methods often aim to improve the quality of generated code by incorporating additional contextual information or guidance into input prompts. Many of these approaches adopt process-oriented reasoning strategies, mimicking human-like step-by-step thinking; however, they may not always align with the structured nature of programming languages. This paper introduces Chain of Grounded Objectives (CGO), a concise goal-oriented prompting approach that embeds functional objectives into prompts to enhance code generation. By focusing on precisely defined objectives rather than explicit procedural steps, CGO aligns more naturally with programming tasks while retaining flexibility. Empirical evaluations on HumanEval, MBPP, their extended versions, and LiveCodeBench show that CGO achieves accuracy comparable to or better than existing methods while using fewer tokens, making it a more efficient approach to LLM-based code generation.
Cite as

Sangyeop Yeo, Seung-Won Hwang, and Yu-Seung Ma. Chain of Grounded Objectives: Concise Goal-Oriented Prompting for Code Generation. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 35:1-35:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yeo_et_al:LIPIcs.ECOOP.2025.35,
  author =	{Yeo, Sangyeop and Hwang, Seung-Won and Ma, Yu-Seung},
  title =	{{Chain of Grounded Objectives: Concise Goal-Oriented Prompting for Code Generation}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{35:1--35:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.35},
  URN =		{urn:nbn:de:0030-drops-233271},
  doi =		{10.4230/LIPIcs.ECOOP.2025.35},
  annote =	{Keywords: Artificial Intelligence, Natural Language Processing, Prompt Design, Large Language Models, Code Generation}
}
Document
Vision
DOI: 10.4230/TGDK.1.1.3
Knowledge Engineering Using Large Language Models

Authors: Bradley P. Allen, Lise Stork, and Paul Groth

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Knowledge engineering is a discipline that focuses on the creation and maintenance of processes that generate and apply knowledge. Traditionally, knowledge engineering approaches have focused on knowledge expressed in formal languages. The emergence of large language models and their capabilities to effectively work with natural language, in its broadest sense, raises questions about the foundations and practice of knowledge engineering. Here, we outline the potential role of LLMs in knowledge engineering, identifying two central directions: 1) creating hybrid neuro-symbolic knowledge systems; and 2) enabling knowledge engineering in natural language. Additionally, we formulate key open research questions to tackle these directions.
Cite as

Bradley P. Allen, Lise Stork, and Paul Groth. Knowledge Engineering Using Large Language Models. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{allen_et_al:TGDK.1.1.3,
  author =	{Allen, Bradley P. and Stork, Lise and Groth, Paul},
  title =	{{Knowledge Engineering Using Large Language Models}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{3:1--3:19},
  ISSN =	{2942-7517},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.3},
  URN =		{urn:nbn:de:0030-drops-194777},
  doi =		{10.4230/TGDK.1.1.3},
  annote =	{Keywords: knowledge engineering, large language models}
}
Document
Position
DOI: 10.4230/TGDK.1.1.2
Large Language Models and Knowledge Graphs: Opportunities and Challenges

Authors: Jeff Z. Pan, Simon Razniewski, Jan-Christoph Kalo, Sneha Singhania, Jiaoyan Chen, Stefan Dietze, Hajira Jabeen, Janna Omeliyanenko, Wen Zhang, Matteo Lissandrini, Russa Biswas, Gerard de Melo, Angela Bonifati, Edlira Vakaj, Mauro Dragoni, and Damien Graux

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Large Language Models (LLMs) have taken Knowledge Representation - and the world - by storm. This inflection point marks a shift from explicit knowledge representation to a renewed focus on the hybrid representation of both explicit knowledge and parametric knowledge. In this position paper, we will discuss some of the common debate points within the community on LLMs (parametric knowledge) and Knowledge Graphs (explicit knowledge) and speculate on opportunities and visions that the renewed focus brings, as well as related research topics and challenges.
Cite as

Jeff Z. Pan, Simon Razniewski, Jan-Christoph Kalo, Sneha Singhania, Jiaoyan Chen, Stefan Dietze, Hajira Jabeen, Janna Omeliyanenko, Wen Zhang, Matteo Lissandrini, Russa Biswas, Gerard de Melo, Angela Bonifati, Edlira Vakaj, Mauro Dragoni, and Damien Graux. Large Language Models and Knowledge Graphs: Opportunities and Challenges. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 2:1-2:38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{pan_et_al:TGDK.1.1.2,
  author =	{Pan, Jeff Z. and Razniewski, Simon and Kalo, Jan-Christoph and Singhania, Sneha and Chen, Jiaoyan and Dietze, Stefan and Jabeen, Hajira and Omeliyanenko, Janna and Zhang, Wen and Lissandrini, Matteo and Biswas, Russa and de Melo, Gerard and Bonifati, Angela and Vakaj, Edlira and Dragoni, Mauro and Graux, Damien},
  title =	{{Large Language Models and Knowledge Graphs: Opportunities and Challenges}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{2:1--2:38},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.2},
  URN =		{urn:nbn:de:0030-drops-194766},
  doi =		{10.4230/TGDK.1.1.2},
  annote =	{Keywords: Large Language Models, Pre-trained Language Models, Knowledge Graphs, Ontology, Retrieval Augmented Language Models}
}
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, Cécilia 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, Cécilia 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, C\'{e}cilia 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.FSTTCS.2015.489
On the Problem of Computing the Probability of Regular Sets of Trees

Authors: Henryk Michalewski and Matteo Mio

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We consider the problem of computing the probability of regular languages of infinite trees with respect to the natural coin-flipping measure. We propose an algorithm which computes the probability of languages recognizable by game automata. In particular this algorithm is applicable to all deterministic automata. We then use the algorithm to prove through examples three properties of measure: (1) there exist regular sets having irrational probability, (2) there exist comeager regular sets having probability 0 and (3) the probability of game languages W_{i,k}, from automata theory, is 0 if k is odd and is 1 otherwise.
Cite as

Henryk Michalewski and Matteo Mio. On the Problem of Computing the Probability of Regular Sets of Trees. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 489-502, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{michalewski_et_al:LIPIcs.FSTTCS.2015.489,
  author =	{Michalewski, Henryk and Mio, Matteo},
  title =	{{On the Problem of Computing the Probability of Regular Sets of Trees}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{489--502},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.489},
  URN =		{urn:nbn:de:0030-drops-56390},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.489},
  annote =	{Keywords: regular languages of trees, probability, meta-parity games}
}
Document
DOI: 10.4230/LIPIcs.STACS.2012.396
On the separation question for tree languages

Authors: André Arnold, Henryk Michalewski, and Damian Niwinski

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract
We show that the separation property fails for the classes Sigma_n of the Rabin-Mostowski index hierarchy of alternating automata on infinite trees. This extends our previous result (obtained with Szczepan Hummel) on the failure of the separation property for the class Sigma_2 (i.e., for co-Buchi sets). It remains open whether the separation property does hold for the classes Pi_n of the index hierarchy. To prove our result, we first consider the Rabin-Mostowski index hierarchy of deterministic automata on infinite words, for which we give a complete answer (generalizing previous results of Selivanov): the separation property holds for Pi_n and fails for Sigma_n-classes. The construction invented for words turns out to be useful for trees via a suitable game.
Cite as

André Arnold, Henryk Michalewski, and Damian Niwinski. On the separation question for tree languages. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 396-407, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{arnold_et_al:LIPIcs.STACS.2012.396,
  author =	{Arnold, Andr\'{e} and Michalewski, Henryk and Niwinski, Damian},
  title =	{{On the separation question for tree languages}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{396--407},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.396},
  URN =		{urn:nbn:de:0030-drops-34156},
  doi =		{10.4230/LIPIcs.STACS.2012.396},
  annote =	{Keywords: Alternating automata on infinite trees, Index hierarchy, Separation property}
}
Document
DOI: 10.4230/LIPIcs.STACS.2009.1849
On the Borel Inseparability of Game Tree Languages

Authors: Szczepan Hummel, Henryk Michalewski, and Damian Niwinski

Published in: LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

Abstract
The game tree languages can be viewed as an automata-theoretic counterpart of parity games on graphs. They witness the strictness of the index hierarchy of alternating tree automata, as well as the fixed-point hierarchy over binary trees. We consider a game tree language of the first non-trivial level, where Eve can force that 0 repeats from some moment on, and its dual, where Adam can force that 1 repeats from some moment on. Both these sets (which amount to one up to an obvious renaming) are complete in the class of co-analytic sets. We show that they cannot be separated by any Borel set, hence {\em a fortiori\/} by any weakly definable set of trees. This settles a case left open by L. Santocanale and A. Arnold, who have thoroughly investigated the separation property within the $\mu $-calculus and the automata index hierarchies. They showed that separability fails in general for non-deterministic automata of type $\Sigma^{\mu }_{n} $, starting from level $n=3$, while our result settles the missing case $n=2$.
Cite as

Szczepan Hummel, Henryk Michalewski, and Damian Niwinski. On the Borel Inseparability of Game Tree Languages. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 565-576, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{hummel_et_al:LIPIcs.STACS.2009.1849,
  author =	{Hummel, Szczepan and Michalewski, Henryk and Niwinski, Damian},
  title =	{{On the Borel Inseparability of Game Tree Languages}},
  booktitle =	{26th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{565--576},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-09-5},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{3},
  editor =	{Albers, Susanne and Marion, Jean-Yves},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1849},
  URN =		{urn:nbn:de:0030-drops-18493},
  doi =		{10.4230/LIPIcs.STACS.2009.1849},
  annote =	{Keywords: Tree automata, Separation property, Borel sets, Parity games}
}
  • Refine by Type
  • 11 Document/PDF
  • 6 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 1 2025
  • 2 2023
  • 1 2017
  • 1 2016
  • Show More...

  • Refine by Author
  • 5 Michalewski, Henryk
  • 2 Niwinski, Damian
  • 2 Skrzypczak, Michal
  • 1 Allen, Bradley P.
  • 1 Arnold, André
  • Show More...

  • Refine by Series/Journal
  • 9 LIPIcs
  • 2 TGDK

  • Refine by Classification
  • 2 Computing methodologies → Natural language processing
  • 1 Computing methodologies → Artificial intelligence
  • 1 Computing methodologies → Knowledge representation and reasoning
  • 1 Computing methodologies → Machine learning
  • 1 Computing methodologies → Philosophical/theoretical foundations of artificial intelligence
  • Show More...

  • Refine by Keyword
  • 2 Large Language Models
  • 2 Separation property
  • 1 Alternating automata on infinite trees
  • 1 Artificial Intelligence
  • 1 Borel sets
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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