Bruno Courcelle
email: courcell@labri.fr

On regular trees defined from unfoldings and coverings

Keywords: graph unfolding, graph covering, universal covering, regular tree, strongly regular tree, weighted graph, automorphism, first-order logic

We study the infinite trees that arise, first as complete unfoldings of finite weighted directed graphs, and second, as universal coverings of finite weighted undirected graphs. They are respectively the regular rooted trees and the strongly regular trees, a new notion. A rooted tree is regular if it has finitely many subtrees up to isomorphism. A tree (without root) is strongly regular if it has only finitely many rooted trees, up to isomorphism, obtained by taking each of its nodes as a root. We prove the first-order definability of each regular or strongly regular tree with respect to the class of trees (that is not itself first-order definable). We characterize the strongly regular trees among the regular ones and we establish several decidability results.

Introduction

Unfolding and covering are graph theoretical notions that arise in several areas of the Theory of Programming. We studied them in [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] by highlighting their similarities. Here,we continue this research by focusing on the infinite trees that are the complete unfoldings of finite directed graphs and the universal coverings of finite undirected graphs. They are all regular which means that they have finitely many subtrees, u.t.i., i.e., up to isomorphism. Precise definitions will be given soon.

Infinite trees arise frequently in semantics of programs. One occurrence is in the study of recursive program schemes [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF][START_REF] Courcelle | Recursive applicative program schemes[END_REF]: regular and algebraic trees give syntactic formalizations of their semantics. Different notions of trees are 1 associated with different types of higher-order recursive program schemes [START_REF] Knapik | Higher-order pushdown trees are easy[END_REF][START_REF] Knapik | Unsafe grammars and panic automata[END_REF][START_REF] Ong | On Model-Checking Trees Generated by Higher-Order Recursion Schemes[END_REF], and they have been studied by tools of logic and automata theory. Another occurrence concerns the study of certain abstract programs called transition systems. They can be seen as directed graphs equipped with edge and vertex labels holding semantical information. The complete unfolding of such a directed graph from a distinguished vertex representing an initial state, defines a rooted and directed tree that is infinite if the graph has directed cycles. This tree captures all possible computations, hence its semantics [START_REF] Arnold | Finite transition systems[END_REF][START_REF] Courcelle | The Monadic Second-Order Logic of Graphs IX: Machines and their Behaviours[END_REF][START_REF] Courcelle | Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems[END_REF]. If the graph is finite, its complete unfolding is a regular rooted tree.

Independently, the theory of distributed computing uses the notion of covering of an undirected graph that represents a network. This notion makes it possible to identify what is possible to compute or not in the considered network [START_REF] Angluin | Local and Global Properties in Networks of Processors (Extended Abstract)[END_REF]. The universal covering of a finite graph is a regular tree of a special form that we call strongly regular.

Unfoldings and coverings are defined as surjective graph homomorphisms that induce bijections between the neighbourhoods of vertices related by the homomorphism. The notion of neighboorhoud is a parameter that gives rise to unfoldings, coverings and yet other notions [START_REF] Courcelle | Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems[END_REF]. For unfoldings of directed graphs, the neighbourhood of a vertex x is the set of directed edges (that we call arcs) outgoing from x. For coverings of undirected graphs, it is the set of edges incident to x.

In [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF], we studied these two notions in parallel. Furthermore, we generalized them to weighted graphs. A weighted directed graph has a weight on each arc belonging to N + ∪ {ω}, hence, that is a positive integer or the infinite cardinal ω. An arc of weight 3 (resp. ω) unfolds into 3 arcs (resp. countably many) originating from a same node. In this way, we can obtain regular trees having nodes of infinite (countable) degree. We call complete unfolding what is usually called the unfolding [START_REF] Courcelle | Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems[END_REF], and we define as an unfolding of a weighted directed graph H a weighted directed graph that lies inbetween H itself and its complete unfolding. "Inbetween" is formally defined in terms of surjective homomorphisms that are locally bijective as explained above.

The complete unfoldings of finite weighted and directed graphs are the regular rooted trees. The regularity of a rooted tree means that it has finitely many subtrees (rooted trees issued from nodes) u.t.i.. We obtain trees of infinite degree, arising from directed edges of weight ω, which provides an extension of the usual notion. Each regular rooted tree T is the complete unfolding Unf (H) of a finite unique canonical weighted directed graph H, somewhat analogous to a minimal deterministic automaton on words. It can be used as a finitary description of it as it can be computed from any other finite and weighted directed graph G such that T = Unf (G). Hence, this finitary description is effective.

In [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF], we have also extended the notion of covering to weighted undirected graphs. In this case, weights in N + ∪ {ω} are attached to half-edges : an edge that is not a loop has two weights. Each such graph H has, u.t.i., a unique universal covering that is a tree without root. If H is finite, this tree is strongly regular. This means that it yields finitely many regular rooted trees, u.t.i., by taking its different nodes as roots. This is a new notion of which we give equivalent characterizations. Each strongly regular tree is the universal covering of a canonical finite weighted graph (of minimal size), and thus, also has a finitary, computable description.

By using results from [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] that generalize one by Norris for coverings of unweighted graphs [START_REF] Krebs | Universal Covers, Color Refinement, and Two-Variable Counting Logic: Lower Bounds for the Depth[END_REF][START_REF] Norris | Universal Covers of Graphs: Isomorphism to depth n -1 Implies Isomorphism to all Depths[END_REF], we prove the first-order definability of each regular tree with respect to the classes of trees. As the class of trees is not first-order definable 1 , our definability result must be relative to the class of trees, and not to the class of graphs. We have a similar definability result for strongly regular trees. For handling trees having nodes of infinite degree, we use an extension of first-order logic denoted by FO ω allowing generalized quantifiers ∃ ω x... expressing that "there exist infinitely x such that...".

Main new results :

(1) Equivalent characterizations of the strongly regular trees among regular trees.

(2) Classification of their automorphisms in relation with the finiteness of the diameter.

(3) First-order definability of each regular or strongly regular tree with respect to trees.

(4) Decidability of the strong regularity of a regular tree.

Summary of the article: Basic definitions are in Section 1. Unfoldings of finite and weighted directed graphs and the associated regular trees that are their complete unfoldings, are studied in Section 2. Coverings of weighted undirected graphs are studied in Section 3. The strongly regular trees that are the universal coverings of these finite graphs are studied in Section 4, which contains the main difficult results. Section 5 is a conclusion and presents open problems.

Basic definitions

This section reviews notation and some easy lemmas. Definitions for graphs and trees are standard, but we make precise some possibly ambigous terminological points.

Sets, multisets and weighted sets. All sets, graphs and trees are finite or countably infinite (of cardinality ω). The cardinality of a set X is denoted by |X| ∈ N ∪ {ω}. This latter set is equipped with an addition + that is the standard one on N together with the rule ω + x = x + ω = ω for all x in N ∪ {ω}. We denote by [p] the set {1, ..., p} and by N + the set of positive integers.

A weighted set is a pair (X, λ) where X is a set and λ is a mapping X → N + ∪ {ω}. We call λ(x) the weight of x, and, for Y ⊆ X, we define 2 λ(Y ) := Σ{λ(x) | x ∈ Y }. A weighted set can be seen as a multiset, where λ(x) is the number of occurrences of x in X. From a set X, we get a weighted set denoted by (X, 1) with all weights equal to 1.

We denote by ⊎ the union of multisets, equivalently of weighted sets:

(X, λ)⊎ (Y, λ ′ ) := (X ∪ Y, λ ′′ ) where λ ′′ (x) is λ(x) + λ ′ (x) if x ∈ X ∩ Y and is λ(x) or λ ′ (x) otherwise.
Let (X, λ) and (Y, λ ′ ) be weighted sets. A surjective mapping κ : X → Y is a weighted surjection or a surjection of multisets : (X, λ) → (Y, λ ′ ) if, for every y ∈ Y , we have λ ′ (y) = λ(κ -1 (y)).

Graphs

By a graph we mean an undirected graph, and we call digraph a directed graph, for shortness sake.

A graph is defined as a triple G = (V, E, Inc) where V is the set of vertices, E is the set of edges, and Inc is the incidence relation. The notation e : x -y indicates that edge e links vertices x and y, equivalently, that (e, x) and (e, y) belong to the set Inc ⊆ E × V . A pair in Inc is called an half-edge. We write e : x -x if e is a loop at x, i.e., incident with x. We denote by E(x) the set of edges incident with x, and by N (x) the set {y ∈ V | x -y}. We have x ∈ N (x) if there is a loop at x. A graph is simple if no two edges have the same set of ends. It may have loops.

A walk starting at a vertex x is a possibly infinite sequence x 0 , e 1 , x 1 , ..., e n , x n , ... such that x = x 0 , x 1 , ..., x n , ... are vertices and each e i is an edge whose ends are x i-1 and x i . It is a path if the vertices x 0 , ..., x n , ... are pairwise distinct. In both cases, we say that each x i is accessible from x 0 .

A directed graph (a digraph) is defined similarly as a triple G = (V, E, Inc). Its edges are called arcs. An arc a is directed from its tail x to its head y, and we denote this by a : x → y. Its half-arcs are the pairs (x, a) and (a, y), which encodes the direction of a. Hence Inc ⊆ (V × E) ∪ (E × V ). A loop at x has two half-arcs (x, e) and (e, x). A digraph is simple if, for any x, y, it has no two arcs from x to y. In that case, it can be defined as a pair (V, E) where E ⊆ V × V .

We denote by E + (x) the set of arcs outgoing from x, and by N + (x) the set of heads of the arcs in E + (x). We have x ∈ N + (x) if there is a loop at x.

A directed walk starting at a vertex x is a possibly infinite sequence x = x 0 , e 1 , x 1 , ..., e n , x n , ... as above such that x = x 0 and e i : x i-1 → x i for each i. Without ambiguity unless it is reduced to such x 0 , it can be specified as the sequence of arcs e 1 , ..., e n , .... It is a directed path if the vertices x 0 , ..., x n , ... are pairwise distinct. We say that each x i is accessible from x 0 . We denote by G/x the induced subgraph of G whose vertices are those accessible from x by a directed path, and x is called the root. We denote by Und(G) the graph underlying G : each arc e : x → y of G is made into an edge e : x -y of U nd(G).

We write

V G , E G , E G (x), E + G (x), N + G (x)
, Inc G etc. to specify, if necessary, the relevant graph or digraph G.

For graphs and digraphs, inclusion is denoted by

⊆, i.e. G = (V, E, Inc) ⊆ H = (V ′ , E ′ , Inc ′ ) if and only if V ⊆ V ′ , E ⊆ E ′ and Inc ⊆ Inc ′ . Induced inclusion denoted by ⊆ i holds if,
furthermore, E is the set of edges or arcs of E ′ whose ends, tails and heads are in V . We write then

G = H[V ]. If G ⊆ H, we denote by H -G the induced subgraph of H[V H -V G ]
of H obtained by removing the vertices of G and the edges or arcs incident to them.

The diameter of a graph or digraph G is the least upper of the distance of any two vertices. The distance is the length of a shortest path in the graph G, The

or in U nd(G) if G is directed. A homomorphism η : G → H of graphs or of digraphs maps V G to V H , E G to E H , Inc G to
quotient graph G/ ∼ has vertex set V G / ∼, edge set E G / ∼ and incidence relation Inc G/∼ such that ([e], [v]) ∈ Inc G/∼ if and only if (e ′ , v ′ ) ∈ Inc G for some e ′ ∼ e and v ′ ∼ v.
(b) The definition is similar for a digraph G: we require that if e and f are equivalent arcs, then the tail (resp. the head) of e is equivalent to that of f . The quotient graph is defined as for graphs.

