Document

Invited Talk

**Published in:** LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

An introduction to orbit-finite sets, which are a type of sets that are infinite enough to describe interesting examples, and finite enough to have algorithms running on them. The notion of orbit-finiteness is illustrated on the example of register automata, an automaton model dealing with infinite alphabets.

Mikolaj Bojanczyk. Orbit-Finite Sets and Their Algorithms (Invited Talk). In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.ICALP.2017.1, author = {Bojanczyk, Mikolaj}, title = {{Orbit-Finite Sets and Their Algorithms}}, booktitle = {44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)}, pages = {1:1--1:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-041-5}, ISSN = {1868-8969}, year = {2017}, volume = {80}, editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.1}, URN = {urn:nbn:de:0030-drops-74295}, doi = {10.4230/LIPIcs.ICALP.2017.1}, annote = {Keywords: Orbit-finite sets, sets with atoms, data words, register automata} }

Document

**Published in:** LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of MSO, called TMSO+zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size
and the emptiness problem of nonzero automata is decidable, with complexity co-NP. These results imply that TMSO+zero has decidable satisfiability.

Mikolaj Bojanczyk, Hugo Gimbert, and Edon Kelmendi. Emptiness of Zero Automata Is Decidable. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 106:1-106:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2017.106, author = {Bojanczyk, Mikolaj and Gimbert, Hugo and Kelmendi, Edon}, title = {{Emptiness of Zero Automata Is Decidable}}, booktitle = {44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)}, pages = {106:1--106:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-041-5}, ISSN = {1868-8969}, year = {2017}, volume = {80}, editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.106}, URN = {urn:nbn:de:0030-drops-74745}, doi = {10.4230/LIPIcs.ICALP.2017.106}, annote = {Keywords: tree automata, probabilistic automata, monadic second-order logic} }

Document

**Published in:** LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

We study various models of transducers equipped with origin information. We consider the semantics of these models as particular graphs, called origin graphs, and we characterise the families of such graphs recognised by streaming string transducers.

Mikolaj Bojanczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle. Which Classes of Origin Graphs Are Generated by Transducers. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 114:1-114:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2017.114, author = {Bojanczyk, Mikolaj and Daviaud, Laure and Guillon, Bruno and Penelle, Vincent}, title = {{Which Classes of Origin Graphs Are Generated by Transducers}}, booktitle = {44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)}, pages = {114:1--114:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-041-5}, ISSN = {1868-8969}, year = {2017}, volume = {80}, editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.114}, URN = {urn:nbn:de:0030-drops-73984}, doi = {10.4230/LIPIcs.ICALP.2017.114}, annote = {Keywords: Streaming String Transducers, Origin Semantics, String-to-String Transductions, MSO Definability} }

Document

**Published in:** LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

The classic algorithm of Bodlaender and Kloks solves the following problem in linear fixed-parameter time: given a tree decomposition of a graph of (possibly suboptimal) width k, compute an optimum-width tree decomposition of the graph. In this work, we prove that this problem can also be solved in MSO in the following sense: for every positive integer k, there is an MSO transduction from tree decompositions of width k to tree decompositions of optimum width. Together with our recent results, this implies that for every k there exists an MSO transduction which inputs a graph of treewidth k, and nondeterministically outputs its tree decomposition of optimum width.

