L’analyse d’accessibilité est une des composantes de l’analyse de modèles. Elle consiste à modéliser un système complexe par trois ensembles : le langage initial, le langage des configurations indésirables et un système de réécriture. Le langage initial et le langage des configurations indésirables sont des ensembles de termes. Un terme est un mot mais construit à partir de symboles d’arités supérieures à 1. Le système de réécriture représente la dynamique du système complexe. C’est un ensemble de règles qui permettent d’obtenir un nouveau terme à partir d’un terme original. Pour effectuer une analyse d’accessibilité à partir de cette modélisation, on peut calculer l’ensemble des configurations accessibles. Cet ensemble aussi appelé ensemble des descendants est obtenu en appliquant le système de réécriture sur le langage initial jusqu’à ne plus obtenir de nouveaux termes. Une fois l’ensemble des descendants calculé, il reste à faire l’intersection entre celui-ci et l’ensemble des configurations indésirables. Si cette intersection est vide, alors il n’y a pas de configuration indésirable accessible, sinon les configurations présentes dans cette intersection sont accessibles. Cependant, l’ensemble des descendants n’est pas calculable dans le cas général. Pour contourner ce problème, nous calculons une sur-approximation des descendants. Ainsi, si l’intersection est vide, cela signifie toujours qu’aucune configuration indésirable n’est accessible. A contrario, s’il existe un terme dans l’intersection, il n’est pas possible de déterminer s’il s’agit d’un faux positif ou d’une configuration indésirable accessible. La précision de la sur-approximation est alors déterminante. / Reachability analysis is part of model checking. It consists to model complex systems by three sets : initial language, unwanted configurations and rewrite system. The initial language and the unwanted configurations language are sets of terms. Terms are words which are construct with symbols that have an arity that can be greater than 1. The rewrite system represent the dynamic of the complex system. It is a set of rules that permit from a initial term to obtain a new term. One of the approaches to analyze reachability from this modelling is to compute the set of reachable configurations. This set which is called set of descendants is obtained by applying the rewrite system on the initial language until obtaining no more new terms. After the set of descendants is computed, we need to compute the intersection between this set and the unwanted configurations set. If this intersection is empty then there is no unwanted configuration reachable, else the configurations in this intersection are reachable. However, the set of descendants is not computable in the general case. To bypass this problem, we compute an over-approximation of descendants.Now, if the intersection is empty, we keep proving that no unwanted configuration is reachable. Nevertheless, if the intersection is not empty, it is not possible to know if it comes from false-positives or form unwanted reachable configurations. So, the precision of the over-approximation is decisive.

This thesis is concerned with theoretical as well as practical aspects of tree languages. It consists of an introduction and eight papers, organised into three parts. The first part is devoted to algorithmic learning of regular tree languages, the second part to bisimulation minimisation of tree automata, and the third part to tree-based generation of music. We now summarise the contributions made in each part. In Part I, an inference algorithm for regular tree languages is presented. The algorithm is a generalisation of a previous algorithm by Angluin, and the learning task is to derive, with the aid of a so-called MAT-oracle, the minimal (partial and deterministic) finite tree automaton M that recognises the target language U over some ranked alphabet Σ. The algorithm executes in time O(|Q| |δ| (m + |Q|)), where Q and δ are the set of states and the transition table of M , respectively, r is the maximal rank of any symbol in Σ, and m is the maximum size of any answer given by the oracle. This improves on a similar algorithm by Sakakibara as dead states are avoided both in the learning phase and in the resulting automaton. Part I also describes a concrete implementation which includes two extensions of the basic algorithm. In Part II, bisimulation minimisation of nondeterministic weighted tree automata (henceforth, wta) is introduced in general, and for finite tree automata (which can be seen as wta over the Boolean semiring) in particular. The concepts of backward and forward bisimulation are extended to wta, and efficient minimisation algorithms are developed for both types of bisimulation. In the special case where the underlying semiring of the input automaton is either cancellative or Boolean, these minimisation algorithms can be further optimised by adapting existing partition refinement algorithms by Hopcroft, Paige, and Tarjan. The implemented minimisation algorithms are demonstrated on a typical task in natural language processing. In Part III, we consider how tree-based generation can be applied to algorithmic composition. An algebra is presented whose operations act on musical pieces, and a system capable of generating simple musical pieces is implemented in the software Treebag: starting from input which is either generated by a regular tree grammar or provided by the user via a digital keyboard, a number of top-down tree transducers are applied to generate a tree over the operations provided by the music algebra. The evaluation of this tree yields the musical piece generated.

In this thesis, we investigate different theoretical questions concerning weighted automata models over tree-like input structures. First, we study exact and approximated determinisation and then, we turn to Kleene-like and Büchi-like characterisations. We consider multiple weighted automata models, including weighted tree automata over semirings (Chapters 3 and 4), weighted forest automata over M-monoids (Chapter 5), and rational weighted tree languages with storage (Chapter 6). For an explanation as to why the last class can be considered as a weighted automaton model, we refer to page 188 of the thesis. We will now summarise the main contributions of the thesis. In Chapter 3, we focus on the determinisation of weighted tree automata and present our determinisation framework, called M-sequentialisation, which can model different notions of determinisation from the existing literature. Then, we provide a positive M-sequentialisation result for the case of additively idempotent semirings or finitely M-ambiguous weighted tree automata. Another important contribution of Chapter 3 is Theorem 77, where we provide a blueprint theorem that can be used to find determini- sation results for more classes of semirings and weighted tree automata easily. In fact, instead of repeating an entire determinisation construction, Theorem 77 allows us to prove a determinisation result by finding certain finite equivalence relations. This is a very potent tool for future research in the area of determinisation. In Chapter 4, we move from exact determinisation towards approximate determini- sation. We lift the formalisms and the main results from one approach from the literature from the word case to the tree case. This successfully results in an approximated determinisation construction for weighted tree automata over the tropical semiring. We provide a formal mathematical description of the approximated determinisation construction, rather than an algorithmic description as found in the related approach from the literature. In Chapter 5, we turn away from determinisation and instead consider Kleene-like and Büchi-like characterisations of weighted recognisability. We introduce weighted forest automata over M-monoids, which are a generalisation of weighted tree automata over M-monoids and weighted forest automata over semirings. Then, we prove that our recognisable weighted forest languages can be decomposed into a finite product of recognisable weighted tree languages. We also prove that the initial algebra semantic and the run semantic for weighted forest automata are equivalent under certain conditions. Lastly, we define rational forest expressions and forest M-expressions and and prove that the classes of languages generated by these formalisms coincide with recognisable weighted forest languages under certain conditions. In Chapter 6, we consider rational weighted tree languages with storage, where the storage is introduced by composing rational weighted tree languages without storage with a storage map. It has been proven in the literature that rational weighted tree languages with storage are closed under the rational operations. In Chapter 6, we provide alternative proofs of these closure properties. In fact, we prove that our way of introducing storage to rational weighted tree languages preserves the closure properties from rational weighted tree languages without storage.:1 Introduction 2 Preliminaries 2.1 Languages 2.2 WeightedLanguages 2.3 Weighted Tree Automata 3 A Unifying Framework for the Determinisation of Weighted Tree Automata 3.1 Introduction 3.2 Preliminaries 3.3 Factorisation in Monoids 3.3.1 Ordering Multisets over Monoids 3.3.2 Cayley Graph and Cayley Distance 3.3.3 Divisors and Rests 3.3.4 Factorisation Properties 3.4 Weighted Tree Automata over M_fin(M) and the Twinning Property 3.4.1 Weighted Tree Automata over M_fin(M) 3.4.2 The Twinning Property 3.5 Sequentialisation of Weighted Tree Automata over M_fin(M) 3.5.1 The Sequentialisation Construction 3.5.2 The Finitely R-Ambiguous Case 3.6 Relating WTA over M_fin(M) and WTA over S 3.7 M-Sequentialisation of Weighted Tree Automata 3.7.1 Accumulation of D_B 3.7.2 M-Sequentialisation Results 3.8 Comparison of our Results to the Literature 3.8.1 Determinisation of Unweighted Tree Automata 3.8.2 The Free Monoid Case 3.8.3 The Group Case 3.8.4 The Extremal Case 3.9 Conclusion 4 Approximated Determinisation of Weighted Tree Automata 125 4.1 Introduction 4.2 Preliminaries 4.3 Approximated Determinisation 4.3.1 The Approximated Determinisation Construction 4.3.2 Correctness of the Construction 4.4 The Approximated Twinning Property 4.4.1 Implications for Approximated Determinisability 4.4.2 Decidability of the Twinning Property 4.5 Conclusion 5 Kleene and Büchi Theorems for Weighted Forest Languages over M-Monoids 5.1 Introduction 5.2 Preliminaries 5.3 WeightedForestAutomata 5.3.1 Forests 5.3.2 WeightedForestAutomata 5.3.3 Rectangularity 5.3.4 I-recognisable is R-recognisable 5.4 Kleene’s Theorem 5.4.1 Kleene’s Theorem for Trees 5.4.2 Kleene’s Theorem for Forests 5.4.3 An Inductive Approach 5.5 Büchi’s Theorem 5.5.1 Büchi’s Theorem for Trees 5.5.2 Büchi’s Theorem for Forests 5.6 Conclusion 6 Rational Weighted Tree Languages with Storage 6.1 Introduction 6.2 Preliminaries 6.3 Rational Weighted Tree Languages with Storage 6.4 The Kleene-Goldstine Theorem 6.5 Closure of Rat(S¢,Σ,S) under Rational Operations 6.5.1 Top-Concatenation, Scalar Multiplication, and Sum 6.5.2 α-Concatenation 6.5.3 α-Kleene Star 6.6 Conclusion 7 Outlook References

Diese Arbeit untersucht ordnungsinvariante Formeln der Logik erster Stufe (FO) und einiger ihrer Erweiterungen, sowie andere eng verwandte Konzepte der endlichen Modelltheorie. Viele Resultate der endlichen Modelltheorie nehmen an, dass Strukturen mit einer Einbettung ihres Universums in ein Anfangsstück der natürlichen Zahlen ausgestattet sind. Dies erlaubt es, beliebige Relationen (z.B. die lineare Ordnung) und Operationen (z.B. Addition, Multiplikation) von den natürlichen Zahlen auf solche Strukturen zu übertragen. Die resultierenden Relationen auf den endlichen Strukturen werden als numerische Prädikate bezeichnet. Werden numerische Prädikate in Formeln verwendet, beschränkt man sich dabei häufig auf solche Formeln, deren Wahrheitswert auf endlichen Strukturen invariant unter Änderungen der Einbettung der Strukturen ist. Wenn das einzige verwendete numerische Prädikat eine lineare Ordnung ist, spricht man beispielsweise von ordnungsinvarianten Formeln. Die Resultate dieser Arbeit können in drei Teile unterteilt werden. Der erste Teil betrachtet die Lokalitätseigenschaften von FO-Formeln mit Modulo-Zählquantoren, die beliebige numerische Prädikate invariant nutzen. Der zweite Teil betrachtet FO-Sätze, die eine lineare Ordnung samt der zugehörigen Addition auf invariante Weise nutzen, auf endlichen Bäumen. Es wird gezeigt, dass diese dieselben regulären Baumsprachen definieren, wie FO-Sätze ohne numerische Prädikate mit bestimmten Kardinalitätsprädikaten. Für den Beweis wird eine algebraische Charakterisierung der in dieser Logik definierbaren Baumsprachen durch Operationen auf Bäumen entwickelt. Der dritte Teil der Arbeit beschäftigt sich mit der Ausdrucksstärke und der Prägnanz von FO und Erweiterungen von FO auf Klassen von Strukturen beschränkter Baumtiefe. / This thesis studies the concept of order-invariance of formulae of first-order logic (FO) and some of its extensions as well as other closely related concepts from finite model theory. Many results in finite model theory assume that structures are equipped with an embedding of their universe into an initial segment of the natural numbers. This allows to transfer arbitrary relations (e.g. linear order) and operations (e.g. addition, multiplication) on the natural numbers to structures. The arising relations on the structures are called numerical predicates. If formulae use these numerical predicates, it is often desirable to consider only such formulae whose truth value in finite structures is invariant under changes to the embeddings of the structures. If the numerical predicates include only a linear order, such formulae are called order-invariant. We study the effect of the invariant use of different kinds of numerical predicates on the expressive power of FO and extensions thereof. The results of this thesis can be divided into three parts. The first part considers the locality and non-locality properties of formulae of FO with modulo-counting quantifiers which may use arbitrary numerical predicates in an invariant way. The second part considers sentences of FO which may use a linear order and the corresponding addition in an invariant way and obtains a characterisation of the regular finite tree languages which can be defined by such sentences: these are the same tree languages which are definable by FO-sentences without numerical predicates with certain cardinality predicates. For the proof, we obtain a characterisation of the tree languages definable in this logic in terms of algebraic operations on trees. The third part compares the expressive power and the succinctness of different ex- tensions of FO on structures of bounded tree-depth.