
$\omega$clones are multisorted structures that naturally emerge as algebras
for infinite trees, just as $\omega$semigroups are convenient algebras for
infinite words. In the algebraic theory of languages, one hopes that a language
is regular if and only if it is recognized by an algebra that is finite in some
simple sense. We show that, for infinite trees, the situation is not so simple:
there exists an $\omega$clone that is finite on every sort and finitely
generated, but recognizes a nonregular language.

We prove that for every positive integer $k$, there exists an
$\text{MSO}_1$transduction that given a graph of linear cliquewidth at most
$k$ outputs, nondeterministically, some clique decomposition of the graph of
width bounded by a function of $k$. A direct corollary of this result is the
equivalence of the notions of $\text{CMSO}_1$definability and recognizability
on graphs of bounded linear cliquewidth.

We define a new class of languages of $\omega$words, strictly extending
$\omega$regular languages.
One way to present this new class is by a type of regular expressions. The
new expressions are an extension of $\omega$regular expressions where two new
variants of the Kleene star $L^*$ are added: $L^B$ and $L^S$. These new
exponents are used to say that parts of the input word have bounded size, and
that parts of the input can have arbitrarily large sizes, respectively. For
instance, the expression $(a^Bb)^\omega$ represents the language of infinite
words over the letters $a,b$ where there is a common bound on the number of
consecutive letters $a$. The expression $(a^Sb)^\omega$ represents a similar
language, but this time the distance between consecutive $b$'s is required to
tend toward the infinite.
We develop a theory for these languages, with a focus on decidability and
closure. We define an equivalent automaton model, extending B\"uchi automata.
The main technical result is a complementation lemma that works for languages
where only one type of exponenteither $L^B$ or $L^S$is used.
We use the closure and decidability results to obtain partial decidability
results for the logic MSOLB, a logic obtained by extending monadic secondorder
logic with new quantifiers that speak about the size of sets.

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

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 firstorder 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.

The classic algorithm of Bodlaender and Kloks [J. Algorithms, 1996] solves
the following problem in linear fixedparameter time: given a tree
decomposition of a graph of (possibly suboptimal) width $k$, compute an
optimumwidth 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 [LICS
2016], 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. We also show that MSO transductions can be
implemented in linear fixedparameter time, which enables us to derive the
algorithmic result of Bodlaender and Kloks as a corollary of our main result.

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.

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:
constantwidth 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

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. The goal of this paper
is to propose monads as a unifying framework for discussing existing algebras
and designing new algebras.

We consider the logic MSO+U, which is monadic secondorder 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.

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.

This paper shows that over infinite trees, satisfiability is decidable for
weak monadic secondorder 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.

Call a stringtostring transducer regular if it can be realised by one of
the following equivalent models: mso transductions, twoway deterministic
automata with output, and streaming transducers with registers. This paper
proposes to treat origin information as part of the semantics of a regular
stringtostring transducer. With such semantics, the model admits a
machineindependent characterisation, Angluinstyle learning in polynomial
time, as well as effective characterisations of natural subclasses such as
oneway transducers or firstorder definable transducers.

We investigate finite deterministic automata in sets with nonhomogeneous
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. The proof is subtle and refers to decidability of
existential Presburger arithmetic with divisibility predicates. Interestingly,
the minimization is not obtained by the standard partition refinement
procedure, and we demonstrate that this procedure does not necessarily
terminate for semilinear automata.

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 Jtrivial.

We show that the problem `whether a finite set of regularlinear axioms
defines a rigid theory' is undecidable.

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 automatatheoretic approach may be applied to answer
decidability and expressibility questions for XPath.

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