Bruno Courcelle
email: courcell@labri.fr

Irène Durand
email: idurand@labri.fr

Computations by fly-automata beyond monadic second-order logic

Keywords: monadic second-order logic, graph algorithms, infinite automata, parameterized algorithms, tree-width, clique-width, dynamic programming, model-checking, data complexity, algorithmic meta-theorems

The validity of a monadic-second order (MS) expressible property can be checked in linear time on graphs of bounded tree-width or clique-width given with appropriate decompositions. This result is proved by constructing from the MS sentence expressing the property and an integer that bounds the tree-width or clique-width of the input graph, a finite automaton intended to run bottom-up on the algebraic term representing a decomposition of the input graph. As we cannot construct practically the transition tables of these automata because they are huge, we use flyautomata whose states and transitions are computed "on the fly", only when needed for a particular input. Furthermore, we allow infinite sets of states and we equip automata with output functions. Thus, they can check properties that are not MS expressible and compute values, for an example, the number of p-colorings of a graph. We obtain XP and FPT graph algorithms, parameterized by tree-width or clique-width. We show how to construct easily such algorithms by combining predefined automata for basic functions and properties. These combinations reflect the structure of the MS formula that specifies the property to check or the function to compute.

Introduction

Fixed-parameter tractable (FPT) algorithms can be built by many techniques.

In their recent book [START_REF] Downey | Fundamentals of parameterized complexity[END_REF], Downey and Fellows distinguish "elementary techniques" (bounded search trees, kernelization, color coding, iterative compression etc.) and techniques based on well quasi-orders from those "based on graph structure". The notion of graph structure includes the graph decompositions from which tree-width, path-width, local tree-width, clique-width etc. are defined. A central result is the following algorithmic meta-theorem [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][START_REF] Flum | Parameterized complexity theory[END_REF]:

The validity of a monadic-second order (MS) expressible property can be checked in linear time on graphs of bounded tree-width and on graphs of bounded clique-width given with appropriate decompositions.

As in [START_REF] Grohe | Methods for algorithmic meta-theorems[END_REF][START_REF] Kreutzer | Algorithmic meta-theorems[END_REF], we call it a meta-theorem because it applies in a uniform way to all graph properties expressed by MS sentences. An easy proof of this result consists in defining by an algorithm a finite automaton intended to run bottomup on the labelled tree or the algebraic term that represents the structure of the input graph ( [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], Chapter 6). This automaton is built from the MS sentence expressing the property and an integer, say k, that bounds the tree-width or clique-width of the input graph. The number of states is a tower of exponentials of height essentially equal to the number of quantifier alternations of the considered sentence, with the bound k at the top. In most cases we cannot construct practically the sets of states and the transition tables of these automata. This obstacle is intrinsic [START_REF] Frick | The complexity of first-order and monadic secondorder logic revisited[END_REF], it is not due to the choice of finite automata to implement the meta-theorem.

However, we can remedy this problem in many significant cases by using fly-automata (introduced in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]). They are automata whose states and transitions are computed "on the fly", only when needed for a particular input 1 . A deterministic fly-automaton A having 2 1000 states only computes 100 states on a tree or term of size 100. Actually, the evaluation algorithm determines the smallest subautomaton A ae t of A able to process the given term t.

In this article we develop a theory of fly-automata and extend the notion introduced in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]. In particular, we allow infinite sets of states (e.g., a state may contain counters recording the unbounded numbers of occurrences of particular symbols) and we equip automata with output functions that map the accepting states to some effective domain D (e.g., the set of integers, or of pairs of integers, or the set of words over a fixed alphabet). Thus, fly-automata can check properties that are not monadic second-order expressible, for example that a graph is regular (has all its vertices of same degree) and compute values, for example, the number of p-colorings. We will construct fly-automata that yield FPT and XP algorithms (definitions are reviewed in Section 1.5) for tree-width or clique-width as parameter. We will combine basic fly-automata by means of products, direct and inverse images in a way that reflects the structure of the defining formula. For example, product of automata implements conjunction and taking a direct image implements existential quantification. We have implemented these constructions in the system AUTOGRAPH2 and tested them successfully on coloring and connectedness problems.

Our model-checking algorithms are intended for fixed graph properties and we are interested in analyzing their data complexity formulated in the framework of fixed-parameter tractability. However, these algorithms are constructed in uniform ways from logical expressions that cover a large variety of problems. The constructions are easily extendable to labelled graphs and relational structures.

Our computation model. We now motivate our choices. Fly-automata have several advantages: they overcome in many significant cases the "size problem" met with usual finite automata, they are not restricted to fixed bounds on clique-width, they allow to check some properties that are not MS expressible and to compute values attached to graphs and, last but not least, they offer a flexible framework: a slight change in the formula that specifies the problem is quickly reflected in the construction of a new automaton, performed by the system AUTOGRAPH.

We study fly-automata over the signature of graph operations from which clique-width is defined. We have chosen to deal with these operations rather than those for tree-width because the automata are much simpler [START_REF] Courcelle | On the model-checking of monadic second-order formulas with edge set quantifications[END_REF]. This choice also yields a gain in generality because the clique-width of a simple graph G is bounded in terms of its tree-width but not vice-versa. All our FPT and XP algorithms parameterized by clique-width are also FPT and XP respectively for tree-width. Furthermore, replacing a graph G by its incidence graph allows to handle in our setting edge quantifications, see the conclusion and [START_REF] Courcelle | Fly-automata for checking monadic second-order properties of graphs of bounded tree-width[END_REF][START_REF] Courcelle | Fly-automata for checking MSO 2 graphs properties[END_REF].

At the end of this introduction, we review methods for implementing the verification of MS properties on graphs of bounded tree-width that are not based on automata.

Overview of the main definitions.

An automaton takes as input a term t P T pF q over a signature F , i.e., a set of operations, each given with a fixed arity. The graphs of clique-width at most k are those defined by a term over a finite signature F k , and F 8 is the union of the signatures F k . We will construct fly-automata over the infinite signature F 8 , with which all finite graphs can be defined.

We will construct fly-automata for basic properties and functions, for example the regularity of a graph or the degree of a vertex, and we will also use the automata constructed in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] for some basic MS properties. We will combine these automata in order to define more complex properties and functions, for example the possibility of partitioning the vertex set of a graph into two sets inducing regular subgraphs.

Here are some typical examples of decision problems and functions that we can handle in this way:

(1) Is it possible to cover the edges of a graph with those of s cliques? (2) Does there exist an equitable s-coloring? Equitable means that the sizes of any two color classes differ by at most 1 [START_REF] Fellows | On the complexity of some colorful problems parameterized by treewidth[END_REF]. We can express this property by DX 1 , . . . , X s .pP artitionpX 1 , . . . , X s q ^StrX 1 s ^... ^StrX s s ^"|X 1 | " ...

" |X i´1 | ě |X i | " ... " |X s | ě |X 1 | ´1
for some i") where StrXs means that the induced subgraph GrXs of the considered graph G is stable, i.e., has no edge.

(3) Assuming the graph s-colorable, what is the minimum size of the first color class of an s-coloring?

(4) What is the minimum number of edges between X and Y for a partition pX, Y q of the vertex set such that GrXs and GrY s are connected?

More generally, let P pX 1 , ..., X s q be a property of sets of vertices X 1 , ..., X s or of positions of a term; we will use X to denote pX 1 , ..., X s q and t |ù P pXq to mean that X satisfies P in the term t or in the graph Gptq defined by t; this writing does not assume that P is written in any particular logical language. We are interested, not only to check the validity of DX.P pXq in t or in Gptq for some given term t, but also to compute (among others) the following objects associated with t: #X.P pXq, defined as the number of assignments X such that t |ù P pXq, SpX.P pXq, the spectrum of P pXq, defined as the set of tuples p|X 1 |, . . . , |X s |q such that t |ù P pXq, MSpX.P pXq, the multispectrum of P pXq, defined as the multiset of tuples p|X 1 |, . . . , |X s |q such that t |ù P pXq, MinCardX 1 .P pXq defined as mint|X 1 | | t |ù DX 2 , ..., X s .P pXqu, SatX.P pXq, defined as the set of tuples X such that t |ù P pXq.

We will say that the functions #X.P pXq, SpX.P pXq, MSpX.P pXq, MinCardX 1 .P pXq and SatX.P pXq taking terms as arguments are MS expressible if P pXq is an MS expressible property. Their values are numbers or sets of tuples of numbers in the first four cases and our automata will give XP or FPT algorithms. Computing SatX.P pXqptq is more difficult because the result may be of exponential size in the size of t.

Our main results

Here are the four main ideas and achievements. First, we recall that the state of a deterministic bottom-up automaton collects, at each position u of an input term, some information about the subterm issued from u. This information should be of size as small as possible so that the computation of a run be efficient. An appealing situation is when the set of states is finite, but finiteness alone does not guarantee efficient algorithms. This is well-known for MS definable sets of terms over a finite signature: the number of states of an automaton that implements an MS formula has a number of states that cannot be bounded by an elementary function (an iterated exponentiation of bounded height) in the size of the formula, see [START_REF] Frick | The complexity of first-order and monadic secondorder logic revisited[END_REF][START_REF] Reinhardt | The complexity of translating logic to finite automata, in Automata, logics, and infinite games: A guide to current research[END_REF]. The notion of fly-automaton permits to construct usable algorithms based on finite automata whose transitions cannot be compiled in manageable tables.

Second, as we do not insist on compiling transitions in tables, we have no reason to insist on finiteness of the set of states. So we use fly-automata whose states are integers, or pairs of integers or any information representable by a finite word over a fixed finite alphabet. These automata yield polynomialtime dynamic programing algorithms if the computation of each transition takes polynomial time in the size of the input term.

Third, fly-automata can run on terms over countably infinite signatures, encoded in effective ways. In particular, we will define automata that run on terms describing input graphs. These terms yield upper-bounds to the cliquewidth of these graphs. As no finite set of such operations can generate all graphs, the use of an infinite signature is necessary 3 . By analyzing how these automata are constructed from logical descriptions, we can understand (in part) why some algorithms constructed from automata are FPT whereas others are only XP.

Fourth, we go beyond MS logic in two ways. We adapt the classical construction of finite automata from formulas exposed in Chapter 6 of [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] and in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] to properties of terms and graphs that are not MS expressible (for example the regularity of a graph) and we build automata that compute functions (for example, the largest size of an induced subgraph that is regular). Such properties and functions are defined by formulas using new atomic formulas, such as RegrXs expressing that the induced subgraph GrXs of the considered graph G is regular, and new constructions, such as #X.P pXq or SpX.P pXq, that can be seen as generalized quantifications, as they bind the variables of X while delivering more information than DX.P pXq. From the usual case of MS logic, we keep the inductive construction of an automaton based on the structure of the defining formula.

We generalize results from [START_REF] Arnborg | Easy problems for treedecomposable graphs[END_REF][START_REF] Courcelle | Linear time solvable optimization problems on graphs of bounded clique-width[END_REF][START_REF] Courcelle | Monadic second-order evaluations on treedecomposable graphs[END_REF] that build algorithms for properties of terms or of graphs of bounded tree-width or clique-width that are of the form DX 1 , . . . , X s .pϕpX 1 , . . . , X s q ^Rp|X 1 |, . . . , |X s |qq where ϕpX 1 , . . . , X s q is an MS formula and R is an s-ary arithmetic relation that can be checked in polynomial time. However, we cannot allow such atomic formulas Rp|X 1 |, . . . , |X s |q to occur everywhere in formulas. We discuss this issue in Section 4. [START_REF] Broersma | Tight complexity bounds for FPT subgraph problems parameterized by the clique-width[END_REF].

Our automata that compute functions generalize the automata with cost functions of [START_REF] Seidl | Finite tree automata with cost functions[END_REF] and the weighted automata of [START_REF]Handbook of weighted automata[END_REF], Chap. 9. However, these automata do not allow infinite signatures that we use for handling graphs, and the results they prove for finite automata are not related with our constructions.

We do not investigate here the parsing problem: graphs are given by terms over the signature of graph operations F 8 from which clique-with is defined.

To summarize, we provide logic based methods for constructing FPT and XP dynamic programming graph algorithms by means of fly-automata on terms. The system AUTOGRAPH, currently under development, implements the presented constructions.

Alternative tools.

There are other methods intended to overcome the "size problem" that is unavoidable with finite automata [START_REF] Frick | The complexity of first-order and monadic secondorder logic revisited[END_REF][START_REF] Reinhardt | The complexity of translating logic to finite automata, in Automata, logics, and infinite games: A guide to current research[END_REF]. Kneis et al. [START_REF] Kneis | Courcelle's theorem -a gametheoretic approach[END_REF][START_REF] Langer | Practical algorithms for MSO model-checking on tree-decomposable graphs[END_REF] use games in the following way. From a graph G given with a tree-decomposition T and an MS sentence ϕ to check, they build a model-checking game GpT, ϕq that is actually a tree. An alternating automaton running on this tree can decide if the graph G satisfies ϕ. The game GpT, ϕq is of bounded size because equivalent subgames are merged by taking into account the fact that MS formulas of bounded quantifier height have a limited power of distinguishing structures. It depends on G, and not only on ϕ and on a bound on its tree-width. This is similar to our use of fly-automata where a subautomaton A ae t of a "huge" automaton A is computed for the input term t. (A precise comparison of the states of A ae t and these games would be interesting but is beyond the scope of the present article.) This game approach extends to optimization problems such as computing MinCardX 1 .P pXq or more generally, those considered in [START_REF] Courcelle | Monadic second-order evaluations on treedecomposable graphs[END_REF]. It has been implemented and works for several problems on graphs with about 200 vertices. However, the correctness proof of the method and the programming task are by far much more complex than those for our fly-automata.

Another proposal consists in using Datalog [START_REF] Foustoucos | The monadic second-order logic evaluation problem on finite colored trees: a database-theoretic approach[END_REF][START_REF] Gottlob | Monadic datalog over finite structures of bounded treewidth[END_REF]. However, it seems to be nothing but a translation of automata on terms into monadic Datalog programs together with some manual optimization. It is unclear whether and how the "size problem" is avoided. This approach is discussed in detail in [START_REF] Langer | Practical algorithms for MSO model-checking on tree-decomposable graphs[END_REF].

Summary of article: Section 1 reviews notation and definitions relative to terms, graphs and computability notions. Section 2 reviews the definitions concerning fly-automata. Section 3 gives the main algorithms to build fly-automata by transforming or combining previously constructed automata. Section 4 details some applications to graphs. It gives also some direct constructions of automata smaller than those obtained by the general construction based on logic. Section 5 gives an overview of the software AUTOGRAPH and reports some experiments. Section 6 is a conclusion. An appendix recalls definitions concerning MS logic and establishes a technical lemma about terms that define graphs.

Fly-automata and AUTOGRAPH have been presented in conferences; see [START_REF] Courcelle | Model-checking by infinite fly-automata[END_REF][START_REF] Courcelle | Infinite transducers on terms denoting graphs[END_REF][START_REF] Courcelle | Fly-automata, model-checking and recognizability[END_REF].

Definitions

We review all necessary definitions, mostly from [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], and we give some new ones. Monadic second-order logic on graphs is reviewed in the appendix.

General notation

We denote by N the set of natural numbers, by N `the set of positive ones, by rn, ms the interval ti | n ď i ď mu and by rns the interval r1, ns. We denote by wris the i-th element of a sequence or the i-th letter of a word w. As usual, logarithms are in base 2 and logpxq stands for maxt1, log 2 pxqu. Countable means countably infinite.

The cardinality of a set A is denoted by |A|. An encoding of a finite set is larger than its cardinality. For example, a set of m integers in rns can be encoded in size Opm. logpnq `1q by a word over a fixed finite alphabet. We denote by }A} the size of such an encoding.

We denote by A ´B the difference of two sets A, B and by B c (the complement of B in A) if B Ď A and A is clear from the context. We denote by rA Ñ Bs the set of mappings (i.e., of total functions): A Ñ B. If C Ď A and f P rA Ñ Bs, we denote by f ae C the restriction of f to C and we will consider that rC Ñ Cs is a subset of rA Ñ As by identifying h : C Ñ C with its extension h 1 to A such that h 1 paq :" a if a P A ´C. However, no such identification is needed if we represent h by the set of pairs pa, hpaqq such that a P C and hpaq ‰ a, because in this case the set of pairs corresponding to h 1 is exactly the same. This observation yields a way to implement h if C is finite and A is infinite.

If A is any set PpAq, P f pAq, P n pAq, P ďn pAq denote respectively its set of subsets, of finite subsets, of subsets of cardinality n and of subsets of cardinality at most n, and Z denotes the union of disjoint sets (B Z C is undefined if B and C are not disjoint).

