Abstract 1 Introduction 2 Linear decompositions and semigroup theory 3 Transducing an ordering 4 Definable decompositions and definable properties References

Transducing Linear Decompositions of Tournaments

Colin Geniet ORCID Discrete Mathematics Group, Institute for Basic Science, Daejeon, South Korea    Fatemeh Ghasemi ORCID Univ Paris Est Creteil, LACL, F-94010 Creteil, France    Mamadou Moustapha Kanté ORCID Université Clermont Auvergne, Clermont Auvergne INP, LIMOS, CNRS, Clermont-Ferrand, France
Abstract

Bojańczyk, Pilipczuk, and Grohe [LICS ’18] proved that for graphs of bounded linear clique-width, clique-width decompositions of small width can be produced by a CMSO transduction. We show that in the case of tournaments, a first-order transduction suffices. This implies that the logics CMSO and existential MSO are equivalent over bounded linear clique-width tournaments.

Keywords and phrases:
Clique-width, definable decompositions, tournaments
Category:
Track B: Automata, Logic, Semantics, and Theory of Programming
Funding:
Colin Geniet: Supported by the Institute for Basic Science (IBS-R029-C1).
Fatemeh Ghasemi: Supported by the ANR project DIFFERENCE (ANR-20-CE48-0002) and by IUT Sénart-Fontainebleau.
Copyright and License:
[Uncaptioned image] © Colin Geniet, Fatemeh Ghasemi, and Mamadou Moustapha Kanté; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Mathematics of computing → Graph theory
; Theory of computation → Finite Model Theory
Related Version:
Full Version: https://arxiv.org/abs/2601.02999
Editors:
Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

1 Introduction

Bojańczyk and Pilipczuk proved the following conjecture of Courcelle:

Theorem 1 ([2, 3]).

For any k, there is a monadic second-order (MSO) transduction Φ from graphs to tree-decompositions of graphs such that, on every input graph G:

  1. 1.

    If G is a graph of tree-width at most k, then Φ non-deterministically outputs a tree-decomposition of G of width at most k, and

  2. 2.

    every output of Φ is a tree-decomposition of width at most k.

This can be understood as saying that tree-decomposition can be constructed not in a usual algorithmic sense, but through a process described by MSO logic. The motivation for this result is to prove the converse of Courcelle’s theorem: for graphs of tree-width k, if 𝒫 is a property that can be tested by a tree automaton running on tree decompositions of width k, then 𝒫 is definable by an MSO formula. The proof of Theorem 1 proceeds in two main steps:

  1. 1.

    First, one considers bounded path-width graphs. Path decompositions are seen as words in a semigroup, to which can be applied the Factorisation Forest Theorem of Simon [10]. This reduces the problem to path decomposition with a crucial regularity property – idempotence – which notably ensures the existence of paths without excessive detours.

  2. 2.

    In the general case, one constructs a tree decomposition whose bags have bounded path-width, and are in a sense maximal. Careful connectivity considerations, involving path systems with low congestion, allow to MSO transduce this decomposition, reducing the problem to the previous path-width case.

A natural generalisation of Theorem 1 is to consider dense graphs, replacing tree-width by clique-width. The same authors and Grohe generalised step (1) to this setting, replacing path-width by its dense equivalent linear clique-width, and using the slightly stronger logic CMSO, i.e. MSO with counting modulo 2. Their proof is once again crucially based on Simon’s theorem.

Theorem 2 ([1]).

For any k, there is a CMSO transduction Φ from graphs to clique-width decompositions, and k′∈ℕ such that for any input graph G,

  1. 1.

    If G has linear clique-width at most k, then Φ non-deterministically outputs a clique-width decomposition of G of width at most k′,

  2. 2.

    every output of Φ is a clique-width decomposition of width at most k′.

Pushing this generalisation to graphs of bounded clique-width however remains an open problem: the second step of the proof of Theorem 1 seems strongly tied to the behaviour of paths in tree decompositions, hence much harder to generalise to dense graphs. The proof of Theorem 2 is already quite involved, requiring to define a dense equivalent of connectivity.

We propose considering these questions for a restricted class of graphs, namely tournaments, i.e. directed graphs in which between every pair of vertices x,y, exactly one of the edges x→y or y→x exists. In this setting, we strengthen Theorem 2 in two ways:

  • ■

    We only use first-order (FO) logic, which is much weaker than MSO.

  • ■

    Our transduction always produces linear decompositions, whereas the output decompositions sometimes need to be tree-like in Theorem 2 and step (1) of Theorem 1.

That is, we prove the following.

Theorem 3.

For any k, one can compute an FO transduction Φ from graphs to linear clique-width decompositions, and k′∈ℕ, such that on any input graph T,

  1. 1.

    if T is a tournament of linear clique-width at most k, then Φ non-deterministically outputs a linear clique-width decomposition of T of width at most k′, and

  2. 2.

    every output of Φ is a linear clique-width decomposition of width at most k′.

The proof of Theorem 3 is also significantly simpler than Theorem 2. The key difference is that we do not refer to any notion of connectivity. Oversimplifying greatly, in the path-width case, the relative ordering of vertices in the path decomposition is determined by queries such as “is there a small separator between x and y”. For tournaments, our queries are rather “is x→y an edge” or “is there a vertex z with edges x→z→y”’. The latter, unlike the former, can be expressed using first-order logic.

In a sense, this is possible because in tournaments, the highly regular substructures provided by Simon’s factorisation are linear orders (also called transitive tournaments); by contrast, in the graph case, these highly regular substructures could be paths or edgeless graphs, for which FO is insufficient to describe a decomposition. Simon’s factorisation theorem remains a key tool in our proof (see Section 2 for the statement).