(c) A quotient graph or digraph G can be defined from an equivalence relation ∼ on V G . The associated equivalence relation is defined on edges or arcs as follows :

(i) two edges are equivalent if and only if each end of one is equivalent to some end of the other;

(ii) two arcs are equivalent if and only if their tails are equivalent and so are their heads.

(d) In all cases, we have a surjective homomorphism η ∼ : G → G/ ∼ that maps a vertex, an edge or an arc to its equivalence class. An edge e : x -y is mapped to a loop e ′ in G/ ∼ if x ∼ y. The same holds for arcs.

Trees

A tree is a nonempty simple graph that is connected and has neither loops nor cycles. We call nodes its vertices. This convention is useful in the frequent case where we discuss simultaneously a graph and a tree constructed from it.

The set of nodes of a tree T is denoted by N T . A subtree of a tree T is a connected subgraph of it, hence, it is a tree.

A tree has (locally) finite degree if each node has finite degree. It has bounded degree if the degrees of its nodes are bounded.

An infinite path is a tree with one node of degree 1 and all others of degree 2. A biinfinitepath has all its nodes of degree 2.

A rooted tree is a tree T equipped with a distinguished node called its root and denoted by rt T . We denote it also by T r to specify simultaneously the root r and the underlying undirected tree T . In a way depending on r, we direct its edges so that every node is accessible from r by a directed path. If x → y in T r , then y is called a son of x, and x is the (unique) father of y. The depth of a node is its distance to the root (the root has depth 0). The height of a rooted tree is the least upper-bound of the depths of its nodes.

Let R be a rooted tree. By forgetting its root and making its arcs into undirected edges, we get a tree T := Unr(R). Hence, R = T rtR . If x is a node of R, then the digraph R/x is a rooted tree with root x, called the subtree of R issued from x. It is induced on the set of nodes accessible from x by a directed path. If i ∈ N, the truncation at depth i of R, denoted by R ↾ i, is the induced subgraph of R whose nodes are at distance at most i of the root. It is a rooted tree with same root as R and R ↾ 0 is the tree reduced to rt R . We denote by R x the rooted tree U nr(R) x : that is, we take x as new root for R.

A homomorphism of rooted trees : R → R ′ maps rt R to rt R ′ . A star is a rooted tree of height 1.

A homomorphism from a rooted tree R to a tree T is defined as a homomorphism of trees : U nr(R) → T . Lemma 1.2 : An isomorphism of rooted trees η : R → R ′ induces, for each u ∈ N R , an isomorphism : R/u → R ′ /η(u) and, in particular, a bijection

N + R (u) → N + R ′ (η(u)) such that R/v ≃ R ′ /η(v) if v ∈ N + R (u).
Definition 1.3 : Combinations of rooted trees.

(a) We define the profile π(R) of a rooted tree R as the multiset of isomorphism classes [R/u] ≃ for all u in N + R (rt R ), i.e., all sons u of the root. As trees may have infinite degree, π(R) may have ω occurrences of some [R/u] ≃ . It follows from Lemma 1.2 that two rooted trees are isomorphic if and only if they have the same profile. Hence, a rooted tree is fully defined, u.t.i., by its profile.

(b) If R and S are disjoint rooted trees, we denote by R ⊲ S the rooted tree obtained by taking the union of R and S, and by adding an arc from the root of R to that of S. The root of R is thus the root of R ⊲ S. The finite rooted trees are generated from single nodes by this operation.

It is clear that

π(R ⊲ S) = π(R) ⊎ {[S] ≃ }. Clearly, π(R ⊲ S) = π(R) if [S] ≃ has ω occurrences in π(R). Lemma 1.4 : Let S, S ′ , R and R ′ be rooted trees. (1) If R ⊲ S ≃ R ′ ⊲ S ′ and S ≃ S ′ , then R ≃ R ′ . (2) If R ⊲ S ≃ R ′ ⊲ S ′ , R ≃ R ′ and the root of R has finite degree, then S ≃ S ′ . Proof: (1) Since R ⊲ S ≃ R ′ ⊲ S ′ , we have π(R ⊲ S) = π(R ′ ⊲ S ′ ) = π(R) ⊎ {[S] ≃ } = π(R ′ ) ⊎ {[S ′ ] ≃ }.
If [S] ≃ has finitely many occurrences in π(R ⊲ S), say p, then it has p -1 occurrences in π(R) and the same number in π(R ′ ). We get

π(R) = π(R ′ ) hence R ≃ R ′ . The same holds if [S] ≃ has ω occurrences in π(R ⊲ S).
(

) We have π(R) = π(R ′ ) and π(R) ⊎ {[S] ≃ } = π(R ′ ) ⊎ {[S ′ ] ≃ }. Since π(R) is finite, we can conclude that [S] ≃ = [S ′ ] ≃ . 2

Unfoldings of directed graphs

We review from [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] some definitions relative to weighted directed graphs and their unfoldings. Complete unfoldings yield a notion of regular tree that generalizes the classical one [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF][START_REF] Courcelle | Recursive applicative program schemes[END_REF] in that their nodes can have infinite degree, and their sets of sons are not ordered. They are the complete unfoldings of finite, weighted, directed and rooted graphs.

In this section, all trees are rooted and thus directed in a canonical way. All graphs are directed; we will call them digraphs to shorten writings.

Equality of trees and digraphs is understood in the strict sense : same nodes or vertices, and same arcs. Their isomorphisms are specified explicitely and denoted by ≃. We recall that u.t.i abreviates up to isomorphism, and that unique means unique u.t.i.

Weighted directed graphs and their unfoldings Definition : Weighted directed graphs (or digraphs).

A weighted digraph is a triple G = (V, E, λ) such that (V, E) is a simple3 digraph whose set of arcs E is weighted, that is, equipped with a labelling λ : E → N + ∪ {ω}. We recall from Section 1 that simple digraphs have no parallel edges, but can have loops, and that E is a subset of V × V. Actually, we can handle parallel arcs by means of weights: an arc (x,y) with weight λ(x, y) > 1 encodes λ(x, y) parallel arcs from x to y. A simple digraph is a weighted one whose arcs have all weight 1.

A weighted digraph G is rooted if it has a distinguished vertex called its root, denoted by rt G such that every vertex is accessible from the root by a directed path (i.e., G = G/rt G ). A homomorphism of rooted digraphs : G → H maps rt G to rt H .

Definition 2.2: Unfoldings

Let H and G be rooted and weighted digraphs. (a) A surjective homomorphism η : G → H is an unfolding of a H if it satisfies the following condition:

U) If (x, y) ∈ E H , u ∈ V G , and η(u) = x, then λ H (x, y) = Σ{λ G (u, v) | η(v) = y}, equivalently, if η(u) = x, then η induces a weighted surjection: (E + G (u), λ G ) → (E + H (x), λ H ).
If all weights in G and H are 1, Condition (U) means that η is a bijection of N + G (u) onto N + H (x). We will also say that G is an unfolding of H. From the accessibility condition in the definition of a rooted digraph, unfoldings only concern connected graphs. They are called op-fibrations by Boldi and Vigna [START_REF] Boldi | Fibrations of graphs[END_REF].

(b) A complete unfolding η : G → H is an unfolding such that G is a rooted tree. We will also say that G is a complete unfolding of H or that H unfolds completely into G.

Examples 2.3 : (1) An arc x → y with weight ω such that x is taken as root unfolds (not completely) into a finite star, where at least one arc has weight ω. It unfolds completely into S ω , i.e., the tree, u.t.i., whose root has ω sons that are leaves.

(2) Let x → y be as in [START_REF] Angluin | Local and Global Properties in Networks of Processors (Extended Abstract)[END_REF]. If in addition, there is a loop y → y of weight 1, this rooted and weighted digraph unfolds completely into the union of ω infinite directed paths with same origin, and that are otherwise disjoint.

(3) A loop z → z of weight 2 unfolds completely into a complete binary rooted tree.

(4) The left part of Figure 1 shows an unfolding of the digraph on the right part. The roots are s and [s]. The common complete unfolding of these two rooted digraphs consists of an infinite directed path augmented with two pendent arcs originating from each node.

Lemma 2.4 : If η : G → H and κ : H → K are unfoldings, then κ • η : G → K is an unfolding.
Theorem 2.5 [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] Theorem 3.5 [START_REF] Angluin | Local and Global Properties in Networks of Processors (Extended Abstract)[END_REF][START_REF] Arnold | Finite transition systems[END_REF] : Every rooted and weighted directed graph H has a complete unfolding. Any two complete unfoldings of it are isomorphic.

Proof sketch: We recall the proof of the construction of a complete unfolding of H. We first assume that H has no weight, i.e. that all arcs have weight 1. We define Unf (H) as the rooted tree of finite directed walks in H starting from rt H . The root is the empty walk (reduced to rt H ), and the father of a node (e 1 , ..., e n ) is (e 1 , ..., e n-1 ). The unfolding homomorphism γ:Unf (H) → H maps a node (e 1 , ..., e n ) to the head of e n , and the arc (e 1 , ..., e n ) → (e 1 , ..., e n-1 ) to e n .

If H has weights, we replace each arc e : x → y having weight λ H (e) by λ H (e) parallel arcs (e, i)

: x → y, for i ∈ N + , 1 ≤ i ≤ λ H (e)
. We obtain a rooted digraph Exp(H), called the expansion of H, and we define Unf (H) from walks in Exp(H) instead of H. This construction shows that if

x ∈ N Unf (H) , then Unf (H)/x ≃ Unf (H/γ(x)).
We will denote by U nf(H) the complete unfolding of H, a rooted tree defined u.t.i that we distinguish from the concrete tree Unf (H) whose nodes are walks in Exp(H), or in H if H has no weight, equivalently, if all the weights are 1.

Complete unfoldings and regular trees

The notion of an infinite regular tree is important in applications to semantics, in particular because the complete unfolding of a finite transition system is regular [START_REF] Arnold | Finite transition systems[END_REF][START_REF] Courcelle | Fundamental properties of infinite trees[END_REF][START_REF] Courcelle | Recursive applicative program schemes[END_REF], and more generally for the monadic second-order logic of infinite structures, see [START_REF] Courcelle | The Monadic Second-Order Logic of Graphs IX: Machines and their Behaviours[END_REF][START_REF] Courcelle | Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems[END_REF]. We will consider regular trees that are complete unfoldings of finite digraphs.

A digraph or a tree can have labels attached to its vertices, nodes or arcs. We review definitions and results from [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF].

Definition 2.6 : Regular trees. (a) A rooted, possibly labelled, tree T is regular 4 if it has, u.t.i, finitely many subtrees T /x, inheriting the possible labels of T , i.e., if the set of isomorphism classes {[T/x] | x ∈ N T } is finite. In the latter case, its cardinality is the regularity index of T, denoted by Ind(T ).

(b) If T is a regular rooted tree of index p, then T /x is regular of index at most p for each x ∈ N T , because (T/x)/y = T /y for y ≤ T x (meaning that x is on the directed path from the root to y).

Every finite tree is regular. A rooted tree of height 1 (a star ) is regular of index 2 even if its infinite.

Definition and remarks 2.7 : The canonical quotient of a rooted and weighted digraph.

Let G be a rooted and weighted digraph. Let ≈ be the equivalence relation on V G such that x ≈ y if and only if Unf (G/x) ≃ Unf (G/y). Its quotient H := G/ ≈ is defined as follows (we repeat Definition 1.1):

V H := {[x] ≈ | x ∈ V G }, rt H := [rt G ] ≈ , E H := {([x] ≈ , [y] ≈ ) | (u, v) ∈ E G for some u ∈ [x] ≈ , v ∈ [y] ≈ }, λ H ([x] ≈ , [y] ≈ ), the weight of the arc ([x] ≈ , [y] ≈ ), is the number of arcs (x, v) in H, for some v ∈ [y] ≈ .
The labelling λ H is well-defined by Lemma 1.2 (more details in Lemma 3.9 of [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF]). By the definition of H, the mapping η :

