Bruno Courcelle Labri

Fly-automata for checking MSO 2 graph properties

Keywords: monadic second-order logic, edge quantification, tree-width, clique-width, algorithmic meta-theorem, fly-automaton

est destinée au dépôt

Introduction

Graphs are finite and, either directed or undirected. Our goal is to check their monadic second-order (MSO ) properties by using finite automata running on the terms that denote input graphs, and to obtain in this way fixed-parameter tractable (FPT ) algorithms whose parameters are tree-width or clique-width. We want these automata to be constructable automatically from logical formulas and practically usable. We recall the following algorithmic meta-theorem [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] 1 ; the notions it uses will be reviewed in Section 2.

Theorem 1 : (a) For every integer k and every MSO sentence ϕ, there exists a linear time algorithm that checks the validity of ϕ in any graph of clique-width at most k given by a relevant term.

(b) For every integer k and every MSO 2 sentence ϕ, there exists a linear time algorithm that checks the validity of ϕ in any graph of tree-width at most k given by a relevant tree-decomposition.

A sentence is a logical formula without free variables. An MSO sentence can only use quantifications over vertices and sets of vertices, whereas an MSO 2 sentence can also use quantifications over edges and sets of edges. The incidence graph Inc(G) of a graph G is a bipartite graph constructed as follows: its vertices are those of G together with new vertices representing its edges; its adjacency relation is the incidence relation of G (relating an edge and its ends). Assertion (b)2 is actually a consequence of (a) because:

(1) an MSO 2 property of a graph G is nothing but an MSO property of its incidence graph Inc(G) and

(2) if G has tree-width k, then Inc(G) has clique-width at most f (k) for some fixed linear function f ,

(3) a tree-decomposition of G of width k can be converted in linear time (for fixed k) into a clique-width term of width at most f (k) that defines Inc(G).

Point ( 1) is just a matter of definitions. Point [START_REF] Bouvier | Graphes et décompositions[END_REF], in particular the fact that f is linear (f (k) ≤ 2k + 5, see details in Section 3) together with the linear time transformation of (3) make practically usable this reduction of (b) to (a).

Automata constructions.

The classical proof of Assertion (a) constructs from an MSO sentence ϕ and a positive integer k a finite automaton A ϕ,k that takes as input a term t of width at most k that denotes an input graph assumed of clique-width ≤ k. This automaton recognizes the terms that denote graphs satisfying ϕ. The construction is done by induction on the structure of ϕ. First, one constructs automata for the atomic formulas that are of only two kinds3 : X ⊆ Y (set inclusion) and edg(X, Y ) (meaning that X = {x}, Y = {y} and there is an edge from x to y, or between them if the graph is undirected). As we will recall, MSO formulas can be written with set variables only and these two types of atomic formulas. From automata A ϕ,k and A ψ,k , one can build automata for A ϕ∨ψ,k and A ϕ∧ψ,k by taking the product of A ϕ,k and A ψ,k equipped with appropriate accepting states. Other constructions handle negation and existential quantification. See [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

It is actually useful to precompute automata A ϕ,k for some formulas ϕ expressing basic MSO properties, such as P artition(X 1 , ..., X p ) (meaning that X 1 , ..., X p is a partition of the vertex set), stability of X (denoted by St(X) and meaning that there are no edges between vertices in X, equivalently, that X is an independent set), connectedness of the considered graph, existence of directed or undirected cycles, degree bounds etc. See [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]. The logical expression of a property can be made simpler as we allow, in some sense, more atomic formulas. For example, 3-colorability is expressed by : ∃X 1 , X 2 , X 3 .(P artition(X 1 , X 2 , X 3 ) ∧ St(X 1 ) ∧ St(X 2 ) ∧ St(X 3 )).

However, even with this technique, this construction is intractable because A ϕ,k has in most cases, even for k = 2, so many states that it cannot be implemented in the classical way. This is not avoidable [START_REF] Frick | The complexity of first-order and monadic secondorder logic revisited[END_REF]. The notion of a fly-automaton (an FA in short) remedies to this fact. Its states are not listed in huge tables. Although numerous, they have a common syntactic structure and can be described by words 4 . The necessary transitions are not stored in tables but computed by (small) programs. A deterministic FA having 2 2 10 states needs and computes only 100 states on a term of size 100. The maximum size of a state (the number of bits for encoding it) used on an input term is more important to bound the computation time than the total number of states. Implementation of FA has been tested in significant cases [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Computations by fly-automata beyond monadic second-order logic[END_REF].

The present contribution : Our objective is to apply to Assertion (b) the tools developped in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Computations by fly-automata beyond monadic second-order logic[END_REF]. However, the reduction of (b) to (a) necessitates some work on automata. For instance, the clique-width operations allow to write terms that do not define incidence graphs. For example, if some vertex intended to represent an edge has degree more than 2, the defined graph is not an incidence graph. We will define an automaton A CT to check whether a given term is correct, i.e, defines an incidence graph.

Furthermore, in MSO 2 logic seen as MSO logic on incidence graphs, the property edg(X, Y ) is no longer atomic. It is expressed by: "there exists a vertex representing an edge that is adjacent to the unique vertex of X and to the unique vertex of Y ", hence, the automaton for this formula is more complicated than the one for edg(X, Y ) in the case of MSO logic because of the quantification on vertices representing edges. We will detail the construction of such an FA for edg(X, Y ) and of other FA for related properties such as domination. We will also construct FA for checking Hamiltonicity, a graph property that is MSO 2 -expressible but not MSO-expressible.

We consider directed graphs because they are in general algorithmically more difficult to handle than undirected ones. In the present setting they are no more 4 FA can have infinitely many states: a state can record the (unbounded) number of occurrences of a particular symbol. We can thus construct fly-automata that check properties that are not MSO expressible (for example that a graph is regular or can be partitioned into p disjoint regular graphs). These automata yield FPT or XP algorithms [START_REF] Downey | Parameterized complexity[END_REF][START_REF] Downey | Fundamentals of parameterized complexity[END_REF] for clique-width as parameter. By equipping fly-automata with output functions, we can make them compute values attached to graphs: for example, assuming that the input graph is s-colorable, the minimum size of X 1 in an s-coloring (X 1 , . . . , Xs). We can compute the number of p-vertex colorings, and also the number of so-called of acyclic 4-colorings of Petersen's graph: 10800. The number of acyclic 3-colorings of McGee's graph is 57024. See [START_REF] Courcelle | Computations by fly-automata beyond monadic second-order logic[END_REF].

difficult to deal with, and it is easy to simplify our automata, constructed for directed graphs so as they handle undirected graphs.

Our method, that consists in computing automata from logical formulas, yields usable algorithms very quickly as it consists in combining predefined automata by means of a few standard procedures operating on FA. It has been implemented 5 . The produced algorithms follow the general scheme of dynamic programming over graph decomposition, however, specialized algorithms for particular problems designed with ad hoc data structures can be quicker. Our purpose is to obtain by meta-algorithmic tools, usable algorithms with reasonable, but not necessarly optimal, time complexity.

Section 2 reviews definitions and constructions of automata. Although this article is a continuation of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], we recall most definitions to make it readable independently. In Section 3, we adapt definitions to incidence graphs. Our constructions of automata for the correctness of terms and for properties based on adjacency are in Section 4. Other properties, in particular Hamiltonicity, are discussed in Section 5. We review related work in our conclusion.

Definitions and background constructions.

First, some notation : P(X) denotes the powerset of a set X, P f (X), the set of its finite subsets and P ≤m (X) the set of its subsets of cardinality at most m and [X → Y ] f the set of partial functions : X → Y having a finite domain.

A (functional) signature is a set F of function symbols, where f ∈ F has arity ρ(f ) ∈ N and T (F ) is the set of (finite) terms over F . The set of positions of a term t is P os(t) and positions are formally denoted by Dewey words. They are considered as the nodes of a labelled tree, and the terminology of trees will be used for expressing properties of positions in terms. The positions of t = f (a, g(a, b)) are the words ε that it is the root of t, also denoted by root t and the unique occurrence of f , 1 and 21, the occurrences of a, 2 the occurrence of g and 22, the occurrence of b. If t ′ is the subterm t/u of t issued from position u, then P os(t ′ ) is the set of words w such that uw ∈ P os(t). Positions of t are partially ordered by ≤ t such that u ≤ t v if and only if v is a prefix of u, i.e., v is an ancestor of u or is equal to it.

By a language, we mean a set of words or of terms, not to be confused with a logical language such as monadic second-order (MSO in short) logic.

Graphs and MSO logic.

A simple graph is, here, a finite directed graph without parallel edges and loops. These graphs will be used as incidence graphs of more general graphs, to be defined in the next section. We identify a simple graph G to the logical structure V G , edg G whose domain is V G , the set of vertices, and where edg G is the binary relation such that (x, y) ∈ edg G if and only if there is an edge from x to y, which we denote by x → G y, or by x → y if G is clear from the context.

MSO logic uses individual variables (x, y, z, ...) to denote vertices, and set variables (X, Y, Z, ...) to denote set of vertices. Quantifications over binary relations is not allowed. Rather than giving a formal syntax (see [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]), we take the example of 3-vertex colorability, expressed by the MSO formula ∃X, Y.α(X, Y ) where α(X, Y ) is the formula

X ∩ Y = ∅ ∧ ∀u, v.{edg(u, v) =⇒ [¬(u ∈ X ∧ v ∈ X) ∧¬(u ∈ Y ∧ v ∈ Y ) ∧ ¬(u / ∈ X ∪ Y ∧ v / ∈ X ∪ Y )]}.
The formula α(X, Y ) expresses that X, Y and V G -(X ∪ Y ) are the three color classes of a 3-vertex coloring of G. More generally, p-vertex colorability is expressible in a similar way. Other MSO expressible graph properties are connectedness, strong connectedness, planarity (via forbidden minors) and the existence of directed cycles.

Every MSO formula can be written so as to use only set variables and the atomic formulas X ⊆ Y (for set inclusion) and edg(X, Y ) (meaning that X = {x}, Y = {y} and x → y): for doing that, we replace the atomic formula x ∈ Y by X ⊆ Y where X denotes a singleton set. The property that X is singleton, denoted by Sgl(X), can be expressed itself in terms of inclusions. It is however useful to allow X = Y, X = ∅, Sgl(X), P artition(X 1 , ..., X p ) (meaning that (X 1 , ..., X p ) is a partition of the vertex set, where some sets X i may be empty) as atomic formulas. Furthermore, universal quantifications ∀X.ϕ are replaced by ¬∃X.¬ϕ. These syntactic constraints facilitate the construction of automata. Details are in [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

A sentence is a formula without free variables. It expresses a property of the considered graph.

Clique-width

Clique-width is a graph complexity measure, comparable to tree-width, that is defined from operations that construct simple graphs equipped with vertex labels. Let C be a finite or countable set of labels. A C-graph is a triple

G = V G , edg G , π G where π G is a mapping: V G → C. If π G (x) =
a we say to be short that x is an a-vertex.

We let F C be the following set of operations on C-graphs:

⊕ is the union of two disjoint C-graphs, relab a→b , for a = b, a, b ∈ C, is the the unary operation that changes every vertex label a into b, --→ add a,b , for a = b, a, b ∈ C, is the unary operation that adds an edge from each a-vertex x to each b-vertex y (unless we already have an edge from x to y),

∅ is a nullary symbol denoting the empty graph, and for each a ∈ C, the nullary symbol a denotes an isolated avertex.

The set F C is finite if C is finite. Every term t in T (F C ) defines a C-graph G = val(t) (a formal definition is in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]). Its vertex set is the set of positions in t of the nullary symbols a, a ∈ C. The clique-width of a graph G, denoted by cwd(G), is the least cardinality of a set of labels C such that G is isomorphic, up to vertex labels, to val(t) for some t in

T (F C ). It is clear that cwd(G) ≤ |V G | .
Let t ′ be a subterm t/u of t ∈ T (F C ) for u ∈ P os(t). The graph val(t ′ ) is, up to vertex labels, isomorphic to a subgraph G ′ of G = val(t). More precisely, let i u : P os(t ′ ) → P os(t) map w to uw (we recall that positions are Dewey words). Then i u (P os(t ′ )) = {v ∈ P os(t) | v ≤ t u} is the set of vertices of G ′ and i u is the isomorphism : val(t ′ ) → G ′ . If x → val(t ′ ) y, then i u (x) → G i u (y), however we may have i u (x) → G i u (y) without having x → val(t ′ ) y because an edge from i u (x) to i u (y) can be added to G ′ by an operation --→ add a,b above u in t. To simplify notation, we will use in the above case the following:

Convention about subterms: we will forget i u and consider val(t ′ ) as identical to the subgraph G ′ of G = val(t).

Hence, a node w of val(t ′ ) will be identified to the node i u (w) = uw of G. A term t in T (F C ) is irredundant if an operation --→ add a,b never "tries to create" an edge from an a-vertex x to a b-vertex y such that we already have x → y. In particular, t has no subterm of the form --→ add a,b (t ′ ) such that val(t ′ ) has an a-vertex x and a b-vertex y such that x → val(t ′ ) y. (The formal definition is more complicated because of relabellings). Every term can be made irredundant by an easy preprocessing [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] consisting in removing some operations --→ add a,b .

Lemma 2 : Let t ∈ T (F C ) be irredundant, u ∈ P os(t), t ′ = t/u. If a vertex x of val(t ′ ) has indegree p in this graph, then it has indegree p + q in val(t), where q is nonnegative and depends only on t, u and the label of x in val(t ′ ). The same holds for outdegrees. This statement uses our Convention about subterms. Its proof is straightforward from the definition (Definition 5 of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]). It follows that if t, t ′ , x, q are as in the statement and x ′ is another vertex of val(t ′ ) with same label and of indegree p ′ , then it has indegree p ′ + q in val(t).