Theorem 2, together with Courcelle’s Backwards Translation Theorem [6, Theorem 1.40], implies that for bounded linear clique-width graphs, a property 𝒫 is CMSO definable if and only if it is testable by a finite automaton running on linear clique-width decompositions. In the case of tournaments, our FO transduction implies that the same holds with existential MSO (EMSO) instead of CMSO. Therefore, by going back and forth through automata on linear clique-width decompositions, we obtain the following.

Theorem 4.

For any k and any CMSO sentence φ on tournaments, there is an EMSO sentence ψ such that φ and ψ are equivalent for tournaments of linear clique-width at most k.

Let us conclude by discussing potential generalisations of our results to (non-linear) clique-width, and limits to them. Theorem 3 cannot directly generalise to bounded clique-width tournaments: A Ramsey-like argument of Mikołaj Bojańczyk (personal communication) shows that for 𝒯 the class of tournaments obtained by iterated lexicographic products of directed triangles (which has clique-width 3), no FO transduction can produce a clique-width decomposition of bounded width for all tournaments in 𝒯. On the other hand, it is simple to do so for the class 𝒯 with a transduction in the logic FO with counting modulo 2 (FO+C). To our knowledge, it is possible that Theorem 3 generalises to clique-width if we allow FO+C transductions.

A major part of our proof focuses on constructing a vertex ordering with low cut-rank, as a first step towards a linear clique-width decomposition. We believe that asking to transduce any total vertex ordering is an interesting intermediate question. For which tournament classes 𝒞 and logics ℒ, is there an ℒ-transduction that produces a total vertex ordering on any given T∈𝒞? Bojańczyk’s example once again implies that this is not possible for bounded clique-width tournaments and the logic FO, but FO+C could be sufficient. Note that from a clique-width decomposition of small width of a tournament (represented with the ancestor–descendent relation of the tree), one can always transduce a linear vertex ordering, corresponding to some left-to-right ordering on the leaves of the decomposition tree.111Let us point out that in the context of e.g. Theorem 2, one needs to consider a generalisation of clique-width decompositions where the decomposition tree may have nodes of unbounded degree. These high degree nodes make it impossible to transduce a total vertex ordering from the decomposition tree. In the case of tournaments however, they cannot exist. Indeed, a high degree node implies that there is a large subset X of vertices such that every bipartition of X is a cut of bounded rank, which is impossible in a tournament. Thus transducing a total ordering is an easier question than transducing clique-width decompositions of small width.

Structure of the paper

In Section 2, we introduce an infinite monoid ℭK corresponding to linear clique-width decompositions of width K, and a finite quotient MK of ℭK. This gives us the power to use Simon’s forest factorisation theorem, stated in Section 2, which for any word in ℭK yields a factorisation, subject to regularity conditions relative to MK, and with depth only depending on |MK|. In Section 3, we use induction on the factorisation given by Simon’s theorem to prove a weakening of Theorem 3: we construct a transduction which yields not a clique-width decomposition, but simply the associated vertex ordering. Section 4 then shows how to transduce from this ordering to the linear clique-width decomposition, completing the proof of Theorem 3, and finally shows how it implies Theorem 4.

Omitted proofs can be found in the full version of the paper.

Notations

We denote by [n] the interval of integers {1,…,n}. A tournament T=(V,E) is a directed graph with for each pair u≠v of vertices in V, exactly one of the two possible directed edges (u,v) or (v,u) in E. We also write V⁢(T)≔V and E⁢(T)≔E for the vertex and edge sets of T, and denote an oriented edge (u,v)∈E⁢(T) as u→v to emphasise its orientation. A bipartite tournament B=(L,R,E) is defined similarly restricting to edges between the two vertex sets L and R: the edge set E consists of exactly one of u→v or v→u for each pair of vertices u∈L and v∈R. In a tournament T, two disjoint subsets of vertices A,B⊂V⁢(T) are called homogenous if the edges between them are either all oriented from A to B, i.e. a→b is an edge for all a∈A and b∈B, or inversely all from B to A.

There are several graph complexity measures that are equivalent to (linear) clique-width. For our purposes, we will use the monoid structure defined in Section 2.

Our logic terminology is standard, we refer to [6] for instance. We refer also to [6] for definitions of transductions. In our setting, an FO transduction is a composition of the following atomic transductions:

  • ■

    interpretation, which consists in adding to the input structure a new relation defined by an FO-formula,

  • ■

    colouring, which consists in adding unary relations to the input structure,

  • ■

    filtering, which consists in outputting the input only if it satisfies an FO-formula.

  • ■

    universe restriction, which consists in restricting the universe of the input to the elements satisfying an FO formula, and binding each relation to the restricted universe.

It is well-known that any FO transduction can be equivalently expressed using only one instance of each operation, in the following order: colouring, filtering, interpretation, and universe restriction222Usually one allows copying first to linearly increase the domain, but we do not use copying in our setting.. If Φ is an FO transduction, we denote by Φ⁢(K) the set of outputs for input K. A transduction Φ is an extension transduction if for any input S of Φ, any T∈Φ⁢(S) is an extension of S.

2 Linear decompositions and semigroup theory

This section presents linear decompositions as constructed from pieces called bags, which can be composed, giving them a monoid structure. In this context, we will describe a linear decomposition as a sequence of small bags. We then introduce Simon’s Factorisation Forest Theorem, which will be used to obtain factorisations of such sequences, subject to some regularity conditions. While all the notions presented here can be defined for directed graphs of small clique-width, we restrict the definitions to tournaments to simplify notions and notations. We refer to [1] for a similar monoid for undirected graphs of small clique-width, which trivially extends to directed graphs.

Linear decompositions as a monoid

