Showing 1–47 of 47 results for author: Bojańczyk, M

Low rank MSO

Authors: Mikołaj Bojańczyk, Michał Pilipczuk, Wojciech Przybyszewski, Marek Sokołowski, Giannos Stamoulis

Abstract: We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. - Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separa… ▽ More We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. - Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs. - Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs. - Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Bojańczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time. △ Less

Submitted 12 February, 2025; originally announced February 2025.

Comments: 33 pages

Graphs of unbounded linear cliquewidth must transduce all trees

Authors: Mikołaj Bojanczyk, Pierre Ohlmann

Abstract: The Pathwidth Theorem states that if a class of graphs has unbounded pathwidth, then it contains all trees as graph minors. We prove a similar result for dense graphs: if a class of graphs has unbounded linear cliquewidth, then it can produce all trees via some fixed CMSO transduction. The Pathwidth Theorem states that if a class of graphs has unbounded pathwidth, then it contains all trees as graph minors. We prove a similar result for dense graphs: if a class of graphs has unbounded linear cliquewidth, then it can produce all trees via some fixed CMSO transduction. △ Less

Submitted 29 January, 2025; originally announced January 2025.

Function spaces for orbit-finite sets

Authors: Mikołaj Bojańczyk, Lê Thành Dũng Nguyên, Rafał Stefański

Abstract: Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they do not support function spaces, i.e. if X and Y are orbit-finite sets, then the space of finitely supported functions from X to Y is not orbit-finite. In this paper we propose two solutions to this problem: one is obtaine… ▽ More Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they do not support function spaces, i.e. if X and Y are orbit-finite sets, then the space of finitely supported functions from X to Y is not orbit-finite. In this paper we propose two solutions to this problem: one is obtained by generalising the notion of orbit-finite set, and the other one is obtained by restricting it. In both cases, function spaces and the original closure properties are retained. Curiously, both solutions are "linear": the generalisation is based on linear algebra, while the restriction is based on linear logic. △ Less

Submitted 8 April, 2024; originally announced April 2024.

Rank-decreasing transductions

Authors: Mikołaj Bojańczyk, Pierre Ohlmann

Abstract: We propose to study transformations on graphs, and more generally structures, by looking at how the cut-rank (as introduced by Oum) of subsets is affected when going from the input structure to the output structure. We consider transformations in which the underlying sets are the same for both the input and output, and so the cut-ranks of subsets can be easily compared. The purpose of this paper i… ▽ More We propose to study transformations on graphs, and more generally structures, by looking at how the cut-rank (as introduced by Oum) of subsets is affected when going from the input structure to the output structure. We consider transformations in which the underlying sets are the same for both the input and output, and so the cut-ranks of subsets can be easily compared. The purpose of this paper is to give a characterisation of logically defined transductions that is expressed in purely structural terms, without referring to logic: transformations which decrease the cut-rank, in the asymptotic sense, are exactly those that can be defined in monadic second-order logic. This characterisation assumes that the transduction has inputs of bounded treewidth; we also show that the characterisation fails in the absence of any assumptions. △ Less

Submitted 24 January, 2024; originally announced January 2024.

Comments: 22 pages, 13 figures

Polyregular functions on unordered trees of bounded height

Authors: Mikołaj Bojańczyk, Bartek Klin

Abstract: We consider injective first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a k-tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e. given two such interpretations, one can decide whether, for every i… ▽ More We consider injective first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a k-tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e. given two such interpretations, one can decide whether, for every input tree, the two output trees are isomorphic. We also give a calculus of typed functions and combinators which derives exactly injective first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, coproducts and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus. As an application, we show that the equivalence problem is decidable for first-order interpretations between classes of graphs that have bounded tree-depth. In all cases studied in this paper, first-order logic and MSO have the same expressive power, and hence all results apply also to MSO interpretations. △ Less

Submitted 7 November, 2023; originally announced November 2023.

Comments: Authors' version of a paper published at 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)

The category of MSO transductions

Authors: Mikołaj Bojańczyk