A multiset over a finite or countable set A is a mapping α: A Ñ N Y tωu where αpaq is the number of occurrences of a P A in the multiset α. We denote by H the empty multiset (αpaq " 0 for all a) and by \ the union of two multisets (we have pα \ βqpaq " αpaq `βpaq). The cardinality of α is |α| :" Σ aPA αpaq and this gives a notion of finite multiset. If furthermore A is a commutative monoid with an addition `and a zero 0, we define α as finite if Σ aPA´t0u αpaq is finite. Then we define Σα :" Σ aPA´t0u αpaq.a. We have ΣH " 0 and Σpα \ βq " Σα `Σβ. Furthermore, Σα " 0 if α consists of countably many occurrences of 0. We denote respectively by MpAq and M f pAq the sets of multisets and of finite multisets over A.

Let f P rA Ñ Bs and X Ď A where A is finite or countable. We denote by f pxq | x P X the multiset β over B such that βpbq :" ˇˇf ´1pbq X X ˇˇand by tf pxq | x P Xu, or f pXq as usual, the corresponding set. Let for an example A :" ta, b, c, du, B :" t1, 2, 3u, f paq :" f pbq :" f pcq :" 1, f pdq :" 2 and X :" ta, b, du. Then tf pxq | x P Xu " t1, 2u, f pxq | x P X is the multiset t1, 1, 2u and Σ f pxq | x P X " 4.

The set of finite words over an alphabet Z is denoted by Z ˚and the empty word is ε.

Terms and their syntactic trees

A signature F is a finite or countable set of function symbols, each being given with a natural number called its arity: ρpf q denotes the arity of the symbol f and ρpF q the maximal arity of a symbol of F, provided its symbols have bounded arity. We denote by T pF q the set of finite terms over F and by Posptq the set of positions of a term t. Each position is an occurrence of some symbol and Pos f ptq is the set of occurrences of f P F . Positions are defined as Dewey words. For example, the positions of the term f pgpa, bq, gpb, cqq are denoted by the Dewey words ε, 1, 11, 12, 2, 21, 22. For a term t " hpt 1 , t 2 , t 3 q, we have P osptq " tεu Y 1.P ospt 1 q Y 2.P ospt 2 q Y 3.P ospt 3 q where . denotes concatenation. (If function symbols have arity at most 9, we can omit the concatenation marks, as in the above example). We denote by Sigptq the finite subsignature of F consisting of the symbols that have occurrences in t.

The syntactic tree of a term t is a rooted, labelled and ordered tree with set of nodes in bijection with P osptq; each node u is labelled by a symbol f and has a sequence of ρpf q sons; its root denoted by root t corresponds to the first position relative to the linear writing of t, and the leaves to the occurrences of the nullary symbols.

We denote by t{u the subterm of t issued from position u and by P osptq{u the set of positions of t below u or equal to it. In terms of Dewey words, we have P osptq{u " u.P ospt{uq. Note that P osptq{u ‰ P ospt{uq unless u " ε corresponding to the root. If X is a set of positions of t, then X{u denotes X X pP osptq{uq, hence is the set of elements of X below or equal to u. The height htptq of a term t is 1 if t is a nullary symbol and 1`maxthtpt 1 q, ..., htpt r qu if t " f pt 1 , ..., t r q.

Let H be a signature and h : H Ñ F be an arity preserving mapping, i.e., a mapping such that ρphpf qq " ρpf q for every f P H. For every t P T pHq, we let hptq P T pF q be the term obtained from t by replacing f by hpf q at each of its occurrences. Such a mapping is called a relabelling.

We denote by |t| the number of positions of a term t. In order to discuss algorithms taking terms as input, we must define the size of t. If F is finite, we can take |t| as its size. If F is infinite, its symbols must be encoded by words of variable length. We define the size }t} of t as the sum of lengths of the words that encode its symbols 4 . In both cases, we denote the size of t by }t}. We have |Sigptq| ď |t| ď }t}. We say that an algorithm takes time polyp}t}q if its computation time is bounded by pp}t}q for some polynomial p that we do not specify.

A language is either a set of words or a set of terms.

F-algebras

Let F be a signature and D " xD, pf D q f PF y be an F -algebra. The set D is its domain. We denote by val D the mapping: T pF q Ñ D that yields the value of a term. We let then F ] be the signature F Z t], 0u such that ] is binary and 0 is nullary.

A distributive F-algebra is an F ] -algebra E " xE, ] E , 0 E , pf E q f PF y such that ] E is associative and commutative with neutral element 0 E , and the functions f E satisfy the following distributivity properties:

f E p..., d ] E d 1 , ...q " f E p..., d, ...q ] E f E p..., d 1 , ...q, f E p..., 0 E , ...q " 0 E .
We extend ] E to finite subsets of E by:

] E pA Z Bq :" p] E Aq ] E p] E Bq and ] E H :" 0 E ,
and similarly for finite multisets. If A is infinite and g : A Ñ E is a mapping such that gpaq ‰ 0 E for finitely many a P A, then ] E gpaq | a P X and gpaq ‰ 0 E is well-defined and will be denoted more shortly by ] E gpaq | a P X .

The powerset algebra (of finite subsets) of an F -algebra D is5 :

P f pDq :" @ P f pDq, Y, H, pf P f pDq q f PF D f P f pDq pA 1 , ..., A r q :" tf D pa 1 , ..., a r q | a 1 P A 1 , ..., a r P A r u.
We define also its multiset algebra (of finite multisets):

M f pDq :" @ M f pDq, \, H, pf M f pDq q f PF D where
f M f pDq pα 1 , ..., α r q is the multiset β such that βpbq (the number of occurrences in β of b P Dq is the sum over all r-tuples pa 1 , ..., a r q such that a 1 P α 1 , ..., a r P α r and b " f D pa 1 , ..., a r q of the numbers α 1 pa 1 q ˆ... ˆαr pa r q.

It is easy to check that P f pDq and M f pDq are distributive F -algebras. If t P T pF q, then its values in P f pDq and in M f pDq are tval D ptqu.

Graphs and clique-width

Notation and definitions are as 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]. Some technical points are developped in the appendix.

Graphs

All graphs are finite, loop-free and simple (without parallel edges). A graph G is identified with the relational structure xV G , edg G y where edg G is a binary relation representing the directed or undirected adjacency. If X Ď V G , we denote by GrXs the induced subgraph of G with vertex set X, i.e., GrXs :" xX, edg G X pX ˆXqy. If E Ď edg G , then GrEs :" xV G , Ey.

If P is a property of graphs and X Ď V G , then P rXs expresses that GrXs satisfies P . A graph is stable if it has no edge and we denote this property, called stability, by St. Hence, StrXs used in the introduction says that GrXs has no edge.

In order to build graphs by means of graph operations, we use labels attached to vertices. We let L be a fixed countable set of port labels. A p-graph (or graph with ports) is a triple G " xV G , edg G , π G y where π G is a mapping: V G Ñ L. So, π G pxq is the label of x and, if π G pxq " a, we say that x is an a-port. If X is a set of vertices, then π G pXq is the set of its port labels. The set πpGq :" π G pV G q is the type of G. A p-graph G is identified with the relational structure xV G , edg G , plab a G q aPL y where lab a is a unary relation and lab a G is the set of a-ports of G. Since we only consider simple graphs, two graphs or p-graphs G and H are isomorphic if and only if the corresponding relational structures are isomorphic. In this article, we will take port labels in L :" N `.

We denote by G « G 1 the fact that two p-graphs G and G 1 are isomorphic and by G » G 1 that they are isomorphic up to port labels.

Operations on p-graphs

We let F k consist of the following function symbols; they define operations on the p-graphs of type included in the set of port labels C :" rks that we also define:

-the binary symbol ' denotes the union of two disjoint p-graphs (i.e., G '

H :" xV G Y V H , edg G Y edg H , plab a G Y lab a H q aPC y with V G X V H " Hq,
-the unary symbol relab h denotes the relabelling that replaces in the argument p-graph every port label a by hpaq, where h is a mapping from C to C defined as a subset6 of C ˆC, as explained in Section 1.1; -the unary symbol Ý Ý Ñ add a,b , for a ‰ b, denotes the edge-addition that adds an edge from every a-port x to every b-port y, unless there is already an edge x Ñ y because graphs are simple; this operation is idempotent, -the nullary symbol a, for a P C, denotes an isolated a-port, and the nullary symbol ∅ denotes the empty graph.

We denote ta | a P Cu by C. For constructing undirected graphs, we use the operation add a,b where a ă b (the set C is linearly ordered as it is of the form rks) as an abbreviation of Ý Ý Ñ add a,b ˝Ý Ý Ñ add b,a . For constructing undirected graphs, we will use the signature F u k defined as F k where the operations

Ý Ý Ñ add a,b are replaced by add a,b . Every operation of F k (resp. F u k q is an operation of F k 1 (resp. F u k 1 q if k ă k 1
by our convention on mappings h in relab h . We let F 8 (resp. F u 8 ) be the union of the signatures F k (resp. F u k q. Hence, F k (resp. F u k q is the restriction of F 8 (resp. F u 8 ) to the operations and constants involving labels in rks.

Let t P T pF 8 q. We say that a port label a occurs in t if either a, Ý Ý Ñ add a,b , Ý Ý Ñ add b,a or relab h such that hpaq ‰ a or hpbq " a ‰ b has an occurrence in t. We denote by µptq the set of port labels that occur in t and by max µptq its maximal element. We also denote by πptq the set of port labels πpGptqq and by max πptq its maximal element. Clearly, πptq Ď µptq.

Clique-width

Every term t in T pF k q Y T pF u k q denotes a p-graph Gptq that we now define formally. We let P os 0 ptq be the set of occurrences in t of the symbols from C. For each u P P osptq, we define a p-graph Gptq{u, whose vertex set is P os 0 ptq{u, the set of leaves of t below u that are not occurrences of ∅. The definition of Gptq{u is by bottom-up induction on u.

If u is an occurrence of ∅, then Gptq{u is the empty graph, if u is an occurrence of a , then Gptq{u has the unique vertex u that is an a-port, if u is an occurrence of ' with sons u 1 and u 2 , then Gptq{u :" Gptq{u 1 ' Gptq{u 2 ; note that Gptq{u 1 and Gptq{u 2 are disjoint, if u is an occurrence of relab h with son u 1 , then Gptq{u :"

relab h pGptq{u 1 q, if u is an occurrence of Ý Ý Ñ add a,b with son u 1 , then Gptq{u :" Ý Ý Ñ add a,b pGptq{u 1 q,
if u is an occurrence of add a,b with son u 1 , then Gptq{u :" add a,b pGptq{u 1 q.

Finally, Gptq :" Gptq{root t . Its vertex set is thus P os 0 ptq. Note the following facts:

(1) up to port labels, Gptq{u is a subgraph of Gptq: a port label of a vertex of Gptq{u can be modified by a relabelling occurring on the path in t from u to its root;

(2) if u and w are incomparable positions under the ancestor relation, then the graphs Gptq{u and Gptq{w are disjoint.

If t P T pF k q Y T pF u k q, X Ď P os 0 ptq and t 1 is the term obtained by replacing, for each u P X, the symbol occurring there by ∅, then Gpt 1 q is the induced subgraph GptqrP os 0 ptq ´Xs of Gptq.

The clique-width of a graph G, denoted by cwdpGq, is the least integer k such that G » Gptq for some term t in To avoid this, we define a term t P T pF 8 q as good if, for some k, we have t P T pF k q, k ď |V Gptq | and |t| ď pk `1q 2 .|V Gptq | `1. We denote by T good pF 8 q the set of good terms. In Proposition 35 of the appendix, we give an algorithm that transforms a term t P T pF k q into an equivalent good term in T pF k 1 q for some k 1 ď k. Its proof constructs a kind of normal form that justifies the bound pk `1q A term t is irredundant if, for each of its subterms of the form Ý Ý Ñ add a,b pt 1 q (or add a,b pt 1 q), there is in Gpt 1 q no edge from an a-port to a b-port (or between an aport and a b-port). This means that none of its operations Ý Ý Ñ add a,b tries to add an edge, say from x to y, when there exists already one. The construction of several automata in Section 4 will be based on the assumption that the input terms are irredundant. The corresponding preprocessing is considered in Proposition 35.

T pF k q (in T pF u k q if G is undirected). A term t in T pF k q Y T pF u k q is optimal if k " cwdpGq.
We do not investigate the parsing problem, that consists, for fixed k, in finding a term in T pF k q that denotes a given graph. See however Section 1.5.

Sets of positions of terms and sets of vertices

Let E be a set, X Ď E and u P E. Then ru P Xs denotes the Boolean value 1 (i.e., T rue) if u P X and 0 otherwise. An s-tuple X " pX 1 , ..., X s q of subsets of E can be described by the function r

X : E Ñ t0, 1u s such that, for u P E, r Xpuq is the word ru P X 1 s...ru P X s s. If X is a partition of E (a typical case is when it represents a vertex coloring with s colors of a graph G and E " V G ), then r X can be replaced by p X : E Ñ rss such that p Xpuq " i if and only if u P X i . We now consider in more detail the two cases where E is the set of positions of a term and the set of vertices of a graph defined by a term.

Sets of positions of terms.

Let F be a signature and s be a positive integer. Our objective is to encode a pair pt, Xq such that t P T pF q and X P PpP osptqq s by a term t ˚X P T pF psq q where F psq is the new signature F ˆt0, 1u s with arity mapping ρppf, wqq :" ρpf q. We let pr s : F psq Ñ F be the relabelling that deletes the second component of a symbol pf, wq. We denote it by pr if s need not be specified.

If t P T pF q and X P PpP osptqq s , then the term t ˚X P T pF psq q is obtained from t by replacing, at each position u of t, the symbol f occurring there by pf, r Xpuqq P F psq . It is clear that t ˚X P T pF psq q and pr s pt ˚Xq " t; we define νpt ˚Xq :" X. Every term in T pF psq q is of the form t ˚X and encodes a term t in T pF q and the s-tuple νpt ˚Xq P PpP osptqq s . A property 7 P pX 1 , ..., X s q of sets of positions of terms over a signature F is thus characterized by the language T P pXq :" tt ˚X | t |ù P pXqu Ď T pF psq q. It can also be considered as the property P of the terms in T pF psq q such that t ˚X |ù P if and only if t |ù P pXq. Conversely, every subset of T pF psq q is T P pXq for some property P pXq. A key fact about the relabelling pr s is that T DX.P pXq " pr s pT P pXq q.

More generally (because every property is a Boolean-valued function) a function α whose arguments are t P T pF q and s-tuples X of positions of t, and whose values are in a set D, corresponds to the function α : T pF psq q Ñ D such that αpt ˚Xq :" αpt, Xq.

In a situation where the tuples X are partitions of P osptq, we can use p X instead of r X, and the signature F ˆrss denoted by F psq col (because of the applications to coloring problems) instead of F psq " F ˆt0, 1u s .

Sets of vertices.

A similar technique applies to sets of vertices of graphs defined by terms in T pF 8 q. We first recall that the vertices are the occurrences of the nullary symbols a. We define F psq 8 from F 8 by replacing each symbol a by the nullary symbols 8 pa, wq for all w P t0, 1u s . We define pr : F psq 8 Ñ F 8 as the mapping that deletes the sequences w from nullary symbols. It extends into a relabelling pr : T pF psq 8 q Ñ T pF 8 q. A term t 1 in T pF psq 8 q defines the graph Gpprpt 1 qq and the s-tuple X P PpV Gpprpt 1 qq q s such that r

Xpuq " w if and only if u is an occurrence of pa, wq for some a. The nullary symbol pa, wq defines an isolated a-port together with the information about the components of X to which it belongs, hence it does not define an pa, wq-port. The edge additions and relabellings do not depend on the components w. They act in a term t P T pF psq 8 q exactly as in the term prptq P T pF 8 q.

As for sets of positions in terms, we use the notation t˚X (where t " prpt 1 q). Hence, a property P pX 1 , ..., X s q of sets of vertices of Gptq is characterized by the language L P pX1,...,Xsq :" tt ˚X P T pF psq 8 q | Gptq |ù P pXqu. It can also be considered as the property P of terms in T pF psq 8 q such that t ˚X |ù P if and only if Gptq |ù P pXq.

As for terms, this definition extends to functions on graphs taking sets of vertices as auxiliary arguments. For example, let epX 1 , X 2 q be the number of undirected edges between sets X 1 and X 2 if these sets are disjoint and K, a special symbol that means "undefined", if X 1 and X 2 are not disjoint. It can be handled as a mapping e : T pF up2q 8 q Ñ tKu Y N, cf. Section 4.2.2. For handling coloring problems, hence, partitions of vertex sets, we can also use p X instead of r X, as for positions of terms (cf. [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Section 7.3.3). Hence, 7 X abbreviates pX 1 , ..., Xsq and P pXq stands for P pX 1 , ..., Xsq. 8 We need not modify the operations Ý Ý Ñ add a,b and relab h because they do not create vertices.

Hence, the notation F psq 8 is not an instance of the notation F psq of the previous case where F is an arbitrary signature and we want to encode sets of positions of terms in T pF q. We do not set a specific notation, the context will make things clear.

we can use F psq 8 col , where each unary symbol a is replaced by the symbols pa, iq for all i P rss.

Set terms and substitutions of variables. We consider set variables X 1 , ..., X s denoting subsets of E, the set of positions of a term t P T pF q. A set term over X 1 , ..., X s is a term S written with them, the constant symbol ∅ for denoting the empty set and the operations X, Y and c (for complementation). Hence, ∅ c denotes E. An example is S 0 " pX 1 Y X c 3 q X pX 2 Y X 5 q c . To each set term S over X 1 , ..., X s corresponds a mapping r S : t0, 1u s Ñ t0, 1u such that, for each u P E, ru P SpXqs " r Sp r Xpuqq where X " pX 1 , ..., X s q. For S 0 as above, Ă S 0 pw 1 ...w 5 q " pw 1 _ w 3 q ^ pw 2 _ w 5 q. The general definition is clear from this example.

If now Y " pY 1 , ..., Y m q is defined from X " pX 1 , ..., X s q by Y i :" S i pXq for set terms S 1 , ..., S m over X 1 , ..., X s . Let X P PpP osptqq s . Then t ˚Y " hpt ˚Xq where h is the relabelling h:F psq Ñ F pmq that replaces, in each symbol pf, wq, the word w P t0, 1u s by the word Ă S 1 pwq... Ă S m pwq P t0, 1u m . Let now αpY 1 , ..., Y m q be a function on terms in T pF q with set arguments Y 1 , ..., Y m and values in a set D. Let S 1 , ..., S m be set terms over X 1 , ..., X s and βpXq :" αpS 1 pXq, ..., S m pXqq. Hence α maps T pF pmq q into D and β maps T pF psq q into D. We have β " α˝h where h:T pF psq q Ñ T pF pmq q is the relabelling that encodes the tuple (S 1 , ..., S m ). For an example, we take s :" 4, m :" 3, S 1 :" X 1 Y X c 3 , S 2 :" ∅, S 3 :" ∅ c . Then βpX 1 , X 2 , X 3 , X 4 q defined as αpX 1 Y X c 3 , ∅, ∅ c q satisfies the equality β " α ˝h with h defined by: hppf, x 1 x 2 x 3 x 4 qq :" pf, px 1 _ x 3 q01q, that is, for all x, y P t0, 1u and f P F : hppf, 1x0yqq :" hppf, 1x1yqq :" hppf, 0x0yqq :" pf, 101q and hppf, 0x1yqq :" pf, 001q.

This shows that from an automaton that computes α, we get by composition with the relabelling h an automaton having the same states that computes β (cf. Definition 4(5) in Section 2.1 below). This technique can also be used if the terms S 1 , ..., S m are just variables, say X i1 , ..., X im , hence for handling a substitution of variables. We have stated these facts for an arbitrary signature F . They hold with obvious adaptations for the signature F 8 . In this case, t P T pF 8 q, E " P os 0 ptq " V Gptq .

Induced subgraphs and relativization

Let αpX 1 , ¨¨¨, X s´1 q be a function with (vertex) set arguments in graphs G to be defined by terms. We define βpX 1 , ¨¨¨, X s q as αpX 1 X X s , ¨¨¨, X s´1 X X s q computed in the induced subgraph GrX s s. We define h as the relabelling:

F psq 8 Ñ F ps´1q 8
such that, for every a P C and w P t0, 1u s´1 , we have hppa, w0qq :" ∅, hppa, w1qq :" pa, wq and hpf q :" f for all other operations of F 8 . With these hypotheses and notation, we have β " α˝h and a corresponding transformation of automata as in the case of set terms. This fact motivates the introduction of the nullary symbol ∅ to denote the empty graph.

If α is a property P and s " 1, we obtain a property denoted by P rX 1 s called the relativization of P to X 1 .

First-order variables

If P pX, Y, Zq is a property of subsets of a set E, we denote by P pX, y, Zq the property P pX, tyu, Zq where y P E. Accordingly, Dy.P pX, y, Zq abbreviates DY.pP pX, Y, Zq ^SglpY qq where SglpY q means that Y is singleton. If α is a ternary function on PpEq, we let similarly αpX, y, Zq abbreviate αpX, tyu, Zq.

Effectively given sets

A set D is effectively given if it is a decidable subset of Z ˚for some finite alphabet Z and, furthermore, the list of its elements is computable if it is finite. More precisely, such a set can be specified either by a list of words (if not too long) or by a triple pZ, M, kq such that M is an algorithm that decides the membership in D of a word in Z ˚, k " ω if D is infinite and k P N, k ě |w| for every w in D if it is finite. From M and k, one can compute D whenever it is finite 9 . Examples of effectively given sets are B :" tF alse, T rueu, N k , P osptq (for a term t, it is a set of Dewey sequences, cf. Section 1.2). The set of finite graphs up to isomorphism is effectively given (the proof is left to the reader).

We get immediately the notion of a computable mapping from an effectively given set to another one. If D is effectively given, then so are D s , P f pDq and M f pDq.

In many cases, an effectively given set D has a special element that we call a zero, denoted by zero D . It can be a special symbol K standing for an undefined value, it can be 0 if D " N, the empty set if D " P f pEq or the neutral element

0 D if D is a distributive algebra. A mapping f : D 1 Ñ D is finite if the set of elements d of D 1 such that f pdq ‰ zero D is finite. Then, f can be identified with the finite set tpd, f pdqq | f pdq ‰ zero D u. If D 1 is
also effectively given, the set rD 1 Ñ Ds f of finite mappings: D 1 Ñ D is effectively given.

We will consider terms over finite or countable signatures F that satisfy the following conditions:

(a) the set F is effectively given, (b) the arity of a symbol can be computed in constant time, (c) its symbols have bounded arity and ρpF q denotes the maximal arity. We will simply say that F is an effectively given signature. To insure (b), we can begin the word that encodes a symbol by its arity. It follows that one can check in linear time whether a labelled tree is actually the syntactic tree of a "well-formed" term in T pF q. We will only use relabellings: F Ñ F 1 that are computable in linear time. Their extensions: T pF q Ñ T pF 1 q are also computable in linear time by our definition of the size of a term (cf. Section 1.1).

An F -algebra D is effectively given if its signature and its domain are effectively given and its operations are computable. The mapping val D is then computable.

Parameterization

We give definitions relative to parameterized complexity [START_REF] Downey | Parameterized complexity[END_REF][START_REF] Downey | Fundamentals of parameterized complexity[END_REF][START_REF] Flum | Parameterized complexity theory[END_REF].

Let F be a signature, for which the notion of size of a term is fixed. A function h : T pF q Ñ N is P-bounded if there exists a constant a such that hptq ď }t} a for every term t in T pF q. It is FPT-bounded if hptq ď f pSigptqq.}t} a and XP-bounded if hptq ď f pSigptqq.}t} gpSigptqq for some fixed functions f and g and constant a. Since |t| ď }t} ď |t| .ℓpSigptqq for some function ℓ, }t} can be replaced by |t| in the last two cases.

A function α : T pF q Ñ D is P-computable (resp. FPT-computable, XPcomputable) if it has an algorithm whose computation time is P-bounded (resp. FPT-bounded, XP-bounded). We use Sigptq as a parameter in the sense of parameterized complexity. If F is finite, these three notions are equivalent. If α is a property, we say that it is, respectively, P-, FPT-or XP-decidable.

We will consider graph algorithms whose inputs are given by terms t over F 8 . By constructing automata, we will obtain algorithms that are polynomialtime, FPT or XP for Sigptq as parameter. The size of the input is }t}. If the graph is given without any defining term t, we must construct such a term and we get algorithms with same parameterized time complexity for the following reasons.

First we observe that every graph with n vertices is defined by a good term in T pF n q where each vertex has a distinct label and no relabelling is made. Such a term has size Opn 2 . logpnqq (cf. Section 1.2) and can be constructed in polynomial time in n. Hence, if a function α on graphs whose input is a term in T pF 8 q is P-computable, then it is also P-computable if the graph of interest is given without any defining term.

The situation is more complicated for FPT-and XP-computability. The parsing problem, i.e., the problem of deciding if a graph has clique-width at most k is NP-complete where k part of the input [START_REF] Fellows | Clique-width is NP-Complete[END_REF]. However, finding an optimal term is not necessary. There is an algorithm that computes, for every directed or undirected graph G, a good term in T pF hpcwdpGqq q that defines this graph without being necessarily optimal ([16], Proposition 6.8). This algorithm takes time gpcwdpGqq.|V G | 3 where g and h are fixed functions. It follows that an FPT or XP graph algorithm taking as input a term in T pF 8 q yields an equivalent FPT or XP graph algorithm for clique-width as parameter that takes a graph as input.

2 Fly-automata

Fly-automata: definitions

We review definitions from [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] and we extend them by equipping automata with output functions.

Definitions 1: Fly-automata that recognize languages. (a) Let F be an effectively given signature. A fly-automaton over F (in short, an FA over F ) is a 4-tuple A " xF, Q A , δ A , Acc A y 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 states, (equivalently, Acc A " α ´1pT rueq for some computable mapping α : Q A Ñ tT rue, F alseuq, and δ A is a computable function such that, for each tuple pf, q 1 , . . . , q m q such that q 1 , . . . , q m P Q A , f P F and ρpf q " m, δ A pf, q 1 , . . . , q m q is a finite (enumerated) set of states. The transitions are f rq 1 , . . . , q m s Ñ A q if and only if q P δ A pf, q 1 , . . . , q m q. We say that f rq 1 , . . . , q m s Ñ A q is a transition that yields q.

Each state is a word over a finite alphabet Z hence has a size defined as the length of that word. Each set δ A pf, q 1 , . . . , q m q is ordered by some linear order on Z ˚. We say that A is finite if F and Q A are finite. If furthermore, Q A , Acc A and its transitions are listed in tables, we call A a table-automaton.

Remark : An infinite FA A is specified by a finite tuple A of programs, or in an abstract setting, of Turing machines, that decide membership in F , Q A and Acc A and compute δ A and the arity function of F . But since one cannot decide if the function defined by a program or a Turing machine is total on its domain, the set of such tuples A is not recursive. We could strengthen the definition (and make it heavier) by requiring that each program of A is accompanied with a proof that it is terminating. This requirement will hold for the FA we will construct because their "termination properties" will be straightforward to prove. Furthermore, all transformations and combinations of fly-automata will preserve these termination properties.

(b) A run of an FA A on a term t P T pF q is a mapping r : Posptq Ñ Q A such that: if u is an occurrence of a function symbol f P F and u 1 , ..., u ρpf q is the sequence of its sons, then f rrpu 1 q, . . . , rpu ρpf q qs Ñ A rpuq; if ρpf q " 0, the condition reads f Ñ A rpuq.

Automata are bottom-up without ε-transition. For state q, LpA, qq is the set of terms t in T pF q on which there is a run r of A such that rproot t q " q. A run r on t is accepting if rproot t q is accepting. The language recognized ( or accepted by A) is LpAq :" Ť tLpA, qq | q P Acc A u Ď T pF q. A state q is accessible if

LpA, qq ‰ H. We denote by Q A ae t the set of states that occur in the runs on t and on its subterms, and by Q A ae L the union of the sets Q A ae t for t in L Ď T pF q.

A sink is a state s such that, for every transition f rq 1 , . . . , q ρpf q s Ñ 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, an automaton has at most one sink. A state named Success (resp. Error) will always be an accepting (resp. a nonaccepting) sink, but accepting (resp. nonaccepting) states may be different from Success (resp. from Error).

Unless A is finite, we cannot decide if a state is accessible, hence we cannot perform on FA the classical trimming operation that removes the inaccessible states. This fact raises no problem as we will see next.

(c) Deterministic automata. An FA A is deterministic if all sets δ A pf, q 1 , . . . , q ρpf q q have cardinality 1, hence, "deterministic" means deterministic and complete. A deterministic FA A has, on each term t, a unique run denoted by run A,t and q A ptq :" run A,t proot t q. The mapping q A is computable and the membership in LpAq of a term t is decidable.

Every FA A over F can be determinized as follows. For every term t P T pF q, we denote by run Å,t the mapping: P osptq Ñ P f pQ A q that associates with every position u the finite set of states of the form rproot t{u q for some run r on the subterm t{u of t. If A is finite, then run Å,t " run B,t where B is its classical determinized automaton, denoted by detpAq, with set of states included in P f pQ A q. If A is infinite, we have the same equality where B is a deterministic FA with set of states P f pQ A q that we denote also by detpAq (cf. [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Proposition 45(2)). In both cases, the run of detpAq on a term is called the determinized run of A on this term. The mapping run Å,t is computable and the membership in LpAq of a term in T pF q is decidable because t P LpAq if and only if the set run Å,t proot t q contains an accepting state. We define ndeg A ptq, the nondeterminism degree of A on t, as the maximal cardinality of run Å,t puq for u in P osptq. We have ndeg A ptq ď |Q A ae t|.

If A is deterministic, then detpAq is not identical to A because its accessible states are singletons tqu such that q P Q A . However, the determinized run of A is isomorphic to the run detpAq and the two automata recognize the same languages. It is not decidable whether an FA A given by a tuple A is deterministic. However, when we construct an FA, we know whether it is deterministic. Whether all states of an FA are accessible or not, does not affect the membership algorithm: the inaccessible states never appear in any run. There is no need to remove them as for table-automata, in order to get small transition tables. The emptiness of LpAq is semi-decidable (one can enumerate all terms and, for each of them, check its membership in LpAq) but undecidable ( [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]; Proposition 3.95).

Definition 2: Fly-automata that compute functions. An FA with output is a 4-tuple A " xF, Q A , δ A , Out A y as in Definition 1 except that the set Acc A is replaced by a computable output function Out A :

Q A Ñ D where D is effectively given. If A is deterministic, the function com- puted by A is ComppAq : T pF q Ñ D such that ComppAqptq :" Out A pq A ptqq.
In the general case, the computed function is Comp nd pAq : T pF q Ñ P f pDq such that Comp nd pAqptq :" tOut A pqq | q P run Å,t proot t qu. The latter set is equal to ComppBqptq where B is detpAq equipped with the output function Out B : P f pQ A q Ñ P f pDq such that Out B pαq :" tOut A pqq | q P αu. If A is deterministic, then Comp nd pAqptq :" tComp A ptqu.

Examples 3: (a) The height htptq of a term t is computable by a deterministic FA. More generally, if M is an effectively given F -algebra, then val M is computable by a deterministic FA over F with set of states M , the identity as output function and transitions f rm 1 , ..., m ρpf q s Ñ f M pm 1 , ..., m ρpf q q.

(b) Let F be an effectively given signature, r :" ρpF q and f P F . If t P T pF q, P os f ptq is the set of occurrences of f in t. The function P os f is computed by the following deterministic FA A f : its states are the finite sets of words over rrs (denoting positions of terms in T pF q). The transitions are as follows, for q 1 , ..., q r P P f prrs ˚q :

f rq 1 , ..., q s s Ñ tεu Y 1.q 1 Y ... Y s.q s , f 1 rq 1 , ..., q s 1 s Ñ 1.q 1 Y ... Y s 1 .q s 1 if f 1 ‰ f .
At each position u of t, run A f ,t puq " P os f pt{uq, hence ComppA f q " P os f if we take the identity as output function.

Definitions 4: Subautomata; products and other transformations of automata .

(1) Subautomata. We say that a signature H is a subsignature of F , written H Ď F , if every operation of H is an operation of F with same arity. We say that an FA B over H is a subautomaton of an FA A over F , which we denote by B Ď A, if:

H Ď F , Q B Ď Q A , δ B pf, q 1 ,
. . . , q ρpf q q " δ A pf, q 1 , . . . , q ρpf q q Ď Q B if f P H and q 1 , . . . , q ρpf q P Q B , and

Acc B " Acc A X Q B or Out B " Out A ae Q B .
If A is deterministic then B is so. If A recognizes a language, then LpBq " LpAq X T pHq. If it computes a function and is deterministic, then ComppBq " ComppAq ae T pHq; in the general case, Comp nd pBq " Comp nd pAq ae T pHq. If A is an FA over F and H Ď F, then A ae H :" xH, Q A , δ AaeH , Out A y where δ AaeH is the restriction of δ A to the tuples pf, q 1 , . . . , q ρpf q q such that f P H, is a subautomaton of A. Its set of states is Q A (some states may not be accessible).

The Weak Recognizability Theorem ( [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], Chapters 5 and 6 and [START_REF] Courcelle | Fly-automata, model-checking and recognizability[END_REF]) states that, for each MS sentence ϕ expressing a graph property and each integer k, one can construct a deterministic finite automaton A ϕ,k over F k that recognizes the set of terms t P T pF k q such that Gptq |ù ϕ. In [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Section 7.3.1 we prove more: we construct a deterministic FA A ϕ,8 on F 8 that recognizes the terms t P T pF 8 q such that Gptq |ù ϕ. The automata A ϕ,k are subautomata of A ϕ,8 .

(2) Products of fly-automata. Let A 1 , ..., A k be FA over a signature F , and g be a computable mapping from Q A1 ˆ...ˆQ A k to some effectively given domain D. We define A :" A 1 ˆg ... ˆg A k as the FA with set of states Q A1 ˆ... ˆQA k , transitions defined by: δ A pf, q 1 , . . . , q ρpf q q :" tpp 1 , . . . , p ρpf q q | p i P δ Ai pf, q 1 ris, . . . , q ρpf q risq for each iu where qris is the i-th component of a ρpf q-tuple of states q, and output function defined by:

Out A ppp 1 , . . . , p k qq :" gpp 1 , . . . , p k q.
Depending on g, A recognizes a language or defines a function.

(3) Output composition. Let A be an FA with output mapping: Q A Ñ D and g be computable: D Ñ D 1 . We let g ˝A be the automaton obtained from A by replacing Out A by g ˝Out A . If A is deterministic, then Comppg ˝Aq " g ˝ComppAq. In the general case, Comp nd pg ˝Aq " p g ˝Comp nd pAq where p gpαq :" tgpdq | d P αu.

(4) Image. Let h : T pHq Ñ T pF q be a relabelling having a computable inverse h ´1 such that h ´1pf q is finite for each f P F . If L Ď T pHq, then hpLq :" thptq | t P Lu. If A is an FA over H, we let hpAq be the automaton over F obtained from A by replacing each transition f rq 1 , ¨¨¨, q ρpf q s Ñ A q by hpf qrq 1 , ¨¨¨, q ρpf q s Ñ q. It is an FA by Proposition 45 of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]. We say that hpAq is the image of A under h. It is not deterministic in general, even if A is. We have hpLpA, qqq " LphpAq, qq for every state q and, if A defines a language, then hpLpAqq " LphpAqq because hpAq has the same accepting states as A. If A computes a function, then Comp nd phpAqqptq= Ť tComp nd pAqpt 1 q | t 1 P h ´1ptqu.

(5) Inverse image. Let h : T pHq Ñ T pF q be a computable relabelling. If K Ď T pF q, then h ´1pK q :" tt P T pHq | hptq P Ku. If A is an FA over F , we define h ´1pAq as the FA over H with transitions of the form f rq 1 , ¨¨¨, q ρpf q s Ñ q such that hpf qrq 1 , ¨¨¨, q ρpf q s Ñ A q. We call h ´1pAq the inverse image of A under h ( [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Definition 17(h)); it is deterministic if A is so. We have Lph ´1pAq, qq " h ´1pLpA, qqq for every state q. If A defines a language, then Lph ´1pAqq " h ´1pLpAqq. If A computes a function α: T pF q Ñ D, then h ´1pAq defines α ˝h : T pHq Ñ D. In Section 1.3 we have noted that if αpY 1 , ..., Y m q is a function on terms in T pF q, S 1 , ..., S m are set terms over X 1 , ..., X s and βpXq :" αpS 1 pXq, ..., S m pXqq (with X " pX 1 , ..., X s q) then β " α ˝h where h:T pF psq q Ñ T pF pmq q is the relabelling that encodes the tuple pS 1 , ..., S m q. If α is computed by an FA A, then β is computed by h ´1pAq.

Example 5: The number of runs of a nondeterministic FA. Let A be a nondeterministic FA over F without output. For each t P T pF q, we define # AccRun ptq as the number of accepting runs of A on t. We will construct a deterministic FA B that computes # AccRun . We define it from detpAq in such a way that, for each term t, if q detpAq ptq " tq 1 , ..., q p u, then q B ptq " tpq 1 , m 1 q, ..., pq p , m p qu where m i is the number of runs of A that yield q i at the root of t. It is convenient to consider such a state as the finite mapping µ:Q A Ñ N such that µpq i q " m i and µpqq " 0 if q R tq 1 , ..., q p u. As output function, we take Out B pµq :" Σ µpqq | q P Acc A . Some typical transitions are as follows, with states handled as finite mappings:

a Ñ µ such that µpqq :" if a Ñ A q then 1 else 0, for each q P Q A , f rµ 1 , µ 2 s Ñ µ such that µpqq :" Σ µ 1 pq 1 q.µ 2 pq 2 q | f rq 1 , q 2 s Ñ A q , for each q P Q A .
The summations are over multisets and do not give the infinite value ω. If A has nondeterminism degree d on a term t, then it has at most |t| d runs on this term; the size of a state of B is thus Opd 2 . logp|t|qq where numbers of runs are written in binary.

In this example, we can consider that a state q of A at a position u is enriched with an attribute that records information about all the runs of A on the subterm issued from u that reach state q at u. This information is the number of such runs. We get a nondeterministic FA A 1 whose states are pairs pq, mq in Q A ˆN`. The FA B is then obtained from detpA 1 q. This observation will be developped and formalized in Section 3.2.

Polynomial-time fly-automata

We now classify fly-automata according to their computation times. Definitions 6: Polynomial-time fly-automata and related notions A deterministic FA over a signature F , possibly with output, is a polynomialtime FA (a P-FA) if its computation time on any term t P T pF q is P-bounded (cf. Section 1.5). It is an FPT-FA or an XP-FA if its computation time is, respectively, FPT-bounded or XP-bounded. It is a linear FPT-FA if the computation time is bounded by f pSigptqq.}t} (equivalently by f 1 pSigptqq. |t|) for some fixed function f (or f 1 ). The first three notions coincide if F is finite. A deterministic FA A over F is an XP-FA if and only if A ae F 1 is a P-FA for each finite subsignature F 1 of F . Lemma 7: Let A be an FA over a signature F.

(1) If A is deterministic, it is a P-FA, an FPT-FA or an XP-FA if and only if there are functions p 1 , p 2 , p 3 such that, in the run of A on any term t P T pF q: p 1 p}t}q bounds the time for computing a transition, p 2 p}t}q bounds the size of a state, p 3 p}t}q bounds the time for checking if a state is accepting or for computing the output 10 , and these functions are respectively polynomials, FPT-bounded or XP-bounded.

(2) In the general case, detpAq is a P-FA, an FPT-FA or an XP-FA if and only if there are functions p 1 , ..., p 4 such that, in the determinized run of A on any term t P T pF q: p 1 p}t}q bounds the time for computing the next transition 11 , p 2 p}t}q and p 3 p}t}q are as in (1), p 4 p}t}q bounds the nondeterminism degree of A on t, and these functions are respectively polynomials, FPT-bounded or XP-bounded.

Proof : We prove (2) that yields (1). "Only if". If detpAq is a P-FA with bounding polynomial p (i.e., the computation time is bounded by pp}t}q), then, one can take p i " p for i " 1, ..., 4.

"If". Let us conversely assume that A has bounding polynomials p 1 , ..., p 4 . Let t be a term of size }t} " n. The states of detpAq on t are sets of at most p 4 pnq words of length at most p 2 pnq, that we organize as trees with at most p 4 pnq branches. Firing a transition of detpAq at an occurrence u in t of a binary symbol f with sons u 1 and u 2 uses the following operations: for all states q 1 at u 1 and q 2 at u 2 , we compute in time bounded by p 4 pnq 2 .p 1 pnq the states of δ A pf, q 1 , q 2 q and we insert them in the already constructed tree intended to encode the state of detpAq at u. In this way we eliminate duplicates. Each insertion takes time at most p 2 pnq, hence the total time is bounded by p 4 pnq 3 .pp 1 pnqp 2 pnqq.

In time bounded by p 3 pnq.p 4 pnq we can check if the state at the root is accepting, and in this case, we can compute the output. The case of symbols of different arities is similar. As |t| ď n, we can take the polynomial ppnq :" n.pp 1 pnq `p2 pnqq.p 4 pnq ρpF q`1 `p3 pnq.p 4 pnq to bound the global computation time.

The proof yields the result for the two other types of bound. 10

By using Out A ; it bounds also the size of the output.

Remarks and examples 8: (1) For finding if a deterministic FA is a P-FA, an FPT-FA or an XP-FA, the main value to examine is the maximal size of a state, to be bounded by p 2 , because in most cases, computing the output or the state yielded by a transition is doable in polynomial time (with a small constant exponent) in the size of the considered states. For an FA that is not deterministic, we must also examine the degree of nondeterminism to be bounded by p 4 .

(2) For every MS formula ϕpXq with X " pX 1 , ..., X s q that expresses a graph property, we can construct a linear FPT-FA A 8 over F psq 8 that recognizes the set of terms t ˚X such that Gptq |ù ϕpXq. The functions p 1 , p 2 , p 3 of Lemma 7(1) depend only on the minimum k such that t P T pF psq k q. The recognition time is thus f pkq. |t| and even f 1 pkq. ˇˇV Gptq ˇˇif t is a good term (cf. the end of Section 1.2). The function f pkq may be a polynomial or a hyper-exponential function. (Concrete cases are shown in Table 20 of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF].) For each k, A 8 has a finite subautomaton A k over F psq k that recognizes the set tt ˚X P T pF

psq k q | Gptq |ù ϕpXqu. We have A k Ď A k 1 if k ă k 1 ([12], Section 7.3.1).
(3) In our applications to graphs, ρpF q " 2. Furthermore, the only nondeterministic transitions are those from the nullary symbols. It follows that the bound p 4 pnq 3 .pp 1 pnq`p 2 pnqq in the proof of Lemma 7 can be replaced by p 4 pnq 2 .pp 1 pnq`p 2 pnqq. As global time complexity, we get n.pp 1 pnq`p 2 pnqq.p 4 pnq 2 `p3 pnq.p 4 pnq and, in most cases, Opn.p 1 pnq.p 4 pnq 2 q.

(4) If t P T pF 8 q, its height, the number of vertices of Gptq (it is the number of occurrences of the nullary symbols in C) and the finite sets of port labels πptq and µptq (cf. Section 1.2) can be computed by P-FA. The set of good terms is thus P-FA recognizable.

The states of the P-FA A ht that computes the height are positive integers and its transitions are such that q A ht ptq " htptq. A term t is uniform if and only if any two leaves of its syntactic tree are at the same distance to the root. This property is not MS expressible. It is equivalent to the condition that, for every position u with sons u 1 and u 2 , the subterms t{u 1 and t{u 2 have same height. The automaton A ht can thus be modified into a P-FA A Unif that decides uniformity. Its set of states is N `Y tErroru and its transitions are such that q A Unif ptq is htptq if t is uniform and Error otherwise.

(5) The mapping SatX.P pXq that associates with a term t the set of sets X Ď P osptq that satisfy P pXq is not P-FA computable, and even not XP-FA computable in general for the obvious reason that its output is not always of polynomial size (take P pXq always true) 12 .

Proposition 9: Let F be a signature. Every P-computable (resp. FPTcomputable or XP-computable) function α on T pF q is computable by a P-FA (resp. by an FPT-FA or an XP-FA).

Proof : Consider the deterministic FA A over F with set of states T pF q that associates with each position u of the input term t the state t{u, i.e., the subterm of t issued from u. The state at the root is t itself, and is obtained in linear time. We take α as output function. Then A is a P-FA (resp. an FPT-FA or an XP-FA).

Hence, our three notions of FA may look uninteresting. Actually, we will be interested by giving effective constructions of P-FA, FPT-FA and XP-FA from logical expressions of functions and properties (possibly not MS expressible) that are computable or decidable in polynomial time on graphs of bounded tree-width or clique-width. Our motivation is to obtain uniform, flexible and implementable constructions.

All our existence proofs are effective. When we say that a function is P-FA computable, we mean that it is computable by a P-FA that we have constructed or that we know how to construct by an algorithm, and for which the polynomial bound on the computation time can be proved. The same remark applies to FPT-FA and XP-FA computability.

Transformations and compositions of automata

In view of building algorithms by combining previously constructed automata, we define and analyze several operations on automata.

Proposition 10: Let A 1 , ..., A r be P-FA that compute functions α 1 , ..., α r : T pF q Ñ D. There exists a P-FA A that computes the function α : T pF q Ñ D r such that αptq :" pα 1 ptq, ..., α r ptqq. If A 1 , ..., A r are FPT-FA or XP-FA, then A is of same type.

Proof : The product automaton A " A 1 ˆg ... ˆg A r where gpq 1 , ..., q r q :" pOut A1 pq 1 q, ..., Out Ar pq r qq is a deterministic FA (cf. Definition 4(2)) that computes α. The computation time of A on a term is the sum of the computation times of A 1 , ..., A r on this term. The claimed results follow.N ext we consider operations defined in Definition 4 that transform single automata.

Proposition 11: Let A be a P-FA that computes α : T pF q Ñ D.

(1) If g is a P-computable function D Ñ D 1 , then, there is a P-FA over F that computes g ˝α.

(2) Let h : F 1 Ñ F be a relabelling. There exists a P-FA over F 1 that computes the mapping α ˝h : T pF 1 q Ñ D.

The same implications hold for FPT-FA and XP-FA.

Proof : (1) The deterministic FA g ˝A defined from A (output composition) by replacing Out A by g ˝Out A computes g ˝α. The size of an output is polynomially bounded, hence, we get a P-FA.

(2) Immediate by the inverse image construction. Recall that h is computable in linear time (cf. Section 1.4).

Each class P-FA, FPT-FA and XP-FA is preserved in both cases. Proposition 12: Let h : F Ñ F 1 be a relabelling with a computable inverse. Let A be a P-FA (resp. an FPT-FA or an XP-FA) that computes α : T pF q Ñ D. The fly-automaton detphpAqq over F 1 is a P-FA (resp. an FPT-FA or an XP-FA) if and only if the nondeterminism degree of hpAq is P-bounded (resp. FPT-bounded or XP-bounded) in the size of terms over F 1 .

Proof : Immediate consequence of the definitions and Lemma 7.

In the sufficient conditions, the bounds on ndeg hpAq ptq can be replaced by bounds on ˇˇQ A ae h ´1ptq ˇˇ, the number of states of A used on input terms t 1 such that hpt 1 q " t, that are frequently easier to evaluate. The following counter-example shows that unless P"NP, there is no alternative image construction that preserves the polynomial-time property.

Counter-example 13:

There exist a finite signature F and a P-FA decidable property P pXq of terms in T pF p1q q such that DX.P pXq is not P-FA decidable unless P"NP.

We give a sketch of proof that uses a reduction from SAT, the satisfiability problem for propositional formulas. There exists a finite signature F and a Pdecidable property P pXq of terms in T pF p1q q such that each instance of SAT is encoded by a term t P T pF p1q q and each solution of this problem corresponds to a set X of positions of t that satisfies P pXq. Hence P pXq is P-FA decidable by Proposition 9. Since DX.P pXq is not P-decidable unless P"NP, it is not P-FA decidable, again by Proposition 9.

Examples 14: P-FA for cardinality and identity. (a) We consider the function Card that associates with a set X of positions of a term t P T pF q its cardinality |X|. Hence, the corresponding mapping : T pF p1q q Ñ N is computed by a P-FA A CardpXq whose states are the natural numbers. The computation time is Opn. logpnqq. It is Opnq if we admit that the addition of two numbers can be done in constant time.

From A CardpXq we can construct, for each integer p, a P-FA A CardpXqďp to check that X has at most p elements. However, the automata A CardpXqďp can be handled as instanciations of a unique P-FA that takes as input a term t, a set of positions X of this term and an integer p as auxiliary input.

(b) We consider the function Id that associates with a set X of positions of a term this set itself. The construction of a FA denoted by A Id pXq for the function Id is straightforward (cf. Example 3(b)). Its states are sets of positions of the input term, hence have size Op}t} 2 q (cf. Section 1.1). The automaton A Id pXq is a P-FA. It may look trivial, but it will be useful for Corollary 18 or when combined with others, by means of Proposition 15 (see Section 4.1.1 for an example).

3 Fly-automata for logically defined properties and functions

We now examine if and when the transformations of automata representing certain logical constructions preserve the classes P-FA, FPT-FA and XP-FA. From Counter-example 13, we know that this is not the case for existential set quantifications. We also examine in the same perspective the logic based functions defined in the Introduction. We consider automata on general effectively given signatures, that check properties or compute functions on terms. Applications to graphs will be considered in Section 4.

Two functions (or properties) α and β are of same type if they have the same number of set arguments.

Proposition 15: (1) If α 1 , ..., α r are P-FA computable functions of same type and g is a P-computable function (or relation) of appropriate type, the function (or the property) g ˝pα 1 , ..., α r q is P-FA computable (or P-FA decidable).

(2) If α 1 , α 2 and P are P-FA computable functions of same type and P is Boolean-valued, then the function if P then α 1 else α 2 is P-FA computable.

(3) If P and Q are P-FA decidable properties of same type, then, so are P , P _ Q and P ^Q.

(4) The same three properties hold with FPT-FA and XP-FA.

Proof: Straightforward consequences of Propositions 10 and 11 (1). We denote by α ae P ^... ^Q the function if P ^... ^Q then α else K: it is the restriction of α to its arguments that satisfy P ^... ^Q and could be written p...pα ae P q ae ...q ae Q. (The symbol K stands for an undefined value). We now consider substitutions of set terms and variables (cf. Section 1.3).

Proposition 16: Let αpY 1 , ..., Y m q denote a P-FA function on terms in T pF q with set arguments Y 1 , ..., Y m . Let S 1 , ..., S m be set terms over X 1 , ..., X s . The function βpX 1 , ..., X s q :" αpS 1 , ..., S m q is P-FA computable. The same holds with FPT-FA and XP-FA.

Proof : We recall from Section 1.3 that β " α ˝h where h is a relabelling: T pF psq q Ñ T pF pmq q that modifies only the Boolean part of each symbol. If A is a P-FA that computes α, then B :" h ´1pAq is a P-FA by Proposition 11(2) that computes β. The same proof works for FPT-FA and XP-FA.

In Proposition 15, we combine functions and properties of same type. With the previous proposition, we can extend it to properties and functions that are not of same type. For example if we need P pX 1 , X 2 q ^QpX 1 , X 2 , X 3 q, we redefine P pX 1 , X 2 q into P 1 pX 1 , X 2 , X 3 q that is true if and only if P pX 1 , X 2 q is, independently of X 3 . Proposition 16 shows how to transform an automaton for P pX 1 , X 2 q into one for P 1 pX 1 , X 2 , X 3 q. Then P pX 1 , X 2 q ^QpX 1 , X 2 , X 3 q is equivalent to P 1 pX 1 , X 2 , X 3 q ^QpX 1 , X 2 , X 3 q and we can apply Proposition 15.

By the definitions, Comppdetppr s pCqqq is equal to SetValx.αpxq hence, is P-FA, or FPT-FA or XP-FA computable by Lemma 7, depending on A as above. ˝The construction of this proof is generic in that it applies to any deterministic FA A over F psq , even that is not of type XP. The hypotheses on the type, P, FPT or XP of A are only used to determine the type of the resulting automaton.

Corollary 18: If P pXq is a P-FA decidable property, then the functions Satx.P pxq and #x.P pxq are P-FA computable. The same implication holds with FPT-FA and XP-FA.

Proof: We observe that Satx.P pxq " SetValx.αpxq where αpxq :" if P pxq then x else K. The result follows then from Propositions 15(2), Theorem 17 and a variant of A IdpXq of Example 14(b). However, we can give a direct construction that modifies the one of the proof of Theorem 17. We replace each B i by B 1 i such that:

run B 1 i ,t˚X puq " H if X i {u " H, run B 1
i ,t˚X puq " twu if X i {u " tu.wu (positions are Dewey words) and

run B 1 i ,t˚X puq " Error B 1 i if |X i {u| ě 2.
Then, we make the product A ˆB1 1 ˆ... ˆB1 s into a deterministic automaton C 1 with set of states tError C 1 u Y ppQ A ´tError A uq ˆPď1 prρpF qs ˚qs q similarly as in the proof of Theorem 17. The deterministic automaton C 2 , defined as detpprpC 1 qq equipped with the output function such that for Z Ď Q C 1 " Q prpC 1 q : Out C 2 pZq :" tpx 1 , ..., x s q | pq, tx 1 u, ..., tx s uq P Z, Acc A pqq " T rueu, p1q defines Satx.P pxq. The states of prpC 1 q at a position u of t are Error C 1 and tuples prun A,t˚pX1,...,Xsq puq, X 1 , ..., X s q such that |X 1 |, ..., |X s | ď 1 and X 1 Y ... YX s Ď rrs ˚. Since A is deterministic, there are at most 1 `p|t| `1q s different such states at each position u. The nondeterminism degree of detpprpC 1 qq is bounded as in the proof of Theorem 17. The conclusions follow from Lemma 7.

Since the value #x.P pxq on a term t is computable in linear time from that of Satx.P pxq, we get the corresponding assertions (by using Proposition 11(1)). However there is a more direct construction that does not use Satx.P pxq as an intermediate step (see below (3.2,2.4)). It is related to (but does not coincide with) counting the number of accepting runs of prpC 1 q, which we did in Example 5.

˝Remarks 19: (1) From SetValx.αpxq, we can obtain in polynomial time the maximum or the minimum value of αptx 1 u, ..., tx s uq if the range of α is linearly ordered and two values can be compared in polynomial time. The corresponding functions are thus P-FA (or FPT-FA, or XP-FA) computable. Alternative constructions will be given below.

(2) The results of Theorem 17 and Corollary 18 remain valid if each condition SglpX i q is replaced by CardpX i q " c i or CardpX i q ď c i for fixed integers c i . In particular, we can compute: #X.pP pXq ^CardpX 1 q ď c 1 ^... ^CardpX s q ď c s q.

The exponents in the bounding polynomial become larger, but they still depend only on the numbers c 1 , ..., c s . (The polynomial ppnq " 1 `pn `1q s in the proof of Theorem 17(1) is replaced by 1 `pn `1q c1`...`cs ). By Counterexample 20 below, this fact does not hold with CardpX i q ě c i : just take c i " 0. ˝In Theorem 17, we only handle first-order quantifications. Counter-example 13 has shown that we cannot replace them by arbitrary set quantifications. We now give a counter-example that does not use any complexity hypothesis.

Counter-example 20: We sketch a proof that the image construction for FA that corresponds to an existential set quantification does not preserve the polynomial-time property.

We consider terms over F " tf, g, au where f is binary, g is unary and a is nullary. For every position u of t P T pF q, we let spuq :" |P osptq{u|. For a set X of positions of t, we define mpXq as the multiset of numbers spuq | u P X . We let P pXq mean the following: (i) X ‰ H, its elements are first sons of occurrences of f and (ii) the multiset mpXq contains exactly two occurrences of each of its elements.

There is a P-FA A over F p1q that decides P pXq. The state run A,t˚X puq is Error if X{u contains a position different from u that is not the first son of an occurrence of f or if mpX{uq contains at least three occurrences of some integer. Otherwise, run A,t˚X puq " pα, mpX{uqq with α :" if u P X then 1 else 0. The accepting states are p0, mq where m is not empty and contains exactly two occurrences of each of its elements.

The nondeterministic FA pr 1 pAq decides DX.P pXq. The second components of any state belonging to run prpAq,t puq are the multisets mpX{uq that do not contain three occurrences of a same integer and are associated with a set X of positions containing only first sons of occurrences of f . The maximum cardinality of the set run prpAq,t puq is the nondeterminism degree of prpAq on t. It is not polynomially bounded in |t| hence prpAq is not a P-FA.

For a comparison with Counter-example 13, note that we can easily build a P-FA that decides DX.P pXq without using prpAq as an intermediate step. [START_REF] Ganian | A unified approach to polynomial algorithms on graphs of bounded (bi-)rank-width[END_REF]

Monadic Second-order constructions

Although Theorem 17 does not extend to arbitrary existential set quantifications, we can get some results for them and more generally, for the computation of multispectra and the derived functions such as #X.P pXq, SpX.P pXq, MinCardX.P pXq defined in the introduction and some others. In particular, we will consider SatX.P pXqptq (the set of tuples X that satisfy P in t). This function generalizes Satx.P pxqptq considered in Section 3.1. We first present some general constructions relative to FA. To simplify notation, we write definitions, conditions and transitions of automata for operation symbols of arity 0 or 2. The generalization to other arities is immediate.

Attributed automata

Let H be an effectively given signature and A be a deterministic FA over H without output. Let D be an effectively given H-algebra. The mapping val D ae LpAq (a partial function: T pHq Ñ Dq is computed by the deterministic FA A ˆg D with set of states Q A ˆD and output function g (cf. Definition 4(2) and Example 3(a)) such that gpq, dq :" if q P Acc A then d else K (with K R D, standing for "undefined"). We will denote this FA by A ˙D and call it an attributed fly-automaton. We consider d in a state pq, dq as an attribute of q (cf. Example 5). We will give a slightly more general notion of attributed FA at the end of this section.

Assume that we also have a signature F and a computable relabelling h : H Ñ F (cf. Definition 4(4); in particular h ´1pf q is finite for each f ) extended into h : T pHq Ñ T pF q. We want to compute, for every term t P T pF q, the following objects: (a) γptq :" tval D pt 1 q | t 1 P LpAq X h ´1ptqu P P f pDq, (b) ξptq :" val D pt 1 q | t 1 P LpAq X h ´1ptq P M f pDq (ξptq is a finite multiset over D).

In the next case, D is a distributive H-algebra and we want to compute: (c) θptq :" ]ξptq, where ] is applied to finite multisets over D, that is a commutative monoid with neutral element 0 D . We recall from Section 1.1 that a multiset over D is finite if the total number of occurrences of its elements different from 0 D is finite. Then, ]α is well-defined if α is finite. We have ]α :" ]β where β is obtained from α by removing all occurrences of 0 D and we evaluate ]β with the rules ]pβ 1 \ β 2 q :" p]β 1 q ] p]β 2 q and ]H :" 0 D .

We will prove that SpX.P pXq and SatX.P pXq are instances of Case (a), MSpX.P pXq of Case (b) and #X.P pXq of Case (c) with A " A P pXq , H " F psq and h " pr : F psq Ñ F . Case (c) will also be useful for computing optimizing functions (see Section (3.2.3)).

Proposition 21: Let F, H, h,A and D be as above. The functions γ, ξ and θ are computable by deterministic FA's.

Proof : In all cases we will use B :" hpA˙Dq, the image of the deterministic FA A ˙D under h, that is not deterministic in general. Cases (a) and (b) are particular instances of Case (c), but we think useful to present Case (a) first.

Case (a) The function computed by detpBq is γ, up to the value K that is not in D. More precisely γptq " Comp nd pBqptq ´tKu.

To prove this claim, we consider an element of γptq of the form val D pt 1 q for t 1 P LpAq X h ´1ptq. We have q A˙D pt 1 q " pq, val D pt 1 qq for some q in Acc A . Then B has a run on t " hpt 1 q that yields state pq, val D pt 1 qq at the root. Since val D pt 1 q ‰ K, we have val D pt 1 q " gppq, val D pt 1 qqq P Comp nd pBqptq´tKu. For the other direction, let d P Comp nd pBqptq´tKu. Then pq, dq P run B,t proot t q for some accepting state q. There is t 1 P LpA, qq such that hpt 1 q " t and d " val D pt 1 q. Hence, d P γptq and we have the claimed equality.

The set γptq can thus be computed by running B deterministically (i.e., by running detpBq, cf. Section 2.1) or by using an enumeration algorithm that outputs one by one its elements [START_REF] Durand | Object enumeration[END_REF].

Remarks: (1) When defining detpBq or running B deterministically, we can eliminate the pairs pError, dq as the values d arising from the corresponding runs will not contribute to γptq (but they can occur in alternative accepting runs).

(2) The states of detpBq are finite subsets of Q A ˆD (or rather pQ A tErroruq ˆD). It is convenient to identify such a set α with the mapping α : Q A Ñ P f pDq such that αpqq :" td P D | pq, dq P αu. This mapping is finite in the sense of Section (1.4) if the empty set is the "zero element" of P f pDq. That is, α ´1pP f pDq ´tHuq is finite. It can also be identified with the finite set of pairs pq, αpqqq such that αpqq ‰ H. In further constructions, the sets αpqq will be aggregated into combinations of values by the associative and commutative operation ] of a distributive algebra with domain of D.

(3) For clarity, we spell out the transitions of detpBq by using the latter presentation of its states. For a nullary symbol a P F , we have a Ñ detpBq β where β is the set of pairs pq, tb D | b P h ´1paq X δ ´1

A pqquq such that h ´1paq X δ ´1 A pqq ‰ H. For a binary symbol f P F, we have f rα 1 , α 2 s Ñ detpBq β where β is the set of pairs of the form pq, Ť tg D pα 1 pq 1 q, α 2 pq 2 qq | g P h ´1pf q, grq 1 , q 2 s Ñ A quq such that the second component of this pair is not empty. This formulation shows that β can be computed with the following operations on P f pDq: set union and the extensions to sets of the operations g D . Case (c) Here D "xD, ], 0, pg D q gPH y is a distributive H-algebra, and we want to compute:

θptq :" ] val D pt 1 q | t 1 P LpAq X h ´1ptq .
First we extend the mapping val D to finite sets of terms T Ď T pHq by: val D pT q :" ] val D ptq | t P T .

Note that val D ptq | t P T is a finite multiset. The associativity and commutativity of ] and the distributivity of g D over ] yield: val D pT Z T 1 q " val D pT q ] val D pT 1 q and p2q val D pgpT, T 1 qq " g D pval D pT q, val D pT 1 qq. p3q

Recall that we only write such equalities for binary symbols g because their extensions to other positive arities are obvious.

For q P Q A , we define θpt, qq :" val D pLpA, qq X h ´1ptqq and we get θptq " ] θpt, qq | q P Acc A . The righthand side of this equality is well-defined because θpt, qq ‰ 0 for finitely many states q, since h ´1ptq is finite. The sets LpA, qq X h ´1ptq for q P Q A are pairwise disjoint because A is deterministic, which ensures the equality.

We define as follows a deterministic FA C over F : its states are functions σ : Q A Ñ D such that σ ´1pD ´t0uq is finite (they can be seen as finite subsets of Q A ˆpD ´t0uqq; its transitions are defined in such a way that q C ptq, the state reached by C at the root of any term t P T pF q, is the mapping λq P Q A .θpt, qq (that can be seen as the finite set of pairs pq, θpt, qqq P Q A ˆD such that θpt, qq ‰ 0); its output function is Out C pσq :" ] σpqq | q P Acc A .

We now define the transitions. For a nullary symbol a P F , we define:

a Ñ C λq P Q A .val D ph ´1paq X δ ´1 A pqqq.
It is well-defined because h ´1paq X δ ´1 A pqq is finite. For a binary symbol f P F, we define:

f rσ 1 , σ 2 s Ñ C λq. ] g D pσ 1 pq 1 q, σ 2 pq 2 qq | hpgq " f , grq 1 , q 2 s Ñ A q . (4)
The operation ] is applied to a finite multiset (having finitely many elements different from 0) because h ´1pf q is finite, σ 1 pq 1 q ‰ 0 for finitely many states q 1 , similarly for σ 2 pq 2 q and g D p0, dq " g D pd, 0q " 0.

Before proving the validity of this construction, we compare C with detpBq. The state q detpBq ptq is a finite subset, say α, of Q A ˆD (we use the same notation as in the remark after Case (a)). The state q C ptq can be seen as the finite subset of Q A ˆD obtained by replacing the pairs pq, dq of α having the same first component q by the single pair pq, ]βpqqq where βpqq is a finite multiset whose underlying set is αpqq. The multiplicity of an element d of βpqq counts the number of ways it can be produced with state q.

Claim: For every t P T pF q, we have q C ptq " λq P Q A .θpt, qq. Proof : By induction on the structure of t. If t " a P F , the equality follows from the definitions. Let t " f pt 1 , t 2 q and q P Q A . By definition, we have θpt, qq " val D pLpA, qqX h ´1ptqq. For each term t 1 in LpA, qqXh ´1ptq, there is a unique 5-tuple pg, t 1 1 , t 1 2 , q 1 , q 2 q such that t 1 " gpt 1 1 , t 1 2 q and: hpgq " f , t 1 1 P LpA, q 1 q X h ´1pt 1 q, t 1 2 P LpA, q 2 q X h ´1pt 2 q and grq 1 , q 2 s Ñ A q. p5q

The existence and unicity of pg, t 1 1 , t 1 2 q follows from the equality hpt 1 q " t. The pair pq 1 , q 2 q such that t 1 1 P LpA, q 1 q, t 1 2 P LpA, q 2 q is unique because A is deterministic. Then we have grq 1 , q 2 s Ñ A q because t P LpA, qq.

Conversely, every such 5-tuple satisfying (5) yields a term t 1 " gpt 1 1 , t 1 2 q P LpA, qq X h ´1ptq. It follows that LpA, qq X h ´1ptq is the disjoint union of the sets gpT 1 pq 1 q, T 2 pq 2 qq for all triples pg, q 1 , q 2 q such that hpgq " f and grq 1 , q 2 s Ñ A q where, for every state p P Q A , T 1 ppq :" LpA, pqXh ´1pt 1 q and T 2 ppq :" LpA, pqX h ´1pt 2 q. For each such triple:

val D pgpT 1 pq 1 q, T 2 pq 2 qqq " g D pval D pT 1 pq 1 qq, val D pT 2 pq 2 qqq (6)
by (3). Hence, by (2) and the definitions:

θpt, qq " ] g D pval D pT 1 pq 1 qq, val D pT 2 pq 2 qqq | hpgq " f
and grq 1 , q 2 s Ñ A q " ] g D pθpt 1 , q 1 q, θpt 2 , q 2 qq | hpgq " f and grq 1 , q 2 s Ñ A q . [START_REF] Courcelle | Equivalences and transformations of regular systems; applications to recursive program schemes and grammars[END_REF] This equality is true for all states q P Q A . By induction, we have θpt 1 , pq " q C pt 1 qppq and θpt 2 , pq " q C pt 2 qppq for all p P Q A . Hence, θpt, qq " ] g D pq C pt 1 qpq 1 q, q C pt 2 qpq 2 qq | hpgq " f , grq 1 , q 2 s Ñ A q (8) and λq P Q A .θpt, qq " q C ptq by the definition of C, which completes the proof of the claim.H ence, the deterministic FA C computes θ, as desired. As noted above in Case (a), we can delete the Error state of A and define C so that q C ptq " λq P pQ A ´tErroruq.θpt, qq.

Case (b) is a special case of (c): we replace the effectively given H-algebra D by the distributive H-algebra E :" M f pDq (cf. Section 2.1). For t 1 P T pHq, val E pt 1 q " tval D pt 1 qu, as observed in Section 2.1. It follows that

ξptq :" val D pt 1 q | t 1 P LpAq X h ´1ptq " val E pLpAq X h ´1ptqq.
The states of C are finite mappings σ : Q A Ñ M f pDq such that we have q C ptq " λq P Q A . val D pt 1 q | t 1 P LpA, qq X h ´1ptq .

Case (a) is the instance of Case (c) where we take similarly E :" P f pDq. Remark

22:

More general attributed automata. Let A be a deterministic FA over a signature H. We define H ˚QA as the signature of ρpf q-ary symbols pf, q 1 , ..., q ρpf q q for all f P H and q 1 , ..., q ρpf q P Q A . Let D be an effectively given H ˚QA -algebra. Extending the notation of Section 1.1, we define val D : T pHq Ñ D by using the run of A on the considered term: val D pf pt 1 , ..., t ρpf q q :" pf, q 1 , ..., q ρpf q q D pd 1 , ..., d ρpf q q where q i " q A pt i q and d i " val D pt i q for i " 1, ..., ρpf q.

Hence val D ptq is computed by a deterministic FA with set of states Q A ˆD. We denote this FA by A ˙D and call it also an attributed fly-automaton. (As we do not exclude to extend in future articles the notion of an attributed FA, we leave "open" the definition).

As in Proposition 21, we let h be a computable relabelling: T pHq Ñ T pF q and we are interested in computing the functions γ, ξ and θ defined as above in terms of val D , now based on the H ˚QA -algebra D. For θ, we also assume that D is distributive. The construction for Case (c) (that yields the two other cases) works with the following adaptations: Equality (3) is replaced by: val D pgpT, T 1 qq " ] pg, q 1 , q 2 q D pval D pT XLpA, q 1 qq, val D pT 1 XLpA, q 2 qqq | q 1 , q 2 P Q A , and, in Equalities ( 4),( 6), ( 7) and ( 8), g D is replaced by pg, q 1 , q 2 q D .3 .2.2 Sets of satisfying tuples and counting functions.

We now compute the functions SatX.P pXq, #X.P pXq, SpX.P pXq, MSpX.P pXq, MinCardX 1 .P pXq and a few others by FA derived in uniform ways from a deterministic FA A that recognizes the language T P pXq representing P . (This language is defined Section 1.3).

As before, F is an effectively given signature, X " pX 1 , ..., X s q and P pXq is a property of terms in T pF q with s set arguments. We will use Proposition 21 with H :" F psq and h " pr : F psq Ñ F . We first consider the computation of the function SatX.P pXq. All other functions (they are called aggregate functions in the context of databases [1]) can be computed from it, but we will give direct constructions yielding XP algorithms whereas SatX.P pXq is not XPcomputable in general.

(3.2.2.1) Computation of SatX.P pXq. In order to apply Case (a) of Proposition 21, we define an F psq -algebra D such that: val D pt ˚Xq " X for all t ˚X P T pF psq q. p9q Each tuple X is an s-tuple of finite sets positions of t (they are Dewey words). We let r :" ρpF q and we take D :" P f prrs ˚qs . If X P D and i P rrs, we define i.X by replacing in X each word u P rrs ˚by i.u.

If pa, wq is a nullary symbol in F psq , (a P F and w P t0, 1u s ) we define: pa, wq D :" w where w :" tpX 1 , ..., X s qu such that:

X i :" if wris " 1 then tεu else H.
If pf, wq is binary, and with w as above, we define:

pf, wq D pX, Y q :" w Y 1.X Y 2.Y
where the union of sets is extended to tuples by: X Y Y :" pX 1 Y Y 1 , ..., X s Y Y s q. The validity of ( 9) is easy to check. We will denote by A Sat the deterministic FA detpBq obtained by Proposition 21 to compute γptq :" tX | t ˚X P LpAqu " SatX.P pXqptq.

For later use of we will denote it by D F,s .

Remarks: (1) The definitions are similar if X is a partition of P osptq encoded by a finite subset p X of rrs ˚ˆrss (cf. Section 1.3). ( 2) To make things (hopefully) clear we work out the construction of A Sat . Our description is based on the construction of Proposition 21 and the remark about Case (a). Each state of detpBq is handled as a finite function σ: Q A Ñ P f pDq " P f pP f prrs ˚qs q. We fix t P T pF q. For each state q of A, we define σpqq as the finite set of s-tuples X P PpP osptqq s such that q A pt ˚Xq " q. Since A is deterministic, σpqq X σpq 1 q " H if q ‰ q 1 and clearly, SatX.P pXqptq " Ť qPAccA σpqq. The transitions of detpBq are thus, for a nullary symbol a in F :

a Ñ λq P Q A .tw | pa, wq Ñ A qu.
For definining in a compact way the transitions on binary symbols, we define for disjoint sets E and E 1 , Z Ď PpEq s and Z 1 Ď PpE 1 q s :

Z f Z 1 :" tpX 1 Y Y 1 , . . . , X s Y Y s q | X P Z, Y P Z 1 u.
This operation is nothing but the extension to sets of the union of tuples of sets. Then, for a binary symbol f :

pf, wqrσ 1 , σ 2 s Ñ λq P Q A . Ť pf,wqrq1,q2sÑAq w f 1.σ 1 pq 1 q f 2.σ 2 pq 2 q, Out A Sat pσq :" Ť qPAccA σpqq. (3.2.2.2)
Computation of SpX.P pXq. We use again Case (a) of Proposition 21 with D such that: val D pt ˚Xq " p|X 1 | , ..., |X s |q for all t ˚X P T pF psq q. p10q We take D :" N s and we define (with `denoting the addition of vectors): pa, wq D :" pwr1s, ..., wrssq, pf, wq D pm, pq :" pwr1s, ..., wrssq `m `p.

The verification that ( 10) is true is straightforward. We will denote by A Sp the deterministic FA detpBq obtained in this way to compute γptq :" tp|X 1 | , ..., |X s |q | t ˚X P LpAqu " SpX.P pXqptq.

(3.2.2.3) Computation of MSpX.P pXq. We use Case (b) of Proposition 21 with the same F psq -algebra D as in the previous case. We will denote by A MSp the obtained deterministic FA that computes ξptq :" p|X 1 | , ..., |X s |q | t ˚X P LpAq " MSpX.P pXqptq.

We now detail the transitions of A MSp . A finite multiset over N s is a function m : N s Ñ N such that m ´1pN `q is finite. We have the following transitions: a Ñ λq P Q A .pλx P N s .if x P t0, 1u s ^pa, xq Ñ A q then 1 else 0q and f rσ 1 , σ 2 s Ñ λq P Q A .pλx P N s .Σ σ 1 pq 1 qpyq.σ 2 pq 2 qpzq | w P t0, 1u s , pf, wqrq 1 , q 2 s Ñ A q and x " w `y `z q.

In the second transition, the multiset is indexed by the 5-tuples pw, q 1 , q 2 , y, zq that satisfy x " w `y `z ^pf, wqrq 1 , q 2 s Ñ A q.

Hence, q A MSp ptq is a finite mapping, say σ, from Q A to M f pN s q such that, for every state q of A, σpqq is the finite multiset of tuples p|X 1 | , ..., |X s |q such that q A pt ˚Xq " q. Here, σpqq is a particular aggregation of the values in γpqq relative to the FA A Sat .

(3.2.2.4) Computation of #X.P pXq. We want to compute #X.P pXqptq " θptq defined as the cardinality of the set tX | t ˚X P LpAqu. As the multiset X | t ˚X P LpAq has only one occurrence of each element, θptq is its cardinality. In order to apply Case (c) of Proposition 21, we define a distributive F psq -algebra D :" xN, `, 0, pg D q gPF psq y with pa, wq D :" 1 and pf, wq D pm, pq :" m.p. Clearly, val D pt ˚Xq " 1 for all t ˚X P T pF psq q. We will denote by A # the deterministic FA C obtained in this way by Case (c) of Proposition 21.

Theorem 23: Let A be a deterministic FA over F psq that decides a property P pXq. The functions SatX.P pXq, MSpX.P pXq, SpX.P pXq and #X.P pXq are computable by deterministic FA's constructed from the tuple A that defines A. Complexity issues will be discussed in Section (3.2.4).

Optimizing functions

We now consider how to compute certain values defined by optimizing functions that minimize or maximize values defined from the set SatX.P pXqptq without using it as intermediate value for efficiency purposes. We will only discuss minimizations because maximizations are fully similar. This construction works because αpX 1 Z Y 1 , ..., X s Z Y s q " αpXq `αpY q. We will denote by A Min α the obtained deterministic FA.

(3.2.3.2) Minimal satisfying sets. We describe, in a uniform way, several FA that extract particular "minimal" sets from SatX.P pXqptq. (The extension to SatX.P pXqptq is easy.)

Let ď be a partial order on P f prrs ˚q. For each Z Ď P f prrs ˚q, we define MinpZq as the subset of Z consisting of its minimal elements with respect to ď. We want to compute, for each term t P T pF q, the set Min ď X.P pXqptq :" MinpSatX.P pXqptqq. Some interesting orders X ď Y on P f prrs ˚q are:

(i) X Ď Y, (ii) X Ď Pref pY q, (Pref pY q is the set of prefixes of the words in Y ), (iii) |X| ď |Y | , (iv) |X| ă |Y | or, |X| " |Y | and X ď lex Y, (v) X ď lex Y,
where ď lex is a lexicographic order on P f prrs ˚q defined below.

In the last two cases, ď is a linear order so that MinpZq is empty or singleton. Our method is also applicable to the quasi-order mint|u| | u P Xu ď mint|u| | u P Y u, but we will not discuss this extension.

The following notion will be useful in several cases.

Definition 24: Minimizing algebras. Let D be an effectively given H-algebra whose domain D has a decidable partial order ď and whose functions g D are increasing, i.e., g D p..., d, ...q ď g D p..., d 1 , ...q if d ď d 1 . For Z P P f pDq, the subset MinpZq of Z consists of its minimal elements with respect to ď. Hence it is empty if and only if Z is empty; it is computable if Z is finite.

We let MinpDq Ď P f pDq be the set of finite subsets Z of D such that MinpZq " Z. It is effectively given as the property MinpZq " Z is decidable. We define a distributive H-algebra:

MinpDq " xMinpDq, ], H, pg D q gPH y such that:

Z ] Z 1 :" MinpZ Y Z 1 q, a MinpDq :" ta D u if a is nullary, g MinpDq pZ, Z 1 q :" Minpg D pZ, Z 1 qq (" Minptg D pd, d 1 q | d P Z, d 1 P Z 1 uq if g is binary.
It is clear that ] is associative and commutative with neutral element H. We need only verify the distributivity property of g D over ]. We check that, for Z, Z 1 , Z 2 in MinpDq:

g MinpDq pZ ] Z 1 , Z 2 q " g MinpDq pZ, Z 2 q ] g MinpDq pZ 1 , Z 2 q,
i.e., by the definitions:

Minpg D pMinpZYZ 1 q, Z 2 qq " MinpMinpg D pZ, Z 2 qqYMinpg D pZ 1 , Z 2 qqq.
The righthand side is Minpg D pZ, Z 2 q Y g D pZ 1 , Z 2 qq. Clearly:

g D pMinpZ Y Z 1 q, Z 2 q Ď g D pZ, Z 2 q Y g D pZ 1 , Z 2 q,
but, since g D is increasing, for every d P g D pZ, Z 2 q Y g D pZ 1 , Z 2 q, there is

d 1 P g D pMinpZ Y Z 1 q, Z 2 q such that d 1 ď d. It follows that: Minpg D pMinpZ Y Z 1 q, Z 2 qq " Minpg D pZ, Z 2 q Y g D pZ 1 , Z 2 qq.
Hence, MinpDq is a distributive H-algebra. We call it a minimizing Halgebra.

In order to compute minimizing functions by FA, we will use the F p1qalgebra D " D F,1 :" @ P f prrs ˚q, pg D q gPF p1q D defined for computing SatX.P pXq (cf. Section 3.2.2.1). For each partial order ď on P f prrs ˚q such that the functions pf, wq D with f of positive arity and w P t0, 1u are increasing, we make D into a minimizing F p1q -algebra. We recall the definition of pf, wq D for a binary function f pX, X 1 q where X, X 1 are finite subsets of rrs ˚):