Mikolaj Bojanczyk and Michal Pilipczuk. Optimizing Tree Decompositions in MSO. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 15:1-15:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2017.15, author = {Bojanczyk, Mikolaj and Pilipczuk, Michal}, title = {{Optimizing Tree Decompositions in MSO}}, booktitle = {34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)}, pages = {15:1--15:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-028-6}, ISSN = {1868-8969}, year = {2017}, volume = {66}, editor = {Vollmer, Heribert and Vall\'{e}e, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.15}, URN = {urn:nbn:de:0030-drops-70173}, doi = {10.4230/LIPIcs.STACS.2017.15}, annote = {Keywords: tree decomposition, treewidth, transduction, monadic second-order logic} }

Document

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

This paper is about a variant of MSO on infinite trees where:
- there is a quantifier "zero probability of choosing a path pi in 2^{omega} which makes omega(pi) true";
- the monadic quantifiers range over sets with countable topological closure.
We introduce an automaton model, and show that it captures the logic.

Mikolaj Bojanczyk. Thin MSO with a Probabilistic Path Quantifier. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 96:1-96:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.ICALP.2016.96, author = {Bojanczyk, Mikolaj}, title = {{Thin MSO with a Probabilistic Path Quantifier}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {96:1--96: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.96}, URN = {urn:nbn:de:0030-drops-62315}, doi = {10.4230/LIPIcs.ICALP.2016.96}, annote = {Keywords: Automata, mso, infinite trees, probabilistic temporal logics} }

Document

Invited Talk

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

This is an overview of the invited talk delivered at the 41st International Symposium on Mathematical Foundations of Computer Science (MFCS-2016).

Mikolaj Bojanczyk. Decidable Extensions of MSO (Invited Talk). In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.MFCS.2016.2, author = {Bojanczyk, Mikolaj}, title = {{Decidable Extensions of MSO}}, booktitle = {41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)}, pages = {2:1--2:1}, 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.2}, URN = {urn:nbn:de:0030-drops-65089}, doi = {10.4230/LIPIcs.MFCS.2016.2}, annote = {Keywords: monadic second-order logic, extensions, decidability, automata} }

Document

**Published in:** LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.

Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U Theory of (N,<) Is Undecidable. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 21:1-21:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2016.21, author = {Bojanczyk, Mikolaj and Parys, Pawel and Torunczyk, Szymon}, title = {{The MSO+U Theory of (N,\langle) Is Undecidable}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {21:1--21:8}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.21}, URN = {urn:nbn:de:0030-drops-57223}, doi = {10.4230/LIPIcs.STACS.2016.21}, annote = {Keywords: automata, logic, unbounding quantifier, bounds, undecidability} }

Document

**Published in:** Dagstuhl Reports, Volume 5, Issue 9 (2016)

Over the years, there has been a lot of interplay between circuit complexity and logic. There are tight connections between small-depth circuit classes and fragments and extensions of firstorder logic, and ideas from games and finite model theory have provided powerful lower bound techniques for circuits. In recent years, there has been an impressive and sustained growth of interest and activity in the intersection of finite model theory and Boolean circuit complexity. The central aim of the seminar was to bring together researchers from these two areas to further strengthen the mutual
fertilisation. The seminar focussed on the following specific topics:
-The algebraic approach to circuit complexity with its applications to finite model theory
-The logic-circuit connection, with a particular emphasis on circuit lower bounds that trigger results in finite model theory like separations between logics
- New connections between uniformity conditions on circuit families and logical predicates
- Structural complexity and circuit lower bounds inherently using methods from logic and algebra Proof systems with low circuit complexity
- Dynamic complexity: understanding the dynamic expressive power of small depth circuit classes
The seminar had 43 participants from 11 countries and was very successful with respect to the exchange of recent results, ideas and methodological approaches.

Mikolaj Bojanczyk, Meena Mahajan, Thomas Schwentick, and Heribert Vollmer. Circuits, Logic and Games (Dagstuhl Seminar 15401). In Dagstuhl Reports, Volume 5, Issue 9, pp. 105-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{bojanczyk_et_al:DagRep.5.9.105, author = {Bojanczyk, Mikolaj and Mahajan, Meena and Schwentick, Thomas and Vollmer, Heribert}, title = {{Circuits, Logic and Games (Dagstuhl Seminar 15401)}}, pages = {105--124}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2016}, volume = {5}, number = {9}, editor = {Bojanczyk, Mikolaj and Mahajan, Meena and Schwentick, Thomas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.9.105}, URN = {urn:nbn:de:0030-drops-56872}, doi = {10.4230/DagRep.5.9.105}, annote = {Keywords: computational complexity theory, finite model theory, Boolean circuits, regular languages, finite monoids, Ehrenfeucht-Fraiss\'{e}-games} }

Document

**Published in:** Dagstuhl Reports, Volume 3, Issue 10 (2014)

This report documents the program and the outcomes of Dagstuhl Seminar 13422 "Nominal Computation Theory". The underlying theme of the seminar was nominal sets (also known as sets with atoms or Fraenkel-Mostowski sets) and they role and applications in three distinct research areas: automata over infinite alphabets, program semantics using nominal sets and nominal calculi of concurrent processes.

Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts. Nominal Computation Theory (Dagstuhl Seminar 13422). In Dagstuhl Reports, Volume 3, Issue 10, pp. 58-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{bojanczyk_et_al:DagRep.3.10.58, author = {Bojanczyk, Mikolaj and Klin, Bartek and Kurz, Alexander and Pitts, Andrew M.}, title = {{Nominal Computation Theory (Dagstuhl Seminar 13422)}}, pages = {58--71}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2014}, volume = {3}, number = {10}, editor = {Bojanczyk, Mikolaj and Klin, Bartek and Kurz, Alexander and Pitts, Andrew M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.10.58}, URN = {urn:nbn:de:0030-drops-44285}, doi = {10.4230/DagRep.3.10.58}, annote = {Keywords: nominal sets, Fraenkel-Mostowski sets} }