We denote by twd(G) the tree-width of a graph G [START_REF] Bodlaender | A linear-time algorithm for finding tree-decompositions of small treewidth[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF][START_REF] Downey | Parameterized complexity[END_REF][START_REF] Downey | Fundamentals of parameterized complexity[END_REF].

Proposition 3 : For every simple graph G, we have cwd(G) ≤ 2 2twd(G)+2 + 1, and cwd(G) is not polynomially bounded in terms of twd(G), as it can be at least 2 k-1 for some graphs of tree-width 2k.

References for the proofs and comments are in [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], Proposition 2.114.

Finally, we explain how a term in T (F C ) can be enriched so as to define, not only a graph, but also vertex sets X 1 , ..., X p of this graph. We replace in F C each nullary symbol a by the nullary symbols (a, w) for all w ∈ {0, 1} p . We obtain a set of operations

F (p) C .
Let t ∈ T (F C ), X 1 , ..., X p ⊆ V val(t) and x ∈ V val(t) . We let w(x) be the sequence in {0, 1} p whose i-th element w(x)[i] is 1 if x ∈ X i and 0 otherwise. We replace in t a nullary symbol a at position u by (a, w(u)) (u is a vertex of val(t)). We obtain a term in T (F (p) C ) that defines the graph val(t) and also the p-tuple (X 1 , ..., X p ). We denote this term by t * (X 1 , ..., X p ). Conversely, every term t ′ in T (F (p) C ) is of this form, and we will also denote by val(t ′ ) the graph val(t).

If P is a property of graphs6 , then L P,C is defined as the set of terms t ∈ T (F C ) such that val(t) satisfies P . More generally, if P (X 1 , ..., X p ) is a property of vertex sets X 1 , ..., X p of graphs, then L P (X1,...,Xp),C is the set of terms t * (X 1 , ..., X p ) ∈ T (F (p) C ) such that P (X 1 , ..., X p ) holds in val(t).

If P (X 1 , ..., X p ) is expressed by an MSO formula ϕ(X 1 , ..., X p ), we denote by L ϕ(X1,...,Xp),C the language L P (X1,...,Xp),C .

Automata.

If ϕ(X 1 , ..., X p ) is an MSO formula and C is finite, then L ϕ(X1,...,Xp),C is a recognizable language, hence, is definable by a finite automaton. However, if C is infinite, L ϕ(X1,...,Xp),C can be defined by an infinite automaton that is usable in algorithms.

Definition 4: Fly-automata. (a) A set is effectively given if, either it is finite and the list of its elements is known, or it is countably infinite and its elements are bijectively encoded by words over {0, 1} (or another finite alphabet) that form a decidable set. Through this encoding, we have the notion of computable functions on effectively given sets. If D is effectively given, then so are D s for s ≥ 2, P f (D), the set of finite subsets of D and the set [D ′ → D] f of partial functions having a finite domain, where D ′ is effectively given. A signature F is effectively given if the set F is effectively given, the arity mapping ρ is computable and the least upper bound ρ(F ) of the arities is finite.

(b) Let F be an effectively given signature. A fly-automaton over F (in short, an FA over

F ) is a 4-tuple A = F, Q A , δ A , Acc A such that Q A is an effectively given set called the set of states, Acc A is a decidable subset of Q A called the
set of accepting states7 , and δ A is a computable function such that, for each tuple (f, q 1 , . . . , q ρ(f ) ) such that q 1 , . . . , q ρ(f ) ∈ Q A and f ∈ F, the set of states δ A (f, q 1 , . . . , q ρ(f ) ) is finite. The transitions are the pairs f [q 1 , . . . , q ρ(f ) ] → A q (and f → A q if f is nullary) such that q ∈ δ A (f, q 1 , . . . , q ρ(f ) ). We say that f [q 1 , . . . , q ρ(f ) ] → A q is a transition that yields q. We say that A is finite if F and Q A are finite, and we get the usual notion of a finite automaton.

(c) A run of an FA A on a term t ∈ T (F ) is a mapping r :

Pos(t) → Q A such that : if u is an occurrence of a function symbol f ∈ F and u 1 , ..., u ρ(f ) is the sequence of sons of u, then f [r(u 1 ), . . . , r(u ρ(f ) )] → A r(u); (if ρ(f ) = 0, the condition reads f → A r(u)).
For q ∈ Q A , we define L(A, q) as the set of terms t in T (F ) on which there is a run r of A such that r(root t ) = q. A run r on t is accepting if the state r(root t ) is accepting. We define L(A) := {L(A, q) | q ∈ Acc A } ⊆ T (F ). It is the language accepted (or recognized ) by A. A state q is accessible if L(A, q) = ∅. We denote by Q A ↾ t the set of states that occur in the runs on t and on its subterms, and by

Q A ↾ L the union of the sets Q A ↾ t for t ∈ L ⊆ T (F ).
We denote by run * A,t the mapping: P os(t) → P f (Q A ) that associates with every position u the finite set of states of the form r(root t/u ) for some run r on the subterm t/u of t issued from u. This mapping is computable and the membership in L(A) of a term in T (F ) is decidable because t ∈ L(A) if and only if the set run * A,t (root t ) contains an accepting state. Hence, whether all states of an FA are accessible or not does not affect the membership algorithm: the inaccessible states simply never appear in any run. There is no need to try to remove them, which is actually impossible in general, unless if A is finite. Removing them in the case of a "small" finite automaton permits to reduce the size of small the transition table.

We define ndeg A (t), the nondeterminism degree of A on t, as the maximal cardinality of run * A,t (u) for u in P os(t). We have ndeg A (t) ≤ |Q A ↾ t|. A sink is a state s such that, for every transition f [q 1 , . . . , q m ] → A q, we have q = s if q i = s for some i. If F has at least one symbol of arity at least 2, then an automaton has at most one sink. A state named Error (resp. Success) will always be a nonaccepting (resp. accepting) sink.

We say that an FA

B = H, Q B , δ B , Acc B is a subautomaton of an FA A if H ⊆ F , Q B ⊆ Q A , Acc B = Acc A ∩Q B and δ B (f, q 1 , . . . , q ρ(f ) ) = δ A (f, q 1 , . . . , q ρ(f ) ) if f ∈ H and q 1 , . . . , q ρ(f ) ∈ Q B . Then L(B) = L(A) ∩ T (H).
(d) Deterministic automata. An FA A is deterministic (implicitly, and complete) and if all sets δ A (f, q 1 , . . . , q ρ(f ) ) have cardinality 1. A deterministic FA A has, on each term t, a unique run denoted by run A,t ; we let q A (t) := run A,t (root t ). The mapping q A is computable.