pf, wq D pX, X 1 q :" w Y 1.X Y 2.X 1 , p11q where w :" if w " 1 then tεu else H. Proposition 25: Let F be an effectively given signature and P pXq be a property of terms over it defined by a deterministic FA A over F p1q . Let ď be partial order making D F,1 into a minimizing algebra. The function Min ď X.P pXq is computable by a deterministic FA constructed from A (defined by a tuple of programs A) and the algorithm that decides ď.

Proof : We apply Case (c) of Proposition 21 to the distributive and minimizing F p1q -algebra MinpDq defined from ď.

We now examine the first four partial orders on P f prrs ˚q defined above. In each case we use Equality [START_REF] Courcelle | Fly-automata for checking MSO 2 graphs properties[END_REF] to verify that pf, wq D is increasing.

(i) Case of Ď. Each function pf, wq D is increasing, hence, we can compute for t P T pF q the set Min Ď X.P pXqptq :" MinpSatX.P pXqptqq of inclusion minimal sets X such that t |ù P pXq.

(ii) Case of X ď anc Y :ô X Ď Pref pY q. Each function pf, wq D is increasing, in particular because X ď anc Y ñ i.X ď anc i.Y . Hence, MinpSatX.P pXqptqq is the set of minimal sets X such that t |ù P pXq where minimality means that one cannot reduce a satisfying set by removing a node u or replacing it by one of its ancestors in Pref ptuuq. We denote by Min anc X.P pXq the corresponding function.