Document

**Published in:** LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)

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

Mikolaj Bojanczyk, Tomasz Idziaszek, and Michal Skrzypczak. Regular languages of thin trees. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 562-573, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2013.562, author = {Bojanczyk, Mikolaj and Idziaszek, Tomasz and Skrzypczak, Michal}, title = {{Regular languages of thin trees}}, booktitle = {30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)}, pages = {562--573}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-50-7}, ISSN = {1868-8969}, year = {2013}, volume = {20}, editor = {Portier, Natacha 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.2013.562}, URN = {urn:nbn:de:0030-drops-39655}, doi = {10.4230/LIPIcs.STACS.2013.562}, annote = {Keywords: infinite trees, regular languages, effective characterizations, topological complexity} }

Document

**Published in:** LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

We define an imperative programming language, which extends while programs with a type for storing atoms or hereditarily orbit-finite sets. To deal with an orbit-finite set, the language has a loop construction, which is executed in parallel for all elements of an orbit-finite set. We show examples of programs in this language, e.g. a program for minimising deterministic orbit-finite automata.

Mikolaj Bojanczyk and Szymon Torunczyk. Imperative Programming in Sets with Atoms. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 4-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2012.4, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Imperative Programming in Sets with Atoms}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)}, pages = {4--15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-47-7}, ISSN = {1868-8969}, year = {2012}, volume = {18}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.4}, URN = {urn:nbn:de:0030-drops-38437}, doi = {10.4230/LIPIcs.FSTTCS.2012.4}, annote = {Keywords: Nominal sets, sets with atoms, while programs} }

Document

**Published in:** LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

We study the satisfiability problem for XPath over XML documents of bounded depth. We define two parameters, called match width and braid width, that assign a number to any class of documents. We show that for all k, satisfiability for XPath restricted to bounded depth documents with match width at most k is decidable; and that XPath is undecidable on any class of documents with unbounded braid width. We conjecture that these two parameters are equivalent, in the sense that a class of documents has bounded match width iff it has bounded braid width.

Vince Bárány, Mikolaj Bojanczyk, Diego Figueira, and Pawel Parys. Decidable classes of documents for XPath. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 99-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{barany_et_al:LIPIcs.FSTTCS.2012.99, author = {B\'{a}r\'{a}ny, Vince and Bojanczyk, Mikolaj and Figueira, Diego and Parys, Pawel}, title = {{Decidable classes of documents for XPath}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)}, pages = {99--111}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-47-7}, ISSN = {1868-8969}, year = {2012}, volume = {18}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.99}, URN = {urn:nbn:de:0030-drops-38512}, doi = {10.4230/LIPIcs.FSTTCS.2012.99}, annote = {Keywords: XPath, XML, class automata, data trees, data words, satisfiability} }

Document

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

We prove that, over infinite trees, satisfiability is decidable for Weak Monadic Second-Order Logic extended by the unbounding quantifier U. We develop an automaton model, prove that it is effectively equivalent to the logic, and that the automaton model has decidable emptiness.

Mikolaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 648-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2012.648, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Weak MSO+U over infinite trees}}, booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)}, pages = {648--660}, 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.648}, URN = {urn:nbn:de:0030-drops-34279}, doi = {10.4230/LIPIcs.STACS.2012.648}, annote = {Keywords: Infinite trees, distance automata, MSO+U, profinite words} }

Document

**Published in:** LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

We develop an algebraic theory for languages of data words. We prove that, under certain conditions, a language of data words is definable in first-order logic if and only if its syntactic monoid is aperiodic.