A bag is essentially a tournament with some additional information describing how it should be glued with other bags, so as to define a deterministic product operation on bags. For k∈ℕ, a bag B of order k consists of the following:

  1. 1.

    An internal tournament (V⁢(B),Eint⁢(B)), whose vertices V⁢(B) and edges Eint⁢(B) are called internal vertices and internal edges.

  2. 2.

    A boundary bipartite tournament ([k],V⁢(B),E∂⁢(B)). Here, 1,…,k are called input vertices, and stand for colour classes of vertices to the left of B.

  3. 3.

    A colouring λB:V⁢(B)→[k] of the internal vertices.

  4. 4.

    A recolouring function ρB:[k]→[k], which can be seen as a re-colouring of the input vertices.

A visual representation of bags is depicted in Figure 1 below. We do not define linear clique-width and refer to [7] for its definition. The objective is to prove that if a tournament has linear clique-width k, then it is a value of a word from a finite alphabet composed of bags. Let us define for that the multiplication operator on bags. Intuitively, when multiplying on the right by the bag B, the following happens: edges are added between any v∈V⁢(B) and all existing vertices of colour c according to the direction of the edge c→v or c←v in E∂⁢(B). Then, existing vertices have their colours modified by applying ρB, while internal vertices of B are given their colour from λB.

Formally, the product B1⋅B2 of two bags B1 and B2 of order k is defined as follows:

  1. 1.

    The internal vertices are V⁢(B1⋅B2)≔V⁢(B1)⊎V⁢(B2). Internal edges Eint⁢(B1⋅B2) are obtained as follows: Inside V⁢(B1) and V⁢(B2) respectively, edges are exactly as in Eint⁢(B1) and Eint⁢(B2). Between them, for x∈V⁢(B1) with colour c≔λB1⁢(x) and y∈V⁢(B2), there is an edge x→y (resp. x←y) if and only if c→y (resp. c←y) is a boundary edge in E∂⁢(B2).

  2. 2.

    For i∈[k] an input vertex and x∈V⁢(B2), there is a boundary edge i→x (resp. x→i) in E∂⁢(B1⋅B2) if and only if there is the edge ρB1⁢(i)→x (resp. x→ρB1⁢(i)) in E∂⁢(B2). When x∈V⁢(B1), the edge between i and x is simply the same as in E∂⁢(B1).

  3. 3.

    The colouring λB1⋅B2 of internal vertices coincides with ρB2∘λB1 inside V⁢(B1), and simply with λB2 inside V⁢(B2).

  4. 4.

    Finally, the recolouring function is ρB2∘ρB1.

In this product, we think of B1 as being to the left of, or earlier than B2. See Figure 1 for an example. Note that we only define the product of two bags of the same order, although it would be simple to lift this restriction by extending the set of colours of one bag. It is easy to check that the product is associative, and the empty bag with identity recolouring is the neutral element. Thus, the set of bags of order k has a monoid structure. We often write A⁢B instead of A⋅B when it is clear from the context.

Figure 1: Product of two bags. The two bags are drawn on the left, with the output vertices of the first identified with the input of the second. The result is on the right. Filled vertices are internal vertices; empty vertices represent colours, and dotted arrows show the colour/recolouring maps.

A bag is called atomic if it has at most one internal vertex. We denote by ℭk the submonoid generated by atomic bags of order k. The following essentially says that we can concentrate on ℭk when dealing with tournaments of linear clique-width at most k.

Lemma 5.

If a tournament T has linear clique-width at most k, then T is isomorphic to the internal tournament of some B∈ℭk. Conversely, if T is isomorphic to the internal tournament of some B∈ℭk, then T has linear clique-width at most 2⁢k+2.

Thanks to Lemma 5, we call by extension any word B1⋅B2⋅…⋅Bn of atomic bags a linear decomposition.

Types and abstraction

We next define some finite abstraction of bags. The first step is to define types of vertices inside a bag. Consider a bag B and an internal vertex v∈V⁢(B). The type of v describes its interactions with bags which may be multiplied to the left or right of B. Specifically, 𝗍𝗒𝗉𝖾B⁡(v) consists of the following information:

  1. 1.

    the colour λB⁢(v), and

  2. 2.

    the direction of edges i→v or i←v for each input vertex i∈[k].

We use σ,τ,… to denote vertex types. When the order k of the bag is fixed, there are only k⋅2k distinct vertex types.

Next, we define the abstraction of a bag. If B is a bag and τ is a vertex type, we denote by τ⁢(B)≔{v∈V⁢(B):𝗍𝗒𝗉𝖾B⁡(v)=τ} the set of vertices with type τ in B. The type τ is inhabited in B if τ⁢(B) is non-empty. The abstraction of B, denoted by ⟦B⟧, now consists of the following information:

  1. 1.

    the recolouring function ρB:[k]→[k],

  2. 2.

    the set of inhabited vertex types in B, and

  3. 3.

    for each pair of inhabited types σ,τ, whether σ⁢(B) and τ⁢(B) are homogeneous or not in the internal tournament of B, and when they are, the direction of edges σ⁢(B)→τ⁢(B) or σ⁢(B)←τ⁢(B).

We use α,β,… to denote abstractions of bags. For fixed order k, the number of bag abstractions is some constant 22O⁢(k).

One checks that the map B↦⟦B⟧ from bags to abstractions is a monoid homomorphism. We denote by Mk this monoid of abstractions of bags of order k. We summarise all these properties in the following.

Lemma 6.

For any k, the set Mk of abstractions has size bounded by 22O⁢(k), and there is an associative operation ⋅~ such that

⟦B1⋅B2⟧=⟦B1⟧⋅~⟦B2⟧.

Simon’s Factorisation Forest Theorem

Given a linear decomposition B=B1⁢B2⁢…⁢Bn, Simon’s theorem gives a factorisation forest, which is a more structured way to construct B from B1,…,Bn, subject to some restrictions relative to a finite semigroup S of our choice – in our case the monoid of abstractions.