Abstract: MSO transductions are binary relations between structures which are defined using monadic second-order logic. MSO transductions form a category, since they are closed under composition. We show that many notions from language theory, such as recognizability or tree decompositions, can be defined in an abstract way that only refers to MSO transductions and their compositions. MSO transductions are binary relations between structures which are defined using monadic second-order logic. MSO transductions form a category, since they are closed under composition. We show that many notions from language theory, such as recognizability or tree decompositions, can be defined in an abstract way that only refers to MSO transductions and their compositions. △ Less

Submitted 29 May, 2023; originally announced May 2023.

Folding interpretations

Authors: Mikołaj Bojańczyk

Abstract: We study the polyregular string-to-string functions, which are certain functions of polynomial output size that can be described using automata and logic. We describe a system of combinators that generates exactly these functions. Unlike previous systems, the present system includes an iteration mechanism, namely fold. Although unrestricted fold can define all primitive recursive functions, we ide… ▽ More We study the polyregular string-to-string functions, which are certain functions of polynomial output size that can be described using automata and logic. We describe a system of combinators that generates exactly these functions. Unlike previous systems, the present system includes an iteration mechanism, namely fold. Although unrestricted fold can define all primitive recursive functions, we identify a type system (inspired by linear logic) that restricts fold so that it defines exactly the polyregular functions. We also present related systems, for quantifier-free functions as well as for linear regular functions on both strings and trees. △ Less

Submitted 26 April, 2023; v1 submitted 12 January, 2023; originally announced January 2023.

Comments: Author's version of a LICS 23 paper

On the growth rate of polyregular functions

Authors: Mikołaj Bojańczyk

Abstract: We consider polyregular functions, which are certain string-to-string functions that have polynomial output size. We prove that a polyregular function has output size $\mathcal O(n^k)$ if and only if it can be defined by an MSO interpretation of dimension $k$, i.e. a string-to-string transformation where every output position is interpreted, using monadic second-order logic MSO, in some $k$-tuple… ▽ More We consider polyregular functions, which are certain string-to-string functions that have polynomial output size. We prove that a polyregular function has output size $\mathcal O(n^k)$ if and only if it can be defined by an MSO interpretation of dimension $k$, i.e. a string-to-string transformation where every output position is interpreted, using monadic second-order logic MSO, in some $k$-tuple of input positions. We also show that this characterization does not extend to pebble transducers, another model for describing polyregular functions: we show that for every $k \in \{1,2,\ldots\}$ there is a polyregular function of quadratic output size which needs at least $k$ pebbles to be computed. △ Less

Submitted 26 April, 2023; v1 submitted 22 December, 2022; originally announced December 2022.

Comments: Author version of LICS 23 paper

Journal ref: Author version of a LICS 2023 paper

Monadic Monadic Second Order Logic

Authors: Mikołaj Bojańczyk, Bartek Klin, Julian Salamanca

Abstract: One of the main reasons for the correspondence of regular languages and monadic second-order logic is that the class of regular languages is closed under images of surjective letter-to-letter homomorphisms. This closure property holds for structures such as finite words, finite trees, infinite words, infinite trees, elements of the free group, etc. Such structures can be modelled using monads. In… ▽ More One of the main reasons for the correspondence of regular languages and monadic second-order logic is that the class of regular languages is closed under images of surjective letter-to-letter homomorphisms. This closure property holds for structures such as finite words, finite trees, infinite words, infinite trees, elements of the free group, etc. Such structures can be modelled using monads. In this paper, we study which structures (understood via monads in the category of sets) are such that the class of regular languages (i.e. languages recognized by finite algebras) are closed under direct images of surjective letter-to-letter homomorphisms. We provide diverse sufficient conditions for a monad to satisfy this property. We also present numerous examples of monads, including positive examples that do not satisfy our sufficient conditions, and counterexamples where the closure property fails. △ Less

Submitted 24 January, 2022; originally announced January 2022.

Separator logic and star-free expressions for graphs

Authors: Mikolaj Bojanczyk

Abstract: We describe two formalisms for defining graph languages, and prove that they are equivalent: 1. Separator logic. This is first-order logic on graphs which is allowed to use the edge relation, and for every $n \in \{0,1,\ldots \}$ a relation of arity $n+2$ which says that "vertex $s$ can be connected to vertex $t$ by a path that avoids vertices $v_1,\ldots,v_n$". 2. Star-free graph expressions.… ▽ More We describe two formalisms for defining graph languages, and prove that they are equivalent: 1. Separator logic. This is first-order logic on graphs which is allowed to use the edge relation, and for every $n \in \{0,1,\ldots \}$ a relation of arity $n+2$ which says that "vertex $s$ can be connected to vertex $t$ by a path that avoids vertices $v_1,\ldots,v_n$". 2. Star-free graph expressions. These are expressions that describe graphs with distinguished vertices called ports, and which are built from finite languages via Boolean combinations and the operations on graphs with ports used to construct tree decompositions. Furthermore, we prove a variant of Schützenberger's theorem (about star-free languages being those recognized by a periodic monoids) for graphs of bounded pathwidth. A corollary is that, given $k$ and a graph language represented by an \mso formula, one can decide if the language can be defined in either of two equivalent formalisms on graphs of pathwidth at most $k$. △ Less

Submitted 2 September, 2021; v1 submitted 29 July, 2021; originally announced July 2021.

Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata

Authors: Mikołaj Bojańczyk, Joanna Fijalkow, Bartek Klin, Joshua Moerman

Abstract: We develop a theory of vector spaces spanned by orbit-finite sets. Using this theory, we give a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with… ▽ More We develop a theory of vector spaces spanned by orbit-finite sets. Using this theory, we give a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with the same complexity, language equivalence for unambiguous register automata, which improves previous results in three ways: (a) we allow for order comparisons on atoms, and not just equality; (b) the complexity is exponentially better; and (c) we allow automata with guessing. △ Less

Submitted 3 May, 2024; v1 submitted 6 April, 2021; originally announced April 2021.

Comments: Journal Version for TheoretiCS

ACM Class: F.1.1; F.4.3

Journal ref: TheoretiCS, Volume 3 (May 6, 2024) theoretics:11208

Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic

Authors: Mikołaj Bojańczyk

Abstract: These are lecture notes on the algebraic approach to regular languages. The classical algebraic approach is for finite words; it uses semigroups instead of automata. However, the algebraic approach can be extended to structures beyond words, e.g.~infinite words, or trees or graphs. The purpose of this book is to describe the algebraic approach in a way that covers these extensions. These are lecture notes on the algebraic approach to regular languages. The classical algebraic approach is for finite words; it uses semigroups instead of automata. However, the algebraic approach can be extended to structures beyond words, e.g.~infinite words, or trees or graphs. The purpose of this book is to describe the algebraic approach in a way that covers these extensions. △ Less

Submitted 26 August, 2020; originally announced August 2020.

Comments: The most recent version can be found here: https://www.mimuw.edu.pl/~bojan/2019-2020/algebraic-language-theory-2020

Extensions of $ω$-Regular Languages

Authors: Mikołaj Bojańczyk, Edon Kelmendi, Rafał Stefański, Georg Zetzsche

Abstract: We consider extensions of monadic second order logic over $ω$-words, which are obtained by adding one language that is not $ω$-regular. We show that if the added language $L$ has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the $ω$-regular languages are the only decidable Boolean-closed full trio over $ω$-words. We consider extensions of monadic second order logic over $ω$-words, which are obtained by adding one language that is not $ω$-regular. We show that if the added language $L$ has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the $ω$-regular languages are the only decidable Boolean-closed full trio over $ω$-words. △ Less

Submitted 21 February, 2020; originally announced February 2020.

First-order tree-to-tree functions

Authors: Mikołaj Bojańczyk, Amina Doumane

Abstract: We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition. We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition. △ Less

Submitted 30 January, 2023; v1 submitted 21 February, 2020; originally announced February 2020.

Comments: This version contains an erratum. Theorem 6.1 in the published version was not valid in its full generality

Single use register automata for data words

Authors: Mikołaj Bojańczyk, Rafał Stefański

Abstract: Our starting point are register automata for data words, in the style of Kaminski and Francez. We study the effects of the single-use restriction, which says that a register is emptied immediately after being used. We show that under the single-use restriction, the theory of automata for data words becomes much more robust. The main results are: (a) five different machine models are equivalent as… ▽ More Our starting point are register automata for data words, in the style of Kaminski and Francez. We study the effects of the single-use restriction, which says that a register is emptied immediately after being used. We show that under the single-use restriction, the theory of automata for data words becomes much more robust. The main results are: (a) five different machine models are equivalent as language acceptors, including one-way and two-way single-use register automata; (b) one can recover some of the algebraic theory of languages over finite alphabets, including a version of the Krohn-Rhodes Theorem; (c) there is also a robust theory of transducers, with four equivalent models, including two-way single use transducers and a variant of streaming string transducers for data words. These results are in contrast with automata for data words without the single-use restriction, where essentially all models are pairwise non-equivalent. △ Less

Submitted 7 May, 2020; v1 submitted 24 July, 2019; originally announced July 2019.

Comments: 59 pages

ACM Class: F.1.1; F.4.3

String-to-String Interpretations with Polynomial-Size Output

Authors: Mikołaj Bojańczyk, Sandra Kiefer, Nathan Lhote

Abstract: String-to-string MSO interpretations are like Courcelle's MSO transductions, except that a single output position can be represented using a tuple of input positions instead of just a single input position. In particular, the output length is polynomial in the input length, as opposed to MSO transductions, which have output of linear length. We show that string-to-string MSO interpretations are ex… ▽ More String-to-string MSO interpretations are like Courcelle's MSO transductions, except that a single output position can be represented using a tuple of input positions instead of just a single input position. In particular, the output length is polynomial in the input length, as opposed to MSO transductions, which have output of linear length. We show that string-to-string MSO interpretations are exactly the polyregular functions. The latter class has various characterizations, one of which is that it consists of the string-to-string functions recognized by pebble transducers. Our main result implies the surprising fact that string-to-string MSO interpretations are closed under composition. △ Less

Submitted 30 May, 2019; originally announced May 2019.

Comments: 35 pages, full version of a paper accepted for the 46th International Colloquium on Automata, Languages and Programming (ICALP 2019)

MSO+nabla is undecidable

Authors: Mikołaj Bojańczyk, Edon Kelmendi, Michał Skrzypczak

Abstract: This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying ``almost surely a branch π \in {0, 1}^w satisfies a formula φ(π)''. This logic was introduced by Michalewski and Mio; we call it MSO+nabla following notation of Shelah and Lehmann. The logic MSO+nabla subsumes many qualitative probabilistic formalisms, including qualitative proba… ▽ More This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying ``almost surely a branch π \in {0, 1}^w satisfies a formula φ(π)''. This logic was introduced by Michalewski and Mio; we call it MSO+nabla following notation of Shelah and Lehmann. The logic MSO+nabla subsumes many qualitative probabilistic formalisms, including qualitative probabilistic CTL, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+nabla is true in the full binary tree. △ Less

Submitted 29 April, 2019; v1 submitted 21 January, 2019; originally announced January 2019.

Comments: Accepted to LICS 2019

Polyregular Functions

Authors: Mikołaj Bojańczyk

Abstract: This paper is about certain string-to-string functions, called the polyregular functions. These are like the regular string-to-string functions, except that they can have polynomial (and not just linear) growth. The class has four equivalent definitions: 1. deterministic two-way transducers with pebbles; 2 the smallest class of string-to-string functions that is closed under composition, contains… ▽ More This paper is about certain string-to-string functions, called the polyregular functions. These are like the regular string-to-string functions, except that they can have polynomial (and not just linear) growth. The class has four equivalent definitions: 1. deterministic two-way transducers with pebbles; 2 the smallest class of string-to-string functions that is closed under composition, contains all sequential functions as well as two extra functions called squaring and iterated reverse 3. a fragment of the lambda-calculus, which has a list type constructor and limited forms of iteration such as map but not fold; 4. an imperative programming language, which has for loops that range over input positions. The first definition comes from [milo2003typechecking], while the remaining three are new to the author's best knowledge. The class of polyregular functions contains known classes of string-to-string transducers, such as the sequential, rational, or regular ones, but goes beyond them because of super-linear growth. Polyregular functions have good algorithmic properties, such as: - the output can be computed in linear time (in terms of combined input and output size); - the inverse image of a regular word language is (effectively) regular. We also identify a fragment of polyregular functions, called the first-order polyregular functions, which has additional good properties, e.g. the output can be computed by an AC0 circuit. △ Less

Submitted 20 October, 2018; originally announced October 2018.

Comments: 95 pages

Undecidability of a weak version of MSO+U

Authors: Mikołaj Bojańczyk, Laure Daviaud, Bruno Guillon, Vincent Penelle, A. V. Sreejith

Abstract: We prove the undecidability of MSO on $ω$-words extended with the second-order predicate $U_1(X)$ which says that the distance between consecutive positions in a set $X \subseteq \mathbb{N}$ is unbounded. This is achieved by showing that adding $U_1$ to MSO gives a logic with the same expressive power as $MSO+U$, a logic on $ω$-words with undecidable satisfiability. As a corollary, we prove that M… ▽ More We prove the undecidability of MSO on $ω$-words extended with the second-order predicate $U_1(X)$ which says that the distance between consecutive positions in a set $X \subseteq \mathbb{N}$ is unbounded. This is achieved by showing that adding $U_1$ to MSO gives a logic with the same expressive power as $MSO+U$, a logic on $ω$-words with undecidable satisfiability. As a corollary, we prove that MSO on $ω$-words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e., sets $X$ such that for some positive integer $p$, ultimately either both or none of positions $x$ and $x+p$ belong to $X$. △ Less

Submitted 10 February, 2020; v1 submitted 23 July, 2018; originally announced July 2018.

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 1 (February 11, 2020) lmcs:5059

Regular tree languages in low levels of the Wadge Hierarchy

Authors: Mikołaj Bojańczyk, Filippo Cavallari, Thomas Place, Michał Skrzypczak

Abstract: In this article we provide effective characterisations of regular languages of infinite trees that belong to the low levels of the Wadge hierarchy. More precisely we prove decidability for each of the finite levels of the hierarchy; for the class of the Boolean combinations of open sets $BC(Σ_1^0)$ (i.e. the union of the first $ω$ levels); and for the Borel class $Δ_2^0$ (i.e. for the union of the… ▽ More In this article we provide effective characterisations of regular languages of infinite trees that belong to the low levels of the Wadge hierarchy. More precisely we prove decidability for each of the finite levels of the hierarchy; for the class of the Boolean combinations of open sets $BC(Σ_1^0)$ (i.e. the union of the first $ω$ levels); and for the Borel class $Δ_2^0$ (i.e. for the union of the first $ω_1$ levels). △ Less

Submitted 2 September, 2019; v1 submitted 6 June, 2018; originally announced June 2018.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (September 4, 2019) lmcs:4647

Two monads for graphs

Authors: Mikolaj Bojanczyk

Abstract: An introduction to algebras for graphs, based on Courcelle's algebras of hyperedge replacement and vertex replacement. The paper uses monad notation. An introduction to algebras for graphs, based on Courcelle's algebras of hyperedge replacement and vertex replacement. The paper uses monad notation. △ Less

Submitted 25 April, 2018; originally announced April 2018.

A non-regular language of infinite trees that is recognizable by a sort-wise finite algebra

Authors: Mikołaj Bojańczyk, Bartek Klin

Abstract: $ω$-clones are multi-sorted structures that naturally emerge as algebras for infinite trees, just as $ω… ▽ More $ω$-clones are multi-sorted structures that naturally emerge as algebras for infinite trees, just as $ω$-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 $ω$-clone that is finite on every sort and finitely generated, but recognizes a non-regular language. △ Less

Submitted 26 November, 2019; v1 submitted 18 April, 2018; originally announced April 2018.

MSC Class: F.4.3 ACM Class: F.4.3

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 4 (November 29, 2019) lmcs:4447

Regular and First Order List Functions

Authors: Mikolaj Bojanczyk, Laure Daviaud, Krishna Shankara Narayanan

Abstract: We define two classes of functions, called regular (respectively, first-order) list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of regular expressions: the functions are constructed by starting with some basic functions (e.g. projections from pairs, or head and tail operations on lists) and putting… ▽ More We define two classes of functions, called regular (respectively, first-order) list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of regular expressions: the functions are constructed by starting with some basic functions (e.g. projections from pairs, or head and tail operations on lists) and putting them together using four combinators (most importantly, composition of functions). Our main results are that first-order list functions are exactly the same as first-order transductions, under a suitable encoding of the inputs; and the regular list functions are exactly the same as MSO-transductions. △ Less

Submitted 16 March, 2018; originally announced March 2018.

Definable decompositions for graphs of bounded linear cliquewidth

Authors: Mikołaj Bojańczyk, Martin Grohe, Michał Pilipczuk

Abstract: We prove that for every positive integer k, there exists an MSO_1-transduction that given a graph of linear cliquewidth at most k outputs, nondeterministically, some cliquewidth 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 CMSO_1-definability and recognizability on graphs of bounded linear cliquewidth. We prove that for every positive integer k, there exists an MSO_1-transduction that given a graph of linear cliquewidth at most k outputs, nondeterministically, some cliquewidth 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 CMSO_1-definability and recognizability on graphs of bounded linear cliquewidth. △ Less

Submitted 21 January, 2021; v1 submitted 15 March, 2018; originally announced March 2018.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 1 (January 25, 2021) lmcs:5295

Boundedness in languages of infinite words

Authors: Mikołaj Bojańczyk, Thomas Colcombet

Abstract: We define a new class of languages of $ω$-words, strictly extending $ω$-regular languages. One way to present this new class is by a type of regular expressions. The new expressions are an extension of $ω$-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 par… ▽ More We define a new class of languages of $ω$-words, strictly extending $ω$-regular languages. One way to present this new class is by a type of regular expressions. The new expressions are an extension of $ω$-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)^ω$ 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)^ω$ 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üchi automata. The main technical result is a complementation lemma that works for languages where only one type of exponent---either $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 second-order logic with new quantifiers that speak about the size of sets. △ Less

Submitted 25 October, 2017; v1 submitted 31 August, 2017; originally announced August 2017.

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 4 (October 26, 2017) lmcs:3916

Star Height via Games

Authors: Mikolaj Bojanczyk

Abstract: This paper proposes a new algorithm deciding the star height problem. As shown by Kirsten, the star height problem reduces to a problem concerning automata with counters, called limitedness. The new contribution is a different algorithm for the limitedness problem, which reduces it to solving a Gale-Stewart game with an ω-regular winning condition. This paper proposes a new algorithm deciding the star height problem. As shown by Kirsten, the star height problem reduces to a problem concerning automata with counters, called limitedness. The new contribution is a different algorithm for the limitedness problem, which reduces it to solving a Gale-Stewart game with an ω-regular winning condition. △ Less

Submitted 11 August, 2017; originally announced August 2017.

It is undecidable if two regular tree languages can be separated by a deterministic tree-walking automaton

Authors: Mikołaj Bojańczyk

Abstract: 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ński from LICS 2016. 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ński from LICS 2016. △ Less

Submitted 20 March, 2017; v1 submitted 15 March, 2017; originally announced March 2017.

Some connections between universal algebra and logics for trees

Authors: Mikołaj Bojańczyk, Henryk Michalewski

Abstract: 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 Co… ▽ 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. △ Less

Submitted 14 March, 2017; originally announced March 2017.

Emptiness of zero automata is decidable

Authors: Mikolaj Bojańczyk, Hugo Gimbert, Edon Kelmendi

Abstract: 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 pro… ▽ More 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 and both in NP and in coNP. These results imply that tmso + zero has decidable satisfiability. △ Less

Submitted 28 March, 2017; v1 submitted 22 February, 2017; originally announced February 2017.

Optimizing tree decompositions in MSO

Authors: Mikołaj Bojańczyk, Michał Pilipczuk

Abstract: 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 tran… ▽ 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. 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 fixed-parameter time, which enables us to derive the algorithmic result of Bodlaender and Kloks as a corollary of our main result. △ Less

Submitted 2 February, 2022; v1 submitted 24 January, 2017; originally announced January 2017.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (February 3, 2022) lmcs:6993

On the Regular Emptiness Problem of Subzero Automata

Authors: Henryk Michalewski, Matteo Mio, Mikołaj Bojańczyk

Abstract: 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. 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. △ Less

Submitted 10 August, 2016; originally announced August 2016.

Comments: In Proceedings ICE 2016, arXiv:1608.03131

Journal ref: EPTCS 223, 2016, pp. 1-23

Definability equals recognizability for graphs of bounded treewidth

Authors: Mikołaj Bojańczyk, Michał Pilipczuk

Abstract: 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, th… ▽ 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 △ Less

Submitted 10 May, 2016; originally announced May 2016.

Comments: 21 pages, an extended abstract will appear in the proceedings of LICS 2016

Recognisable languages over monads

Authors: Mikołaj Bojańczyk

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

Submitted 17 February, 2015; originally announced February 2015.

The MSO+U theory of (N, <) is undecidable

Authors: Mikołaj Bojańczyk, Paweł Parys, Szymon Toruńczyk

Abstract: 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 undec… ▽ 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.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. △ Less

Submitted 17 February, 2015; v1 submitted 16 February, 2015; originally announced February 2015.

Comments: 9 pages, with 2 figures

Decomposition Theorems and Model-Checking for the Modal $μ$-Calculus

Authors: Mikolaj Bojanczyk, Christoph Dittmann, Stephan Kreutzer

Abstract: We prove a general decomposition theorem for the modal $μ$-calculus $L_μ$ in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e., transition system) is composed of two substructures $M_1$ and $M_2$ plus edges from $M_1$ to $M_2$, then the formulas true at a node in $M$ only depend on the formulas true in the respective substructures in… ▽ More We prove a general decomposition theorem for the modal $μ$-calculus $L_μ$ in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e., transition system) is composed of two substructures $M_1$ and $M_2$ plus edges from $M_1$ to $M_2$, then the formulas true at a node in $M$ only depend on the formulas true in the respective substructures in a sense made precise below. As a consequence we show that the model-checking problem for $L_μ$ is fixed-parameter tractable (fpt) on classes of structures of bounded Kelly-width or bounded DAG-width. As far as we are aware, these are the first fpt results for $L_μ$ which do not follow from embedding into monadic second-order logic. △ Less

Submitted 9 May, 2014; originally announced May 2014.

ACM Class: F.4.1

Weak MSO+U with Path Quantifiers over Infinite Trees

Authors: Mikołaj Bojańczyk

Abstract: 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. 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. △ Less

Submitted 29 April, 2014; originally announced April 2014.

Comments: version of an ICALP 2014 paper with appendices

Automata theory in nominal sets

Authors: Mikołaj Bojańczyk, Bartek Klin, Sławomir Lasota

Abstract: 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. 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. △ Less

Submitted 14 August, 2014; v1 submitted 4 February, 2014; originally announced February 2014.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 3 (August 15, 2014) lmcs:1157

Transducers with origin information

Authors: Mikołaj Bojańczyk

Abstract: 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 characterisa… ▽ 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. △ Less

Submitted 24 September, 2013; originally announced September 2013.

Minimization of semilinear automata

Authors: Mikołaj Bojańczyk, Sławomir Lasota

Abstract: 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. The proof is subtle and refers to decidability of existential Presbu… ▽ 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. 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. △ Less

Submitted 17 October, 2012; originally announced October 2012.

Wreath Products of Forest Algebras, with Applications to Tree Logics

Authors: Mikolaj Bojanczyk, Igor Walukiewicz, Howard Straubing

Abstract: 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 an… ▽ More 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. △ Less

Submitted 16 September, 2012; v1 submitted 30 August, 2012; originally announced August 2012.

ACM Class: F.4.3

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (September 19, 2012) lmcs:1215

Piecewise testable tree languages

Authors: Mikołaj Bojańczyk, Luc Segoufin, Howard Straubing

Abstract: 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. 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. △ Less

Submitted 28 September, 2012; v1 submitted 25 August, 2012; originally announced August 2012.

ACM Class: F.4.3,F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (September 29, 2012) lmcs:1216

Rigidity is undecidable

Authors: Mikołaj Bojanczyk, Stanisław Szawiel, Marek Zawadowski

Abstract: We show that the problem `whether a finite set of regular-linear axioms defines a rigid theory' is undecidable. We show that the problem `whether a finite set of regular-linear axioms defines a rigid theory' is undecidable. △ Less

Submitted 22 April, 2012; originally announced April 2012.

Comments: 8 pages

MSC Class: 03D35; 03C05; 03G30; 18C10; 18C15

Journal ref: Math. Struct. Comp. Sci. 24 (2014) e240605

An extension of data automata that captures XPath

Authors: Mikołaj Bojańczyk, Sławomir Lasota

Abstract: 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. 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. △ Less

Submitted 15 February, 2012; v1 submitted 3 January, 2012; originally announced January 2012.

ACM Class: F.1.1, H.2.3

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 1 (February 16, 2012) lmcs:672

Finite Satisfiability for Guarded Fixpoint Logic

Authors: Vince Bárány, Mikołaj Bojańczyk

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

Submitted 9 February, 2012; v1 submitted 12 April, 2011; originally announced April 2011.

Tree Languages Defined in First-Order Logic with One Quantifier Alternation

Authors: Mikolaj Bojanczyk, Luc Segoufin

Abstract: We study tree languages that can be defined in Δ_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. We provide an e… ▽ More We study tree languages that can be defined in Δ_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. We provide an effective characterization of tree and forest languages definable in Δ_2 . This characterization is in terms of algebraic equations. Over words, the class of word languages definable in Δ_2 forms a robust class, which was given an effective algebraic characterization by Pin and Weil. △ Less

Submitted 20 October, 2010; v1 submitted 15 September, 2010; originally announced September 2010.

ACM Class: cs.LO

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 4 (October 20, 2010) lmcs:699

Two-Way Unary Temporal Logic over Trees

Authors: Mikolaj Bojanczyk

Abstract: We consider a temporal logic EF+F^-1 for unranked, unordered finite trees. The logic has two operators: EFφ, which says "in some proper descendant φholds", and F^-1φ, which says "in some proper ancestor φholds". We present an algorithm for deciding if a regular language of unranked finite trees can be expressed in EF+F^-1. The algorithm uses a characterization expressed in terms of forest algebr… ▽ More We consider a temporal logic EF+F^-1 for unranked, unordered finite trees. The logic has two operators: EFφ, which says "in some proper descendant φholds", and F^-1φ, which says "in some proper ancestor φholds". We present an algorithm for deciding if a regular language of unranked finite trees can be expressed in EF+F^-1. The algorithm uses a characterization expressed in terms of forest algebras. △ Less

Submitted 5 August, 2009; v1 submitted 27 April, 2009; originally announced April 2009.

Comments: 29 pages. Journal version of a LICS 07 paper

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 5, Issue 3 (August 5, 2009) lmcs:917

Weak Mso with the Unbounding Quantifier

Authors: Mikolaj Bojanczyk

Abstract: A new class of languages of infinite words is introduced, called the max-regular languages, extending the class of $ω$-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. A new class of languages of infinite words is introduced, called the max-regular languages, extending the class of $ω$-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. △ Less

Submitted 6 February, 2009; originally announced February 2009.

Journal ref: 26th International Symposium on Theoretical Aspects of Computer Science STACS 2009 (2009) 159-170