Mikolaj Bojanczyk. Data Monoids. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 105-116, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.STACS.2011.105, author = {Bojanczyk, Mikolaj}, title = {{Data Monoids}}, booktitle = {28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)}, pages = {105--116}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-25-5}, ISSN = {1868-8969}, year = {2011}, volume = {9}, editor = {Schwentick, Thomas and D\"{u}rr, Christoph}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.105}, URN = {urn:nbn:de:0030-drops-30030}, doi = {10.4230/LIPIcs.STACS.2011.105}, annote = {Keywords: Monoid, Data Words, Nominal Set, First-Order Logic} }

Document

**Published in:** LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Data words and data trees appear in verification and XML processing. The term ``data'' means that positions of the word, or tree, are decorated with elements of an infinite set of data values, such as natural numbers or ASCII strings. This talk is a survey of the various automaton models that have been developed for data words and data trees.

Mikolaj Bojanczyk. Automata for Data Words and Data Trees. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.RTA.2010.1, author = {Bojanczyk, Mikolaj}, title = {{Automata for Data Words and Data Trees}}, booktitle = {Proceedings of the 21st International Conference on Rewriting Techniques and Applications}, pages = {1--4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-18-7}, ISSN = {1868-8969}, year = {2010}, volume = {6}, editor = {Lynch, Christopher}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.1}, URN = {urn:nbn:de:0030-drops-26397}, doi = {10.4230/LIPIcs.RTA.2010.1}, annote = {Keywords: Automata, Data Word, Data Tree} }

Document

**Published in:** LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

The paper presents some automata and logics on $\omega$-words, which capture all $\omega$-regular languages, and yet still have good closure and decidability properties.

Mikolaj Bojanczyk. Beyond omega-Regular Languages. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 11-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.STACS.2010.2440, author = {Bojanczyk, Mikolaj}, title = {{Beyond omega-Regular Languages}}, booktitle = {27th International Symposium on Theoretical Aspects of Computer Science}, pages = {11--16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-16-3}, ISSN = {1868-8969}, year = {2010}, volume = {5}, editor = {Marion, Jean-Yves and Schwentick, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2440}, URN = {urn:nbn:de:0030-drops-24409}, doi = {10.4230/LIPIcs.STACS.2010.2440}, annote = {Keywords: Automata, monadic second-order logic} }

Document

**Published in:** LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

We introduce a new class of automata on infinite words, called
min-automata. We prove that min-automata have the same expressive
power as weak monadic second-order logic (weak MSO) extended with a new
quantifier, the recurrence quantifier. These results are dual to a
framework presented in \cite{max-automata}, where max-automata were proved equivalent
to weak MSO extended with an unbounding
quantifier. We also present a general framework, which tries to
explain which types of automata on infinite words correspond to
extensions of weak MSO. As another example for the usefulness framework,
apart from min- and max-automata, we define an extension of weak MSO
with a quantifier that talks about ultimately periodic sets.

Mikolaj Bojanczyk and Szymon Torunczyk. Deterministic Automata and Extensions of Weak MSO. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 73-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2009.2308, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Deterministic Automata and Extensions of Weak MSO}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {73--84}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2308}, URN = {urn:nbn:de:0030-drops-23081}, doi = {10.4230/LIPIcs.FSTTCS.2009.2308}, annote = {Keywords: Deterministic automata, Weak MSO, min-automata, max-automata, BS-automata} }

Document

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

A new class of languages of infinite words is introduced, called the \emph{max-regular languages}, extending the class of $\omega$-regular languages. The class has two equivalent descriptions: in terms of automata (a type of deterministic counter automaton), and in terms of logic (weak monadic second-order logic with a bounding quantifier). Effective translations between the logic and automata are given.

Mikolaj Bojanczyk. Weak MSO with the Unbounding Quantifier. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 159-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.STACS.2009.1834, author = {Bojanczyk, Mikolaj}, title = {{Weak MSO with the Unbounding Quantifier}}, booktitle = {26th International Symposium on Theoretical Aspects of Computer Science}, pages = {159--170}, 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.1834}, URN = {urn:nbn:de:0030-drops-18345}, doi = {10.4230/LIPIcs.STACS.2009.1834}, annote = {Keywords: Automata, Monadic second-order logic} }