(iii) Case of X ď card Y :ô |X| ď |Y | : Equality [START_REF] Courcelle | Equivalences and transformations of regular systems; applications to recursive program schemes and grammars[END_REF] shows that |pf, wq D pX, X 1 q| " w `|X| `|X 1 |. Hence, |X| ď |Y | implies |pf, wq D pX, X 1 q| ď |pf, wq D pY, X 1 q|. We can thus compute the set MinpSatX.P pXqptqq of sets X of minimal cardinality such that t |ù P pXq. Their common cardinality is MinCardX.P pXqptq that we already know how to compute. We denote by Min card X.P pXq the corresponding function.

(iv) Case of X ď clex Y :ô |X| ă |Y | or, |X| " |Y | and X ď lex Y.
We denote by ĺ lex the lexicographic order on rrs ˚. Hence, every finite subset X of rrs ˚can be written in a unique way as a sequence of words SeqpXq :" pw 1 , ..., w p q such that X " tw 1 , ..., w p u and w 1 ă lex ... ă lex w p ; we have SeqpHq " pq not to be confused with pεq. The set P f prrs ˚q can thus be ordered lexicographically ; we denote this order by ď lex . Its least element is the empty set. If X " t1, 2, 11, ε, 222u and Y " t1, 2, ε, 111u then SeqpXq " pε, 1, 11, 2, 222q and SeqpY q " pε, 1, 111, 2q so that X ă lex Y . The order ď clex is lexicographic with priority on cardinality. We will denote the corresponding function by Min clex X.P pXq. To verify that the functions pf, wq D are increasing for ď clex , we have by [START_REF] Courcelle | Fly-automata for checking MSO 2 graphs properties[END_REF]:

Seqppf, wq D pX, Y qq " Seqpwq˝1.SeqpXq˝2.SeqpY q, p12q where ˝denotes the concatenation of sequences and i.pw 1 , ..., w p q :" pi.w 1 , ..., i.w p q. We have Seqpwq :" if w " 0 then pq else pεq. It is then clear that X ď clex Y and X 1 ď clex Y 1 imply pf, wq D pX, X 1 q ď clex pf, wq D pY, Y 1 q. This technique does not apply to ď lex because the functions pf, wq D are not increasing.

Example: Let F " tf, g, a, b, cu with a, b, c nullary, g unary and f binary. We let P pXq mean that, either each occurrence of a and no occurrence of b or c is below a position in X or, that each occurrence of b and no occurrence of a or c is below a position in X. One can construct terms showing that the five minimization functions based on property P pXq and the orders (i)-(v) are pairwise different.T he constructions of this section establish the following theorem, where F is an effectively given signature and X is an s-tuple of set variables.

Theorem 26: Let A be a deterministic FA over F psq that decides a property P pXq and αpXq be a linear function of the cardinalities of the sets forming its argument. The functions MinCardX 1 .P pXq, Min αX.P pXq, Min Ď X.P pXq, Min anc X.P pXq, Min card X.P pXq and Min clex X.P pXq are computable by deterministic FA constructed from α and the tuple A that defines A.

Proof : The corresponding constructions are done in Section (3.2.3.1) and Proposition 25. This theorem does not exhaust the possibilities of building FA by general methods, see Section 4.2.1.

Parameterized complexity

We now consider conditions ensuring that the automata constructed by Theorems 23 and 26 are P-FA, FPT-FA or XP-FA. We recall that if the signature F is finite, the notions of P-FA, FPT-FA and XP-FA coincide. Lemma 7 shows the importance of the nondeterminism degree for analyzing the computation time of determinized automata.

Theorem 27: Let F, s, A, P pXq and α be as in Theorems 23 and 26.

(1) If A is a P-FA such that the mapping ndeg prpAq is P-bounded, then, the properties DX.P pXq and @X.P pXq are P-FA decidable and the functions MSpX.P pXq, SpX.P pXq, #X.P pXq, MinCardX 1 .P pXq, Min αX.P pXq and Min clex X.P pXq are P-FA computable.

(2) If β: T pF psq q Ñ D is computed by a P-FA A such that ndeg prpAq is P-bounded, then the function SetValX.βpXq is P-FA computable.

(2) We now consider SetValX.βpXq where β is computed by a deterministic FA A over F psq . For each term t and X P PpP osptqq s we have βpt ˚Xq " Out A pq A pt ˚Xqq. Hence, SetValX.βpXqptq is the set of values Out A pqq for q P q detpprpAqq ptq. The time taken to compute SetValX.βpXqptq is that for computing the set q detpprpAqq ptq of cardinality at most ndeg prpAq ptq plus that for computing the final output, bounded by ndeg prpAq ptq.p 3 p}t}q. Hence, we conclude as in the cases considered in (1).

(3) The proofs are similar if p 1 , p 2 , p 3 and ndeg prpAq are FPT-or XP-bounded.R emarks 28: (1) Even if F is finite, we cannot omit in Theorem 27 the hypothesis that prpAq has a nondeterminism degree bounded in some way, because the validity of DX.P pXq can be determined in polynomial time from either MSpX.P pXq, SpX.P pXq, #X.P pXq or MinCardX 1 .P pXq. Otherwise, by Counter-example 13, we would have P=NP.

(2) Theorem 27 does not apply to Min Ď X.P pXq, Min anc X.P pXq and Min card X.P pXq because their outputs may be of exponential size in the size of the input tree.

Summary of results

The following table summarizes the preservation results of this section: we mean by this that the classes of functions and properties that are P-FA, FPT-FA or XP-FA computable (or decidable) are preserved under constructions of three types: composition, first-order and monadic second-order constructions.