The computation time of A on a term t is bounded by p. |t| where p bounds the time used for computing a transition.

For every fly-automaton A, there exists a deteministic FA B denoted by det(A) such that

Q B = P f (Q A ), run B,t = run * A,t and L(B) = L(A).
(See [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Proposition 45(2)). A run of B on a term t, that is, a bottom-up computation of run B,t , is called the determinized run of A. The maximal size of a state of det(A) on a term t is bounded by ndeg A (t).s where s is the maximal size of a state in

Q A ↾ t.
If the state Error is met at any point of the computation of a deterministic FA, the term can be immediately rejected. If the state Success is met at any point of the bottom-up computation of an FA, then the term can be immediately accepted. Hence, using sinks Success and Error in this way can shorten some computations.

(e) Direct and inverse images of automata. Let H and F be effectively given signatures. Let h : H → F be a relabelling, i.e., an arity preserving mapping having a computable inverse, that is, such that h -1 (f ) ⊆ H is finite and computable for each f . Let h be extended from

T (H) to T (F ) in the obvious way. If L ⊆ T (H), then h(L) := {h(t) | t ∈ L}. If A is an FA over H, then h(A) is the fly-automaton over F ( [7], Proposi- tion 45) obtained from A by replacing each transition f [q 1 , • • • , q ρ(f ) ] → A q by h(f )[q 1 , • • • , q ρ(f ) ] → q. We say that h(A) is the image of A under h. It is not deterministic in general, even if A is. We have h(L(A)) = L(h(A)

) (because h(A) has the same accepting states as A).

Let now h : T (H) → T (F ) be a computable relabelling.

If K ⊆ T (F ), then h -1 (K) := {t ∈ T (H) | h(t) ∈ K}. If A is an FA over F , we let h -1 (A) be the FA over H with transitions of the form f [q 1 , • • • , q ρ(f ) ] → q whenever h(f )[q 1 , • • • , q ρ(f ) ] → A q. We have L(h -1 (A)) = h -1 (L(A)). We call h -1 (A) the inverse image of A under h ( [7], Definition 17(h)). It is deterministic if A is so.
Automata from checking graph properties.

Theorem 5 : Let ϕ(X 1 , ..., X p ) be an MSO formula and C be an effectively given set of labels.

(1) There exists a deterministic FA A ϕ(X1,...,Xp),C over F C that recognizes the language L ϕ(X1,...,Xp),C . This automaton can be constructed by an algorithm.

(

) If C ′ ⊆ C is effectively given, then A ϕ(X1,...,Xp),C ′ is a subautomaton of A ϕ(X1,...,Xp),C . 2
(3) If C is finite, then A ϕ(X1,...,Xp),C is finite.

Proof : In [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] and related articles, we construct, for each finite set C, a finite deterministic automaton A ϕ(X1,...,Xp),C that accepts the recognizable language L ϕ(X1,...,Xp),C ⊆ T (F (p) C ). The construction is by induction on the structure of ϕ(X 1 , ..., X p ). We first construct automata for the atomic formulas, X ⊆ Y and edg(X, Y ) and also for some useful MSO properties such as X = ∅, Sgl(X), P artition(X 1 , . . . , X p ), Conn(X) expressing that the induced subgraph with vertex set X is connected, DirCycle expressing that the graph has an directed cycle. These constructions are based on our understanding of the considered properties.

Operations on FA "implement" the logical connectives ∨, ∧, ¬, ∃ and variable substitutions. The operation reflecting existential quantification consists in taking an image automaton, followed by a determinization. We have :

A ∃Xp.ϕ(X1,...,Xp),C = det(h(A ϕ(X1,...,Xp),C ))
where h :

F (p) C → F (p-1) C
deletes the last Boolean of w in each nullary symbol (a, w).

The transformation reflecting substitutions of variables consists in taking an inverse image: if ψ(X 1 , ..., X p ) is defined as ϕ(X i1 , ..., X im ) from ϕ(Y 1 , ..., Y m ), then the automaton A ψ(X1,...,Xp),C is an inverse image of A ϕ(Y1,...,Ym),C ( [7], Lemma 13 and Section 4.2.1). For an example, if ψ(X 1 , X 2 , X 3 ) is defined as edg(X 3 , X 1 ), we obtain A ψ(X1,X2,X3),C = h -1 (A edg(X1,X2),C ) where h((a, w 1 w 2 w 3 )) = (a, w 3 , w 1 ) for all w 1 , w 2 , w 3 ∈ {0, 1}. If ϕ(X 1 , ..., X p ) is the conjunction of two formulas for which we know automata, then the automaton for ϕ(X 1 , ..., X p ) is the product of these two automata, provided they are built for formulas having the same list of free variables. Variable substitution is useful to insure this technical point8 .

As explained in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Section 7.3.1, these constructions work for infinite sets of labels. The three assertions of Theorem 5 can be proved by induction on the structure of ϕ. To be more precise 9 , we define, for each set X and integer i ≥ 0, the set L i (X) as follows:

L 0 (X) := X, L i+1 (X) := L i (X) ∪ P f (L i (X)) ∪ (L i (X) × L i (X)). It is clear that X ⊆ Y implies L i (X) ⊆ L i (Y ) and that L i (X) is finite if X is finite. The set L i (X) is effectively given if X is.
For every MSO formula ϕ(X 1 , ..., X p ), one can define a finite set B and an integer i such that, for each effectively given set C of labels, one can construct a deterministic FA A ϕ(X1,...,Xp),C over F (p) C that recognizes the language L ϕ(X1,...,Xp),C and whose set of states Q(C) satisfies the following properties:

(i) Q(C) ⊆ L i (B ∪ C), (ii) Q(C ′ ) = Q(C) ∩ L i (B ∪ C ′ ) if C ′ ⊆ C, (iii) if ℓ : C → C ′ is
a bijection, then A ϕ(X1,...,Xp),C ′ is the FA obtained from A ϕ(X1,...,Xp),C by replacing in its states and transitions a by ℓ(a) for each a ∈ C (informally, ℓ yields an isomorphism of automata : A ϕ(X1,...,Xp),C → A ϕ(X1,...,Xp),C ′ ).

For an example, the automaton A edg(X,Y ),C constructed in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] has states in {Error, Ok} ∪ (P ≤1 (C) × P ≤1 (C)) that is a subset of L 2 ({Error, Ok} ∪ C). (As they are defined in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], states are in L 1 (B ∪ C) for some finite set B.)

It follows from Properties (i)-(iii) that we need only construct a single FA A ϕ(X1,...,Xp),C over F (p) C
where C is an infinite effectively given set of labels.

We will take C = N + . Running A ϕ(X1,...,Xp),C on terms in T (F

[k] ) can be decided in (FPT) time f (k). |t| for a function f depending only on ϕ(X 1 , ..., X p ). This function bounds the time for computing transitions. This gives a linear time recognition algorithm for graphs of clique-width at most some fixed k given by terms in T (F [k] ), but finding such terms takes (presently) cubic time. See [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] for details and references.

Properties of induced subgraphs

We apply to the relativization of a property P to a set X the notion of inverse image of an FA. If P is a graph property, we denote by P [X] the property of (G, X) where X is a set of vertices of G such that the induced subgraph G[X] satisfies P .

Let t ∈ T (F C ) define a graph G := val(t) and X be a set of vertices of G. (We recall that X is a set of occurrences of the nullary symbols a for a ∈ C.) Let t ′ ∈ T (F C ) be obtained from t by replacing each a by the nullary symbol ∅ (that denotes the empty graph) at its occurrences not in X. Then val(t ′ ) is G[X], the induced subgraph of G with vertex set X. (If t is irredundant, then so is t ′ ).

Then the subset