The general setting of Simon’s theorem is the following. Consider a (usually infinite) semigroup Σ and a generating set A⊂Σ, a finite semigroup S, and a homomorphism φ:Σ→S. In our case, Σ are the bags, A the atomic bags, S the abstractions, and φ(B)=⟦B⟧. Simon’s theorem deals with two kinds of factorisations of elements w∈Σ:

binary factorisation:

w=w1⋅w2 for w1,w2∈Σ with no further restriction.

idempotent factorisation:

w=w1⋅…⋅wn, where the number n of factors is unrestricted, but the factors must all map to the same e=φ⁢(wi) in S, which furthermore must be idempotent, meaning e⋅e=e.

Simon’s theorem states that any w∈Σ can be reduced down to generators in A by applying the previous two operations nested only up to a depth bounded by a linear function of |S|. This process is described as a factorisation forest for w.

Let us introduce some terminology allowing to count binary and idempotent factorisations separately. A factorisation forest has depth (p,q) if the nesting depth of idempotent operations is at most p, and that of binary operations is at most q. Formally:

  • ■

    Generators a∈A have a factorisation forest of depth (0,0).

  • ■

    If w1,w2 have factorisation forests of depth (p1,q1) and (p2,q2) respectively, then w1⋅w2 has a factorisation forest of depth

    (max⁡{p1,p2},max⁡{q1,q2}+1).
  • ■

    If w1,…,wn∈Σ satisfy φ⁢(wi)=e for some idempotent e∈S and all 1≤i≤n, and there are p,q∈ℕ such that each wi has a factorisation forest of depth (pi,qi), then w1⋅…⋅wn has a factorisation forest of depth (max⁡{p1,…,pn}+1,max⁡{q1,…,qn}).

Since this definition depends on the choice of semigroup S and morphism φ, we will call it a factorisation forest over φ to disambiguate.

Theorem 7 (Simon’s Factorisation Forest Theorem, [10, 9]).

Consider a semigroup Σ generated by A⊂Σ, and a homomorphism φ:Σ→S to a finite semigroup. Then all w∈Σ have factorisation forests over φ of depth at most (|S|,2⁢|S|).

In the case of bags, we will apply Theorem 7 to the monoid ℭK with atomic bags as generators, and the abstraction homomorphism ⟦⋅⟧:ℭK→MK. Since we will only consider factorisation forests over the abstraction homomorphism, we will omit the “over ⟦⋅⟧” qualifier in the rest of this work.

Abstractions and vertex deletion

The proof of our main result proceeds by induction over the depth of a given factorisation forest. At some point during this induction, we may need to restrict the bag considered to a subset of vertices. In general, this does not preserve the factorisation depth. Indeed, deleting vertices in a bag may change its abstraction, and what was an idempotent factorisation may thus stop being one. This section describes a sufficient condition to control the depth of factorisation forests when deleting vertices.

Given a bag B and a subset X⊆V⁢(G) of internal vertices, we denote by B⁢[X] the bag obtained by deleting any internal vertex of B outside X, and restricting the edges and colouring map of B to X. If Γ is a set of vertex types, then we denote by Γ⁢(B)=⋃τ∈Γτ⁢(B) the set of vertices with type in Γ, and we say that Γ⁢(B) is a union of types. When deleting vertices from bags, we will only delete unions of types, which is sufficient to control the factorisation depth.

Lemma 8.

Let k be a positive integer and let B be a bag in ℭk. If B has a factorisation forest of depth (p,q) and X⊂V⁢(B) is some union of types, then B⁢[X] has a factorisation forest of depth (p,q+2⁢p).

3 Transducing an ordering

In this section, we show that orderings of bounded cut-rank can be FO transduced. Throughout the section, we work with (non-deterministic) extension transductions Φ with signature {E}→{E,<}, where E,< are binary relational symbols. Explicitly, such a transduction takes as input a (directed) graph G=(V,E), and non-deterministically outputs structures (V,E,<), i.e. the same graph (V,E) plus some binary relation < expected to be a linear ordering.

Theorem 9.

For any k∈ℕ, one can compute an extension FO transduction Φk with signature {E}→{E,<}, and k′∈ℕ such that

  1. 1.

    for any graph G=(V,E), every structure in Φk⁢(G) is (V,E,<) for some linear ordering < of G with cut-rank at most k′, and

  2. 2.

    if T is a tournament with linear clique-width at most k, then Φk⁢(T) contains at least one such structure.

The adjacency matrix of a tournament T is the boolean matrix whose rows and columns are indexed by V⁢(T), where the entry at row x and column y is 1 only if (x,y)∈E⁢(T). In a tournament T, consider a bi-partition V⁢(T)=X⊎Y of the vertices. The rank of this bi-partition, denoted by 𝗋𝗄T⁡(X;Y), is the rank (over the binary field 𝔽2) of the adjacency matrix of X versus Y, i.e. the adjacency matrix restricted to rows indexed by vertices in X and columns indexed by vertices in Y. If x1<⋯<xn is a linear ordering of V⁢(T), the cut-rank of < is defined as

maxi⁡𝗋𝗄⁡({x1,…,xi};{xi+1,…,xn}).

The proof will follow the same line as in [2, 1] and will be by induction on the height of the Simon’s Factorisation Forest of the words generating bags in ℭk. It is not hard to check, by a first-order formula depending only on ℓ, that an ordering < on V has cut-rank at most ℓ. Indeed, this amounts to saying that, for every x, there exist vertices b1,…,bm≤x with m≤ℓ and such that for every z≤x, there is a subset Bz⊆{b1,…,bm} satisfying, for all y>x,

E⁢(z,y)=∑b′∈BzE⁢(b′,y)(mod2).