Construction Conditions and proofs Composition g ˝pα 1 , ..., α r q, g is P-computable, if P then α 1 else α 2 , S 1 , ..., S m are set terms; P , P _ Q, P ^Q, α ae P, by Proposition 15 αpS 1 , ..., S m q, P pS 1 , ..., S m q.

and Theorem 17. FO const.

Dx.P pxq, @x.P pxq, SetValx.αpxq, by Theorem 17, Corollary 18. Satx.P pxq, #x.P pxq. MS const.

DX.P pXq, @X.P pXq, P or α is defined by SetValX.αpXq, a P-FA A #X.P pXq, MSpX.P pXq, such that ndeg prpAq SpX.P pXq, MinCardX.P pXq, is P-, FPT-or XP-bounded; Min clex X.P pXq by Theorem 27.

Table 1: Preservation results.

In the next section, we develop constructions specific to graphs.

Application to graphs

We wish to check DX.P pXq, @X.P pXq and to compute MSpX.P pXq, SpX.P pXq etc. in graphs Gptq defined by terms t in T pF 8 q. We recall that if P pXq is a graph property with s sets of vertices as auxilliary arguments, then L P pXq :"

tt ˚X P T pF psq 8 q | Gptq |ù P pXqu. The following fundamental result is proved in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Section 7.3.1 and in [START_REF] Courcelle | Fly-automata, model-checking and recognizability[END_REF].

Theorem 29: If P pXq is MS expressible, then the language L P pXq is recognized by a linear FPT-FA.

The proof uses an induction on the structure of the formula ϕ that expresses P pXq. Fly-automata are built for the atomic formulas13 X 1 Ď X 2 and edgpX 1 , X 2 q. The constructions of Proposition 15 (3,[START_REF] Bès | Expansions of MSO by cardinality relations[END_REF] and Theorem 27 are then used for handling logical connectives. The inductive construction shows that for each automaton built in this way, the number of states it reaches by runs on a term t depends only on ϕ and max µptq (this number bounds the clique-width of the graph Gptq). It follows from Theorem 27 that the functions MSpX.P pXq, SpX.P pXq, #X.P pXq, MinCardX 1 .P pXq, Min αX.P pXq and Min clex X.P pXq are computable by FPT-FA 14 .

Remark 30: To simplify the discussion, we let P be an MS expressible graph property without set arguments. A consequence of Theorem 29 (called in [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] the Weak Recognizability Theorem) is that for every integer k, the language L P X T pF k q is recognized by a finite automaton A P,k . A quick proof of this fact follows from the observation that the mapping t Þ Ñ Gptq is a monadic second-order transduction from T pF k q to the class of graphs of clique-width at most k and the Backwards Translation Theorem15 . However, this technique is not applicable to L P Ď T pF 8 q because the signature F 8 is infinite so that the mapping t Þ Ñ Gptq is not a monadic second-order transduction on T pF 8 q. From the practical view point, an FA A P,k constructed from this observation would be anyway very complicated and hard to implement. Graphs are always given by terms over F 8 or F u 8 (and not by adjacency lists). The constructions of Section 3 that are done for FA over an arbitrary effectively given signature have immediate applications to graphs via the signature F 8 . One adaptation to make is due to the fact that the set arguments X 1 , ..., X s denote sets of vertices of the defined graphs, hence sets of positions in the input terms of the nullary symbols in C. For example, the algebra D F,s used in Section (3.2.2.1) for computing SatX.P pXq must be modified into D 1 such that, for the binary symbol ', ' D 1 pX, Y q :" 1.X Y 2.Y . Similarily, for computing SpX.P pXq, we take D 2 such that ' D 2 pm, pq :" m `p. For the unary symbols f of F 8 (they are relab h or Ý Ý Ñ add a,b ), we take f D 1 pXq :" 1.X and f D 2 pmq :" m.

Although the FA for the atomic formulas X 1 Ď X 2 , edgpX 1 , X 2 q and Card p,q pX 1 q suffice for proving Theorem 29, it is useful to "precompute" FA for other frequently used MS properties. Table 2 lists bounds the sizes of the states in their runs on terms in T pF k q. We will define FA for some other basic properties and functions. By combining these automata as explained in the previous section, we can easily build automata for checking properties and computing functions expressed by formulas written with the basic ones and the logical connectives of MS logic. The FA of Table 2 concern the following properties: P artitionpX 1 , ..., X s q meaning that pX 1 , ..., X s q is a partition of the vertex set, St that the considered graph is stable, i.e., has no edge, LinkpX 1 , X 2 q that it has at least one edge from some vertex of X 1 to some vertex of X 2 P athpX 1 , X 2 q that X 1 consists of two vertices linked by an undirected path with vertices in X 2 (X 2 must contain X 1 ), Clique that the graph is a clique, Conn that it is connected, Cycle that it has an undirected cycle and DirCycle that it has a directed cycle. Finally, edgpX 1 , X 2 q is equivalent to LinkpX 1 , X 2 q ^SglpX 1 q ^SglpX 2 q. The automata are constructed in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] and the bounds on sizes of states are clear by inspecting the constructions.

Property

Size of a state Sgl, X 1 Ď X 2 , X 1 " H, Card p,q pX 1 q independent of k P artitionpX 1 , ..., X s q independent of k edgpX 1 , X 2 q Oplogpkqq St, LinkpX 1 , X 2 q Opkq P athpX 1 , X 2 q, DirCycle, Clique Opk 2 q Conn, Cycle Oplogpkq. mintn, k.2 Opkq uq Table 2: Sizes of states for some automata running on terms in T pF k q.

All automata are P-FA because computing the transitions involves only polynomial-time calculations. For the automata checking Conn and Cycle, the upper-bound Oplogpkq.nq (n is the number of vertices of the input graph) shows that they are P-FA.

Properties Sgl, St, Conn, DirCycle, Cycle and Clique are relative to the whole graph G. However, we need frequently their relativizations to sets of vertices, for example StrXs meaning that the induced subgraph GrXs is stable (cf. the examples in the Introduction). However, from an FA over F 8 that decides St, one gets by taking an appropriate inverse image 16 an FA over F p1q 8 that decides StrXs.

We defined in Section 1.2 the notions of good and irredundant terms. Proposition 35 in the appendix gives a polynomial-time algorithm that transforms a term into an equivalent good and irredundant one. We can build a P-FA GI that checks if the input term is good and irredundant. If A is a deterministic 16 We recall from Section 1.3 that it is based on the relabelling h: F p1q 8 Ñ F8 such that, for every a P C we have hppa, 0qq :" ∅, hppa, 1qq :" a and hpf q :" f for all other operations of F8. The same inverse image works for relativizing any property.

FA, then an FA constructed with Proposition 15 from the product of A and GI gives correct results on good irredundant terms and rejects the others. It has the same type (P, FPT or XP) as A.

A last technical point concerns notation. When dealing with terms t over effectively given signatures, we denote by #X.P pXq the mapping associating with a term t the number of tuples X of sets of positions that satisfy property P in t. In the present section, we will denote in the same way the mapping associating with a graph G the number of tuples of sets of vertices that satisfy P , and also the mapping t Þ ÝÑ #X.P pXqpGptqq for t P T pF 8 q, that we wish to compute by FA. The same convention will apply to MSpX.P pXq, SpX.P pXq etc.

Counting induced subgraphs

Let H be a connected undirected graph. An induced subgraph of an undirected graph G is H-induced if it is isomorphic to H. We can use FA to count and enumerate the H-induced subgraphs of a given graph. The property of a set X Ď V G that GrXs » H is MS expressible. Hence, automata that compute the functions #X.GrXs » H and SatX.GrXs » H will give us the desired algorithms. The property GrXs » H implies that X has fixed cardinality |V H |. Hence, we can apply Corollary 18 and the following remark. However, a direct construction yields in general a smaller FA.

For example let H be the graph House, i.e., the graph K 5 with vertex set r5s minus the four edges 1´4, 1´5, 3´4 and 2´5. We let X " pX 1 , X 2 , X 3 , X 4 , X 5 q and P pXq stand for: edgpX 1 , X 2 q ^edgpX 1 , X 3 q ^edgpX 2 , X 3 q ^edgpX 2 , X 4 q ^edgpX 4 , X 5 qê dgpX 3 , X 5 q^ edgpX 1 , X 4 q^ edgpX 1 , X 5 q^ edgpX 3 , X 4 q^ edgpX 2 , X 5 q.

A P-FA over F u k with Opk 2 q states for edgpX, Y q is constructed in [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], Section 5.1.2 and [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], Section 6.3. From Propositions 15 and 16, we get for P pXq a P-FA that uses Opk 20 q states on terms in T pF up5q k q, but a specific construction yields a P-FA using Opk 5 q states on these terms. By Corollary 18, we get FA that compute #X.P pXq and SatX.P pXq. However, the number of Houseinduced subgraphs of Gptq is only half of #X.P pXqptq because House has one automorphism apart from identity. Hence, the FA that computes #X.P pXqptq does some useless computations. We can avoid this drawback by replacing P pXq by P pXq^X 2 ă X 3 where ă is the lexicographic order on positions of the input term. An FA defining ă is easy to build. The role of this condition is to select a single 5-tuple for each House-induced graph. This linear order on V Gptq depends on the term t and the definition by Dewey words of the vertices. However, the value #X.P pXq is the same for all terms: it is order-invariant (cf. [START_REF] Courcelle | The monadic second-order logic of graphs X: Linear orders[END_REF] on this notion and [START_REF] Engelmann | First-order and monadic second-order model-checking on ordered structures[END_REF] for its applications to model-checking).

The same improvement applies to the enumeration problem in order to avoid duplications in the enumeration of House-induced subgraphs. But even without using any linear order, Theorem 17 and Corollary 18 yield P-FA that compute the functions #X.GrXs » H and SatX.GrXs » H for each fixed graph H.

Edge counting and degree

For a p-graph G and X Ď V G , we denote by β X the mapping that gives, for each label a the number of a-ports in X. If X " V G , we denote it by β G . We denote by Λrk, ns the set of mappings β : rks Ñ r0, ns such that Σ iPrks βpiq ď n. This set has cardinality `n`k k ˘(by an easy bijective proof), hence Θpn k q for fixed k. We will bound it by pn `1q k .

All automata in this section will be constructed so as to work correctly on good irredundant terms 17 . Irredundancy is useful for counting edges and we recall that the size of a good term t P T pF psq k q is Opn.k 2 q where n is the number of vertices of Gptq. Hence, computation times can be bounded in function of n.

(4.2.1) Counting the edges of induced subgraphs Given a directed graph G and X Ď V G , we let epXq be the number of edges of GrXs. This value is not the cardinality of a set Y Ď V G satisfying a property P pX, Y q by an obvious cardinality argument. However, we will compute it by an attributed FA B over F p1q 8 (cf. Remark 22). We let B :" A ˙D where A has set of states rN `Ñ Ns f (N `is the set of port labels), q B pt ˚Xq " pβ X , epXqq for every t ˚X P T pF p1q 8 q where β and e are relative to Gptq. The transitions of A are as follows:

'rβ, β 1 s Ñ λx P N `.pβpxq `β1 pxqq, Ý Ý Ñ add a,b rβs Ñ β, relab aÑb rβs Ñ β 1 where β 1 paq :" 0, β 1 pbq :" βpaq`βpbq and β 1 pxq :" βpxq if x R ta, bu, pa, iq Ñ λx P N `.pif x " a then i else 0q, where i P t0, 1u.

We now define an (F p1q 8 ˆQA q-algebra D (cf. Remark 22). Its domain is N and its operations are: p', β, β 1 q D pm, m 1 q :" m `m1 , p Ý Ý Ñ add a,b , βq D pmq :" m `βpaq.βpbq, prelab aÑb , βq D pmq :" m, pa, iq D :" 0.

The definition of p Ý Ý Ñ add a,b , βq D is correct because we assume t irredundant. The value epXq is the second component of the state reached by B :" A ˙D at the root of t ˚X P T pF p1q 8 q. Let t ˚X P T pF p1q k q denote a graph Gptq with n vertices (and X Ď V G ptq). Then q B pt˚Xq " pβ X , epXqq P Λrk, xsˆr0, xpx´1qs Ď Λrk, ns ˆr0, npn ´1qs where x :" |X|. There are less than pn `1q k`2 such states and they have size Opk. logpnqq. Transitions and outputs can be computed in time Opk. log 2 pnqq and so, B is a P-FA. (The log 2 pnq factor comes from the multiplication of two positive integers in r0, ns).

An algorithm of [START_REF] Broersma | Tight complexity bounds for FPT subgraph problems parameterized by the clique-width[END_REF] 18 computes the function Min eX.p|X| " pq, i.e., the minimum number of edges of an induced subgraph having p vertices. This is called the sparse p-subgraph problem. This algorithm takes time n.p Opkq on terms in T pF u k q. We can obtain it as an instance of our constructions by applying Case (c) of Proposition 21 and Definition 24. The construction we will describe works for directed graphs and, by an easy adaptation, for undirected ones.

We let A Card"p be the deterministic FA over F p1q 8 that checks the equality |X| " p. We let B p :" pA Card"p ˆAq ˙D (we omit some easy formal details) be the attributed FA that computes epXq for sets X of cardinality at most p. Let t ˚X P T pF p1q k q. The state q Bp pt ˚Xq is p|X| , β X , epXqq if |X| ď p and pError, β X , epXqq otherwise. Clearly, p|X| , β X , epXqq P r0, ps ˆΛrk, ps r0, ppp ´1qs. The states pError, β X , epXqq can be merged into a unique Error state. The accepting states are those of the form pp, β, mq and the computed value is m " epXq if the given set X has cardinality p. The number of states p|X| , β X , epXqq is less than pp `1q k`3 , these states have size Opk. logppqq, the computation time of a transition is Opk. log 2 ppqq and B p is a P-FA 19 .

For computing Min eX.p|X| " pq, we make D into a minimizing algebra (cf. Definition 24) by using the natural order on N. Then, 0 D " 0, m ] m 1 :" mintm, m 1 u. We take then C :" pr 1 pB p q whose nondeterminism degree is less than pp `1q k`3 on a term in T pF k q. The construction of Case (c) of Proposition 21 gives a deterministic FPT-FA C 1 , whose computation time is Op|t| .k. log 2 ppq.p 2k`6 q " Opn.k 3 . log 2 ppq.p 2k`6 q on input t P T pF k q where n is the number of vertices of Gptq.

More generally, we define epXq :" epX 1 q`...`epX s q and we want to compute the function Min eX.P pXq where P pXq is defined by a deterministic FA A P over F psq 8 . We extend the construction given above for Min eX.p|X| " pq: for each i " 1, ..., s, we let A i compute β Xi (it is an inverse image of A) and we build an attributed FA B P :" pA 1 ˆ... ˆAs ˆAP q ˙D such that q BP pt ˚Xq " pβ X1 , ..., β Xs , epXqq. Then, we make D into a minimizing algebra as above and we obtain in the same way a deterministic FA that computes Min eX.P pXq. Its type, FPT or XP, depends on A P . (4.2.2) Counting the edges between disjoint sets of vertices We consider directed graphs. We generalize the notion of outdegree of a vertex by defining epX 1 , X 2 q as the number of edges from X 1 to X 2 if X 1 and X 2 are disjoint sets of vertices and as K otherwise. Hence eptxu, V G ´txuq is the outdegree of x in G. To compute this function similarly as in (4.2.1), we define an attributed FA B :" A˙D over F p2q 8 . Its set of states is tpError, 0quYprN `Ñ Ns 2

f ˆNq and we want that, for t ˚pX 1 , X 2 q P T pF p2q 8 q:

q B pt ˚pX 1 , X 2 qq " pError, 0q if X 1 X X 2 ‰ H, and q B pt ˚pX 1 , X 2 qq " ppβ X1 , β X2 q, epX 1 , X 2 qq otherwise.

The transitions and the algebra D are easy to define. On a term in T pF p2q k q that denotes a graph with n vertices, each state belongs to the set tpError, 0quY pΛrpk, ns 2 ˆr0, pn ´1q 2 sq of cardinality less than pn `1q 2k`2 hence, has size Opk. logpnqq. Transitions and outputs can be computed in time Opk. logpnq 2 q. Hence, B is a P-FA.

(4.2.3) Maximum directed cut For a directed graph G, we want to compute the maximal number of edges from a subset X of V G to its complement, hence the maximal value of epX, X c q. This problem is considered in [START_REF] Lampis | On the algorithmic effectiveness of digraph decompositions and complexity measures[END_REF][START_REF] Ganian | A unified approach to polynomial algorithms on graphs of bounded (bi-)rank-width[END_REF]. The deterministic FA of Section (4.2.2), adapted by Proposition 16 to check epX, X c q uses less than pn `1q 2k`2 states on a term in T pF p1q k q denoting a graph G with n vertices. By the method used in Section (4.2.1), we get an algorithm that computes the maximal value of epX, X c q, for X Ď V G , in time Opn 4k`a q for some constant a. The article [START_REF] Ganian | A unified approach to polynomial algorithms on graphs of bounded (bi-)rank-width[END_REF] gives an algorithm taking time Opn 4.2 rpGq `bq where rpGq is the bi-rankwidth of the considered graph G. We recall that rpGq{2 ď cwdpGq ď 2.2 rpGq [START_REF] Kanté | The rank-width of edge-coloured graphs[END_REF]. Hence, our method gives an algorithm of comparable time complexity.

Regularity of a graph

The regularity of an undirected graph is not MS expressible because the complete bipartite graph K n,m is regular if and only if n " m and we can apply the arguments of Proposition 5.13 of [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] for proving this claim.

That a graph is not regular can be expressed by the formula DX, Y.pP pX, Y qŜ glpXq ^SglpY qq where P pX, Y q is the property epX, X c q ‰ epY, Y c q. By the construction of (4.2.2) and Propositions 15 and 16 it is P-FA decidable. We can apply Proposition 11(1) to get a P-FA for checking that a graph is not regular, hence also a P-FA that checks regularity. However, we can construct directly a simpler P-FA without using an intermediate nondeterministic automaton.

Let G be defined by an irredundant term t. The key fact is that if in Gptq{u, two a-ports x and y have degrees d and d 1 , then they have in G degrees d `p and d 1 `p for some p ě 0. The reason is that if an operation at position w above u adds an edge between x and some vertex z, then it also adds an edge between y and z because the labels of x and y are the same in Gptq{w and the irredundancy condition implies that there is no edge between y and z. Hence, the degrees of x and y are increased by the same value above u. If the degrees are different in Gptq{u, they are so in G. We recall that πpGq is the set of port labels of the vertices of G and that β G paq is the number of its a-ports. The notation is as in Section 4.2. The set of states of A Reg is defined as tErroru Y prN `Ñ pN Y tKuqs f ˆrN `Ñ Ns f q and we want that, for every term t P T pF 8 q: q AReg ptq " Error if two a-ports of Gptq have different degrees; otherwise, q AReg ptq " pB Gptq , β Gptq q where, for every a in πpGptqq, B Gptq paq is the common degree of all a-ports of Gptq and is K if there is no a-port.

In the run on a term t P T pF k q such that Gptq has n vertices, less than pn `1q 2k states occur and these states have size Opk. logpnqq. In the transition table (Table 3), pB, βq denotes a state that is not Error. Hence, if pB, βq is accessible, we have Bpaq " K if and only if βpaq " 0. We denote respectively by 0 and K the constant mappings with values 0 and K. We take maxtK, nu " n (for the transitions on '). It is clear that the transitions can be computed in time Opk. logpnqq. Hence, we have a P-FA A Reg .

Transitions Conditions

∅ Ñ pK, 0q a Ñ pB, βq Bpxq :" if x " a then 0 else K, βpxq :" if x " a then 1 else 0. add a,b rpB, βqs Ñ pB 1 , βq

If βpaq " 0 or βpbq " 0 then B 1 :" B, else B 1 paq :" Bpaq `βpbq, B 1 pbq :" Bpbq `βpaq and B 1 pxq :" Bpxq for x R ta, bu. relab aÑb rpB, βqs Ñ pB, βq βpaq " 0. relab aÑb rpB, βqs Ñ Error βpaq ‰ 0, βpbq ‰ 0 and Bpaq ‰ Bpbq. relab aÑb rpB, βqs Ñ pB 1 , β 1 q

The previous cases do not apply, B 1 paq :" K, B 1 pbq :" Bpaq, β 1 paq :" 0, β 1 pbq :" βpbq `βpaq, β 1 pxq :" βpxq, B 1 pxq :" Bpxq for x R ta, bu. 'rpB 1 , β 1 q, pB 2 , β 2 qs Ñ Error B 1 paq ‰ B 2 paq for some a such that β 1 paq ‰ 0 and β 2 paq ‰ 0. 'rpB 1 , β 1 q, pB 2 , β 2 qs Ñ pB, βq

The previous case does not apply, Bpxq :" maxtB 1 pxq, B 2 pxqu and βpxq :" β 1 pxq `β2 pxq for all x.

Table 3: Transitions of A Reg

To take an example, we can get by Theorem 27 an XP-FA that computes MaxCardX.RegrXs. It is of type XP because the nondeterminism degree of pr 1 pA RegrXs q is XP-bounded by pn `1q 2k (and not FPT-bounded as one can check).

To specialize the problem, we let Reg d rXs mean that GrXs is d-regular, i.e., has all vertices of degree d. The article [START_REF] Broersma | Tight complexity bounds for FPT subgraph problems parameterized by the clique-width[END_REF] gives an algorithm for checking the existence of a d-regular induced subgraph. We can replace A Reg by an FA B d with set of states tErroru Y prN `Ñ pr0, d `1s Y tKuqs f ˆrN `Ñ r0, d `1ss f q and we get the algorithm of time complexity n.d Opkq given in [START_REF] Broersma | Tight complexity bounds for FPT subgraph problems parameterized by the clique-width[END_REF] to check if the given graph with n vertices defined by a term in T pF k q has a regular induced subgraph of degree d. This article also gives algorithms for computing MaxCardX.Reg d rXs, MinCardX.pReg d rXs ^X ‰ Hq and #X.Reg d rXs, all of time complexity n.d Opkq . We can derive them from Theorem 27, similarly as in Section (4.2.1).

The property DX.pCard ďp pXq ^RegrX c sq expresses that the considered graph becomes regular if we remove at most p vertices. It is P-FA decidable by Corollary 18 and the remark at the end of Section 3.1. The property that the graph can be partioned into at most two regular subgraphs, expressed by DX.pRegrXs ^RegrX c sq is XP-FA computable, with time complexity Opn 8k`a q for some constant a, similar to the case of maximum directed cut.

Partition problems

Many partition problems consist in finding an s-tuple X " pX 1 , ..., X s q satisfying P artitionpXq^P 1 pX 1 q^...^P s pX s q where P 1 , ..., P s are properties of sets of vertices that can be MS expressible or, more generally, defined by FA. We may also wish to count the number of such partitions, or to find one that minimizes or maximizes the cardinality of X 1 or the number epXq :" epX 1 q`...`epX s q (cf. Section (4.2)). We have discussed above the partitioning of a graph into two regular induced subgraphs. Vertex coloring problems are of this type with P i pX i q being StrX i s and a fixed number s of allowed colors (cf. the introduction).

If the properties P i pX i q are MS expressible, then the partition problem P expressed by the MS sentence DX.P artitionpXq^P 1 pX 1 q^...^P s pX s q is decided by an FPT-FA by Theorem 29. If the properties P i pX i q are decided by FPT-FA or XP-FA, then P is decided by an FPT-FA or XP-FA, provided the conditions of Theorem 27 on the degree of nondeterminism are satisfied. Counter-example 13 shows that these conditions cannot be avoided. We now examine some coloring problems. There are other definitions of approximate s-colorings. One of them is the notion of ps, dq-defective coloring, expressed by the MS sentence:

We denote by κpGq the number of connected components of a graph G, by κpG, pq the number of those with p vertices, by M inComppGq (resp. M axComppGq) the minimum (resp. maximum) number of vertices of a connected component of G. We will compute these values by FA.

The MS formula CCpXq defined as ConnrXs ^X ‰ H ^ LinkpX, X c q expresses that X is the vertex set of a connected component. Hence, we have: κpGq " #X.CCpXqpGq, κpG, pq " MSpX.CCpXqpGqppq, M inComppGq " MinCardX.CCpXqpGq and M axComppGq " MaxCardX.CCpXq. These values can be computed by FPT-FA constructed by using Propositions 15, 16 and Theorem 27 in the following way: we build a deterministic FA A to decide LinkpX, X c q; it uses at most 2 2k on terms in T pF up1q k q. The nondeterminism degree of pr 1 pAq on a term in T pF u k q is bounded by 2 2k . The corresponding bound for the deterministic FA that decides ConnrXs is 2 2 k ( [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF]). Then, we can use the above mentioned results. However, we can construct a smaller FA by modifying the FA A Conn of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF].