L P [X],C of T (F (1)
C ) is h -1 (L P,C ) where h : T (F

C ) → T (F C ) replaces in a term of T (F (1)
C ) each nullary symbol (a, 0) by ∅ and (a, 1) by a. Hence, if P is defined by an MSO sentence ϕ, then P [X] is defined by an MSO formula ϕ[X] with free variable X (we need not write this formula) and A ϕ[X],C is the inverse image by h of A ϕ,C . See Definition 4(e) and Lemma 15 of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], or [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

Irredundant terms

The set of irredundant terms in T (F C ) or in T (F (p) C ), denoted by L Irr , is recognized by an FA I ( [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]), whose states are Error and the finite subsets of C 2 . For each term t, q I (t) = Error if t is not irredundant and is {(π val(t) (x), π val(t) (y)) | x → val(t) y} if t is irredundant. Its transitions are easy to define.

We will construct automata A ϕ(X1,...,Xp),C intended to work correctly for irredundant terms. This means that L(A ϕ(X1,...,Xp),C ) ∩ L Irr = L ϕ(X1,...,Xp),C ∩ L Irr . If an input term is not irredundant, the answer of A ϕ(X1,...,Xp),C may be incorrect. By taking the product of A ϕ(X1,...,Xp),C and I, we can get an automaton that recognizes exactly L ϕ(X1,...,Xp),C ∩ L Irr . However, we will assume that the verification of irredundancy is done by the parsing algorithm that builds the term denoting the input graph to be processed by the automaton.

Incidence graphs

When the domain of the relational structure representing a graph is its vertex set, and since quantifications over binary relations are not allowed, MSO formulas cannot use quantified variables denoting sets of edges. In the incidence graph Inc(G) of a graph G, each edge of G is made into a vertex, hence an MSO formula over Inc(G) can be seen as an MSO formula using quantifications on sets of edges and it is called an MSO 2 formula intended to express a property of G. The formula : "there exists a set of edges that induces a directed cycle and goes through all vertices", expresses that the considered graph has a directed Hamiltonian cycle. This property is not expressible in MSO logic over the relational V G , edg G [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF].

Assertion Let G be a directed graph that can have parallel edges and loops. We define it as a triple

V G , E G , inc G such that V G is its set of vertices, E G is its set of edges (of course V G ∩ E G = ∅) and inc G ⊆ (V G × E G ) ∪ (E G × V G ) is such that, for u, v ∈ V G and e ∈ E G , we have (u, e) ∈ inc G and (e, v) ∈ inc G if e is an edge u → v.
We define Inc(G) as the simple, directed and bipartite graph identified to the relational structure V G ∪ E G , inc G , isv G where isv is unary and isv G (u) holds if and only if u ∈ V G . This relation is useful to distinguish the vertices from the edges in an arbitrary relational structure X, inc, isv isomorphic to

V G ∪ E G , inc G , isv G . It follows that G can be reconstructed up to isomorphism from any structure X, inc, isv isomorphic to V G ∪ E G , inc G , isv G . If G is undirected, then we define inc G ⊆ E G × V G
where (e, u) ∈ inc G if u is an end of e. In this case, the predicate isv G is not necessary because the vertices of G are the elements x of the domain such that inc(x, y) holds for no y. We will only discuss directed graphs in the sequel, leaving to the reader the easy task of simplifying our constructions so as to handle undirected graphs.

We will use some adaptations of MSO formulas and clique-width operations. We will consider a relational structure S = D S , inc S , isv S as a simple graph, also denoted by S, whose vertex set is D S , adjacency relation is inc S and that is equipped with a distinguished set of vertices isv S . In such a structure isomorphic to an incidence graph V G ∪ E G , inc G , isv G , we will call v-vertices the vertices of S that satisfy isv and represent the vertices of G and e-vertices the others, that represent its edges. It is FO expressible whether a relational structure S = D S , inc S , isv S is Inc(G) for some directed graph G. If this is true, then G is unique and its vertex set is isv G .

For expressing properties of such structures S, we will write MSO formulas with two types of set variables : X, Y, ... to denote sets of v-vertices and U, V, W to denote sets of e-vertices 10 . The atomic formulas will be of the forms X ⊆ Y, U ⊆ V, inc(X, U ) and inc(U, X); a formula X ⊆ U or inc(X, Y ) is not allowed, and the predicate isv will not occur in formulas, as it is replaced by the typing of variables, forcing them to denote either sets of vertices or sets of edges.

For constructing incidence graphs with clique-width operations, we will use pairs (C, D) of disjoint, effectively given sets of labels. Those in C will define the v-vertices, and those in D the e-vertices. The operations relab and --→ add will be those from F C∪D such that: We obtain an effectively given signature F C,D . Every term t ∈ T (F C,D ) defines a simple bipartite graph val(t) = H = V H , inc H , isv H where isv H (x) holds if and only if x is defined by a for some a ∈ C. We have inc H (x, y) if and only if x → val(t) y. We say that t is correct if H = Inc(G) for some graph G, whose vertex set is then necessarly isv H . This is the case if and only if each vertex having a label in D has indegree and outdegree 1. Proof : See [START_REF] Bouvier | Graphes et décompositions[END_REF][START_REF] Courcelle | Clique-width and tree-width of sparse graphs[END_REF] for the first three assertions. We have actually cwd(Inc(G))

≤ 2k +4 for G directed if we allow relabellings a → d such that a ∈ C and d ∈ D in terms defining Inc(G). Similarly, cwd(Inc(G)) ≤ k + 3 if G is undirected.
The last assertion holds because twd(G) ≤ twd(Inc(G)) and, by [START_REF] Gurski | The Tree-Width of Clique-Width Bounded Graphs Without K n[END_REF] (also in [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], Proposition 2.115), since Inc(G) has no subgraph isomorphic to K 3,3 , we have twd(Inc(G)) ≤ 6.cwd(Inc(G)) -1.

By the last assertion, the reduction of (b) to (a) in Theorem 1 does not work for the verification of MSO 2 properties of graphs of bounded clique-width. This is not a surprise because there are MSO 2 properties that are not FPT for clique-width unless FPT = W[1] ( [START_REF] Fomin | Algorithmic lower bounds for problems parameterized with clique-width[END_REF]) which is unlikely, similarly to N = NP (see [START_REF] Downey | Parameterized complexity[END_REF][START_REF] Downey | Fundamentals of parameterized complexity[END_REF] for the classes FPT and W [START_REF] Bodlaender | A linear-time algorithm for finding tree-decompositions of small treewidth[END_REF]).

In order to represent in terms sets of vertices X 1 , ..., X p and sets of edges U 1 , ..., U m , we replace in F C,D each nullary symbol a, for a ∈ C, by the nullary symbols (a, w) for w ∈ {0, 1} p and each nullary symbol d, for d ∈ D, by the symbols (d, w) for w ∈ {0, 1} m . We obtain a signature

F (p,m) C,D
and, for each MSO formula ϕ(X 1 , ..., X p , U 1 , ..., U m ), a representing language L ϕ(X1,...,Xp,U1,...,Um),C,D ⊆ T (F (p,m) C,D ) consisting of the correct terms t that encode an assignment to X 1 , ..., X p , U 1 , ..., U m for which ϕ holds in val(t). We will construct FA that recognize these languages.

Denotation of subgraphs

Let G be a graph,

X ⊆ V G and U ⊆ E G . We let Inc(G)[X, U ] := X ∪ U, inc G ∩ (X ∪ U ) 2 , isv G ∩ (X ∪ U ) .
This structure is an incidence graph Inc(H) if and only if the ends of all "edges" u ∈ U are in X. If this is the case, then V H = X, E H = U and H is a subgraph of G. We call Subgraph(X, U ) this property of (G, X, U ). Assume now that Inc(G) = val(t) where t ∈ T (F C,D ), and X, U as above are sets of occurrences in t of nullary symbols respectively in C and in D. Let t[X, U ] be obtained from t by replacing by ∅ (denoting the empty graph) the nullary symbols at their occurrences not in

X ∪ U . It is clear that val(t[X, U ]) = Inc(G)[X, U ].
Then t[X, U ] is a correct term if and only if Inc(G)[X, U ] is an incidence graph. The set of correct terms t[X, U ] ∈ T (F

(1,1) C,D ) is h -1 (L)
where L is the set of correct terms in T (F C ) and h maps (a, 1) to a and (a, 0) to ∅ for a ∈ C ∪ D. We will define L by an FA A CT . The property Subgraph(X, U ) will thus be defined by its inverse image, h -1 (A CT ).

Automata

In this section, we construct FA to check MSO 2 properties of directed graphs. It is easy to modify them in order to check similar properties of undirected graphs. These automata will be deterministic and designed so as to work correctly on irredundant terms in T (F C,D ) for pairs (C, D) of disjoint effectively given sets of labels.

They will be linear FPT-FA, meaning that their computation times are linear in the size of input terms over fixed finite subsignatures of F C,D .

Their constructions are the same for C ∪ D either finite or infinite, as explained after Theorem 5. We will construct FA for unspecified pairs C, D, either C = N + and D = {-n | n ∈ N + } (for being concrete) or finite subsets of them. The complexities of our automata will appear from their numbers of states when C and D are finite. An FA constructed from a formula ϕ will be denoted by A ϕ without reference to C, D.

Correct terms

Every term t ∈ T (F C,D ) defines a simple bipartite graph val(t), and is correct if and only if val(t) is an incidence graph. A C-vertex of val(t) is a vertex having a label in C, a D-vertex is one having a label in D. These definitions apply even if t is not correct.

We describe an FA A CT that checks the correctness of terms in T (F C,D ), assumed to be irredundant. Its states are the sink Error and the 6-tuples (γ 1 , γ 2 , δ 00 , δ 01 , δ 10 , δ 11 ) ∈ P f (C) 2 × P f (D) 4 such that γ 1 ∩ γ 2 = ∅ and δ 00 , δ 01 , δ 10 , δ 11 are pairwise disjoint. We will denote (δ 00 , δ 01 , δ 10 , δ 11 ) by -→ δ . At the root of a term t ∈ T (F C,D ), A CT reaches the state (γ 1 , γ 2 , -→ δ ) if and only if, we have in val(t):

(i) γ 1 is the set of labels a ∈ C that label a single C-vertex.

(ii) γ 2 is the set of labels a ∈ C that label at least two C-vertices,

(iii)

-→ δ = (δ 00 , δ 01 , δ 10 , δ 11 ) where for i, j ∈ {0, 1}, δ ij is the set of labels of D-vertices of indegree i and outdegree j, (iv) the sets δ 00 , δ 01 , δ 10 , δ 11 defined in (iii) are pairwise disjoint, (v) no D-vertex has indegree or outdegree 2 or more.

It reaches the state Error if (iv) or (v) does not hold. The accepting states are the tuples (γ 1 , γ 2 , -→ δ ) such that δ 00 = δ 01 = δ 10 = ∅. For any subterm t of a correct term, Condition (iv) is necessary by Lemma 2 and Condition (v) also, because the D-vertices in an incidence graph represent edges. Transitions are listed in Table 1. In order to simplify the table, we use the following notations and conventions. First, we do not list the transitions with Error on the left side as they always yield Error (cf. Definition 4(c)). Furthermore, a, b denote elements of C and d, e denote elements of D,

d ∈ -→ δ means d ∈ δ 00 ∪ δ 01 ∪ δ 10 ∪ δ 11 , Disj( -→ δ ) means that δ 00 , δ 01 , δ 10 , δ 11 are pairwise disjoint, -→ δ ∪ -→ δ ′ := (δ 00 ∪ δ ′ 00 , δ 01 ∪ δ ′ 01 , δ 10 ∪ δ ′ 10 , δ 11 ∪ δ ′ 11 ), γ[a → b]

Transitions

Conditions

∅ → -→ ∅ a → ({a}, - → ∅ ) d → (∅, ∅, {d}, - → ∅ ) relab a→b [(γ 1 , γ 2 , -→ δ )] → (γ 1 , γ 2 , -→ δ ) a / ∈ γ 1 ∪ γ 2 relab a→b [(γ 1 , γ 2 , -→ δ )] → (γ 1 , γ 2 , -→ δ ) {a, b} ⊆ γ 1 ∪ γ 2 , γ 1 = γ 1 -{a, b} and γ 2 = γ 2 ∪ {b} -{a} relab a→b [(γ 1 , γ 2 , -→ δ )] → (γ 1 , γ 2 , -→ δ ) a ∈ γ 1 ∪ γ 2 , b / ∈ γ 1 ∪ γ 2 , γ 1 = γ 1 [a → b] and γ 2 = γ 2 [a → b] relab d→e [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , - → δ [d → e]) Disj( -→ δ [d → e]) relab d→e [(γ 1 , γ 2 , - → δ )] → Error ¬Disj( -→ δ [d → e]) --→ add a,d [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , - → δ ) a / ∈ γ 1 ∪ γ 2 or d / ∈ -→ δ --→ add a,d [(γ 1 , γ 2 , - → δ )] → Error (a ∈ γ 2 and d ∈ -→ δ ) or a ∈ γ 1 and d ∈ δ 10 ∪ δ 11 --→ add a,d [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , - → δ ′ ) a ∈ γ 1 and d ∈ δ 00 ∪ δ 01 , δ ′ 00 = δ 00 -{d}, δ ′ 01 = δ 01 -{d}, δ ′ 10 = if d ∈ δ 00 then δ 10 ∪ {d} else δ 10 , δ ′ 11 = if d ∈ δ 01 then δ 11 ∪ {d} else δ 11 . ⊕[(γ 1 , γ 2 , -→ δ ), (γ ′ 1 , γ ′ 2 , -→ δ ′ )] → (γ 1 , γ 2 , -→ δ ∪ -→ δ ′ ) Disj( -→ δ ∪ -→ δ ′ ), γ 2 = γ 2 ∪ γ ′ 2 ∪ (γ 1 ∩ γ ′ 1 ), γ 1 = (γ 1 -(γ ′ 1 ∪ γ ′ 2 )) ∪ (γ ′ 1 -(γ 1 ∪ γ 2 )). ⊕[(γ 1 , γ 2 , -→ δ ), (γ ′ 1 , γ ′ 2 , -→ δ ′ )] → Error ¬Disj( -→ δ ∪ -→ δ ′ )
Table 1: Some transitions of A CT .

Remarks: (1) We do not list the transitions relative to --→ add d,a because they are similar to those of --→ add a,d . (2) For the transitions relative to --→ add a,d , there are three cases. It is clear that the conditions on a and d are mutually exclusive and cover all possibilities.

(3) The transition --→ add a,d [(γ 1 , γ 2 , -→ δ )] → Error is correct because the input term is assumed irredundant. Without irredundancy, it may happen that a ∈ γ 1 and d ∈ δ 11 ∪ δ 10 but --→ add a,d has no effect because there are already edges from the a-vertex to the d-vertex (or to several d-vertices), so that the d-vertex (or vertices) still have indegree 1. In that case, the transition should yield (γ 1 , γ 2 , -→ δ ). ( 4 (5) Some states (γ 1 , γ 2 , -→ δ ) are not accessible: for example, those such that γ 1 ∪ γ 2 = ∅ and δ 01 ∪ δ 10 ∪ δ 11 = ∅.

If C ∪ D is finite, k = |C| and ℓ = |D|, the number of states is 3 k .5 ℓ + 1 and the size of a state is O(k + ℓ). Each transition is computable in time O(k + ℓ) (our time complexity evaluations are based on straightforward data structures). We obtain a linear FPT-FA.

As noted previously, h -1 (A CT ) = A Subgraph(X,U) where h maps (a, 1) to a and (a, 0) to ∅ for each a ∈ C ∪ D.

Adjacency in incidence graphs

In the case of MSO graph properties reviewed in Section 2 the atomic formula edg(X, Y ) is checked by an FA over F

(2)

C that has k 2 + k + 3 states if C is finite of cardinality k.
This construction is easily applicable to the atomic formula inc(X, U ) (resp. inc(U, X)) stating that X consists of one vertex x and U of one edge u whose tail (resp. head) is x. We will describe A inc(X,U) at the end of the section for purpose of comparison.

In MSO formulas expressing properties of Inc(G), the property edg(X, Y ) is no longer atomic; it is expressed by ∃U.(inc(X, U ) ∧ inc(U, Y )). We can apply the general construction of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] to this formula, but, in view of practical constructions, it is useful to define directly an automaton A edg(X,Y ) over F C,D ). As for irredundancy, we will assume that correctness is guaranteed by the parsing algorithm.

The states of A edg(X,Y ) are Ok, Error and the tuples (γ

1 , γ 2 , -→ δ ) ∈ P ≤1 (C) 2 × P f (D) 3 such that the components of -→ δ = (δ, δ 1 , δ 2 ) verify the condition δ 1 ∪δ 2 ⊆ δ. Let t ∈ T (F (2,0)
C,D ) be a correct and irredundant term. It defines an incidence graph val(t) = Inc(G) and two sets of vertices X, Y of G. Every subterm t ′ of t is irredundant and defines a bipartite graph val(t ′ ) that we consider as a subgraph of val(t) (by our Convention about subterms, cf. Section 2). It may not be an incidence graph, because some D-vertices may be of indegree or outdegree 0. Let

X ′ = X ∩ V val(t ′ ) , Y ′ = Y ∩ V val(t ′ ) .
Their sets of labels are π val(t ′ ) (X ′ ) and π val(t ′ ) (Y ′ ), both subsets of C. To simplify notation we will denote π val(t ′ ) by π and → val(t ′ ) (the edge relation) by →. At the root of t ′ , A edg(X,Y ) reaches the following state:

Error if and only if X ′ or Y ′ has cardinality 2 or more, Ok if and only if X ′ = {x}, Y ′ = {y} for some x, y such that x → u → y for some D-vertex u (so that x → G y), (γ 1 , γ 2 , -→ δ ) otherwise, and we have :

γ 1 = π(X ′ ) and |X ′ | ≤ 1, γ 2 = π(Y ′ ) and |Y ′ | ≤ 1,
δ is the set of labels of D-vertices,

δ 1 = π(Out(X ′ )) ⊆ δ, δ 2 = π(In(Y ′ )) ⊆ δ,
where Out(X ′ ) (resp.

In(Y ′ )) is the set of D-vertices u such that X ′ → u (resp. u → Y ′ ).
The accepting state is Ok.

Transitions Conditions ∅ → -→ ∅ (a, 00) → -→ ∅ (a, 10) → ({a}, - → ∅ ) (a, 01) → (∅, {a}, - → ∅ ) (a, 11) → ({a}, {a}, - → ∅ ) d → (∅, ∅, {d}, - → ∅ ) --→ add a,d [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , - → δ ) a / ∈ γ 1 or d / ∈ δ --→ add a,d [(γ 1 , γ 2 , - → δ )] → Ok a ∈ γ 1 and d ∈ δ 2 --→ add a,d [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , δ, δ ′ 1 , δ 2 ) a ∈ γ 1 , d ∈ δ -δ 2 , δ ′ 1 := δ 1 ∪ {d} --→ add a,d [Ok] → Ok relab a→b [(γ 1 , γ 2 , -→ δ )] → (γ ′ 1 , γ ′ 2 , -→ δ ) γ ′ 1 := γ 1 [a → b], γ ′ 2 := γ 2 [a → b] relab a→b [Ok] → Ok relab d→e [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , - → δ ′ ) -→ δ ′ := -→ δ [d → e] ⊕[Ok, Ok] → Error ⊕[(γ 1 , γ 2 , -→ δ ), Ok] → Error γ 1 = ∅ or γ 2 = ∅ ⊕[(γ 1 , γ 2 , -→ δ ), Ok] → Ok γ 1 = γ 2 = ∅ ⊕[(γ 1 , γ 2 , -→ δ ), (γ ′ 1 , γ ′ 2 , -→ δ ′ )] → Error |γ 1 | + |γ ′ 1 | ≥ 2 or |γ 2 | + |γ ′ 2 | ≥ 2 ⊕[(γ 1 , γ 2 , -→ δ ), (γ ′ 1 , γ ′ 2 , -→ δ ′ )] otherwise → (γ 1 ∪ γ ′ 1 , γ 2 ∪ γ ′ 2 , -→ δ ∪ -→ δ )
Table 2 : Some transitions of A edg(X,Y )

Remarks : (1) The transitions ⊕[(∅, ∅, -→ δ ), Ok] → Ok "loose" the value -→ δ . This value is not needed after Ok is obtained. The only thing that remains to be checked is that the sets X, Y are singletons. It follows that we have transitions such as

⊕[Ok, Ok] → Error and ⊕[(γ 1 , γ 2 , - → δ ), Ok] → Error if γ 1 = ∅ or γ 2 = ∅. The state Ok is not a sink.
(2) Let us comment on δ 2 . A D-vertex u such that u → Y ′ corresponds either to a partially defined edge with head in Y ′ and whose tail is not yet found or to an edge from a vertex not in X ′ to a vertex in Y ′ . The set δ 2 is the set of their labels. The transition --→ add a,d [(γ 1 , γ 2 , -→ δ )] → Ok when γ 1 = {a} and d ∈ δ 2 is correct because, since t is assumed to be a correct term, a D-vertex u with label d cannot correspond to an edge from a vertex not in X ′ to a vertex in Y ′ . Hence, u → y ∈ Y ′ and the operation --→ add a,d creates an edge from the vertex of X ′ to y.

(3) Some states (γ 1 , γ 2 , -→ δ ) are not accessible, for example, those such that

γ 1 = ∅ and δ 1 = ∅. If C ∪ D is finite, k = |C| and ℓ = |D|, the number of states is (k + 1) 2 .5 ℓ + 2 and the size of a state is O(log(k) + ℓ)). Each transition is computable in time O(log(k) + ℓ))
. We obtain a linear FPT-FA.

Comparison with the automaton constructed with Theorem 4.

The automaton

A inc(X,U) over F (1,1)
C,D obtained by a straightforward adaptation of the automaton A edg(X,Y ) over F

C defined in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]. It has states Ok, Error and the pairs (γ, δ) in

P ≤1 (C) × P ≤1 (D). Let t * (X, U ) ∈ T (F (1,1)
C,D ) be correct and irredundant. It defines an incidence graph val(t) = Inc(G), a set X of C-vertices and a set U of D-vertices. Every subterm t ′ of t defines a bipartite graph val(t ′ ). Let

X ′ = X ∩ V val(t ′ ) , U ′ = U ∩ V val(t ′ ) . At the root of t ′ * (X ′ , U ′ ), A inc(X,U) reaches the following state:
Error if and only if X ′ or U ′ has cardinality 2 or more, Ok if and only if X ′ = {x}, U ′ = {u} and x → val(t ′ ) u, (γ, δ) otherwise where

γ = π val(t ′ ) (X ′ ) and |X ′ | ≤ 1, δ = π val(t ′ ) (U ′ ) and |U ′ | ≤ 1.
The accepting state is Ok and the transitions are easy to define. If C ∪ D is finite, k = |C| and ℓ = |D|, the number of states is (k + 1).(ℓ + 1) + 2.

Similarly, we have A inc(U,Y ) with same set of states, except that we write

(δ, γ) = (π val(t ′ ) (U ′ ), π val(t ′ ) (Y ′ )) ∈ P ≤1 (D) × P ≤1 (C) instead of (γ, δ).
Let us now consider edg(X, Y ) defined by ∃U.(inc 1 (X, U, Y ) ∧ inc 2 (X, U, Y )) where inc 1 (X, U, Y ) is defined as inc(X, U ) with extra (useless) variable Y and inc 2 (X, U, Y )) where inc 2 (X, U, Y ) is defined as inc(U, Y ). These useless variables are added so that the two parts of the conjunction inc 1 (X, U, Y ) ∧ inc 2 (X, U, Y ) have the same free variables.

The automaton

B := A inc1(X,U,Y )∧inc2(X,U,Y ) over F (2,1)
C,D is thus the product of A inc1(X,U,Y ) and A inc2(X,U,Y ) . Furthermore, A inc1(X,U,Y ) and A inc2(X,U,Y ) have the sames states as, respectively, A inc(X,U) and A inc(U,Y ) . (See the remarks on variable substitutions after Theorem 5). The construction of Theorem 5 replaces B by a nondeterministic FA C over

F (2,0) C,D that characterizes ∃U.(inc 1 (X, U, Y ) ∧ inc 2 (X, U, Y )).
The FA B has ((k + 1).(ℓ + 1) + 2) 2 states if k = |C| and ℓ = |D|, which gives more than 2 k 2 .ℓ 2 states for the deterministic automaton det(C) obtained from C. However, some states of B are inaccessible, for instance, those of the form ((γ, δ), (δ ′ , γ ′ )) where δ = δ ′ . Furthermore, the states of det(C) are more complicated to write than those of A edg(X,Y ) are in the set {Ok, Error} ∪ (P ≤1 (C) 2 × P f (D) 3 ) whereas those of det(C) are in P f ([{Ok, Error} ∪ (P ≤1 (C) × P ≤1 (D))] 2 ).

This observation motivates our interest for "direct constructions" of FA for properties related to adjacency, as these properties are defined with edg(X, Y ).

Links and domination

We consider the following four properties based on adjacency, ordered by increasing complexity, measured by the sizes of the automata we will construct (G is the graph whose incidence graph is val(t) and t the given correct term) :

Link ∃∃ (X, Y ) meaning that X → G Y, i.e., x → G y for some x ∈ X and y ∈ Y , Link ∀∃ (X, Y ) meaning that for all x ∈ X there is y ∈ Y such that x → G y, (Y dominates X for ← G ),
Link ∀∀ (X, Y ) meaning that x → G y for all x ∈ X and y ∈ Y , Link ∃∀ (X, Y ) meaning that there is x ∈ X such that x → G y for all y ∈ Y (x dominates Y for → G ).

The property that X induces a complete directed graph (with loops on all vertices) is expressed by Link ∀∀ (X, X). That X is stable, i.e., that the induced graph G[X] has no edge, is expressed by ¬Link ∃∃ (X, X).

The logical expressions of these properties by MSO formulas interpreted in V G ∪ E G , inc G have the following respective quantifier structures: ∃∃∃, ∀∃∃, ∀∀∃ and ∃∀∃ with 0, 1,1 and 2 quantifier alternations. We will construct FA or sketch their constructions. Their sets of states will reflect the differences of quantifier alternations. Notation is as for the definition of A edg(X,Y ) . All FA will be intended to run on correct and irredundant terms in T (F

(2,0) C,D ).
The FA A Link ∃∃ (X,Y ) It is similar to A edg(X,Y ) with some interesting differences. It is simpler to describe because it need not check that X and Y are singletons, however, it has more states. Its states are the accepting sink Success and the tuples

(γ 1 , γ 2 , -→ δ ) ∈ P f (C) 2 × P f (D) 3 such that δ 1 ∪ δ 2 ⊆ δ. As above for A edg(X,Y ) , if t ′ * (X ′ , Y ′ ) is a subterm of a correct irredundant term t * (X, Y ) ∈ T (F (2,0) C,D ) where X ′ = X ∩ V val(t ′ ) and Y ′ = Y ∩ V val(t ′ )
, then A Link ∃∃ (X,Y ) reaches the following state at the root of t ′ * (X ′ , Y ′ ) :

Success if and only if x → u → y for some x ∈ X ′ and y ∈ Y ′ and u (so that X ′ → G Y ′ ); otherwise (γ 1 , γ 2 , -→ δ ) where :

γ 1 = π(X ′ ) ⊆ C, γ 2 = π(Y ′ ) ⊆ C,
δ is the set of labels of D-vertices,

δ 1 = π(Out(X ′ )) ⊆ δ, δ 2 = π(In(Y ′ )) ⊆ δ.
Some transitions are listed in Table 3 (the others are easy to define or similar to those for A edg(X,Y ) ).

Transitions

Conditions --→ add a,d [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , - → δ ) a / ∈ γ 1 or d / ∈ δ --→ add a,d [(γ 1 , γ 2 , - → δ )] → Success a ∈ γ 1 and d ∈ δ 2 --→ add a,d [(γ 1 , γ 2 , - → δ )] → (γ 1 , γ 2 , δ, δ 1 ∪ {d}, δ 2 ) a ∈ γ 1 , d ∈ δ -δ 2 ⊕[(γ 1 , γ 2 , -→ δ ), (γ ′ 1 , γ ′ 2 , -→ δ ′ )] → (γ 1 ∪ γ ′ 1 , γ 2 ∪ γ ′ 2 , -→ δ ∪ -→ δ ′ )
Table 3: Some transitions of A Link ∃∃ (X,Y ) .

The accepting state is the sink Success. All transitions with Success on the left yield Success. (In A edg(X,Y ) , we use a state Ok, that looks like Success but is not a sink.) See Remark (2) relative to A edg(X,Y ) to verify the validity of the transition to Success in this table. There is no Error state.

If C ∪ D is finite, k = |C| and ℓ = |D|, the number of states is 4 k .5 ℓ + 1. These states have size O(k + ℓ). Each transition is computed in time O(k + ℓ). We obtain a linear FPT-FA.

The FA A Link ∀∀ (X,Y )
Notation is as for the previous automaton. The state at the root of t ′ will contain the relation :

θ := {(π(x), π(y)) | x ∈ X ′ , y ∈ Y ′ and ∄u.(x → u → y)},
and will be accepting if and only if this relation is empty, because θ indicates the existence of "missing" edges. However, additional information will be needed for the construction of transition rules.

A state of A Link ∀∀ (X,Y ) is a 4-tuple of finite sets (δ, ∆, Λ, Θ) such that:

δ ⊆ D, ∆ ⊆ C × P f (δ), Λ ⊆ P f (δ) × C and Θ ⊆ ∆ × Λ ⊆ C × P f (D) × P f (D) × C.
The state at the root of t ′ * (X ′ , Y ′ ) is (δ, ∆, Λ, Θ) such that :

δ is the set of labels of D-vertices,

∆ = {(π(x), π(Out(x)) | x ∈ X ′ }, Λ = {(π(In(y)), π(y)) | y ∈ Y ′ }, Θ = {(π(x), π(Out(x)), π(In(y)), π(y)) | x ∈ X ′ , y ∈ Y ′ and ∄u.(x → u → y)}.
A tuple (a, η, η ′ , b) in Θ encodes the following information about a "missing edge" from some x ∈ X ′ to some y ∈ Y ′ : a = π(x), b = π(y), η contains the labels of the partially defined edges with tail x and similarly, η ′ contains the labels of those, partially defined, with head y. An edge from x to y in the graph G whose incidence graph is val(t) can be created by

--→ add a,d if d ∈ η ′ or by --→ add d,b if d ∈ η (
assuming that labels a, d are not modified above t ′ ).

Remark : The states of A Link ∀∀ (X,Y ) contain more information than those of A Link ∃∃ (X,Y ) because π(X ′ ) = {a ∈ C | (a, η) ∈ ∆ for some η}, π(Out(X ′ )) is the union of the sets η such that (a, η) ∈ ∆ for some a and similarly for π(Y ′ ) and π(In(Y ′ )). Hence, the state of A Link ∃∃ (X,Y ) at some position u can be computed from that of A Link ∀∀ (X,Y ) at u. One could formalize that by the existence of a homomorphism : A Link ∀∀ (X,Y ) → A Link ∃∃ (X,Y ) .

The accepting states are those such that Θ = ∅ because, at the root of a correct term t, θ is the set of pairs (a, b) such that (a, η, η ′ , b) ∈ Θ for some η, η ′ . Transitions are as follows. We begin with the easier cases.

∅ → -→ ∅ (a, 11) → (∅, {(a, ∅)}, {(∅, a)}, {(a, ∅, ∅, a)}), (a, 10) → (∅, {(a, ∅)}, - → ∅ ), (a, 01) → (∅, {(∅, a)}, - → ∅ ), (a, 00) → -→ ∅ , d → ({d}, -→ ∅ ).
Transitions for relabellings are straightforward:

relab x→y [(δ, ∆, Λ, Θ)] → (δ ′ , ∆ ′ , Λ ′ , Θ ′ ) where δ ′ := δ[x → y]
and similarly for the other components.

Transitions for disjoint union are as follows:

⊕[(δ 1 , ∆ 1 , Λ 1 , Θ 1 ), (δ 2 , ∆ 2 , Λ 2 , Θ 2 )] → (δ 1 ∪ δ 2 , ∆ 1 ∪ ∆ 2 , Λ 1 ∪ Λ 2 , Θ 1 ∪ Θ 2 ∪ Θ ′ ) where Θ ′ := {(a, η, η ′ , b) | ((a, η) ∈ ∆ 1 and (η ′ , b) ∈ Λ 2 ) or ((a, η) ∈ ∆ 2 and (η ′ , b) ∈ Λ 1 ))}.
Transitions for edge addition are as follows:

--→ add a,d [(δ, ∆, Λ, Θ)] → q where we have: q := (δ, ∆, Λ, Θ) if a does not occur in ∆ or d / ∈ δ, q := (δ, ∆ ′ , Λ, Θ ′ ) otherwise, where :

∆ ′ is defined from ∆ by replacing each pair (a, η) by (a, η ∪{d});

Θ ′ is defined from in Θ as follows :

a tuple of the form (a, η, η ′ , b), for any b ∈ C is deleted if d ∈ η ′ ; otherwise it is replaced by (a, η ∪ {d}, η ′ , b).
In the transitions for --→ add a,d , we cannot have a and d occurring both in ∆ because the input term t is assumed irredundant and correct. If d belongs to η ′ , then it labels vertices of indegree 0 because t is correct and irredundant.

If C∪D is finite, k = |C| and ℓ = |D|, the number of states is at most 2 ℓ .5 k 2 4 ℓ . However, there are less accessible states. Counting them precisely seems difficult and is actually not important for our use of FA. The size of a state is O(k 2 .4 ℓ ). We obtain a linear FPT-FA.

The FA A Link ∀∃ (X,Y )

The construction is similar to the previous one. The set of states is a bit smaller, although of similar type. Notation is as in the previous cases. The states are sets of 5-tuples of sets (γ, δ, λ, ∆, Θ)

∈ P f (C) × P f (D) 2 × P f (C × P f (D)) 2 such that: γ ⊆ C, δ ⊆ D, λ ⊆ δ and Θ ⊆ ∆ ⊆ C × P f (δ). The state at the root of t ′ * (X ′ , Y ′ ) is (γ, δ, λ, ∆, Θ) such that : γ = π(Y ′ ), δ is the set of labels of D-vertices, λ = π(In(Y ′ )) ⊆ δ, ∆ = {(π(x), π(Out(X ′ ))) | x ∈ X ′ }, Θ = {(π(x), π(Out(X ′ ))) | x ∈ X ′ and ∄u.(x → u → Y ′ )}.
The accepting states are those such that Θ = ∅.

Transitions for disjoint union are as follows:

⊕[(γ 1 , δ 1 , λ 1 , ∆ 1 , Θ 1 ), (γ 2 , δ 2 , λ 2 , ∆ 2 , Θ 2 )] → (γ 1 ∪ γ 2 , δ 1 ∪ δ 2 , λ 1 ∪ λ 2 , ∆ 1 ∪ ∆ 2 , Θ ′ 1 ∪ Θ ′ 2 ).
where:

Θ ′ 1 := if γ 2 = ∅ then Θ 1 else ∆ 1 , and Θ ′ 2 := if γ 1 = ∅ then Θ 2 else ∆ 2 .
The most complicated transitions are for edge addition:

--→ add a,d [(γ, δ, λ, ∆, Θ)] → q where the following holds: if a does not occur in ∆ or d / ∈ δ, then q := (γ, δ, λ, ∆, Θ), otherwise q := (γ, δ, λ, ∆ ′ , Θ ′ ), where ∆ ′ , Θ ′ are defined as follows from ∆ and Θ : a pair (a, η) in ∆ is replaced by (a, η ∪ {d}), a pair (a, η) in Θ is deleted if d ∈ λ and replaced by (a, η ∪ {d}) otherwise.

--→ add d,b [(γ, δ, λ, ∆, Θ)] → q where the following holds: if b / ∈ γ or d / ∈ δ, then q = (γ, δ, λ, ∆, Θ), otherwise q := (γ, δ, λ ∪ {d}, ∆, Θ ′ ) where Θ ′ is defined from Θ by deleting each pair (a, η) such that if d ∈ η.

If C ∪ D is finite, k = |C| and ℓ = |D|, the number of states is bounded by 2 k 3 ℓ .3 k.2 ℓ . The size of a state is O(k.2 ℓ ) and the computation time of a transition is O(k.2 ℓ ). We obtain a linear FPT-FA.

The FA A Link ∃∀ (X,Y )
This automaton is more complicated than the two previous ones, as it checks a formula with two quantifier alternations instead of one. Its states are triples of finite sets (δ, Λ, Ξ) such that:

δ ⊆ D, Λ ⊆ P f (δ) × C, Ξ ⊆ C × P f (δ) × P f (Λ) ⊆ C × P f (D) × P f (P f (D) × C).
The state at the root of t ′ * (X ′ , Y ′ ) is (δ, Λ, Ξ) such that : δ is the set of labels of D-vertices,

Λ = {(π(In(y)), π(y)) | y ∈ Y ′ }, Ξ is the set of triples (π(x), π(Out(x)), {(π(In(y)), π(y)) | y ∈ Y ′ , ∄u.(x → u → y)}) for all x ∈ X ′ .
The accepting states are those such that Ξ contains a triple of the form (a, Λ, ∅). We show some transitions.

⊕[(δ 1 , Λ 1 , Ξ 1 ), (δ 2 , Λ 2 , Ξ 2 )] → (δ 1 ∪ δ 2 , Λ 1 ∪ Λ 2 , Ξ 1 ∪ Ξ 2 ∪ Ξ ′ )
where Ξ ′ is the set of triples are of the form (a, η, Φ ∪ Λ 2 ) for (a, η, Φ) ∈ Ξ 1 and of the form (a, η, Φ ∪ Λ 1 ) for (a, η, Φ) ∈ Ξ 2 .

The other transitions are easy to define, by the same methods as for the previous automata

. If C ∪ D is finite, k = |C| and ℓ = |D|, the number of states is bounded by 2 ℓ .2 k.2 ℓ .2 k.2 ℓ .2 k.2 ℓ
. The size of a state is O(2 k.2 ℓ ) and the computation time of a transition is O(2 k.2 ℓ ).

Table 4 compares the bounds on the sizes of the states for the linear FPT-FA we just constructed for incidence graphs to the bounds for those constructed in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] for "ordinary" graphs. For terms obtained by Proposition 6 from a treedecomposition of width p, we have k = 2 and ℓ ≤ 2p + 3. So are, for instance, for a directed graph G, connectedness and strong connectedness, the properties that all its vertices are of outdegree at most p, that G has a directed cycle, or an undirected cycle (a cycle in which edge directions do not matter), or that G has a path from vertex x to vertex y.

Property

MSO MSO 2 edg O(log(k)) O(log(k) + ℓ) Link ∃∃ O(k) O(k + ℓ) Link ∀∃ O(k) O(k.2 ℓ ) Link ∀∀ O(k 2 ) O(k.2 ℓ ) Link ∃∀ O(2 k ) O(2 k.2 ℓ )
For such a property P , an FA over F C,D intended to check it on incidence graphs defined by correct terms can be constructed from the FA A P,C over F C that checks P on "ordinary" graphs G, without needing significant modification: essentially, we replace C by C ∪ D. Although the FA for the relation edg(X, Y ) is more complicated in the case of incidence graphs than for ordinary graphs, this increasing complexity does not extend to all properties expressed by means of edg(X, Y ).

An automaton for Directed Hamiltonian cycle

The property DirHam that a graph G has a directed Hamiltonian cycle is MSO 2 expressible but not MSO expressible. It is expressed in Inc(G) by "there exists a set of edges of G that forms a directed cycle going through all vertices". Without using the corresponding logical expression, we will construct an FA for this property.

We let P mean be that the considered graph is a directed cycle or is empty, and L be the set of correct irredundant terms t in T (F C,D ) such that P (val(t)) holds. We first construct an FA B over F C,D that recognizes L among correct and irredundant terms, that is, such that L(B) ∩ L Irr ∩ L CT = L.

Let t ∈ L and t ′ be a subterm of t. Then val(t ′ ) satisfies one of the following properties:

(a) it is a single directed cycle (and then val(t ′ ) = val(t)), (b) it consists of isolated vertices x 1 , ..., x p , (p ≥ 0) and of pairwise disjoint paths from y 1 to z 1 , y 2 to z 2 , ... , y m to z m (m ≥ 0), such that the labels of x 1 , ..., x p , y 1 , ..., y m , z 1 ,... , z m are all different.

Each of them implies :

(c) no C-vertex has indegree or outdegree 2 or more.

Since t is assumed correct, every D-vertex has indegree and outdegree at most one. A transition that shows a violation of (c) will yield Error.

We define B with the following states : Ok, Error and the 3-tuples (α, β, Ψ) in P f (C ∪ D) × P f (C) × P f ((C ∪ D) 2 ). At the root of a term t ′ ∈ T (F C,D ) as above, the automaton B reaches the following state: We denote by D(σ) the conjunction of these two conditions.

Remarks: When B reaches state (α, β, Ψ), the labels of the C-vertices of val(t ′ ) are all in α ∪ β ∪ Ψ 1 ∪ Ψ 2 , but (α, β, Ψ) does not indicate the set δ of labels of the D-vertices that are on the paths from y j to z j but not at their ends. These vertices have indegree and outdegree 1. Since t is assumed correct and irredundant, Lemma 2 yields that δ ∩ (α ∪ Ψ 1 ∪ Ψ 2 ) = ∅.

The accepting state is Ok. We now describe some transitions. (cf. the end of Section 3). Note that t[V val(t) , U ] is a correct irredundant term for all sets U if t is so. This property is thus checked by the nondeterministic FA C obtained from B by adding the transitions d → -→ ∅ for d ∈ D. These new transitions correspond to the elimination of the edges that will not be on the directed cycle under construction. The FPT-FA det(C) checks DirHam in time O(2 2(k+ℓ) 2 .n) where n is the number of vertices and edges of the input graph.

Conclusion

These results indicate that the tools of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF][START_REF] Courcelle | Computations by fly-automata beyond monadic second-order logic[END_REF] can be applied to the verification of MSO 2 properties of graphs of bounded tree-width given by their treedecompositions. The software AUTOGRAPH12 can be used basically as it is (up to minor syntactic adaptations) although the algebras of terms describing tree-decompositions and of terms defining clique-width are fairly different (as discussed in [START_REF] Courcelle | On the model-checking of monadic second-order formulas with edge set quantifications[END_REF]).

We have introduced in [START_REF] Courcelle | On the model-checking of monadic second-order formulas with edge set quantifications[END_REF] a variant of tree-width called special tree-width intended for the verification of MSO 2 properties. It is weaker than tree-width in the sense that bounded special tree-width implies bounded tree-width but not vice-versa. Its advantage is that special tree-decompositions can be formalized in terms of clique-width operations. A decomposition of width p is formalized by a term in T (F [p+2] ). Hence, this article also provides tools for checking MSO 2 properties by FA based on clique-width operations.

For completeness, we also cite [START_REF] Kneis | Courcelle's theorem -A game-theoretic approach[END_REF] where a completely different method is used to check MSO 2 properties of graphs of bounded tree-width.

  ), where [k] := {1, ..., k}, is the same as running A ϕ(X1,...,Xp),[k] . An implementation of A ϕ(X1,...,Xp),C yields a single program that works for all terms in T (F(p) [k] ), k ≥ 1,hence for graphs of all clique-widths.The membership in L ϕ(X1,...,Xp),C of a term t ∈ T (F

  (b) of Theorem 1 does not extend to inputs Inc(G) for G of clique-width at most k because the clique-width of such graphs Inc(G) is unbounded. It can be used for graphs G of tree-width at most k. Proposition 3 gives cwd(Inc(G)) = 2 O(twd(G)) (because twd(Inc(G)) ≤ twd(G) + 1) however cwd(Inc(G)) = O(twd(G)) as we will see. Definition 6 : Incidence graphs.

  no label in C can be changed to a label in D, and vice-versa, no edge-addition --→ add a,b can be used with a, b ∈ C or a, b ∈ D.

Proposition 7 :

 7 If a directed graph G has tree-width k, then Inc(G) is defined by a term in T (F C,D ) such that |C| = 2 and |D| = 2k+3. If G is undirected, then Inc(G) is defined by a term in T (F C,D ) such that |C| = 2 and |D| = k + 2. Terms witnessing these bounds can be constructed in linear time from treedecompositions of G of width k. Conversely, twd(G) = O(cwd(Inc(G))).

  is the set γ where a is replaced by b, and similarly for δ[d → e], -→ δ [d → e] := (δ 00 [d → e], δ 01 [d → e], δ 10 [d → e], δ 11 [d → e]), -→ ∅ denotes a sequence of empty sets of appropriate length.

  ) If we replace the transitions a → ({a}, -→ ∅ ) and d → (∅, ∅, {d}, -→ ∅ ) by (a, w) → ({a}, -→ ∅ ) and (d, w ′ ) → (∅, ∅, {d}, -→ ∅ ) respectively for w ∈ {0, 1} p and w ′ ∈ {0, 1} m , we obtain an automaton that checks the correctness of a term in T (F (p,m) C,D ).

  The FA A edg(X,Y ) We now construct an FA A edg(X,Y ) intended to run on correct and irredundant terms in T (F[START_REF] Bouvier | Graphes et décompositions[END_REF]0)

  Ok if (a) holds, Error if neither (a) nor (b) holds, (α, β, Ψ) if (b) holds and : α is the set of labels of the vertices x 1 , ..., x p , β is the set of labels of the C-vertices of indegree and outdegree 1, Ψ = {(π(y 1 ), π(z 1 )), ..., (π(y m ), π(z m ))}. From any finite set Ψ = {(a 1 , b 1 ), ..., (a m , b m )} ⊆ (C ∪ D) 2 , we define Ψ 1 := {a 1 , ..., a m } and Ψ 2 := {b 1 , ..., b m }.If σ = (α, β, Ψ) is reached at the root of t ′ satisfying (b), then:(i) the sets α, β, Ψ 1 and Ψ 2 are pairwise disjoint, (ii) no two pairs in Ψ have a component in common (by (i) this condition reduces to: a i = a j and b i = b j for i = j).

  a ∈ C ∪ D, ⊕[Ok, -→ ∅ ] → Ok, ⊕[Ok, q] → Error, if q = -→ ∅ (in particular if q = Ok), ⊕[σ, σ ′ ] → σ ∪ σ ′ if α ∩ α ′ = ∅, Ψ ∩ Ψ ′ = ∅ and D(σ ∪ σ ′ ) holds,where, if σ = (α, β, Ψ) and σ ′ = (α ′ , β ′ , Ψ ′ ), we haveσ ∪ σ ′ :=(α ∪ α ′ , β ∪ β ′ , Ψ ∪ Ψ ′ ), ⊕[σ, σ ′ ] → Error otherwise.We denote by a, b any labels in C ∪ D. The transitions for relabellings relab a→b in F C,D are:

Table 4 :

 4 Comparison between MSO and MSO 2 -automata.

	5 Automata for other properties
	5.1 Inc-invariant properties
	Definition 8 : Invariance for taking the incidence graph.
	A graph property P is Inc-invariant if P (G) ⇐⇒ P (Inc(G)) for every graph
	G.

By a result of Bodlaender (see[START_REF] Bodlaender | A linear-time algorithm for finding tree-decompositions of small treewidth[END_REF][START_REF] Downey | Parameterized complexity[END_REF][START_REF] Downey | Fundamentals of parameterized complexity[END_REF]), a tree-decomposition of G of width k can be computed in linear time if there exists one. Hence the variant of (b) where a tree-decomposition is not given but must be computed also holds, but this variant is not a consequence of (a). Furthermore, the linear time decomposition algorithm is not practically implementable.

Automata A ϕ,k can also be defined for formulas ϕ with free variables. See Theorem 5.

The system AUTOGRAPH that builds and runs FA is written in LISP[START_REF] Courcelle | Fly-Automata, their properties and applications[END_REF] and http://deptinfo.labri.u-bordeaux.fr/˜idurand/autograph

Saying that P is a property of graphs means that it is invariant under isomorphisms and arbitrary vertex relabellings. Labels are used for constructing graphs, but at the end, they are forgotten.

Fly-automata can also compute functions if one replaces the accepting states by a computable mapping from states to some effective domain. See[START_REF] Courcelle | Computations by fly-automata beyond monadic second-order logic[END_REF].

We use this observation in Section 4.2.

This definition is used in[START_REF] Courcelle | Fly-automata, model-checking and recognizability[END_REF] to prove that the (Strong) Recognizability Theorem, Theorem 5.68(1) of[START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], can be proved via the construction of automata.

These formulas could be alternatively defined as MSO formulas where each variable X (resp. U ) comes with the condition that the elements x of X (resp. of U ) satisfy isv(x) (resp. ¬isv(x)).

The system AUTOGRAPH that builds and runs FA is written in LISP[START_REF] Courcelle | Fly-Automata, their properties and applications[END_REF] and http://deptinfo.labri.u-bordeaux.fr/˜idurand/autograph

Acknowledgements : I thank R. Sampaio for fruitful discussions on these topics. I thank I. Durand for her ongoing collaboration and her implementation of fly-automata.

This work has been supported by the French National Research Agency (ANR) in the IdEx Bordeaux program "Investments for the future", CPU, ANR-10-IDEX-03-02. 1 The presentation in these two works is much better than those in the usually quoted original references [3,11].

relab a→b [Ok] → Ok, relab a→b [σ] → Error if {a, b} ⊆ α or D(σ ′ ) does not hold 11 where σ ′ is obtained from σ by replacing everywhere a by b;

Let comment on the last case. If a ∈ C and a / ∈ α ∪ β ∪ Ψ 1 ∪ Ψ 2 , then relab a→b has no effect and the last transition yields σ ′ = σ. If a ∈ D and a / ∈ α ∪ Ψ 1 ∪ Ψ 2 , it may happen that a ∈ δ (cf. the above remarks) hence that relab a→b might have some effect. But since the input term is irrendundant and correct, Lemma 2 shows that b cannot belong to α∪Ψ 1 ∪Ψ 2 . Hence δ is replaced by δ[a → b] and nothing else is modified. Hence the transition yields correctly σ ′ = σ.

Transitions for edge additions are as follows:

By Properties (i) and (ii), a, b, c, d are pairwise distinct. Finally, --→ add a→b [(α, β, Ψ)] → Error in all other cases.

Note that by our usual argument using Lemma 2, if --→ add a→b [(α, β, Ψ)] is to be fired, then b cannot belong to δ.

If C ∪ D is finite, k = |C| and ℓ = |D|, then the number of states is bounded by 3 k .2 ℓ .m(k+ℓ) where m(n) is the number of ordered matchings over n elements (of sets of pairwise disjoint ordered pairs). We have ⌊n/2⌋! < m(n) < 2 n 2 . The size of a state is O((k + ℓ) log(k + ℓ)) and the time for computing a transition is also O((k + ℓ) log(k + ℓ)).

The property DirHam, i.e., the existence of a directed Hamiltonian cycle in the graph G such that Inc(G) = val(t) is expressed by : "There exists a set U of D-vertices of val(t) such that P (val(t)[V val(t) , U ]) holds" 11 That D(σ ′ ) holds implies that a and b are not both in Ψ 1 and not both in Ψ 2 .