We can therefore concentrate in proving the second condition of Theorem 9. Let us explain the main induction before proceeding to the proof of the main technical lemma.

Main induction

By Lemma 5, any tournament T with linear clique-width k is also the internal tournament of some bag B in ℭk. Furthermore, by Theorem 7, this bag B has factorisation depth at most (|Mk|,2⁢|Mk|), where Mk is the monoid of abstractions of arity k, whose size is a function of k only. Thus, Theorem 9 follows from the next statement and the arguments given above for checking that an ordering has small cut-rank.

Lemma 10.

For any k,p,q∈ℕ, one can compute f⁢(k,p,q)∈ℕ and an extension FO transduction Φ(p,q)k:{E}→{E,<} such that if T=(V,E) is the internal tournament of a bag B∈ℭk of factorisation depth at most (p,q), then there is some ordering < of T with cut-rank at most f⁢(p,q,k) such that (V,E,<)∈Φ(p,q)k⁢(T).

We once again insist that the output Φ(p,q)k⁢(T) needs to contain some linear ordering of T with the required cut-rank, but may also contain other structures where < is interpreted arbitrarily (possibly not even as a linear ordering). Thus we will show that if non-deterministic steps follow the “right” choices, then the transduction produces the desired ordering, while ignoring anything resulting from a “wrong” choice.

Let us begin the proof of Lemma 10, by induction on the pair (p,q) ordered lexicographically. Choose the bound f⁢(k,p,q) to satisfy:

f⁢(k,0,0) =k,
f⁢(k,p,q) ⩾f⁢(k,p,q−1)+k if q>0, and
f⁢(k,p,q) ⩾f⁢(k,p−1,2⁢p+q)+2⁢k⋅(2k+1) if p>0.

Consider a bag B∈ℭK whose internal tournament is T, and with factorisation depth (p,q).

In the base case p=q=0, the bag B is atomic, and the result is trivial. Assume now that p>0 or q>0, so that the Simon’s factorisation of B has either a binary or an idempotent operation at the root. The transduction Φ(p,q)k starts by guessing which of these two cases occurs (this can be simulated using a colouring step), and will continue with a different transduction for each.

Binary case

Assume B=B1⋅B2 where B1,B2 have factorisations of depth at most (p,q−1). We use a non-deterministic colouring to guess the bipartition V⁢(B1),V⁢(B2). Then, by restricting the quantifiers to V⁢(Bi), one can simulate applying the transduction Φ(p,q−1)k obtained by induction to each T⁢[V⁢(Bi)]. Thus, we obtain linear orderings <1,<2 of cut-rank at most f⁢(k,p,q−1) for T⁢[V⁢(B1)] and T⁢[V⁢(B2)] respectively.

Define < on T by V⁢(B1)<V⁢(B2), where < coincides with <i inside V⁢(Bi). One can transduce < from <1,<2 and the bipartition V⁢(B1),V⁢(B2). Since we are dealing with bags of arity k, we have 𝗋𝗄⁡(V⁢(B1);V⁢(B2))⩽k. Since <i has cut-rank at most f⁢(k,p,q−1) in T⁢[V⁢(Bi)] for i∈{1,2}, this implies that < has cut-rank at most f⁢(k,p,q−1)+k≤f⁢(k,p,q).

Idempotent case

Assume now we are given an idempotent factorisation, that is B=B1⋅…⋅Bn where ⟦Bi⟧=α for all 1≤i≤n, with α idempotent, and each Bi has factorisation depth at most (p−1,q).

Consider the quasi-ordering ⪯ of V⁢(B) defined by V⁢(B1)⪯⋯⪯V⁢(Bn), and call ∼ the equivalence relation whose classes are V⁢(B1),…,V⁢(Bn). Suppose in a first time that we are given ⪯ (transducing it will be the core of this proof). The Parallel Application Lemma [1, Lemma 5.6] allows to apply Φ(p−1,q)k to each Bi simultaneously, yielding a relation < which inside each Bi is interpreted as a linear ordering of cut-rank at most f⁢(k,p−1,q).

Define <′ to be the linear ordering which coincides with < inside each bag Bi, and with ⪯ between the bags. Clearly <′ can be transduced from < and ⪯, and it is not hard to check that its cut-rank depends only on the cut-rank of ⪯ and of <.

We are thus only left with the core problem of transducing the quasi-ordering ⪯. Unfortunately, it is not always possible to transduce exactly ⪯. For instance B might have two strongly connected components X1,X2, each intersecting all Bj. Then, we might be able to transduce ⪯ inside each Xi, but it will be impossible to transduce ⪯ between X1 and X2. Indeed, as X1 and X2 are distinct strongly connected components, we infer that the edges are all oriented from one of them to the other one. For all integers 1≤i<k<j≤n, to transduce ⪯, we should have that the elements of X2∩Bi come before the elements of X1∩Bk, and the elements of X2∩Bj come after the elements of X1∩Bk. However, the adjacency between X1 and X2 is homogenous and can be therefore transduced from an independent set (or a clique), which is not possible to order in CMSO. In this case, we need to reorganise the decomposition of B by first separating X1 and X2, and then decomposing each of them. The precise statement we prove is thus the following.

Lemma 11.

Given k, one can compute an extension FO transduction Ψk with signature {E}→{E,⪯} satisfying the following. If T=(V,E) is the internal tournament of a bag B∈ℭk with factorisation depth at most (p,q), then there is a quasi-ordering ⪯ of V with equivalence classes X1⪯⋯⪯Xm such that

  1. 1.

    for each i∈[m], T⁢[Xi] is the internal tournament of a bag in ℭk having factorisation depth at most (p−1,q+2⁢p),

  2. 2.

    for each i∈[m],

    𝗋𝗄⁡(X1∪⋯∪Xi;Xi+1∪⋯∪Xm)⩽k⋅(2k+1),
  3. 3.

    and (V,E,⪯)∈Ψ(p,q)k⁢(T).

Assuming Lemma 11, we conclude as follows. From the quasi-ordering ⪯, it is simple to transduce the equivalence relation ∼ with equivalence classes X1,…,Xm. Recall that we do induction on (p,q) ordered lexicographically, hence we can assume the transduction Φ(p−1,q+2⁢p)k is already defined. Using the Parallel Application Lemma [1, Lemma 5.6], this transduction can be again applied to each Xi in parallel. This yields a relation < which inside each T⁢[Xi] is a linear ordering with cut-rank at most f⁢(k,p−1,q+2⁢p). Define <′ to coincide with < inside each Xi and with ⪯ between the different Xi, which is easily transduced from <,⪯. Using Condition 2 of Lemma 11, it is not hard to prove that <′ has cut-rank at most

f⁢(k,p−1,q+2⁢p)+2⁢k⋅(2k+1)⩽f⁢(k,p,q).

This concludes the idempotent case, and thus the proof of Lemma 10.

We are now going to prove Lemma 11. From now on, we fix some k∈ℕ, and consider a factorisation B=B1⋅…⋅Bn, where all Bi have the same idempotent abstraction α, and have factorisation depth at most (p−1,q). We also call T=(V,E) the internal tournament of B.

Recall that Lemma 11 asks for a transduction depending only on k. As the very first step of this transduction, one may use non-deterministic colouring to guess the abstraction α (for which there are only finitely many possibilities for a fixed k, by Lemma 6). We may thus instead allow the transductions constructed in this section to depend on both k and α (but not B, the factorisation, or p,q).

For a vertex x∈V⁢(Bi), we call 𝗂𝖽𝗑⁡(x)=i the index of x. Our goal is to answer (with an FO transduction) the question: given x,y, is 𝗂𝖽𝗑⁡(x)⩽𝗂𝖽𝗑⁡(y)? To be formal, for a subset X of V⁢(B), we say that a transduction Φ orders X according to ⪯ if Φ is an extension FO transduction, and there is some (V,E,⪯′)∈Φ⁢(T) such that ⪯ and ⪯′ coincide on X.

Using the non-determinism of transductions, one may show that it suffices to consider vertices whose indices differ by at least some constant. That is, say that Φ approximately orders X according to ⪯ if Φ is an extension FO transduction, and there is (V,E,⪯′)∈Φ⁢(T) such that ⪯,⪯′ coincide for any pair x,y∈X that satisfies |𝗂𝖽𝗑⁡(x)−𝗂𝖽𝗑⁡(y)|⩾2. When X hits all bags of the factorisation, if we can approximately order X, then we can also order it:

Lemma 12.

Let X be a subset of vertices containing at least one vertex for each possible index. For any FO transduction Φ, there is a second transduction Ψ such that if Φ approximately orders X according to ⪯, then Ψ orders X according to ⪯.

Let us call ρ the recolouring function of the bags Bi. It is the same for all bags since it is part of the abstraction α, and it is idempotent (ρ∘ρ=ρ). Consider any vertex of B, say x∈V⁢(Bi). In the bag Bi, x is given some colour λBi⁢(x), which we call its initial colour λi⁢n⁢i⁢t⁢(x). Then, as we multiply by Bi+1, the colour of x changes to ρ⁢(λi⁢n⁢i⁢t⁢(x)). Continuing with Bi+2 will again recolour x by applying ρ, but since ρ is idempotent, this does nothing. Thus, for any j>i, the colour of x in B1⋅…⋅Bj is ρ⁢(λi⁢n⁢i⁢t⁢(x)). We call this its final colour and denote it by λf⁢i⁢n⁢(x).

Recall that to define the abstraction α of the bags Bi, we first defined the vertex type 𝗍𝗒𝗉𝖾Bi⁡(x) of x inside the bag Bi, which indicates its colour λBi⁢(x), i.e. the initial colour, and the direction of edges between x and input vertices in Bi. In what follows, the type of a vertex x will always be understood relative to the bag Bi containing it, and we shorten it to 𝗍𝗒𝗉𝖾⁡(x). Using a non-deterministic colouring, we can guess the types of all vertices in B, and we assume this colouring to be given in all subsequent lemmas. With this in hand, we can already order the vertices of a given type τ. Denote by Vτ=⋃iτ⁢(Bi) the set of vertices of type τ. Note that if Vτ is non-empty, then it intersects all bags B1,…,Bn. Indeed whether or not Bi contains a vertex of type τ is indicated by the abstraction α.

Lemma 13.

For any type τ, there is an FO transduction depending only on k,ρ,τ that orders Vτ according to ⪯.

Thus we can order the vertices of each type independently, and the issue is now to combine these orderings. Denote by Γ the set of inhabited vertex types in B1,…,Bn. Recall that subsets of vertices X,Y are called homogeneous if either all edges are oriented from X to Y, or all from Y to X. We define the synchronisation graph G𝗌𝗒𝗇 with vertices Γ, in which σ,τ are adjacent if and only if Vσ and Vτ are not homogeneous.

We show that when G𝗌𝗒𝗇 is connected, one can transduce the quasi-ordering ⪯ corresponding to the original decomposition B1⋅…⋅Bn:

Lemma 14.

Let Θ⊂Γ be a connected component of the synchronisation graph G, and denote VΘ=⋃τ∈ΘVτ. Then VΘ can be ordered according to ⩽ by an FO transduction depending only on k,α,Θ.

When G𝗌𝗒𝗇 is connected, Lemma 14 concludes the proof of Lemma 11. Note in that case that the given factorisation B=B1⋅…⋅Bn is not modified, i.e. the partition {X1,…,Xm} in the conclusion of Lemma 11 is exactly {B1,…,Bn}, and conditions (1) and (2) of the statement are trivial. We now handle the case where G𝗌𝗒𝗇 is disconnected by slightly modifying this decomposition.

Assume that G𝗌𝗒𝗇 has several connected components that we enumerate as Θ1,…,Θr. We then reorganise the decomposition of B. For i∈[n] and t∈[r], call Xt,i the set of internal vertices of Bi with types in Θt. By Lemma 14, for each t∈[r], the set VΘt can be ordered according to ⪯ with a transduction. Let ⪯′ be the quasi-ordering on the partition {Xt,i∣i∈[n],t∈[r]} obtained by ordering first according to the index t of the connected component Θt of the type, and then by the index i of the bag Bi, i.e.

X1,1⪯′⋯⪯′X1,n⪯′⋯⪯′Xr,1⪯′⋯⪯′Xr,n.

One can prove that this quasi-ordering ⪯′ has small cut-rank. We can therefore complete the proof of Lemma 11, by checking the three conditions of the statement.

  1. 1.

    Firstly, each T⁢[Xt,i] is the internal tournament of a bag in ℭk of factorisation depth at most (p−1,q+2⁢p). Indeed, this follows from Lemma 8 since T⁢[Xt,i] is the restriction of T⁢[V⁢(Bi)] to some union of types, and Bi is a bag in ℭk and has factorisation depth at most (p−1,q) by assumption.

  2. 2.

    We can prove that the quasi-ordering X1,1⪯′⋯⪯′X1,n⪯′⋯⪯′Xr,1⪯′⋯⪯′Xr,n has cut-rank at most k⋅(2k+1).

  3. 3.

    Finally, there is an extension FO transduction Ψk depending only on k such that for T=(V,E) the internal tournament of B, we have (V,E,⪯′)∈Ψk⁢(T). Indeed, from Lemma 14, we can obtain the restriction of ⪯′ to any VΘt by a transduction depending only on k,α,Θ. By first guessing the type of each vertex, ordering by types between the different sets VΘ1,…,VΘr, and by the previous transductions inside each VΘt, we obtain the desired quasi-ordering ⪯′.

    This transduction depends on k, the abstraction α of bags, and the synchronisation graph G𝗌𝗒𝗇. Since there are only finitely many possible choices for α and for G𝗌𝗒𝗇 when k is fixed, thus the transduction Ψk may first guess α and G𝗌𝗒𝗇, and then proceed as above.

This completes the proof of Lemma 11, and with it Theorem 9.

4 Definable decompositions and definable properties

Theorem 9 proved that in tournaments of bounded linear clique-width, one can FO-transduce orderings of bounded cut-rank. We now show that, from this ordering, one can also transduce a linear clique-width decomposition, proving our main result, Theorem 3. Then, we combine this with some of the central ideas from Courcelle’s work [6] to obtain that the logics MSO and EMSO are equivalent over bounded linear clique-width tournaments (Theorem 4).

Let us first explain how we represent a linear decomposition as a relational structure. We choose a representation based on the monoid ℭk from Section 2, but it would be simple to obtain the same results with a representation based on the operations defining linear clique-width.

We use the following standard encoding of words as relational structures. For a finite alphabet A, a word w1,…,wn in A∗ is represented by the ordered structure with vertex set {1,…,n}, one binary relation < for the natural ordering on {1,…,n}, and for each letter a∈A, a unary relation a⁢(x) such that a⁢(i) holds if and only if wi=a. We call this the unary representation of the word w1,…,wn.

Now for any k∈ℕ, let 𝔄k denote the set of atomic bags of order k (up to isomorphism). Recall that 𝔄k by definition generates the monoid ℭk, and that linear clique-width decompositions are equivalent, in the sense of Lemma 5 to words B1,…,Bn with each Bi∈𝔄k. We then represent the linear decomposition B1,…,Bn as a word over the alphabet 𝔄k, in unary representation. Firstly, from a linear decomposition, one can reconstruct the corresponding graph with a transduction.

Lemma 15.

For any k, one can compute an FO transduction Φk which, given a linear decomposition B1,…,Bn with Bi∈𝔄k, outputs the underlying graph of B1⋅…⋅Bn.

Lemma 15 is usually considered for MSO transductions, where it is a very easy result. With FO transductions instead, we need the following definition and result.

Consider a finite semigroup S, and a word w1,…,wn with letters in S. The binary representation of w1,…,wn is the relational structure with again vertices {1,…,n} and the natural ordering < as a binary relation, and additionally, for each a∈S a binary relation a⁢(x,y) such that a⁢(i,j) holds if and only if i⩽j and wi⋅…⋅wj=a. The following is a variant of a result of Colcombet [5, Lemma 3], which is obtained thanks to Simon’s factorization.

Lemma 16.

For any finite semigroup S, one can compute an FO transduction ΨS that, for any word w=w1,…,wn in S∗, given the unary representation of w, outputs its binary representation.

Lemma 16 allows to convert the unary representation of the linear decomposition B1,…,Bn given in Lemma 15 into a binary representation. It is then simple to complete the proof of Lemma 15 by reconstructing the graph from this binary representation.

From Theorems 9 and 15, we obtain the following: Now given a tournament T with small linear clique-width, one can (1) apply the transduction of Theorem 9 to obtain an ordering with small cut-rank, which is also the ordering of a linear decomposition of small width, then (2) guess (using non-deterministic colouring) the atomic bag in corresponding to each vertex in this linear decomposition, and finally (3) apply Lemma 15 to check that the linear decomposition consisting of the ordering from step (1) and the labels from step (2) indeed corresponds to T. This proves our main result:

Theorem 17.

For any k, one can compute an FO transduction Φk and k′∈ℕ such that

  1. 1.

    for any graph G, any S∈Φk⁢(G) is a linear clique-width decomposition of G of width at most k′, and

  2. 2.

    when T is a tournament with linear clique-width at most k, Φk⁢(T) contains at least one such decomposition.

Applications of transductions between graphs and tree- or clique-decompositions in Courcelle’s work typically involve the Backwards Translation Theorem [6, Theorem 1.40], which states that for any MSO transduction Φ with signature Γ→Δ, and any MSO formula ψ on Δ, there is an MSO formula ψ∘Φ such that

G⊧ψ∘Φ⇔∃H∈Φ⁢(G),H⊧ψ.

We will use a similar statement to prove Theorem 4 from Theorem 3.

Backwards translation is easily adapted to CMSO formulas and transductions, as well as FO formulas and deterministic FO transductions. On the other hand, FO formulas are not sufficiently expressive to handle the non-deterministic colouring operation. To this end, one should instead use existential MSO (EMSO) formulas, i.e., formulas of the form

∃X1,…,Xn,ψ,

where the variables Xi range over subsets of vertices, and ψ is an FO formula that may use the predicates x∈Xi. The proof of the following remains essentially the same as in the MSO case.

Lemma 18 (Backwards Translation for FO Transductions).

For any FO transduction Φ with signature Γ→Δ, and any EMSO formula ψ on Δ, there is an EMSO formula ψ∘Φ such that

G⊧ψ∘Φ⇔∃H∈Φ⁢(G),H⊧ψ.

The last tool we need to prove Theorem 4 is the following folklore variant of Büchi–Elgot–Trakhtenbrot theorem.

Theorem 19 (Büchi–Elgot–Trakhtenbrot [4, 8, 11]).

For any finite alphabet A and language L⊆A∗, the following are equivalent:

  1. 1.

    L is a regular language,

  2. 2.

    L is defined by an MSO sentence,

  3. 3.

    L is defined by an CMSO sentence,

  4. 4.

    L is defined by an EMSO sentence.

We are now ready to prove Theorem 4.

Theorem 4. [Restated, see original statement.]

For any k and any CMSO sentence φ on tournaments, there is an EMSO sentence ψ such that φ and ψ are equivalent for tournaments of linear clique-width at most k.

Proof.

Take the transduction Φk and k′∈ℕ given by Theorem 17. Applying backwards translation for CMSO to the transduction from linear decompositions to graphs given by Lemma 15, we obtain a CMSO formula φ′ on linear decompositions of width at most k′, such that for any linear decomposition D with width at most k′ of a tournament T, we have D⊧φ′ if and only if T⊧φ. Since linear decompositions are words, Theorem 19 gives that φ′ is equivalent to some EMSO formula ψ′.

Now apply backwards translation for FO (Lemma 18) to ψ′ and the transduction Φk given by Theorem 17. This yields an EMSO formula ψ such that T⊧ψ if and only if D⊧ψ′ holds for some D∈Φk⁢(T).

Consider T a tournament with linear clique-width at most k. Assume that T⊧φ, and consider a linear decomposition D∈Φk⁢(T) of T with width at most k, guaranteed by Theorem 17. Then the choice of φ′, ψ′, and ψ directly gives

T⊧φ⇔D⊧φ′⇔D⊧ψ′⟹T⊧ψ.

Conversely, assume that T⊧ψ, hence there is some D∈Φk⁢(T) such that D⊧ψ′. Then Theorem 17 guarantees that D is a linear decomposition of T with width at most k, and we once again have the equivalence between D⊧ψ′, D⊧φ′, and finally T⊧φ. Therefore φ is equivalent to the EMSO sentence ψ for any tournament T with linear clique-width at most k. ◀

References

  • [1] Mikolaj Bojanczyk, Martin Grohe, and Michal Pilipczuk. Definable decompositions for graphs of bounded linear cliquewidth. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7125.
  • [2] Mikołaj Bojańczyk and Michał Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, pages 407–416, New York, NY, USA, 2016. Association for Computing Machinery. doi:10.1145/2933575.2934508.
  • [3] Mikolaj Bojanczyk and Michal Pilipczuk. Optimizing tree decompositions in MSO. In Heribert Vollmer and Brigitte Vallée, editors, 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 15:1–15:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.STACS.2017.15.
  • [4] J. Richard Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6(1-6):66–92, 1960. doi:10.1002/malq.19600060105.
  • [5] Thomas Colcombet. A combinatorial theorem for trees. In Lars Arge, Christian Cachin, Tomasz Jurdziński, and Andrzej Tarlecki, editors, Automata, Languages and Programming, pages 901–912, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-73420-8_77.
  • [6] Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics and its applications. Cambridge University Press, 2012. URL: http://www.cambridge.org/fr/knowledge/isbn/item5758776/?site_locale=fr_FR.
  • [7] Bruno Courcelle and Stephan Olariu. Upper bounds to the clique width of graphs. Discret. Appl. Math., 101(1-3):77–114, 2000. doi:10.1016/S0166-218X(99)00184-5.
  • [8] Calvin C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98(1):21–51, 1961. URL: http://www.jstor.org/stable/1993511.
  • [9] Manfred Kufleitner. The height of factorization forests. In Edward Ochmański and Jerzy Tyszkiewicz, editors, Mathematical Foundations of Computer Science 2008, pages 443–454, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. doi:10.1007/978-3-540-85238-4_36.
  • [10] Imre Simon. Factorization forests of finite height. Theoretical Computer Science, 72(1):65–94, 1990. doi:10.1016/0304-3975(90)90047-L.
  • [11] J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Systems Theory, 2:57–81, 1968. doi:10.1007/BF01691346.