We can compute κpGq " #X.CCpXqpGq for G not empty as follows. The formula LinkpX, X c q expresses that X is the vertex set of a (possibly empty) union of connected components. Hence, #X. LinkpX, X c qpGq " 2 κpGq . The construction of the FA computing #X. LinkpX, X c qpGq is clearly easier than that for #X.CCpXqpGq. This FA allows even to check if G is connected (this property is equivalent to #X. LinkpX, X c qpGq " 2q. However, it is an FPT-FA, whereas we noted above (cf. the comments about Table 2) that the automaton A Conn that checks connectedness is a P-FA.

We can alternatively construct directly a deterministic FA A κ to compute κpGq. Its states are sets of pairs pL, mq such that H ‰ L P P f pN `q and m is an integer. For every term t in T pF u 8 q, we want that:

q Aκ ptq " tpL, mq | L and m is the number of connected components of Gptq of type Lu.

The transitions are easy to write; the output function is then defined by: Out Aκ pqq :" Σ m | pL, mq P q .

If t P T pF u k q and Gptq has n vertices, the size of a state on t is Opn. logpkqq and so, A κ is a P-FA.

We now explain why this automaton is better than the one constructed by using Theorem 27. We recall from [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] that the states of A Conn are such that: q AConn ptq " pL, Lq with L P P f pN `q if Gptq is not connected and all its connected components have type L, otherwise, q AConn ptq is the set of types of the connected components of Gptq.

The graph Gptq is connected if and only if the state at the root is tLu or the empty set (because the empty graph is connected). (It is clear that A Conn is a homomorphic image of A κ .) Note that A Conn yields more information than just the connectedness of Gptq: it computes also the set of types of the connected components. By Propositions 15 and 16, we get for property CCpXq an automaton A CCpXq such that, for every t and X: q A CCpXq pt ˚Xq is Error if there is an edge between X and its complement; otherwise, X is a union of connected components of Gptq, and q A CCpXq pt ˚Xq records the set of types, let us denote it by σpXq, of these connected components.

We simplify for clarity: the state q A CCpXq pt ˚Xq contains more than the set σpXq. This is why we write that "it records ..." and not "it is σpXq". Then, let A 1 κ be constructed from A CCpXq by Theorem 27 so as to compute κpGptqq. For each term t, the state q A 1 κ ptq records, for each set α of sets of labels, the number of sets X such that σpXq " α. This is more than needed: the state q Aκ ptq records only information about the connected components of Gptq, not about all unions of connected components. If for example Gptq is the graph: a ´b a ´b b ´c c ´d then q Aκ ptq " tpab, 2q, pbc, 1q, pcd, 1qu whereas q A 1 κ ptq records tpab, 3q, pbc, 1q, pabc, 3q, pcd, 1q, pbcd, 1q, pabcd, 6qu.

We have tested these automata on a connected graph G " add a,b pHq of clique-width 3 with 17 vertices such that H has 8 connected components, each with 2 or 3 vertices. The quickest automaton on a term defining G is A κ (taking 0.0012 s), followed by A Conn (0.0014 s) and A #X. LinkpX,X c q (0.33 s) whereas A #X.CCpXq takes 39 s. It is interesting to note that using unbounded integers in A κ makes the computation quicker than by using A Conn although A Conn is finite on terms in T pF 3 q.

(4.5.2) Counting components by their size. We now compute MSpX.CCpXqpGq. First we observe that for each integer p, MSpX.CCpXqpGqppq is computable from the values MSpX. LinkpX, X c qpGqpp 1 q for all p 1 P r0, ps. (We made above a similar observation for the computation of κpGq from #X. LinkpX, X c qpGqq. However, as in this previous case, we can construct a P-FA B derived from A Conn (and generalizing the previous A κ ) such that, for every term t P T pF u 8 q: q B ptq is the set of triples pL, p, mq such that L is a nonempty set of port labels, m, p P N `and m is the number of connected components of Gptq of type L having p vertices.

If t P T pF u k q and Gptq has n vertices, then n " Σ pL,p,mqPq B ptq m.p. Hence, q B ptq can be described by a word of length Opn. logpkqq (even if numbers are written in unary; the factor logpkq corresponds to the coding of labels). Here are the transitions:

∅ Ñ H, a Ñ tptau, 1, 1qu, 'rq, q 1 s Ñ q 2 where q 2 is the set obtained by replacing iteratively in the multiset q \ q 1 any pair tpL, p, mq, pL, p, m 1 qu by the unique triple pL, p, m `m1 q, relab h rqs Ñ q 1 : for each set L, we let hpLq be the set obtained from L by replacing a by hpaq; then q 1 is the set of triples pL 1 , p, m 1 q such that: L 1 :" hpLq for some pL, p, mq P q, m 1 :" Σ m | L 1 " hpLq and pL, p, mq P q .

Finally, we describe the transitions add a,b rqs Ñ q 1 . There are two cases. Case 1 : a or b is not present in q or they are both present in q but in a unique triple of the form pL, p, 1q (with a, b P L). Then q 1 :" q.

Case 2 : Case 1 does not apply. We let: q 2 be the set of triples in q that contain neither a nor b, L 1 :" ď tL | pL, p, mq P q ´q2 u, and q 1 :" q 2 Y tpL 1 , p 1 , 1qu where p 1 :" Σ p.m | pL, p, mq P q ´q2 .

We illustrate this case with an example:

q " tptau, 2, 1q, ptau, 1, 4q, pta, b, cu, 4, 1q, ptb, du, 3, 2q, ptc, du, 3, 4qu, q 1 " tpta, b, c, du, 16, 1q, ptc, du, 3, 4qu, where 16 is obtained as 2.1 `1.4 `4.1 `3.2 because the connected components of types tau, ta, b, cu and tb, du get fused into a unique one (of type ta, b, c, du).

For computing MSpX.CCpXq we take the output function:

Out B pqq :" µ such that µppq :" Σ m | pL, p, mq P q for p P N `.

It is clear that the transitions and the output function can be computed in time polyp t q. Hence, B is a P-FA. From MSpX.CCpXqpGq we get κpG, pq for each p. For dealing with separation problems, it is useful to compare the cardinality of a set of vertices X to the number of connected components of GrX c s and to the maximal cardinality of a connected component of GrX c s that we denote by M axCardCCpGrX c sq. For this purpose, we define for a graph G: αpGq " tp|X|, κpGrX c sqq | X Ď V G u, βpGq " tp|X|, M axCardCCpGrX c sqq | X Ď V G u.

From αpGq, one can determine, for given integers p and q, if there exists a set X of cardinality at most p whose deletion splits the graph in at least q connected components. Similarly, from βpGq one can determine if there is such a set X whose deletion splits the graph in connected components of size at most q.

Let P pX, U q mean that U has one and only one vertex in each connected component of GrX c s and QpX, Y q mean that Y is the vertex set of a connected component of GrX c s. These properties are MS expressible. Then αpGq " SppX, U q.P pX, U qpGq and βpGq can be computed from SppX, Y q.QpX, Y q. Hence, by Example 14(a), Propositions 15, 16 and Theorem 27, these two values are computable by FPT-FA.

Undecidability and intractability facts.

Let R be an s-ary P-computable numerical predicate (integers being given in binary notation). We denote by MS `R the extension of monadic second-order logic with the atomic formulas Rp|X 1 |, ..., |X s |q. We have seen such formulas in Section (4.4.2). We wish to examine when the model-checking problem 21 for MS`R is FPT or XP. Actually we will only consider the case of words over finite alphabets, so the question reduces to whether it is P-decidable. We first discuss undecidability results. There is no implication between (un)decidability results on the one hand and complexity results on the other, but decidability and FPT results for terms and for graphs of bounded clique-width are proved with the same tools. Undecidability results are actually easier to prove and they help to foresee the difficulties regarding complexity. We let Eqpn, mq mean n " m; this binary relation defines a semi-linear set of pairs of integers. A unary predicate R on N is identified with the corresponding set.

Proposition 31: One cannot decide if a given sentence of MS `Eq or MS `R where R Ď N is not ultimately periodic is true in some word over a fixed finite alphabet.

Proof : The case of MS `Eq is proved in Proposition 7.60 of [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] and the other one in [START_REF] Bès | Expansions of MSO by cardinality relations[END_REF].

We now consider the model-checking problem.

Definition 32: Separating sets of integers.

Let R Ď N, p, n P N such that n ą p. We say that R separates on r0, ns the integers in r0, ps if, for every x, y P r0, ps: occurrence of x such that SpP qru, js " SpP qru 1 , j 1 s where j 1 is maximal such that SpP qru 1 , j 1 s P xt0, 1u ˚, then u 1 P U .

The formula ϕpU q is taken of the form ϕ 1 pU q ^ϕ2 pU q where ϕ 2 pU q is a first-order formula expressing that the truth values of x 1 , ..., x n defined by U satisfying ϕ 1 pU q form a solution of P .

If the sentence DU.ϕpU q could be checked in words w P A ˚in time polyp|w|q, then each instance P of SAT could be checked in time polyp|wpP q|q and we would have P " NP.

We now translate ϕ 1 pU q into a sentence ϕ 3 pU q of MS`R such that DU.pϕ 3 pU q ^ϕ2 pU qq is equivalent to DU.ϕpU q in every structure SpP q. It is clear that 2n ă |wpP q| as all variables x 1 , ..., x n occur in P . Hence, any sequence of 0 and 1's in wpP q has length bounded by 1 `tlogpnqu " tlogp2nqu ď tlogp|wpP q|qu. The equality tests Eqp|X|, |Y |q used in ϕ 1 pU q can be expressed in terms of R that we assume separating. Hence, the satisfiability of P is expressed in SpP q by a sentence of MS `R, and so, the model-checking problem for MS `R is not P-solvable in polynomial time either. Questions

34:

(1) Can one replace in the previous proposition "R is separating" by "R is not ultimately periodic"? It might happen that the modelchecking problem for MS `R where R is very sparse (like the above set D) is P-decidable on words.

(2) Is the model-checking problem for MS `Eq NP-decidable on words? The same question can be raised for MS `R where R is a semi-linear subset of N k , k ě 2.

Implementation

The system AUTOGRAPH 22 , written in LISP (and presented in the conference paper [START_REF] Courcelle | Infinite transducers on terms denoting graphs[END_REF]) is intended for verifications of graph properties and computations of functions on graphs. Its main parts are as follows.

(1) A library of basic fly-automata over F 8 for the following properties and functions:

(1.1) X Ď Y , X " H, SglpXq, Card ďp pXq, Card p,q pXq, P artitionpXq and the function CardpXq (they concern arbitrary sets),

(1.2) edgpX, Y q and lab a pXq, the atomic formulas of MS logic over pgraphs,

(1.3) some MS expressible graph properties: stability, being a clique, LinkpX, Y q, P athpX, Y q, connectedness, existence of directed or undirected cycles, degree at most d, etc. cf. Table 2 and [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] and finally, (1.4) some graph properties and functions on graphs that are not MS expressible: regularity, number of edges between two sets, maximum degree.

(2) A library of procedures that transform or compose fly-automata: these functions implement the constructions of Propositions 10, 15, 16 and Theorems 17 and 27.

AUTOGRAPH includes no parser for the formulas ϕ expressing properties and functions. The translation of these formulas into LISP programs that call the basic FA and the composition procedures is easily done by hand because, since we have FA for many basic graph properties, the formulas that specify the problems are not too complicated. Some automata (in particular for cycles, regularity and other degree computations) are defined so as to work correctly on irredundant terms. A preprocessing can verify whether a term is irredundant, and transform it into an equivalent irredundant one if it is not 23 . Whether input terms are good or not may affect the computation time, but not the correctness of the outputs.

By using FA, we could find24 that Petersen's graph has 12960 4-colorings, and verify the correctness of this result by using the chromatic polynomial. We found also that McGee's graph has 57024 acyclic 3-colorings in less than 30 minutes.

AUTOGRAPH has a method for enumerating (that is, for listing) the sets SatX.P pXq, by using an existing FA A for P pXq. A specific enumeration program is generated for each term (see [START_REF] Durand | Object enumeration[END_REF]). Running it is also interesting for accelerating the verification that DX.P pXq is true, because the computation can stop as soon as the existence of some satisfying tuple X is confirmed. More precisely, the nondeterministic automaton prpAq is not run deterministically (cf. Definition 1(c)), but its potentially accepting runs are constructed "one by one". In this way, we could check in 2 seconds that McGee's graph is acyclically 3colorable. This technique works for DX.P pXq but not for @X.P pXq, #X.P pXq, MSpX.P pXq etc... because these properties and functions are based on a complete knowledge of SatX.P pXq.

Using terms with shared subterms. Equal subterms of a "large" term t can be fused and t can be replaced by a directed acyclic graph (a dag). The construction from t of a dag where any two equal subterms are shared can be done in linear time by using the minimization algorithm of deterministic acyclic finite automata presented in [START_REF] Revuz | Minimisation of acyclic deterministic automata[END_REF]. Deterministic FA can run on such dags in a straightforward manner. We have tested that on 4-colorable graphs defined recursively by G n`1 " tpG n , G n q where t P T pF 7 , tx, yuq (a term with two variables x and y denoting p-graphs; G n has Op2 n q vertices and edges). We checked that these graphs are 4-colorable by using the term in T pF 7 q and the dag resulting from the recursive definition. The computation times are in Table 4 This method raises a question: can one transform a term in T pF k q into an equivalent one in T pF k 1 q for some k 1 not much larger than k, whose associated minimal dag (the one with a maximal sharing of subterms) has as few nodes as possible?

Conclusion

We have given logic based methods for constructing FPT and XP graph algorithms based on automata. Our constructions allow several types of optimizations: different logical expressions of a property can lead to different automata having different observed computation times and direct constructions of FA are sometimes better than the general ones resulting from Theorem 27. We also have cases where FPT-FA are easier to implement and practically more efficient than certain equivalent P-FA, and similarly for XP-FA and FPT-FA. Can one identify general criteria for the possibility of such optimizations and improvements? Do we need optimal terms? Graphs are given by terms in T pF 8 q and no a priori bound on the clique-width must be given since all FA are over F 8 . As an input graph is given by a term t over F k with k ě cwdpGq, one may ask how important it is that k be close to cwdpGq. Every graph with n vertices is denoted by a term in T pF n q where each vertex has a distinct label and no relabelling is made. Such a term, if it is irredundant, has size Opn 2 . logpnqq. Hence, as input to a P-FA, it yields a polynomial time computation. This is of course not the case with an FPT-or XP-FA.

Edge quantifications. The logical representation of graphs used in this article does not allow edge set quantifications in MS formulas. MS formulas written with edge set quantifications (MS 2 formulas in short) are more expressive than MS formulas, and more functions based on them, such as #X.ϕpXq, can be defined. An easy way to allow edge set quantifications is to replace a graph G by its incidence graph IncpGq where edges are made into new vertices and adjacency is replaced by incidence. The clique-width of IncpGq is at most 2.twdpGq `4 for G directed and at most twdpGq `3 for G undirected, where twdpGq is the tree-width of G ( [START_REF] Bouvier | Graphes et décompositions[END_REF]). MS formulas over IncpGq allow quantifications over sets of edges of G and correspond to MS 2 formulas. Hence, the constructions of FA presented in this article work for the expression of properties and functions based on MS 2 formulas and tree-width (but not clique-width) as parameter [START_REF] Courcelle | Fly-automata for checking monadic second-order properties of graphs of bounded tree-width[END_REF]. Other constructions based on a variant of tree-width are discussed in [START_REF] Courcelle | On the model-checking of monadic second-order formulas with edge set quantifications[END_REF]. p t 1 ' relab ℓ ´1˝ht 2 p p t 2 q h t πpt 1 q ‰ H, πpt 2 q ‰ H and (*) Ý Ý Ñ add a,b pt 1 q p t 1 h t1 ta, bu Ę πpt 1 q Ý Ý Ñ add a,b pt 1 q Ý Ý Ñ add h ´1 t 1 paq,h ´1 t 1 pbq p p t 1 q h t1 ta, bu Ď πpt 1 q relab h pt 1 q p t 1 h ˝ht1

h
Table 5: Inductive construction of p t P T pF 8 q and h t .

It is clear that p t and h t can be computed in polynomial time from t.

Claim 1 : p t P T pF k 1 q for some k 1 ď k, πp p t q " rmax πp p t qs, h t is a bijection:πp p t q Ñ πptq and t « relab ht p p t q.

Proof : These facts are clear from the inductive construction and we have k 1 " max µp p t q. Claim 2 : p t is irredundant.

Proof : Because t is assumed irredundant. Claim 3 : p t is good.

Proof : Let n be the number of vertices of Gptq, assumed to have at least one edge. (The case of graphs without edges is easily treated separately). The inductive construction shows that, for each subterm t 1 of p t, each label in πpt 1 q labels some vertex of Gpt 1 q, hence max µp p t q is at most the number of vertices of Gp p t q, equal to n.

Again by induction, we can see that ' has n ´1 occurrences in p t (because p t has no occurrence of ∅ and Gptq » Gpt 1 q), and that the symbols relab h have at most 2n ´1 occurrences (one can of course delete those of the form relab Id ).

The number of operations Ý Ý Ñ add a,b is at most pn ´1q.pk 12 ´k1 q because p t is irredundant by Claim 2. It follows that | p t | ď n`n´1`2n´1`pn´1q.pk 12 ´k1 q ď pk 1 `1q 2 .n`1 as one checks by noting that k 1 ě 2 because Gp p t q has edges. Hence p t is good. ˝65

( 3 . 2 . 3 . 1 )

 3231 Minimizing cardinalities or other values. In order to compute: MinCardX 1 .P pXqptq :" if t |ù DX.P pXq then mint|X 1 | | t |ù DX 2 , ..., X s .P pXqu else 8, we use Case (c) of Proposition 21. We take D :" xNYt8u, min, 8, pg D q gPF psq y with pa, wq D :" wr1s and pf, wq D pm, pq :" wr1s `m `p. Clearly, min H " 8. We will denote by A MinCard the obtained deterministic FA. More generally, in order to compute: Min αX.P pXqptq :" if t |ù DX.P pXq then mintαpXq | t |ù P pXqu else 8 where αpXq :" c 1 . |X 1 | `... `cs . |X s | for fixed integers c 1 , ..., c s in Z, we take D :" xZYt8u, min, 8, pg D q gPF psq y with: pa, wq D :" c 1 .wr1s `... `cs .wrss, pf, wq D pm, pq :" c 1 .wr1s `... `cs .wrss `m `p.

(

( 4 . 5 . 3 )

 453 Tools for separation problems.

  Every graph G has clique-width at most |V G |. Two terms t and t 1 are equivalent, denoted by t » t 1 , if Gptq » Gpt 1 q. and Opk. logpkqq for relab h . Hence, its size }t} is Opk. logpkq.|t|q. Clearly, |V Gptq | ď |t| ď }t} but }t} is not bounded by a function of |V Gptq | because a graph can be denoted by arbitrary large terms, in particular because Ý Ý Ñ add a,b is idempotent.

	Oplogpkqq for a and	Ý Ý Ñ add a,b
	All definitions and results stated below for F k and F 8 apply to F u k and 8 . Let t P T pF k q. Each of its symbols can be encoded by a word of length F u

  2 .|V Gptq | `1 in the definition. For example the term relab 5Ñ1 padd 1,9 padd 1,8 p1 ' 5' 8qqq is not good and can be replaced by the good term relab 2Ñ1 padd 1,3 p1 ' 2 ' 3qq. This preprocessing takes time polyp}t}q.If t is good, we have }t} " Opk. logpkq.|t|q " Opk 3 . logpkq.|V Gptq |q where k " max µptq. A computation time is this case bounded by a polynomial in }t} if and only if it is by a polynomial in |V Gptq | `max µptq.

  4.4.1) Coloring problems We let ColpXq abbreviate the MS property P artitionpXq ^StrX 1 s ^... ŜtrX The function #X.ColpXq counts the number of s-colorings 20 . It is thus FPT-FA computable by Theorem 27. Another number of possible interest is, if G is s-colorable, MinCardX 1 .DX 2 , ..., X s .ColpXq which is 0 if G is ps ´1qcolorable; otherwise, it indicates how close G is to be ps ´1q-colorable. By Theorem 27, this number is computable by an FPT-FA.