V G → V H such that η(x) := [x] ≈ is a surjective homomorphism. Condition (U) is easy to check by means of these lemmas. Hence η : G → H is an unfolding. We call G/ ≈ the canonical quotient of G. Conversely, if α : G → H is an unfolding, then H is isomorphic to G/ ≈ ′ where x ≈ ′ y if and only if α(x) = α(y).
If G is finite, then G/ ≈ ′ is the unique rooted and weighted digraph with a minimal number of vertices of which G is an unfolding.

For the purpose of further reference, we collect these observations. Proposition 2.8: Let G be a rooted and weighted digraph.

(1) The homomorphism η : G → G/ ≈ is an unfolding.

(2) If G is finite, then G/ ≈ is, up to isomorphism, the unique rooted and weighted digraph of minimal size of which G is an unfolding.

The digraph on the right of Figure 1 is the canonical quotient of the one on the left, and of their common complete unfolding. Theorem 2.9 [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF], Theorem 3.13: (1) A rooted tree T is regular of index at most p if it is the complete unfolding of a finite, rooted and weighted digraph with p vertices. Its canonical quotient, of which it is a complete unfolding, has Ind(T ) vertices.

(2) A regular tree T is the complete unfolding of a unique rooted and weighted digraph having Ind(T ) vertices.

Proof sketch : Let H be a finite, rooted and weighted digraph with p vertices. We have observed in Theorem 2.

5 that if x ∈ N Unf (H) , then Unf (H)/x ≃ Unf (H/γ(x)) where γ is the unfolding : Unf (H) → H. Hence the complete unfolding Unf (H) has at most p different subtrees Unf (H)/x, u.t.i..
Conversely, let T be a regular tree of index p. Let ≈ be the equivalence relation on N T such that u ≈ v if and only if T /u ≃ T /v. The quotient construction of Definition 2.7 shows that T is a complete unfolding of the finite, rooted and weighted digraph T / ≈ that has p vertices.

Finite, rooted and weighted digraphs can be used as finite descriptions of regular trees. The following result shows that this description is effective.

Theorem 2.10 [11] Theorem 3.22: (1) Given a finite weighted digraph H and two vertices x, y ∈ V H , one can decide whether U nf (H/x) = U nf (H/y).

(2) If H as above is rooted, one can construct the canonical quotient U nf (H)/ ≈.

The following result is similar to a theorem by Norris [START_REF] Norris | Universal Covers of Graphs: Isomorphism to depth n -1 Implies Isomorphism to all Depths[END_REF] about universal coverings (that we will recall in Section 3).

Theorem 2.11 [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] Theorem 3.20 : Let H be a finite weighted digraph with p vertices. Let x, y ∈ V H . Then:

U nf (H/x) = U nf (H/y) if U nf (H/x) ↾ (p -1) = U nf (H/y) ↾ (p -1).

First-order definition of regular trees

We recall from Section 1 that a tree, either rooted or not, has finite degree if each node has finite degree. It has bounded degree if the degrees of its nodes are bounded by an integer. A regular tree has bounded degree if it has finite degree.

Each rooted tree T can be identified to the relational structure (N T , son T ); the root can be identified as the unique node x such that son T (y, x) does not hold for any node y. In our first-order formulas we will denote the root by the nullary symbol rt for readability. In other words, we will represent T by S(T ) := (N T , son T , rt T ) that we also call a relational structure.

We first prove the following theorem, and later on, an extension.

Theorem 2.12 : A rooted tree of finite degree is regular if and only if it is definable among rooted trees by a first-order sentence.

Saying that a rooted tree T is first-order definable (FO definable in short) among rooted trees means that there exists a first-order sentence5 ϕ such that, a relational structure of the form S(U ) := (N U , son U , rt U ) for some rooted tree U satisfies ϕ, which we denote by S(U) |= ϕ, if and only if

U ≃ T . (Note that rt U is FO-definable from son U ).
There is a monadic second-order (MSO) sentence expressing that a relational structure (D, R) where R is a binary relation on D represents a rooted tree T , hence is of the form (N T , son T ), but no such FO sentence does exist [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]. Hence, an FO definability result for regular trees must be relative to the class of rooted trees.

For having a similar result for regular trees with nodes of infinite degree, we will use the generalized quantifier ∃ ω defined so that a formula ∃ ω x.ϕ(x) is valid if and only if there exist infinitely many objects x such that ϕ(x) is valid. "Infinite" means "countably infinite", because all graphs, trees and relational structures are finite or countably infinite. We obtain an extension of FO logic denoted by FO ω . For an example, the sentence : ∃x{¬arc(x, x)∧∀y[x = y =⇒ (arc(x, y)∧¬∃z(arc(y, z))]∧∃ ω y.arc(x, y)} expresses that a simple directed graph G represented by the relational structure (V, arc) (where arc(u, v) means: u → v) is isomorphic to a star S ω i.e., a tree with root x and countably many leaves adjacent to it. Such an expression is not possible without the generalized quantifier ∃ ω . Theorem 2.13 : A rooted tree is regular if and only if it is definable among rooted trees by an FO ω sentence.

Proof of Theorem 2.12. Let T be a regular tree defined as a complete unfolding of a canonical (cf. Theorem 2.9) finite rooted and weighted digraph H without weights ω, whose vertices are rt H = 1, 2, ..., p. Let α : T → H be the unfolding mapping. Since

H is canonical, Unf (H/i) ≃ Unf (H/j) implies i = j.
For each i = 1, ..., p, let U i be isomorphic to the finite rooted tree Unf (H/i) ↾ (p -1). It follows then from Theorem 2.11 that U i ≃ U j implies i = j.

For every node y of T , we have :

(C) α(y) = i if and only if (T/y) ↾ (p -1) ≃ U i .
Since U i is finite, there is an FO formula θ i (y) such that, for every y ∈ N T , S(T ) |= θ i (y) if and only if (T /y) ↾ (p -1) ≃ U i .

Let W be a rooted tree, given by the relational structure S(W ) = (N W , son W , rt W ).

Claim : W ≃ T if and only if (1) S(W ) |= θ 1 (rt W ).

(2) For every node y of W , there is i ∈ [p] such that S(W ) |= θ i (y), and for every i, there is such a node y.

(3) For every node y of W , if S(W ) |= θ i (y), then, for every j, the node y has exactly s sons z such that S(W ) |= θ j (z) where s is the weight of the arc i → j in H, and s = 0 if there is no such arc.

These three conditions hold if W ≃ T by Property (C) and the definition of an unfolding.

Let us conversely assume that a rooted tree W satisfies (1)-(3). Let α : N W → V H be defined by α(y) = i if and only if S(W ) |= θ i (y). It is well-defined and surjective by Condition (2) and because for every y ∈ N W , there is at most one i ∈ [p] such that S(W ) |= θ i (y) (recall that the trees U i are pairwise nonisomorphic). Condition (1) yields α(rt W ) = 1. Condition [START_REF] Arnold | Finite transition systems[END_REF] shows that α is an unfolding : W → H. As W is assumed to be a rooted tree, it is a complete unfolding of H.

Conditions (1)-( 3) are expressible by a single FO sentence, constructed from the digraph H.

The proof of Theorem 2.13 will establish that, conversely, if a rooted tree of finite degree is FO-definable among rooted trees, then it is regular.

For proving Theorem 2.13, we extend the operation ⊲ defined in Definition 1.

3 into ⊲ s for 1 ≤ s ≤ ω: if R and R ′ are rooted trees, R ⊲ s R ′ is the union of R and s pairwise disjoint copies of R ′ that are also disjoint from R;
we add arcs from rt R to the roots of the copies of R ′ . Then rt R is the root of the resulting tree.

Furthermore, • will denote a rooted tree reduced to a single node.

Proof of Theorem 2.13. "Only if" The proof is a variant of that of Theorem 2.12. The rooted trees U i have bounded height but they may have nodes of infinite degree, hence we need the quantifier ∃ ω for writing formulas θ i (y).

Claim : For each i ∈ [p] there exists an FO ω sentence θ i (y) such that, for every y ∈ N T , S(T ) |= θ i (y) if and only if (T/y) ↾ (p -1) ≃ U i where α(y) = i.

For expressing Condition (3) of the proof of Theorem 2.12. when s = ω, we must express that a node y has infinitely many sons z such that S(W ) |= θ j (z). This is possible with the quantifier ∃ ω .

Proof of the claim.

The trees U i have maximal depth p -1. We will prove the existence of FO ω formulas θ i,q (y) where 0 ≤ q ≤ p -1, such that, for every y ∈ N T , we have :

S(T ) |= θ i,q (y) if and only if (T /y) ↾ q ≃ U i ↾ q.
We will say that θ i,q defines U i ↾ q. Note that if q < p -1, we may have

U i ↾ (q + 1) ≃ U i ↾ q.
The proof is by induction on q, simultaneously for all i.

If q = 0, then U i ↾ q ≃ •, hence θ i,0 (y) is ¬∃z.(son(y, z)).
If q ≥ 0, then we express U i ↾ (q + 1) in terms of the trees U j ↾ q.

Let i → j 1 , ..., i → j r be the arcs in H outgoing from i, with respective weights s 1 , ..., s r . We have :

U i ↾ (q + 1) ≃ ((...((• ⊲ s1 (U j1 ↾ q)) ⊲ s2 (U j2 ↾ q)) ⊲ s3 ...) ⊲ sr U jr ↾ q).
By the induction hypothesis, we have FO ω formulas θ jm,q (y) that define the trees U j m ↾ q. We can combine them into θ i,q+1 (y) such that : S(T ) |= θ i,q+1 (y) if and only if (T /y) ↾ (q + 1) ≃ U i ↾ (q + 1).

To handle the cases where s m = ω, we use the quantifier ∃ ω . Hence, T is defined by an FO ω sentence ϕ T .

"If" We prove that if a rooted tree is definable among rooted trees by an FO ω sentence ϕ, then it is regular.

We first give an idea of the proof. We can describe an arbitrary rooted tree S "inside" a labelled infinite binary rooted tree B, which we write S = τ(B), where τ is an MSO transduction, actually of the most simple type, also called an MSO interpretation, see [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF]. The set of structures B such that τ (B) satisfies ϕ is MSO definable hence, contains a regular tree B 0 . It will follow from the definition of τ that T := τ (B 0 ) is regular. Here are the formal details.

We let B be the set of colored binary trees B := ({0, 1} * , son 0 , son 1 , D) whose nodes are the words on {0, 1}, where son i (u, v) holds if and only if v is ui (i is 0 or 1; in B, one distinguishes a left son from a right son), and

D ⊆ {0, 1} * is prefix-closed (that is u ∈ D if uv ∈ D)
. This set will be handled as a unary relations when writing formulas.

From B as above, we define a rooted tree τ (B) := (N, son) as follows:

N is the set of nodes w in D, that are not the right son of any node (hence ε ∈ N ).

son(u, v) holds if and only if u, v ∈ N , v < B u and no intermediate node on the directed path in B from u to v is in N .

It is clear that τ (B) is a rooted tree and every rooted tree is τ(B) for some B ∈ B .

The condition on D, the set N and the relation son are MSO-definable. (Hence the mapping from B -→ τ (B) is a monadic second-order transduction, cf. [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF], of the most simple type).

It follows that if ϕ is an FO ω sentence relative to structures (N, son) that describe rooted trees, then, one can define (algorithmically, [START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]) an MSO ω sentence ψ such that B |= ψ if and only if T (B) |= ϕ. (MSO ω sentences are monadic second-order sentences written with the generalized quantifier ∃ ω x. This is equivalent to using the set predicate F in(X) expressing that a set X is finite.) However, a linear order ≤ on the set of nodes of any tree B in B, say the lexicographic order on {0, 1} * , can be defined because we distinguish left and right sons in B. It follows that the finiteness of a nonempty set X ⊆ N B can be expressed by : "X has a maximal element M X , a minimal element m X and the pair (m X , M X ) belongs to the reflexive and transitive closure of the successor relation of the linear order (X, ≤)". This is MSO expressible, hence ψ can be translated into an MSO sentence ψ ′ that does not use ∃ ω .

A classical result by Rabin (see [START_REF] Thomas | Automata on infinite objects[END_REF]), shows that if some tree B satisfies ψ ′ , then some regular tree R in B satisfies it. It is easy to see that τ (R) is regular if R is.

Remarks 2.14 : (1) If a rooted tree T is defined by an FO ω sentence on the structure (N T , ≤ T ) instead of (N T , son T ), then, the same proof shows that T is regular.

(2) The same proof shows that if a rooted tree is MSO ω -definable, then it is regular, which is not the result by Rabin as these trees may have infinite degree.

Corollary 2.15 : The MSO ω theory of a regular tree is decidable. Proof : Let T be defined by an FO ω sentence ϕ T . Let θ an MSO ω sentence to be decided. We apply the method of the second part of the proof of Theorem 2.13 to the MSO ω sentence ϕ T ∧ θ. From ϕ T ∧ θ, we construct an MSO sentence ψ such that B |= ψ if and only if τ (B) |= ϕ T ∧ θ. Then, B |= ψ if and only if the tree τ (B) is isomorphic to T and T |= θ. This is decidable [START_REF] Thomas | Automata on infinite objects[END_REF].

Remarks 2.16: Complete unfoldings and equations in trees.

Let C be a rooted tree that is not reduced to a root. Let X be a set of leaves.

For every rooted tree R, let C[R] be the rooted tree defined u.t.i., by substituting in C for each leaf in X an isomorphic copy of R disjoint from C and all others. There exists a unique rooted tree

R such that R ≃ C[R]. Unicity is of course u.t.i.. Then R ≃ U nf(D)
where D is the rooted digraph defined as follows from C :

-we delete the leaves in X, -for every arc u → x of C, we create an arc u → rt C . This is an observation that we state without proof because we will not use equations in trees. Equations in trees are frequently solved by taking least fixed points in complete partial orders [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF][START_REF] Courcelle | Recursive applicative program schemes[END_REF], which needs many preliminary definitions and lemmas. By using complete unfoldings, we obtain unique solutions in a direct way.

Coverings

We consider finite weighted undirected graphs and their coverings. We will use trees (undirected and without root) and also rooted trees, in particular the regular trees considered in the previous section.

Equality of trees and graphs is understood in the strict sense : same nodes or vertices, and same edges. Isomorphisms are specified explicitely and denoted by ≃.

Coverings of weighted graphs

We first review definitions and results about unweighted graphs from [START_REF] Angluin | Local and Global Properties in Networks of Processors (Extended Abstract)[END_REF][START_REF] Krebs | Universal Covers, Color Refinement, and Two-Variable Counting Logic: Lower Bounds for the Depth[END_REF][START_REF] Norris | Universal Covers of Graphs: Isomorphism to depth n -1 Implies Isomorphism to all Depths[END_REF]. More details, proofs and references are in [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF]. Definition 3.1 : Covering. Let G, H be graphs. A covering γ : G → H is a surjective homomorphism such that, if γ(x) = y, then γ defines a bijection : E G (x) → E H (y). We will also say that G is a covering of H.

The following proposition is due to Redemeister. Proposition 3.2: Let γ : G → H be a covering between connected graphs.

(1) If H is a tree, then G is isomorphic to H.

(2) Every connected graph is covered by a tree that is unique u.t.i..

(3) If G is finite, then, either γ is an isomorphism or |V G | > |V H | and |V G | is a multiple of |V H |.
Definition 3.3: Universal coverings of graphs (a) Every connected graph H has a covering that is a tree. We recall its construction. For a vertex x of H, we define U C(H, x) as the rooted tree of all finite walks in H that start at x and do not use a same edge twice in a row. Each (unrooted) tree U nr(U C(H, x)) is a universal covering of H. They are pairwise isomorphic for all vertices x by Proposition 3.2. We define U C(H), called the universal covering of H, as the isomorphism 6 class of the trees U nr(U C(H, x)).

(b) If there is an automorphism of H that maps x to y, then U C(H, x) is isomorphic to U C(H, y): this is clear from the descriptions in terms of walks. However, the converse does not hold : take as counter-example the union of the two graphs of Figure 2 with an edge between the two vertices marked a, that we call x and y. Then U C(H, x) ≃ U C(H, y) but there exists no automorphism of H that maps x to y.

Examples 3.4 : (1) A biinfinite path (defined in Section 1) is a universal covering of two loops at a same vertex, of two parallel edges or of any cycle.

(2) An edge is a universal covering of a single loop.

(3) Any infinite tree whose nodes have all degree k is a universal covering of any connected k-regular graph.

(4) The two graphs of Figure 2 have the same universal coverings. By Proposition 3.2, they cover only themselves.

We will use the notion of an equivalence relation ∼ on a graph of Definition 1.1.

Proposition 3.5 : (1) If ∼ is an equivalence on a graph G such that, if x and x ′ are equivalent vertices, then ∼ defines a bijection between E G (x) and E G (x ′ ), then the canonical homomorphism α : G → G/ ∼ is a covering. (2) Every connected graph H is isomorphic to T / ∼ where T is its universal covering and ∼ is an equivalence relation as in [START_REF] Angluin | Local and Global Properties in Networks of Processors (Extended Abstract)[END_REF].

Proof : (1) The proof is straightforward.

(2) Let H be connected and γ : T → H be a universal covering. We define x ∼ y for x, y ∈ V H ∪ E H if and only if γ(x) = γ(y). The result follows.

We now introduce weighted graphs. Definitions 3.6 : Half-edges and related notions (a) We recall that a graph is defined as a triple G = (V G , E G , Inc G ) and that the elements of Inc G are its half-edges. This description allows graphs with parallel edges and loops. An edge e is a loop at a vertex x if and only if (e, x) ∈ Inc G and there is no pair (e, y) in Inc G such that y = x. We denote by Inc G (x) the set of half-edges (e, x) for some e.

(b) If T is a tree and (e, x) ∈ Inc T , we denote by T/(e, x) the rooted tree induced by the nodes linked to x by a path not going through e; its root is x. We have T /(e, x) ⊆ i T x : here, we have an inclusion of trees having the same root x.

If T = Unr(R) for some rooted tree R, then R/x = T /(e, x) if e links x to its father. If e : x -y is an edge of a tree T , then T x = T /(e, x) ⊲ T/(e, y); the tree T /(e, x) is obtained from T x by removing T/(e, y).

In a tree, an half-edge (e, x) is directed toward a vertex y = x if e is the first edge on the unique path from x to y.

It follows from Lemma 1.4(2) that if e : x -x ′ and f : y -y ′ are two edges of a tree T , if x has finite degree, T x ≃ T y and T /(e, x) ≃ T/(f, y) then T x ′ ≃ T y ′ and T /(e, x ′ ) ≃ T/(f, y ′ ). This may be false if we do not assume that x has finite degree.

We now generalize the notion of covering of Definition 3.1.

Definitions and remarks 3.7 : Weighted graphs and their coverings.

(a) A weighted graph is a 4-tuple G = (V, E, Inc, λ) such that (V, E, Inc) is a simple graph (no parallel edges and no two loops at a same vertex) and λ is a weight function 7 on the set Inc of half-edges.

A graph G is made into a weighted graph W (G) as follows: p parallel edges between x and y are fused into a single edge whose two half-edges have weight p, and, similarly, p loops at x are fused into a single one of weight p.

(b) We say that G is a subgraph of a weighted graph

H, written G ⊆ H, if V G ⊆ V H , E G ⊆ E H ,
each edge (or loop) of G has the same incident vertices in H as in G (which implies Inc G ⊆ Inc H ) and λ G (e, x) ≤ λ H (e, x) for every (e, x) ∈ Inc G . We do not consider a loop (e, x) as included in an edge e : x -y (cf. Definition 3.17(c)).

(c) Let G, H be weighted graphs. A covering γ : G → H is a surjective homomorphism (of unweighted graphs) such that, if γ(x) = y and e ∈ E H (y), then λ H (e, y) = Σ{λ G (e ′ , x) | e ′ ∈ E G (x), γ(e ′ ) = e}, equivalently, if γ(x) = y, then γ induces a weighted surjection (Inc G (x), λ G ) → (Inc H (y), λ H ). We will also say that G is a covering of H.

If all half-edges and loops of G and H have weight 1, these graphs are simple and the covering condition means that γ is injective on each set Inc G (x), whence bijective, and we get the notion of covering of Definition 3. Remarks 3.9 : 1) If pairwise disjoint weighted graphs are coverings of H, then, their union is a covering of H.

2) If γ : G → H is a covering and G is connected, then H is connected because γ maps every path in G to a walk in H. If H is not connected, then G is the union of pairwise disjoint coverings of its connected components. It follows from these facts that we need only consider connected coverings of connected weighted graphs.

3) If G is a covering of a graph H, then G is also a graph, because its half-edges must have weight 1.

Examples 3.10 : 1) The complete bipartite graph K 3,4 (with 3+4 vertices) covers an edge whose half-edges have weights 4 and 3.

2) Three parallel edges cover an edge whose two half-edges have weight 3, which covers itself a loop of weight 3.

3) The two graphs of Figure 2 cover both the weighted graph consisting of the edge e : x -y and the loop f : y -y such that (e, x) has weight 6, (e, y) has weight 1 and (f, y) has weight 2. As they have both 7 vertices, a prime number, they do not cover any graph apart themselves, by Proposition 3.2. This example shows that this proposition does not extend (at least immediately) to weighted graphs.

4) The graph G consisting of two vertices, x and y, an edge e : x -y and loops f and g at x and y with weights λ(e, x) = 3, λ(e, y) = 2, λ(f, x) = 4 and λ(g, y) = 5, covers H consisting of a single vertex with a loop of weight 7.

Theorem 3.11 [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] Theorem 4.24: Given a finite weighted graph H without weights ω, one can decide if it is covered by a finite (unweighted) graph and one can construct one if possible.

Proof sketch : Let H = (V, E, Inc, λ) be as in the statement, and without loops. Assume that γ : G → H is a covering, where G is a finite graph. Let V = [p]. For each i, let w i := γ -1 (i) . Let e i,j : i-j be an edge of H, with i < j. Let m i,j = λ(e i,j , i) and m j,i = λ(e i,j , j). We have γ -1 (e i,j ) = m i,j .w i = m j,i .w j .

The system Σ H of equations of the form m i,j .x i = m j,i .x j , with one equation for each edge e i,j is satisfied by the numbers (w 1 , ..., w p ). For some weighted graphs H, it may have no solution. Otherwise, the solutions (w 1 , ..., w p ) of Σ H in positive integers are the vectors ( γ -1 (1) , ..., γ -1 (p) ) for the finite coverings γ of H by a graph G. The existence of a solution is decidable. A unique one such that w 1 + ... + w p is minimal can be computed if there exists one, and it yields a covering γ : G → H where G is a graph. The extension to the case of H with loops is straightforward because loops bring no constraints.

Example 3.12 : Let H be the cycle C 3 with vertices 1,2,3 and weights on its half-edges such that we get the equations 2x 1 = 3x 2 , 4x 2 = 3x 3 , x 3 = 5x 1 . They have no solution in N + so that H is not covered by any finite graph. It is covered by the tree whose set of nodes is N 1 ∪ N 2 ∪ N 3 where N 1 , N 2 , N 3 are infinite and pairwise disjoint, each node in N 1 has 2 neighbours in N 2 and 5 in N 3 , each node in N 2 has 3 neighbours in N 1 and 4 in N 3 , and each node in N 3 has 1 neighbour in N 1 and 3 in N 3 . This tree does not cover any graph. It covers a finite weighted graph by Theorem 3.15(2) below.

Universal coverings

We extend to weighted graphs the notion of universal covering. Definition 3.13 : Universal coverings A covering of weighted graphs γ : G → H is universal if G is a tree, which implies that H is connected. We also say that G is a universal covering of H. Any two universal coverings of a connected and weighted graph are isomorphic, as we will recall from [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF], Theorem 5.7.

We first give some useful examples.

Examples 3.14 : 1) An infinite tree T whose nodes have all degree p where 1 < p ≤ ω is a universal covering, say by γ, of a loop of weight p > 1 incident to some vertex x, where γ maps all nodes of T to x. It is also a universal covering of an edge whose half-edges have both weight p.

2) A tree such that every node of degree 3 is adjacent to a node of degree 4 and vice-versa is a universal covering of K 3,4 and also, of an edge whose half-edges have weights 4 and 3.

3) A star U nr(S ω ) consisting of one node adjacent to ω leaves is a universal covering of an edge whose half-edges have weights 1 and ω.

4) A universal covering γ of a graph H consisting of a path x -y -z with a loop at x, all weights being 1, is the path

z 1 -y 1 -x 1 -x 2 -y 2 -z 2 with γ(x 1 ) = γ(x 2 ) = x, γ(y 1 ) = γ(y 2 ) = y and γ(z 1 ) = γ(z 2 ) = z.
5) A biinfinite path (cf. Section 1 and Example 3.4(1)), is a universal covering of the following weighted graphs:

(a) a cycle (in particular two parallel edges) having weights 1, or an edge with both half-edges of weight 2, (b) the weighted graph H as in 4) except that the weight of the half-edge at z is 2, (c) one loop of weight 2 or two loops of weight 1 incident to a same vertex, (d) a path both ends of which have a loop of weight 1, or that has a loop of weight 1 at one end and an half-edge of weight 2 at the other (directed towards the loop, cf. Definition 3.6(b)), or half-edges of weight 2 at both ends, directed one toward the other. Theorem 3.15 [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF], Theorem 5.7: (1) Every connected weighted graph has a universal covering. Any two universal coverings are isomorphic.

(2) Every tree T is the universal covering of a connected and weighted graph H such that, if T covers a weighted graph G, then G covers H. This graph H is unique up to isomorphism.

For reviewing these proofs, we need some definitions and constructions. Definition 3.16 [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] Definition 5.3: Expanded symmetrized digraphs and universal coverings (a) Let H = (V, E, Inc, λ) be a connected and weighted graph. We fix a linear order8 ≤ on V . The associated expanded symmetrized digraph of H is the (unweighted) digraph ES(H) := (V, E ′ , Inc ′ ) defined as follows. For each edge e : x -y of E, we define the following arcs of ES(H):

(e + , i) : x → y if x < y, i ∈ N + , 1 ≤ i ≤ λ(e, x), (e -, i) : y → x if x < y, i ∈ N + , 1 ≤ i ≤ λ(e, y), (e ℓ , i) : x → x if x = y (e is a loop), i ∈ N + , 1 ≤ i ≤ λ(e, x).
The set Inc ′ is defined accordingly. The digraph ES(H) is strongly connected.

(b) Construction of universal coverings. Let x be a vertex of H. We let W (H, x) be the set of finite directed walks in ES(H) that start from x and that are defined as sequences of arcs (g 1 , .., g n ) such that, for each p = 1, ..., n -1, if g p = (e + , i), then g p+1 = (e -, 1), if g p = (e -, i), then g p+1 = (e + , 1), if g p = (e ℓ , i), then g p+1 = (e ℓ , 1).

We call them good walks. Hence, W (H, x) is the set of walks used to define the tree Unf (ES(H), x) from which are deleted those involving certain repetitions. This definition generalizes the construction of U C(G, x) for an unweighted graph G, defined from walks in G that do not follow the same edge twice consecutively, cf. Definition 3.3.

We define U C(H, x) as the rooted tree whose set of nodes is W (H, x), whose root is the empty walk, and such that (g 1 , ..., g n ) is the father of (g 1 , ..., g n+1 ).

We define γ : U C(H, x) → H such that9 γ(g 1 , ..., g n ) is the head of g n , and if f is the arc : (g 1 , ..., g n ) → (g 1 , ..., g n+1 ), then γ(f ) := e where g n+1 is (e + , i), (e -, i), or (e ℓ , i). Hence γ is a homomorphism Unr(U C(H, x)) → H, and furthermore a universal covering.

Example 3.17: Figure 3 shows a weighted graph to the left and the corresponding digraph ES(H) to the right. Figure 4 shows the first levels of the unfolding of ES(H) from x. The dotted arcs are deleted so as to ensure the conditions of Definition 3.16(b).

Definitions and remarks 3.18 : Quotients of trees. (a) Let T be a tree and ∼ be an equivalence relation on N T satisfying the following condition:

(N) : if v ∼ v ′ ,
w is a neighbour of v, and v has exactly p (p may be ω) neighbours equivalent to w, then v ′ has exactly p neighbours equivalent to w.

Fact : T is a universal covering of H. (b) We call H the canonical quotient of T if ∼ is the equivalence relation on N T such that x ∼ y if and only if T x ≃ T y .
We will study the trees whose canonical quotient is finite.

Proof sketch of Theorem 3.15 :

(1) We use Definition 3.16(b). Theorem 5.7 of [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] establishes that for any two vertices x and y of H assumed connected, we have U nr(U C(H, x)) ≃ Unr(U C(H, y)). Any of these trees is a universal covering of H and, u.t.i., they define the universal covering U C(H) of H. If γ : T → H is a universal covering of H, connected and weighted, and u ∈ N T , then T u ≃ U C(H, γ(u)).

(2) Let T be a tree and ∼ be the equivalence relation on N T such that x ∼ y if and only if T x ≃ T y . This equivalence relation satisfies Condition (N) of Definition 3.18 because an isomorphism α:T x → T y is also an isomorphism T u → T α(u) for every neighbour u of x. The canonical homomorphism γ :

T → T/ ∼ such that γ(v) = [v] ∼ and γ(e) is the edge [v] ∼ -[w] ∼ if e : v -w is a universal covering of H := T / ∼ because Condition (N) implies that an edge [v] ∼ -[w] ∼ is defined from an edge v -w of T , and that λ(e, [v] ∼ ) is well-defined.
Let β : T → G be a universal covering of a weighted graph G (it must be connected) with p vertices. If u ∈ N T , then T u ≃ U C(G, γ(u)). Let ≈ be the equivalence on G defined by x ≈ y if and only if U C(G, x) ≃ U C(G, y) if and only if T u ≃ T v where β(u) = x and β(v) = y. Hence, x ≈ y implies γ(x) = γ(y) and we have a covering G → G/ ≈ that is isomorphic to T / ∼= H. This weighted is defined in a canonical, hence unique way.

Universal coverings of finite weighted graphs

From now on, we will study universal coverings of finite weighted graphs. We extend the notion of regularity to trees without root and we identify the regular trees that are universal coverings of finite weighted graphs. Not all of them are. (a) A (possibly labelled) tree T is regular if it is Unr(R) for some regular rooted tree R.

Strongly regular trees

(b) It is strongly regular if it has, u.t.i., finitely many associated rooted trees

T x for x ∈ N T , that is, if the set {[T x ] ≃ | x ∈ N T } is finite.
We will prove in Theorem 4.8 that strong regularity implies regularity, which is not immediate from the definition.

Example 4.2 : The infinite path, defined as the rooted tree R such that N R := N and x ≤ R y if and only if y ≤ x is regular but Unr(R) is not strongly regular because the rooted trees U nr(R) x are pairwise non isomorphic. Theorem 4.3 : A tree T is strongly regular if and only if it is the universal covering of a finite weighted graph, if and only if it is the universal covering of a finite weighted bipartite graph.

Proof: Let γ : T → H be a universal covering, where H is weighted graph (it must be connected) with p vertices. When proving Theorem 3.15, we have seen that T u ≃ UC(H, γ(u)) if u ∈ N T . Hence, u.t.i., there are at most p rooted trees T u and T is strongly regular.

Conversely, let T be strongly regular. The proof of Theorem 3.15(2) shows that T is a universal covering of the finite graph H := T / ∼ . Furthermore this assertion proves that H is the unique weighted graph covered by T such that

|V H | + |V G | is minimal.
To get a bipartite graph, we define on T a proper 2-coloring, and we define ∼ ′ such that x ∼ ′ y if and only if T x ≃ T y and x and y have the same color. Then T is a universal covering of the finite weighted graph H ′ := T/ ∼ ′ that is bipartite.

Hence, finite weighted graphs can be used as finitary descriptions of strongly regular trees, even of infinite degree. The above construction defines a minimal and canonical one. These descriptions are effective by Theorem 4.5 below.

It follows from Theorems 3.11 and 4.3 that certain strongly regular trees are not universal coverings of any graphs. The characterization of those that are is arithmetical, cf. Theorem 3.11, rather than logical or combinatorial.

Examples 4.4 : 1) Let T consist of a biinfinite path P where each node x has , in addition, an incident pendent edge x -x ′ . The rooted trees T x for x ∈ N P are all isomorphic. So are the trees T x ′ . The quotient graph is s -s ′ , with a loop at s that represents [T x ] of weight 2. The two other half-edges have weight 1.

2) The canonical quotient of the universal covering of K 3,4 is an edge with weights 3 and 4.F example 3.10(1).

The following theorem collects several results proved in [START_REF] Courcelle | Unfoldings and coverings of weighted graphs[END_REF] Theorems 5.15 and 5.12 and Proposition 5.18 :

Theorem 4.5 : Let H be a connected and weighted graph having p vertices. Let γ : T → H be a universal covering and u, v ∈ N T .

(1) Each rooted tree T u is regular of index at most p.

(2) We have

T u ≃ T v if and only if T u ↾ (p -1) ≃ T v ↾ (p -1).
(3) One can decide whether

T u ≃ T v .
If H is unweighted, Assertion (3) is a result by [START_REF] Norris | Universal Covers of Graphs: Isomorphism to depth n -1 Implies Isomorphism to all Depths[END_REF], see also [START_REF] Krebs | Universal Covers, Color Refinement, and Two-Variable Counting Logic: Lower Bounds for the Depth[END_REF].

Corollary 4.6 : Each strongly regular tree T of finite degree is the unique tree 10 (N T , edg T ) satisfying an FO sentence ϕ T . For a strongly regular tree T with nodes of infinite degree, the same holds for some FO ω sentence ϕ T .

Proof : As for Theorem 2.12 with help of Theorem 4.5 [START_REF] Angluin | Finite common coverings of pairs of regular graphs[END_REF].

The converse does not hold as an infinite path (defined in Example 4.2), is first-order definable among rooted trees but not strongly regular. To find an exact logical characterization of strongly regular trees is an open question.

Corollary 4.7 : (1) One can decide the isomorphism of strongly regular trees defined as universal coverings of finite and weighted graphs.

(2) One can decide whether U nr(U nf(H)) ≃ T where H is a finite, rooted and weighted digraph H, and T is a universal covering of finite and weighted graph G.

Proof : (1) Let G and H be finite, connected and weighted graphs with respectively p and q vertices. Then, Assertions (2) and (3) of Theorem 4.3 can be extended as follows 11 , where u ∈ V G and v ∈ V H :

(2') UC(G, u) ≃ U C(H, v) if and only if U C(G, u) ↾ (p + q -1) ≃ U C(H, v) ↾ (p + q -1), (3'
) one can decide whether U C(G, u) ≃ U C(H, v), whence also whether U C(G) ≃ U C(H) by testing all pairs (u, v).

(2) Let ϕ T be the FO ω sentence that defines T according to Corollary 4.6. By Corollary 2.14, one can decide whether U nr(U nf(H)) satisfies ϕ T , hence whether U nr(U nf(H)) ≃ T.

Hence, finite weighted graphs can be used as finite descriptions of strongly regular trees, even of infinite degree. The above construction defines a minimal and canonical one. It follows from Theorems 3.12 and 4.6 that certain strongly regular trees are not universal coverings of any graphs. The characterization of those that are is arithmetical, cf. Theorem 3.12, rather than logical or combinatorial.

Characterizations of strongly regular trees Theorem 4.8 : The following properties of a tree T are equivalent: 1) T is strongly regular, i.e., the set

{[T x ] ≃ | x ∈ N T } is finite.
2) The rooted trees T x are regular and have bounded index.

3) The set {[T/(e, x)] ≃ | (e, x) ∈ Inc T } is finite.

4) The rooted trees T /(e, x) are regular and have bounded index.

Proof : We first prove that 1) implies 2), 3) and 4). Let T be strongly regular. By Theorem 4.3, there is a covering γ : T → H where H = (V 1 , V 2 , E, Inc, λ) is a finite bipartite and weighted graph, hence without loops. For defining ES(H), we choose a linear order on vertices such that V 1 < V 2 . Without lost of generality, we take T := U nr(U C(H, r)) for some r ∈ V 1 .

We recall from the construction of Definition 3.16(b) that the nodes of a rooted tree UC(H, u) are the good walks starting from u.

We extend as follows the definition of U C(H, u). Let e : u -v be an edge of H. We define UC(H, u, e) as the set of good walks that do not start by an arc specified as follows: if u ∈ V 1 and v ∈ V 2 , we forbid (e + , 1) as first arc; if u ∈ V 2 and v ∈ V 1 , we forbid (e -, 1)as first arc.

Then UC(H, u, e) is a rooted tree, similar to UC(H, u), actually obtained from it by deleting a subtree.

Let x and y be nodes in T . Let y be defined in U C(H, γ(x)) = T x by a good walk (g 1 , .., g n ) in ES(H) starting from γ(x). The walks (g n+1 , .., g p ) such that (g 1 , .., g n , g n+1 , .., g p ) is a good walk are the nodes of UC(H, γ(y), γ(g n )) by the restrictions made to the initial steps of their definitions as walks. It follows that T x /y ≃ U C(H, γ(y), γ(g n )). The subtrees of T x are, apart from itself, isomorphic to the rooted trees U C(H, u, e) where e is incident with u. There are 2. |E| such pairs (u, e), hence T x is regular of index at most 2. |E| + 1. This proves Assertion 2).

For proving Assertion 3), consider an edge f : x -y in T . The subtree T/(f, y) = T x /y is isomorphic to U C(H, γ(y), γ(f )). Hence, there are at most 2. |E| of them, u.t.i.

For proving Assertion 4), we consider (T /(e, x))/z where e : x -y in T and z ∈ T/(e, x). If z = x, then (T /(e, x))/z = T /(e, x). Otherwise there is a path in T y from x to z with last arc f . We have (T /(e, x))/z ≃ U C(H, γ(z), γ(f)). Hence, T /(e, x) has at most 2. |E| + 1 subtrees u.t.i.. It is regular, which proves Assertion 4). 3) =⇒ 1). Let e : x -y be an edge of a tree T and z ∈ N T : we have T x = T /(e, x) ⊲ T /(e, y). (See Definition 1.3 for ⊲). Hence, if there are p subtrees of the form T /(f, z),u.t.i., there are at most p 2 rooted trees T x , u.t.i..

4) =⇒ 2) :

The subtrees T x /y of T x are T x if y = x and (T /(e, z))/y if e : x -z and z is on the path in T x from x to y ; we may have y = z. Hence, each rooted tree T x is regular and its index is at most 1 + Ind(T /(e, z)).

2) =⇒3) : This proof is the most technical one. Let T be a tree. Claim : If each rooted tree T x is regular of index at most p, then T has less than p 2p+3 nonisomorphic rooted subtrees T /(e, y).

Proof : Let us fix x ∈ N T . For each (e, y) ∈ Inc T , we examine how the rooted tree T/(e, y) is related to T x and its subtrees.

Case 1 : x = y. We have T /(e, y) = T /(e, x) = T x ⊲ -1 T /(e, y ′ ) = T x ⊲ -1 (T x /y ′ ) where y ′ is the other end of e. This gives at most p trees T /(e, y).

Case 2 : x = y and (e, y) is directed toward x. Then T /(e, y) = T x /y. This gives at most p trees T /(e, y).

Case 3 : x = y and e is not directed toward x. The path from y to x goes through nodes z 1 , ..., z s and edges f 1 , ..., f s+1 . See Figure 5 for an example. We have :

T /(f s+1 , x) = C, T /(f s , z s ) = B s ⊲ T /(f s+1 , x) = B s ⊲ C, T /(f s-1 , z s-1 ) = B s-1 ⊲ T /(f s , z s ) = B s-1 ⊲ (B s ⊲ C), ... T /(f 1 , z 1 ) = B 1 ⊲ (B 2 ⊲ (... ⊲ (B s-1 ⊲ (B s ⊲ C))...)), T /(e, y) = A ⊲ T /(f 1 , z 1 ) = A ⊲ (B 1 ⊲ (B 2 ⊲ (... ⊲ (B s-1 ⊲ (B s ⊲ C))...))).
We have C = T /(f s+1 , x)) = T y /x. Let us denote x by z s+1 . For each i ≤ s + 1, we have T/(f i , z i )) = T y /z i , and there are at most p nonisomorphic trees T y /z i .

If s + 1 > p, we can shorten the expression of T/(e, y). To do this we let j be the maximum integer ≤ s + 1 such that T /(f j , z j ) ≃ T /(f i , z i ) for some i < j. Let i be the minimal one. Then :

T /(e, y)

≃ A ⊲ (B 1 ⊲ (B 2 ⊲ (... ⊲ (B i-1 ⊲ (B j ⊲ (B j+1 ⊲ ... ⊲ (B s ⊲ C))...))).
If this expression contains more than p -1 trees B k , k ∈ {1, ..., i -1, j, ..., s}, we have T /(f j ′ , z j ′ ) ≃ T /(f i ′ , z i ′ ) for some i ′ < j ′ < j. We can again delete some trees B k , and we repeat deletions until we get an expression with less than p trees B k . We have:

A = T x /y ⊲ -1 T /(e, y ′ ) = T x /y ⊲ -1 T x /y ′ . Similarily, B i = T/(f i+1 , z i ) ⊲ -1 T/(f i , z i-1 ) = T x /z i ⊲ -1 T x /z i-1 for i = 1, ..., s -1, and C = T x ⊲ -1 T x /(f s+1 , z s ).
Hence, we have at most p 2 nonisomorphic trees for each of A, B i , C, hence for Case 3, we get at most (p 2 ) 2 + (p 2 ) 3 + ... + (p 2 ) p + (p 2 ) p+1 < p.(p 2 ) p+1 = p 2p+3 .

Cases 1) and 2) are covered by this large estimate.

Assertion 3) follows. We use the fact that each tree T y has at most p nonisomorphic subtrees T y /z, but the bound on the number of nonisomorphic trees T/(e, y) is done from considering a single tree T x . If, in the proof of the claim, x is a leaf, then C is a single node and we improve the bound to p 2p+1 which remains certainly overestimated.

Deciding strong regularity

We prove that one can decide whether a regular tree is strongly regular. Theorem 4.9 : One can decide if the tree U nr(U nf(H)) where H is a finite rooted and weighted digraph is strongly regular. If it is, one can construct a finite weighted graph of which it is the universal covering. Corollary 4.7 shows that the problem is semi-decidable : if we are given a finite rooted and weighted digraph H and a finite weighted graph G, we can decide whether U nr(Unf (H)) ≃ U C(G). It suffices to decide if the regular tree Unf (H) satisfies the FO ω sentence that describes U C(G) with respect to the class of trees, which is possible by this corollary. For proving the theorem, we need only find a decidable condition ensuring that U nr(U nf(H)) is not strongly regular. The proof needs some definitions and preliminary results. Lemma 4.10 : Let H be a rooted and weighted digraph and T be the tree Unr(Unf (H)). Let e : y → x be an arc of Unf (H) where x is at depth p. One can build rooted and weighted digraphs H ′ and H ′′ such that 12 : Figure 8: Examples for the proof of Theorem 4.9. See also Figure 7.

4.13) C y,x = A 1 ⊲ (A 2 ⊲ ...(A q ⊲ * )...) where A i := R/x i-1 -R/x i and C y ′ ,x ′ = A ′ 1 ⊲ (A ′ 2 ⊲ ... ⊲ (A ′ q ⊲ * )...) where A ′ i := R/x ′ i-1 -R/x ′ i for i = 1, ...q. By (1), we have isomorphisms A i → A ′ i from which we get C y,x ≃ C y ′ ,x ′ and D y,x ≃ D y ′ ,x ′ .
Proposition 4.16 : Let R be a rooted tree. The tree U nr(R) is strongly regular if and only if R has only finitely many subtrees U x up to isomorphism.

Proof : Theorem 4.8 shows that U nr(R) is strongly regular if and only it has, u.t.i., finitely many rooted subtrees U nr(R)/(e, z). These trees are those of the forms R/y and U x for y ∈ N R and x ∈ N R -{rt R }, but since R is regular, there are finitely many trees R/y, u.t.i.. The assertion follows.

In the following proposition, H is a finite rooted weighted digraph with p vertices, γ : R → H a complete unfolding and T := U nr(R). We can assume that H canonical (cf. Definition 2.7) so that have R/x ≃ R/y if and only if γ(x) = γ(y) for any nodes x, y of R. This is effective because one can construct a equivalent canonical digraph from one that is not (Theorem 2.9). Equivalence means that their complete unfoldings are isomorphic.

We let R := {R 1 , ..., R p } be such that each subtree R/x is isomorphic to one and only one tree in R. Proposition 4.17 : If T is strongly regular, if x, y ∈ N R are such that y < R x < R rt R and γ(x) = γ(y), then, for every w such that γ(w) = γ(x), we have U w ≃ R/z for some z.

Proof : Let x, y ∈ N R be such that y < R x < R rt R and γ(x) = γ(y). Let (e 1 , ..., e q ) be the path in R from x to y. Its image by γ is the directed walk (γ(e 1 ), ..., γ(e q )) in H. This path can be extended into an infinite path in R :

x 0 = x → ... → x 1 = y → ... → x 2 → ...... → x n-1 → ... → x n → ...
such that the image by γ of each subpath from x i to x i+1 is (γ(e 1 ), ..., γ(e q )).

We have :

γ(x i ) = γ(x) for each i ≥ 0, C xi+1,xi ≃ C xi,xi-1 and D xi+1,xi ≃ D xi,xi-1 for i ≥ 1 by Lemma 4.15(2).
Assume now that T is strongly regular. As the set of rooted trees U xi is finite u.t.i., one can find two of them, say U y and U s such that y < R s and d R (s, y) > d R (s, rt R ). Lemma 4.12(2) yields that U y and all trees U xi belong to R, u.t.i, which means that they each of them is isomorphic 14 to one in R. The same holds for U w if w ≥ R x i for some i because by Proposition 4.17, they are of the form R/z.

Let now w be any node in R such that γ(w) = γ(x). Since R/x ≃ R/w, there is in R/w a path from w to some node u whose sequence of arcs (g 1 , ..., g q ) is such that γ(g i ) = γ(e i ) for each i. The above proof works then for w and u instead of x and y.

Proof of the Theorem 4.9 : As observed above after the statement, if H is a finite weighted digraph, the property that T := U nr(Unf (H)) is strongly regular is semi-decidable, because if we are given a finite weighted graph G, we can decide if U C(G) ≃ Unr(U nf(H)).

However, the following condition is necessary and sufficient for T to be strongly regular. Its negation is semi-decidable.

(Z) for all x, y ∈ N R such that y

< R x < R rt R , if γ(x) = γ(y) then U x ∈ R.
Claim 1 : T is strongly regular if and only if Condition (Z) holds. Proof : By Proposition 4.17, it holds if T is strongly regular. We now prove the converse. We enumerate R as {R 1 , ..., R p } and we let X i be the set of nodes x = rt R such that R/x = R i . We assume that Condition (Z) holds. We consider each set X i .

Case 1: X i contains two comparable nodes y < R x. For every w ∈ X i , we have u < R w such that u ∈ X i by the argument used at the end of the proof of Proposition 4.17. Hence U w ∈ R.

Case 2 : Case 1 does not hold, hence, X i is an antichain. Let y ∈ X i and rt R → y 1 → y 2 → ... → y n = y be the directed path P in R from the root to y.

We have U y = D y,rt R -{ * }. Subcase (2.1) : Each node y k is in a set X j that is an antichain. Then n ≤ p because no two nodes y k can be in a same antichain, as

y k < R y k ′ if k ′ < k. If
another similar path from rt R to y ′ ∈ X i has the same images by γ as P , then, by Lemma 4.15, we have D y,rtR ≃ D y ′ ,rtR hence U y = D y,rtR -{ * } ≃ U y ′ = D y ′ ,rtR -{ * } (cf. Definition 4.13(c)).

As these paths have bounded lengths, they have finitely many different images by γ. Hence, there are finitely many such trees contexts D y,rtR and trees U y , u.t.i.. Subcase (2.2) : Otherwise, let m be maximal such that y m belongs to a set X j that is not an antichain.

Then Claim 2 : The negation of Condition (Z) is semi-decidable. Proof : The negation of (Z) says that there exist x and y such that y < R x < R rt R , γ(x) = γ(y) and U y / ∈ R. We let R be Unf (H). A node x can be given to an algorithm as a sequence of arcs, from which we get γ(x). Lemma 4.10 shows that for every y ∈ N R , one can construct a finite weighted and rooted digraph H ′′ such that Unf (H ′′ ) ≃ U y . For each i = 1, ..., p, we know the unique node z of H such that Unf (H, z) ≃ R i . We can decide whether Unf (H ′′ ) ≃ Unf (H, z) by Theorem 2.9, hence finally, whether U y ∈ R.

Hence, we have a semi-decidable condition for U nr(R) not to be strongly regular. As we also have a semi-decidable condition for strong regularity, this concludes the proof.

The latter semi-decision procedure finds (painfully) a finite weighted graph G such that U C(G) ≃ U nr(R) if there exists one . Theorem 4.9 is a decidability result. It does not give a usable algorithm. An improvement of Proposition 4.17 might help, see its footnote refering to Remark 4.14.

Diameter and automorphisms of strongly regular trees

To complete our study of strongly regular trees, we characterize those of finite diameter. As we allow nodes of infinite degree, an infinite tree such as S ω may have finite diameter. In relation with diameter, we examine their automorphisms. An ℓ-tree as a tree with loops at some nodes.

Proposition 4.18 : The universal covering of a finite connected weighted graph H has a finite diameter if and only if H is an ℓ-tree such that :

1) it has no two half-edges (e, x) and (f, y) of weights at least 2 such that (e, x) is in the direction of y and (f, y) is in that of x, and 2) it has at most one loop e, its weight λ(e, x) is 1, and there is no half-edge (e, y) of weight at least 2 directed toward x.

Otherwise, U C(H) contains a biinfinite path.

Note that an infinite tree may have an infinite diameter without containing any biinfinite path: an example is the union of finite paths of all lengths that have in common a unique node.

Proof : "Only if" : Assume that U C(H) has finite diameter. As it is a tree, it does not contain a biinfinite path. Examples 3.14 [START_REF] Boldi | Fibrations of graphs[END_REF] show "forbidden" cases, where U C(H) contains an biinfinite path. We examine these cases.

(i) H contains a cycle G, then U C(G) ⊆ U C(H), this is clear from Definition 3.16(b) and U C(G) is a biinfinite path.

Hence, H is an ℓ-tree because a loop is not a cycle, and its universal covering is an edge.

(ii) If H has two half-edges (e, x) and (f, y) of weights at least 2 such that (e, x) is directed toward y and (f, y) is directed toward x, (cf. Example 3.14.5(d)), then H contains a weighted graph G consisting of a path between x and y with end half-edges (e, x) and (f, y) of weight 2 all other weights being 1. Then G is covered by a cycle, U C(G) is a biinfinite path contained in U C(H). This case is thus excluded.

The other cases are : (iii) H has two loops or one loop of weight at least 2, (cf. Examples 3.14.5 (c) and 3.14.5 (d)).

They are excluded by a similar proof. Hence, Conditions 1) and 2) are satisfied.

"If" Let H be a weighted tree (without loops) satisfying Condition 1) of the statement. If all weights are 1, then it is a tree, and U C(H) ≃ H by Proposition 3.2, hence has finite diameter since H is finite.

Otherwise, there is a vertex s such that, on every path from s to a leaf, there is no half-edge (e, x) such that λ(e, s) > 1 and that is directed towards s. We call it a good root. We prove its existence by induction on the number of edges : let x be a leaf with pendent edge e : x -y. By induction, H ′ defined as H minus x and e has a good root s. If λ(e, x) = 1 then s is a good root for H. If λ(e, x) > 1 then x is a good root for H by Condition 1).

Let s be a good root for H and d be its maximum distance to a leaf. Let < be a linear ordering of V H such that the father u in the rooted tree H s of a node v is smaller, u < v. In ES(H), there is no arc of the form (e -, i) for i ≥ 2. Hence on each directed walk that defines a node of U C(H, s), we have only arcs of the form (e + , i) and so the nodes are increasing with respect to <. Hence, they are on paths of length at most d, the rooted tree U C(H, s) has height d and its diameter is at most 2d.

Assume now that H has a loop of weight 1 at some node s and satisfies Conditions 1) and 2). By Condition 2), s is a good root. The graph H is covered by K consisting two copies of H s minus the loop, linked by the nodes that are copies of s. It is clear that K, rooted by any of the two copies of s, is a Case 2 : (f,α(x)) is not directed toward x. We have a path x -y -z 1 -... -z p -α(x) -α(y) in T . As α is an automorphism, we have T x ≃ T α(x) and T y ≃ T α(y) . By Theorem 2.9 we can assume that H is canonical. Hence, γ(x) = γ(α(x)) and γ(y) = γ(α(y)). As in the first part of the proof, we can extend x -y -z 1 -... -z p -α(x) -α(y) infinitely many times to the left and the right, and we get a biinfinite path, hence T has an infinite diameter.

Remark 4.20 : A strongly regular tree U C(H) of infinite diameter, for an example a biinfinite path, may also have automorphisms with a fixed node or edge. But it may also have no such automorphism. For an example, consider H defined as the union of the cycle 1 -2 -3 -1 and paths 1 -a, 2 -b -c and 3 -d -e -f . Its universal covering γ : T → H consists in a biinifinite path P whose image is the biinfinte periodic walk ... -1 -2 -3 -1 -2 -3 -... and paths of lengths 1,2,and 3 attached to P . The neighbourhoods in H of radius 3 of its vertices are pairwise nonisomorphic. Hence, an automorphism of T must be as constructed in the first part of the proof of Theorem 4.19.

Conclusion

The strongly regular trees arise as universal coverings of weighted graphs, a notion that is useful in distributed computing [START_REF] Angluin | Local and Global Properties in Networks of Processors (Extended Abstract)[END_REF]. Here, we have been interested in the structure of such trees, from a purely combinatorial anf logical view.

We have generalized the standard definition of universal coverings to weighted graphs, so that they can have nodes of infinite degree.

We have established several decidability results concerning them, by using related results relative to the complete unfoldings of finite weighted directed graphs representing transition systems.

Open questions:

(1) Can one find a usable, or even efficient, algorithm for deciding strong regularity of a regular tree, as opposed to the decidability result of Theorem 4.9.

(2) Can one find a logical characterization of strongly regular trees? (cf. Theorem 4.12)

(3) What can be said of the universal covering of a graph from Caucal's hierarchy [START_REF] Blumensath | On the structure of graphs in the Caucal hierarchy[END_REF] ? Presumably its monadic second theory is decidable [START_REF] Courcelle | Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems[END_REF].

Figure 1 :

 1 Figure 1: Example 2.3(4).

(

Figure 2 :

 2 Figure 2: Two graphs not covering any graph. Example 3.4(4).

1 .

 1 Each graph G covers the weighted graph W (G). If G, finite, covers H, then |V G | ≥ |V H | but Proposition 3.2 does not hold (see below Example 3.10(3)). If |V G | = |V H | then |E G | ≥ |E H | because several edges get fused into a single one with larger weights. Proposition 3.8 : If γ : G → H and δ : H → K are coverings, then so is δ • γ : G → K.

Figure 3 :

 3 Figure 3: Example 3.17.

Figure 4 :

 4 Figure 4: Example 3.17

  Let H := T / ∼ be the weighted graph defined as follows :V H := N T / ∼, E H contains an edge e : [v] ∼ -[w] ∼ ifand only if v is adjacent to some vertex of [w] ∼ if and only if, by Condition (N), each vertex of [v] ∼ is adjacent to some vertex of [w] ∼ ; the weight λ(e, [v] ∼ ) is the number of edges of T linking v and a vertex of [w] ∼ where w is adjacent to v.

Definition 4 . 1 :

 41 Regular and strongly regular trees.

Figure 5 :

 5 Figure 5: Case 3 in the proof of 2)=⇒ 3) in Theorem 4.8.

  Inc H and preserves incidences in the obvious way. It maps loops to loops but can map a nonloop edge or arc to a loop. It preserves labels if any. We extend the notion of homomorphism by allowing "forgetful" operations. A homomorphism U nd(G) → H where G is directed and H is not is also considered as a homomorphism G → H. Similar conventions concern labelled graphs.Isomorphism is denoted by ≃ and the isomorphism class of G by [G]. We will use u.t.i. to abreviate up to isomorphism. Unless otherwise mentioned, unique with mean unique up to isomorphism.

Definition 1.1 : Quotient graphs and digraphs (a) An equivalence relation ∼ on a graph G is an equivalence on V G ∪ E G such that (i) no vertex is equivalent to an edge, (ii) if e and f are equivalent edges, then each end of e is equivalent to some end of f and vive-versa.

  , U y ≃ D y,ym [U ym ]and U ym ∈ R. As in Subcase (2.1), we have finitely many contexts of the form D y,ym u.t.i.. As R is finite, we obtain finitely many trees U y of this form, u.t.i.. To sum up the trees U x are either in R u.t.i, of the forms described in Subcases (2.1) and (2.2). Hence, they are finitely many u.t.i and T is strongly regular.

It is however monadic second-order definable.

For typographical reasons, we use the notation Σ{λ(x) | x ∈ Y } rather than x∈Y λ(x) and we will do the same below.

We only consider simple digraphs, although definitions and results could be extended to weighted digraphs with parallel arcs. The associated complete unfoldings would be the same trees.

Slightly different notions of regular trees are studied in[START_REF] Courcelle | Fundamental properties of infinite trees[END_REF][START_REF] Courcelle | The Monadic Second-Order Logic of Graphs IX: Machines and their Behaviours[END_REF][START_REF] Courcelle | Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems[END_REF]. However, they have in common the finiteness of the set of subtrees, up to isomorphism.

A sentence is a formula without free variables.

We use boldface symbols to indicate that we consider isomorphism classes of trees. To the opposite, a tree U C(H, x) is constructed concretely from edges and vertices of H.

The two halves of an edge may have different weights.

Another linear order yields isomorphic graphs and trees.

We write γ(g 1 , .., g n ) for γ((g 1 , .., g n )).

0 Edges are specified by a binary relation edg T on nodes. 1 1 See[START_REF] Krebs | Universal Covers, Color Refinement, and Two-Variable Counting Logic: Lower Bounds for the Depth[END_REF] for a thorough analysis of this fact in the case where G and H are graphs.

[START_REF] Angluin | Finite common coverings of pairs of regular graphs[END_REF] The relation ⊆ i denotes induced inclusion of digraphs without their roots. That is formally, U nr(H) ⊆ i Unr(H ′′ ) ⊆ i U nr(H ′ ).

[START_REF] Blumensath | On the structure of graphs in the Caucal hierarchy[END_REF] By using Remark 4.14, one can prove that if R has finite degree, then the trees U x i are all isomorphic. We conjecture that the same holds in general but we have yet no proof.

Unf (H ′ ) ≃ T x and Unf (H ′′ ) ≃ T /(e, y).

Proof : We let γ : Unf (H) → H be the unfolding homomorphism and x 0 → x 1 → ... → x p be the directed path in Unf (H) from the root x 0 to x = x p , so that y = x p-1 . We first build a weighted digraph K by adding vertices and arcs to H as follows. We add new vertices z 0 , z 1 , ..., z p , for each i = 1, ..., p, we add an arc z i → z i-1 of weight 1, for each arc f : x i → w of Unf (H) , i = 0, ..., p, we add an arc z i → γ(w) of weight λ H (γ(f )) if 13 w = x i+1 or of weight λ H (γ(f )) -1 if w = x i+1 and λ H (f ) ≥ 2.

We have Unf (K/z p ) ≃ T x : just consider the directed paths in Exp(K) starting from z p (cf. Theorem 2.5). The unfolding mapping γ ′ is γ extended by γ ′ (z i ) := x i , for i = 0, ..., p. Hence,

Some vertices of H, in particular the root rt H may not be accessible in K from z p . Hence, we take H ′ := K/z p . We take

Example 4.11 Figure 6 shows a weighted digraph H with root 1. The weights 1 are not shown. The tree

, where γ : Unf (H) → H is the unfolding homomorphism. In order to make d into the root of T , we build K with root d1 such that Unf (K) ≃ T d . The vertices added to H by the construction of Lemma 4.10 are d1, c5, b2 and a1, and the added arcs are in red. Some weights of the added arcs are as follows: the arc c5 → 1 has weight 2 whereas the weight of 5 → 1 in H is 3. Similarly, the arc a1 → 2 has weight 1 whereas the weight of 1 → 2 in H is 2. The arc d1 → 2 has weight 2, as the arc 1 → 2 in H.

We denote by d R (x, y) the distance of x and y in a rooted tree R; it is the same as in the unrooted tree Unr(R).

Notation for subtrees: Let R be a rooted tree and e : y → x be an arc of R. Hence, x is a son of y. We let T := U nr(R).

We denote by U x the rooted tree T /(e, y) = T x /y = T y -T y /x. Its root is y. We have

We also have T y /x = T z /x = R/x for any node z ≥ R y.

Lemma 4.12 : Let R be a rooted tree and T := Unr(R).

( Otherwise, let w be the node of this path that is closest to the root. If w = rt R , then the node following w on this path is a son u of w. We have z in R/u = T x /u and so, we have

If w = rt R , then the node following w on this path is a son u of w

(2) Let y, x, w be as stated. We have y < R y ′ ≤ R x < R x ′ ≤ R rt R where x ′ is the father of x and y ′ is that of y.

Let α be an isomorphism :

We first prove that U x ≃ R/z for some z.

We have in T y /y ′ a path P from y ′ to x ′ . (Its edges are directed in opposite directions in T y /y ′ and in R.) Its length is d R (x, y). The isomorphism α maps it to a path P ′ of same length in T x /x ′ from x ′ to some node z := α(x ′ ) below x ′ in the rooted tree T x .

We

Furthermore, the isomorphism α shows that (T x /x ′ )/z ≃ (T y /y ′ )/x ′ .We have

where w ′ is the father of w. We take a path P from y ′ to w ′ , going through x ′ . Its length is d R (x, y) + d R (x ′ , w ′ ) hence again, more than d R (x ′ , rt R ). Its image under α is a path P ′ of equal length from x ′ to z := α(w ′ ). We have by (1) T x ′ /z = R/z. By α we have (T x /x ′ )/z ≃ (T y /y ′ )/w ′ .

We have T x ′ /z = (T x /x ′ )/z and (T y /y ′ )/w ′ = T w /w ′ = U w . Hence, U w ≃ R/z, as claimed. Definitions 4.13 : Contexts and substitutions. (a) A context is a rooted tree C that has a distinguished leaf denoted by * , and that is not the root. Its depth p is that of * (and not the maximal depth of a leaf). A context of depth p can be expressed as

If C and R are not disjoint, we replace one by an isomorphic copy and the resulting tree is well-defined u.t.i.

Its nodes are those of R/x not in R/y together with the leaf * that replaces R/y. Let (e 1 , ..., e q ) be the sequence of arcs of the path from x = x 0 to y = x q and (x 0 , x 1 , ..., x q ) be the sequence of nodes. Then :

where

There is a "dual" context D y,x , defined from C y,x as above by : D y,x = A q ⊲ (A q-1 ⊲ ...(A 1 ⊲ * )...).

If

This follows from Lemma 1.4(2) for contexts C and C ′ of depth 1. Then, we use an induction of the common depth of C and C ′ , that we can both express of the form:

A 1 ⊲ (... ⊲ (A p ⊲ * )...). This implication may be false if C is not of finite degree. (1) If e : x → y and f :

(2) If (e 1 , ..., e q ) is (the sequence of arcs of) a path from x = x 0 to y = x q , if (f 1 , ..., f q ) is a path from x ′ = x ′ 0 to y ′ = x ′ q , and γ(e i ) = γ(f i ) for each i, then C y,x ≃ C y ′ ,x ′ and D y,x ≃ D y ′ ,x ′ .

Proof : Without loss of generality, we can assume that R = U nf(H).

(1) Hence, x is a walk (g 1 , ..., g p ) in H from rt H to u and γ(x) = u.

Then, y = (g 1 , ..., g p , (g, i)) cf. Theorem 2.5, g : u → v is an arc of H, 1 ≤ i ≤ λ(g), γ(y) = v and γ(e) = g.

The tree R/x -R/y consists of the walks in starting from rt H and of the form (g 1 , ..., g p , h p+1 , ....., h n ) such that h p+1 = (g, i).

Similarly, x ′ is a walk (g ′ 1 , ..., g ′ m ) from rt H to u and we have γ(x ′ ) = u. Then y ′ = (g ′ 1 , ..., g ′ m , (g, j)) and 1 ≤ j ≤ λ(g) , γ(y) = v.γ(f ) = g. The tree R/x ′ -R/y ′ consists of the walks in Exp(H) of the form (g ′ 1 , ..., g ′ m , h ′ m+1 , ....., h ′ q ) with h ′ p+1 = (g, j). If i = j, the mapping:

Otherwise, we the mapping :

, and h p+1 otherwise. (Recall that h p+1 = (g, i)).

(2) Let (e 1 , ..., e q ) be a path from x = x 0 to y = x q in R. Then (cf. Definition tree satisfying Condition 1). We have U C(H) ≃ Unr(K) and the diameter of K is at most 2d + 1.

Let α : T → T be an automorphism of a tree T . A node x is fixed if α(x) = x and an edge e : x -y is fixed if x and y are fixed or if α(x) = y and α(y) = x. By automorphism we mean one that is not the identity. A tree may have no automorphism, according to this shortened terminology.

Theorem 4.19 : A strongly regular tree has an infinite diameter if and only if it has an automorphism without any fixed node or edge.

Proof : Let γ : T → H be a universal covering of a finite weighted graph H. By Proposition 4.18, T has a biinfinite path P . Since V H is finite, P has a subpath x -y -z 1 -... -z p -x ′ -y ′ such that: γ(x) = γ(x ′ ), γ(y) = γ(y ′ ). Since H is simple, the two edges x-y and x ′ -y ′ have the same image by γ.

Without loss of generality, we can consider that T = U C(H, γ(x)). It follows from the construction described in Definitionq 3.3 and 3.16 that P can be extended into a path :

x

We can repeat this extension, to the right and to the left, infinitely many times, and we get a biinfinite path P ′ in T of the form:

x 0 = x, y 0 = y, x 1 = x ′ , y 1 = y ′ , z 0,j = z j , z 10,j = z ′ j , for all i and j = 1, ..., p.

We now define an automorphism α of T . We first define: α(x i ) := x i+1 , α(y i ) := y i+1 , α(z i,j ) := α(z i+1,j ) for all i ∈ Z and j = 1, ..., p.

Then we extend α outside of P ′ . We let U be T minus the edges of P ′ (we keep in U the nodes of P ′ ). It is a union of disjoint trees. Let U w be the connected component containing w where w is any node of P ′ : it is a tree with root w. We can extend α so that it defines isomorphisms of rooted trees : U x i -→ U x i+1 , U x i -→ U x i+1 , U z i,j -→ U z i+1,j for all i ∈ Z and j ∈ [p].We obtain an automorphism of T without any fixed vertex or edge.

"If" Conversely, assume that α is an automorphism of T with no fixed vertex or edge. Let x = α(x) such that the distance between x and α(x) is minimal. Let e : x -y be an edge on the path from x to α(x) (we may have y = α(x)). Let f : α(x) -α(y).

Case 1 : (f,α(x)) is directed toward x. If y = α(x) and x = α(y), we have a fixed edge. If y = α(y), we have a fixed vertex. Otherwise, y and α(y) are at smaller distance than x and α(x). This case cannot happen.


Shannan Blystone
email: shannan.blystone@inrae.fr

Guilhem Pagès

Hervé H Cochard

Pierre Conchon

† G Pagès

Measuring tree water content with a portable, unilateral magnet

Keywords: portable MRI, low-field NMR, ¹H NMR, imaging, plants, trees

The use of MRI in the plant sciences has traditionally been limited due to the immobility of the devices, and restrictions with regard to sample size and shape. To overcome these limitations and to be able to study plants directly in their natural environment, we evaluated the capacities of a portable, unilateral magnet: The Nuclear Magnetic Resonance Mobile Universal Surface Explorer (NMR-MOUSE), designed by Blümich et al. [1]. This device permits measuring the water NMR signal in a 100-micrometer slice, and by means of a built-in lift, the magnet can be moved to record an NMR profile within a depth of approximately 25-millimeters from the surface of the device. We tested its capacity to measure tree water content by following the dehydration dynamic of thirty cut branches from six different species and two different functional types. We also tested the device on four in-situ trees. There was a linear correlation between the integral of the MRI profiles obtained and the water content of the branches and trees. This correlation was present regardless of tree species or functional type. Using the profiles obtained on the branches, we then tested the capacity of the device to differentiate the conductive tissues, i.e. the xylem and phloem fluxes. The MRI profiles of the branches presented distinct peaks which corresponded to the xylem and phloem tissues, whose location was validated with x-ray microtomography imaging. In conclusion, the NMR-MOUSE is a promising candidate for measuring tree water dynamics in the field.