# Mikolaj Bojanczyk - University of Warsaw

## Contact Details

NameMikolaj Bojanczyk |
||

AffiliationUniversity of Warsaw |
||

CityWarszawa |
||

CountryPoland |
||

## Pubs By Year |
||

## External Links |
||

## Pub CategoriesComputer Science - Logic in Computer Science (18) Mathematics - Logic (3) Computer Science - Data Structures and Algorithms (2) Computer Science - Discrete Mathematics (2) Mathematics - Category Theory (1) Computer Science - Computational Complexity (1) Computer Science - Computer Science and Game Theory (1) |

## Publications Authored By Mikolaj Bojanczyk

The following problem is shown undecidable: given regular languages L,K of finite trees, decide if there exists a deterministic tree-walking automaton which accepts all trees in L and rejects all trees in K. The proof uses a technique of Kopczy\'nski from LICS 2016. Read More

One of the major open problems in automata and logic is the following: is there an algorithm which inputs a regular tree language and decides if the language can be defined in first-order logic? The goal of this paper is to present this problem and similar ones using the language of universal algebra, highlighting potential connections to the structural theory of finite algebras, including Tame Congruence Theory. Read More

**Affiliations:**

^{1}LaBRI,

^{2}LaBRI,

^{3}LaBRI

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. Read More

The classic algorithm of Bodlaender and Kloks [J. Algorithms, 1996] 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. Read More

**Affiliations:**

^{1}University of Warsaw, Poland,

^{2}CNRS and ENS-Lyon, France,

^{3}University of Warsaw, Poland

Subzero automata is a class of tree automata whose acceptance condition can express probabilistic constraints. Our main result is that the problem of determining if a subzero automaton accepts some regular tree is decidable. Read More

We prove a conjecture of Courcelle, which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the following sense: constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. While the forward implication is a classic fact known as Courcelle's theorem, the converse direction remained open Read More

The principle behind algebraic language theory for various kinds of structures, such as words or trees, is to use a compositional function from the structures into a finite set. To talk about compositionality, one needs some way of composing structures into bigger structures. It so happens that category theory has an abstract concept for this, namely a monad. Read More

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. Read More

We prove a general decomposition theorem for the modal $\mu$-calculus $L_\mu$ in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e. Read More

This paper shows that over infinite trees, satisfiability is decidable for weak monadic second-order logic extended by the unbounding quantifier U and quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while emptiness for the automaton model is decided using profinite trees. Read More

**Affiliations:**

^{1}University of Warsaw,

^{2}University of Warsaw,

^{3}University of Warsaw

We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts. Read More

Call a string-to-string transducer regular if it can be realised by one of the following equivalent models: mso transductions, two-way deterministic automata with output, and streaming transducers with registers. This paper proposes to treat origin information as part of the semantics of a regular string-to-string transducer. With such semantics, the model admits a machine-independent characterisation, Angluin-style learning in polynomial time, as well as effective characterisations of natural subclasses such as one-way transducers or first-order definable transducers. Read More

We investigate finite deterministic automata in sets with non-homogeneous atoms: integers with successor. As there are uncount- ably many deterministic finite automata in this setting, we restrict our attention to automata with semilinear transition function. The main re- sults is a minimization procedure for semilinear automata. Read More

**Affiliations:**

^{1}University of Warsaw,

^{2}LaBRI,

^{3}Boston College

We use the recently developed theory of forest algebras to find algebraic characterizations of the languages of unranked trees and forests definable in various logics. These include the temporal logics CTL and EF, and first-order logic over the ancestor relation. While the characterizations are in general non-effective, we are able to use them to formulate necessary conditions for definability and provide new proofs that a number of languages are not definable in these logics. Read More

**Affiliations:**

^{1}University of Warsaw,

^{2}INRIA,

^{3}Boston college

**Category:**

This paper presents a decidable characterization of tree languages that can be defined by a boolean combination of Sigma_1 sentences. This is a tree extension of the Simon theorem, which says that a string language can be defined by a boolean combination of Sigma_1 sentences if and only if its syntactic monoid is J-trivial. Read More

We show that the problem `whether a finite set of regular-linear axioms defines a rigid theory' is undecidable. Read More

**Affiliations:**

^{1}University of Warsaw,

^{2}University of Warsaw

We define a new kind of automata recognizing properties of data words or data trees and prove that the automata capture all queries definable in Regular XPath. We show that the automata-theoretic approach may be applied to answer decidability and expressibility questions for XPath. Read More

The finite satisfiability problem for guarded fixpoint logic is decidable and complete for 2ExpTime (resp. ExpTime for formulas of bounded width). Read More

**Affiliations:**

^{1}Warsaw University,

^{2}INRIA

We study tree languages that can be defined in \Delta_2 . These are tree languages definable by a first-order formula whose quantifier prefix is forall exists, and simultaneously by a first-order formula whose quantifier prefix is . For the quantifier free part we consider two signatures, either the descendant relation alone or together with the lexicographical order relation on nodes. Read More

We consider a temporal logic EF+F^-1 for unranked, unordered finite trees. The logic has two operators: EF\phi, which says "in some proper descendant \phi holds", and F^-1\phi, which says "in some proper ancestor \phi holds". We present an algorithm for deciding if a regular language of unranked finite trees can be expressed in EF+F^-1. Read More

A new class of languages of infinite words is introduced, called the 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. Read More