s s.

Table 4 :

 4 . Computations using dags instead of terms.

	n	term	dag
	6	11 mn 1 mn, 6 s
	9	88 mn 1 mn, 32 s
	20		4 mn
	28		40 mn
	30		2 h, 26 mn

  t is a bijection: r|πptq|s Ñ πptq such that h t piq " h t1 piq for i P rmax πpt 1 qs; (clearly, |πptq| ě max πpt 1 qq.

	t	t	∅	p t	h t Id	Conditions πptq " H (i.e., Gptq " ∅)
	a		1		1 Ñ a
	t 1 ' t 2 t 1 ' t 2 t 1 ' t 2	t 2 p t 1 p		h t2 h t1	πpt 1 q " H πpt 2 q " H

Fly-automata are useful when the number of states is large compared to the number of function symbols and the size of input terms. Symbolic automata[START_REF] Veanes | Symbolic automata: the toolkit[END_REF] are defined for the case when the number of states is manageable but the set of function symbols is very large, and possibly infinite. In these automata, states are listed but function symbols and transitions are described by logical formulas. Fly-automata also admit infinite sets of function symbols.

See http://dept-info.labri.u-bordeaux.fr/˜idurand/autograph

The corresponding constructed algorithms that are FPT (or XP) for clique-width are immediately FPT (or XP) for tree-width.

If wx ‰ ε encodes a symbol x, then }f pgpa, bq, gpb, cqq} " |w f |`2.|wg|`|wa|`2.|w b |`|wc|.The length of a LISP list implementing a term t is between }t} and 3.}t}. (We use LISP to implement fly-automata, see Section

5.)

Powerset algebras are called powerset magmas in[START_REF] Courcelle | Equivalences and transformations of regular systems; applications to recursive program schemes and grammars[END_REF].

For example, if k " 3, then relab tp1,2q,p3,1qu " relab h where hp1q :" 2, hp2q :" 2 and hp3q :" 1. We denote also relab tpa,bqu by relab aÑb . Each operation relab h can be expressed as a composition of operations relab aÑb . See Proposition 2.118 of[START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] for details.

In[START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], Definition 2.8, we take for k the cardinality of D. This gives an equivalent notion but in our applications, it is easier to bound the length of a word in D than to determine its exact cardinality.

We recall from Definition 1 that the sets δ A pf, q 1 , . . . , q ρpf q q are linearly ordered; firing the next transition includes recognizing that there is no next transition.

Unless SatX.P pXq is encoded in a particular compact way; here we take it as a straight list of sets.

For formulas of counting monadic second-order logic, we also need FA for the atomic formulas Cardp,qpX 1 q expressing that X 1 has cardinality p modulo q, see the appendix.

We will also apply this theorem to properties P pXq that are defined by FA without being MS expressible.

It says that if τ is a monadic second-order transduction and L is a monadic second-order definable class of structures, then τ ´1pLq is monadic second-order definable ([16], Theorem 7.10).

It is not hard to see that a term t in T pF psq 8 q is good (resp. irredundant) if and only if prsptq is.

The algorithms of this article assume implicitly that the input terms are irredundant. Since the preprocessing that makes a term irredundant takes linear time, the given upper bounds to computation times are correct. This article also gives tight lower bounds to these computation times under the exponential time hypothesis.

Its parameter is the bound k on clique-width, but it is also a P-FA for k `p as parameter.

This number is χ G psq where χ G is the chromatic polynomial of G. So, for some graphs with known chromatic polynomial, we could check the correctness of our computations.

We are interested in the data-complexity of the model-checking problem for a language L. For each fixed sentence in L that describes some property of interest, we consider an algorithm whose input is a word or a term that may describe a graph.

See http://dept-info.labri.u-bordeaux.fr/˜idurand/autograph

Another type of preprocessing defined in[START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] consists in annotating the given term.

AUTOGRAPH is written in Common Lisp and run on a MacBook Pro laptop with processor 2.53 GHz Intel Core Duo and a 4 GB memory.

, ..., X n qq, also written Dx n .ϕpX 1 , ..., X n´1 , tx n uq for readability. All quantifications of a first-order formula have this form. First-order order formulas may

[START_REF] Fellows | On the complexity of some colorful problems parameterized by treewidth[END_REF] We do not distinguish monadic second-order formulas from counting monadic secondorder formulas, defined as those using Cardp,qpX i q, because all our results hold in the same way for both types. See Chapter 5 of[START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] for situations where the distinction matters.

This FA guesses a pair of occurrences of edge addition operations showing that the considered term is not irredundant.

Acknowledgements: We thank C. Paul and the referees for their many useful comments.

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.

First-order constructions

Let P be a property of terms t taking also as argument an s-tuple of sets of positions X " pX 1 , ..., X s q. We recall that Dx 1 , ..., x s .P px 1 , ..., x s q (also written Dx.P pxq) abbreviates DX.pP pXq ^SglpX 1 q ^... ^SglpX s qq.

We define Satx.P pxqptq as tpu 1 , ..., u s q P pP osptqq s | P ptu 1 u, ..., tu s uq holds in term tu. This set is in bijection with SatX.pP pXq^SglpX 1 q^...^SglpX s qqptq. (The function SatX.p.q is defined in the introduction).

If αpXq is a function, we define SetValX.αpXqptq as the set of values αpXq different from K and SetValx.αpxqptq as SetValX.pαpXq ae SglpX 1 q^...^SglpX s qqptq.

Theorem 17: (1) If P pXq is a P-FA decidable property, then the properties Dx.P pxq and @x.P pxq are P-FA decidable.

(2) If αpXq is a P-FA computable function, then the function SetValx.αpxq is P-FA computable.

(3) The same implications hold for the classes FPT-FA and XP-FA.

Proof : (1) and (3). We let A be a deterministic FA over F psq that decides P pXq. We let B i be the deterministic FA over F psq for SglpX i q with states 0,1 and Error Bi such that:

There is, by Proposition 15, a deterministic FA that decides property P pX 1 , ..., X s q ^SglpX 1 q ^... ^SglpX s q. Its set of states is Q A ˆQB1 ˆ... ˆQBs and its set of accepting states is Acc A ˆt1u ˆ... ˆt1u. We build a smaller deterministic FA C with set of states tError C u Y ppQ A ´tError A uq ˆt0, 1u s q and same set of accepting states by merging into a unique error state Error C all tuples of Q A ˆQB1 ˆ... ˆQBs , one component of which is an error state.

The nondeterministic automaton pr s pCq decides the property Dx.P pxq. Its states at a position u in a term t P T pF q are Error C or the tuples of the form prun A,t˚X puq, |X 1 {u|, ..., |X s {u|q such that |X 1 {u|, ..., |X s {u| ď 1. Since A is deterministic, there are at most 1 `p|t| `1q s different such states and the nondeterminism degree of pr s pCq is bounded by the polynomial ppnq " 1 `pn `1q s that does not depend on Sigptq. Hence detppr s pCqq is a P-FA, an FPT-FA or an XP-FA by Lemma 7 if A is so.

Property @x.P pxq can be written Dx. P pxq. The results follow since, by by Proposition 15 (3,[START_REF] Bès | Expansions of MSO by cardinality relations[END_REF] the classes of P-FA, FPT-FA and XP-FA that check properties are closed under the transformation implementing negation.

(2) and (3). We apply the same construction to an FA A over F psq that computes αpXq. As output function for C, we take:

Out C ppq, 1, ..., 1qq :" Out A pqq, for q P Q A , Out C ppq :" K, for all other states p of C. DX.pP artitionpXq ^Deg ďd rX 1 s ^... ^Deg ďd rX s sq.

For fixed s, we can consider the problem of determining the smallest d for which this property holds. This number is at most rn{ss for a graph with n vertices.

The property Deg ďd rXs meaning that each vertex of X has degree at most d in GrXs is decided by an FPT-FA whose number of states on a term in T pF up1q k q is Opd 2k q. It follows that the existence of an ps, dq-defective coloring can be checked, for a graph with n vertices, in time Opn.d 4s.k`a q for some constant a. By checking the existence of an ps, dq-defective coloring for successive values of d starting from 1, one can find the minimal value of d in time Opn 4s.k`a`1 q hence Opn 8s.2 rwdpGq `a`1 q which is similar to the time bound Opn 4s.2 rwdpGq `bq given in [START_REF] Ganian | A unified approach to polynomial algorithms on graphs of bounded (bi-)rank-width[END_REF] (because for every undirected graph G, we have cwdpGq ď 2 rwdpGq`1 ´1q.

Another possibility is to define MD pXq :" pM axDegrX 1 s, ..., M axDegrX s sq and to compute the set: SetValX.MD pXq ae P artitionpXq, from which the existence of an ps, dq-defective coloring can easily be determined. Since the automaton for M axDeg uses Opn 2k q states for a graph with n vertices defined by a term in T pF k q, we get for MD pXq the bound Opn 2k.s q and, by Lemma 7 and Theorem 27, the bound Opn 4s.k`c q for some constant c, which is of same order as by the first method.

(4.4.2) Graph partition problems with numerical constraints Some partition problems consist in finding an s-tuple X satisfying:

where P 1 , ..., P s are properties of sets and R is a P-computable arithmetic condition. An example is the notion of equitable s-coloring: P i pX i q is StrX i s for each i and Rp|X 1 |, ..., |X s |q expresses that any two numbers |X i | and |X j | differ by at most 1. The existence of an equitable 3-coloring is not trivial: it holds for the cycles but not for the graphs K n,n for large n. The existence of an equitable s-coloring is W [1]-hard for the parameter defined as s plus the tree-width [START_REF] Fellows | On the complexity of some colorful problems parameterized by treewidth[END_REF], hence presumably not FPT for this parameter. Our constructions yield, for each integer s, an FPT-FA for checking the existence of an equitable s-coloring for clique-width as parameter. We obtain the answer from SpX.pP artitionpXq ŜtrX 1 s ^... ^StrX s sq that is computable by an FPT-FA.

Connected components

The empty graph is defined as connected and a connected component as nonempty.

In [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF], we have discussed in detail connectedness, denoted by Conn, and we come back to this important graph property. We show that the general constructions of Theorem 27 can be improved in some cases. We consider undirected graphs.

(4.5.1) Number and sizes of connected components.

x ‰ y if and only if there exists z P N such that x `y `z P r0, ns and, either x `z P R and y `z R R or y `z P R and x `z R R.

We say that an infinite set R Ď N is separating if there exists n 0 such that, for every n ą n 0 , R separates on r0, ns the integers in r0, tlogpnqus. The sets tn! | n P Nu, t2 n | n P Nu and that of prime numbers are separating. An ultimately periodic set of integers is not separating. The set D :" ta n | n P Nu such that a 0 " 1, a n`1 " 2 an`3 is not ultimately periodic and not separating either. (To see this, observe that D does not separate a n `1 and a n `2 on r0, a n`1 ´1s.q

If R separates on r0, ns the integers in r0, ps, then, for any two disjoint subsets X and Y of rns of cardinality at most p we have:

|X| " |Y | if and only if:

This means that the equipotence of small sets can be expressed in MS `R.

Proposition 33: Let R be a separating subset of N. If P ‰ NP, the modelchecking problems for MS `Eq and MS `R are not P-decidable.

Proof : We first consider MS `Eq. We use a method similar to that of Counter-example 13. Let P be an instance of SAT in conjunctive normal form whose variables are x 1 , ..., x n . Let wpP q be the word representing P with x i written as x followed by the binary writing of i (with no leading 0). For example, if P is px 1 _x 2 _ x 3 q^px 3 _ x 4 _ x 5 q then wpP q is the word px1_x10_ x11qp x11_ x100_ x101q over the alphabet A :" tp, q, _, ^, , x, 0, 1u. The factors of this word that belong to t0, 1u ˚have length at most 1 `tlogpnqu. The word wpP q is represented by the logical structure SpP q :" xr|wpP q|s, ď, plab a q aPA y such that lab a piq holds if and only if wpP qris " a.

We build a formula ϕpU q of MS `Eq, written with ď and the unary relations lab a for a P A, such that P as above has a solution if and only if SpP q |ù DU.ϕpU q. The set U defines a set of occurrences of x in the word wpP q whose corresponding variable x i takes value T rue. We require that, either all occurrences of a variable x i or none of them has value T rue. We express this condition by a formula ϕ 1 pU q of MS `Eq where Eqp|X|, |Y |q is only used for sets X and Y of consecutive occurrences of 0 and 1's. We sketch its construction. If i ă j, we denote by SpP qri, js the factor of SpP q from position i to position j. We construct a formula θpi, j, i 1 , j 1 q expressing that SpP qri, js is a prefix of SpP qri 1 , j 1 s: it says that for each u P ri, js there is u 1 P ri 1 , j 1 s such that u 1 ´i1 " u ´i and SpP qru 1 s " SpP qrus. This formula uses Eq. Then, by using θ, we construct ϕ 1 pU q saying that U is a set of occurrences of x and that, for each u P U , if j is maximal such that SpP qru, js P xt0, 1u ˚, if u 1 is another

Appendix Monadic second-order logic

Representing graphs by logical structures.

We define a simple graph G as the relational structure xV G , edg G y with domain V G and a binary relation edg G such that px, yq P edg G if and only if there is an edge from x to y (or between x and y if G is undirected). A pgraph G whose type πpGq is included in N `is identified with the structure xV G , edg G , plab a G q aPN`y where lab a G is the set of a-ports of G. Since only finitely many sets lab a G are not empty, this structure can be encoded by a finite word over a fixed finite alphabet. We only consider properties of (and functions on) graphs rather than of (and on) p-graphs, but the formal setting allows that. By considering a graph as a relational structure, we have a welldefined notion of logically expressible graph property. However, in the present article, we do not use this relational structure: we handle graphs through terms in T pF 8 q (F 8 is the signature of clique-width operations defined in Section (1.2)) and we construct automata over F 8 from MS formulas.

Monadic second-order formulas

The basic syntax of monadic second-order formulas (MS formulas in short) uses set variables X 1 , ..., X n , ... but no first-order variables. Formulas are written without universal quantifications and they can use set terms (cf. Section 1.3). These constraints yield no loss of generality (see, e.g., Chapter 5 of [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]).

To express properties of p-graphs we use the atomic formulas X i Ď X j , X i " H, SglpX i q (meaning that X i denotes a singleton set) and Card p,q pX i q (meaning that the cardinality of X i is equal to p modulo q, with 0 ď p ă q and q ě 2q 25 where the variables denote sets of vertices. We also use the atomic formulas edgpX i , X j q meaning that X i and X j denote respectively txu and tyu such that x Ñ G y and lab a pX i q meaning that X j denotes a singleton consisting of an a-port.

It is convenient to require that the free variables of every formula and its subformulas of the form DX n .ϕ are among X 1 , ..., X n´1 . This syntactic constraint yields no loss of generality (see Chapter 6 of [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]) but it makes easier the construction of automata. In examples, we use set variables X, Y , universal quantifications, and other obvious notation to make formulas readable. A firstorder existential quantification is a construction of the form DX n .pSglpX n q φpX have free set variables and may be built with set terms. So, Dx 2 .ϕpX 1 , X c 1 ´tx 2 uq is a first-order formula if ϕ contains only first-order quantifications.

A graph property P pX 1 , ..., X s q is M S expressible if there exists an MS formula ϕpX 1 , ..., X s q such that, for every p-graph G and for all sets of vertices X 1 , ..., X s of this graph, we have xV G , edg G , plab a G q aPN`y |ù ϕpX 1 , ..., X s q if and only if P pX 1 , ..., X n q is true in G.

Good and irredundant terms

We prove a technical result about terms over F 8 , the signature of clique-width operations. If t,t 1 P T pF 8 q, then t « t 1 means that these terms define isomorphic p-graphs, πptq is the set of port labels of Gptq, max πptq is the maximal label in πptq, µptq is the set of port labels that occur in t and max µptq is the maximal one in µptq; we recall that port labels are positive integers.

Proposition 35: (1) The set of good and irredundant terms in T pF 8 q is P-FA recognizable.

(2) There exists a polynomial-time algorithm that transforms every term in T pF 8 q into an equivalent term that is good and irredundant.

Proof : (1) We have observed after Definition 7 that the set of good terms is P-FA recognizable. By Proposition 8(2) of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] the set of terms that are not irredundant is accepted by a nondeterministic FA 26 whose states on a term t are pairs of port labels in µptq and nondeterminism degree is at most |µptq| 2 , hence polyp}t}q. By determinizing it and exchanging accepting states and nonaccepting ones, we get a P-FA A that recognizes the set of irredundant terms. By taking the product of A with the FA recognizing good terms, we get a P-FA (by Proposition 15) that recognizes the good and irredundant terms.

(2) Proposition 8 of [START_REF] Courcelle | Automata for the verification of monadic second-order graph properties[END_REF] gives, for each integer k, a linear-time algorithm that transforms a term t in T pF k q into an equivalent irredundant one t 1 P T pF k q such that |t 1 | " |t| and }t 1 } ď }t} by deleting occurrences of operations that create redundancies. This algorithm attaches to each position of t a set of pairs of port labels from µptq. These sets can be encoded in size |µptq| 2 . logpkq ď polyp}t}q. We obtain a polynomial-time algorithm taking as input a term in T pF 8 q.

We now consider an input term t that is irredundant and we transform it into an equivalent one that is good and still irredundant. By induction on the structure of t P T pF k q, we define: a good term p t P T pF k 1 q such that πp p t q " rmax πp p t qs and k 1 ď k, and a bijection h t : πp p t q Ñ πptq such that t « relab ht p p t q.

The inductive definition is shown in Table 5 where Condition (*) says the following: