Les langages formels sont des séquences sur un ensemble discret de symboles appelé alphabet. On les spécifie souvent par des formules dans une certaine logique, par des expressions rationnelles ou bien par des automates discrets de types variés. La théorie actuelle est principalement qualitative, dans le sens où ses objets sont des séquence sur un temps discret, non-métrique, dans le sens où l'acceptation d'une séquence sur un automate dépend du fait que l'on visite ou non un état accepteur, et enfin dans le sens où la comparaison de langages est plus souvent considérée en termes d'inclusion, plutôt qu'en termes de mesures quantitatives. Cette thèse contribue à l'étude de ces aspects souvent négligés en présentant des résultats fondamentaux dans trois nouvelles classes de problèmes quantitatifs sur les langages formels. Dans la première partie, nous étudions une classe de problèmes d'ordonnancement qui combine les aspects structurels associés aux dépendances entre tâches avec les aspects dynamiques liés au fait qu'un flux de requêtes arrive en continu pendant l'exécution. Nous montrons que, dans cette classe de problèmes, certains flux, pourtant admissibles dans le sens que les requêtes ne représentent pas plus de travail que ce que les machines peuvent traiter, ne peuvent pas être ordonnancé avec une latence bornée. Cependant nous développons une politique d'ordonnancement que peut garantir une accumulation de retard bornée pour tout flux de requêtes admissible, même sans le connaître à l'avance. Nous montrons que si les flux sont sous-critiques, alors cette même politique peut garantir une latence bornée. En vérification quantitative, les états et transitions d'un système peuvent être associés à des coûts, et ceux-ci utilisés pour associer des coûts moyens aux comportements infinis. Dans cette seconde partie, nous proposons de définir des omega-langages par des requêtes booléennes sur les coûts moyens. Des spécifications concernant des moyennes, tels que " le taux de perte moyen de messages est inférieur à un certain seuil " ne sont pas omega-régulières, mais exprimables dans notre modèle. Ainsi, nous étudions l'expressivité et la complexité de Borel de telles spécifications. Nous montrons que pour la clôture par intersection, il est nécessaire de considérer des coûts multi-dimensionnels. Nous mettons en évidence que dans le cas général, les conditions d'acceptation portent sur l'ensemble des points d'accumulation de la séquence des coûts moyens des préfixes d'une exécution, et nous donnons une caractérisation précise de tels ensembles. Nous proposons une classe de langages de coût moyen à seuils multiples, comparant les coordonnées minimales et minimales des points de cet ensemble à des constantes. Nous montrons enfin que cette classe est close par opérations booléennes et analysable. Enfin, dans le dernier volet, nous définissons deux mesures pour un langage temporisé : le volume de ses sous-langages de mots à nombre d'événements fixe et l'entropie (vitesse de croissance), mesure asymptotique pour un nombre non borné d'événements. Ces mesures peuvent être utilisées pour la comparaison quantitative de langages, et l'entropie peut être vue comme la quantité d'information par événement dans un mot typique du langage temporisé. Pour les langages acceptés par des automates temporisés déterministes, nous donnons une formule exacte pour le volume. Ensuite, nous caractérisons l'entropie, en utilisant des méthodes d'analyse fonctionnelle, en tant que logarithme du rayon spectral d'un opérateur intégral positif. Nous établissons plusieurs méthodes pour calculer l'entropie : une symbolique pour les automates que nos appelons " à une horloge et demie ", et deux numériques : une utilisant les techniques d'analyse fonctionnelle, l'autre basée sur la discrétisation. Nous donnons une interprétation de l'entropie en théorie de l'information en termes de complexité de Kolmogorov.

Cette thèse s'inscrit dans l'étude des graphes infinis de présentation finie. Nous nous intéressons à la fois à leurs propriétés logiques et aux langages qui leur sont associés. Nous nous concentrons sur l'étude des graphes infinis associés aux automates à pile d'ordre supérieur. Notre première contribution est la définition d'une notion de rationalité pour les piles d'ordre supérieur. Nous montrons que cette notion partage de nombreuses propriétés de la rationalité sur les mots : clôture par complémentaire, accepteurs déterministes et complets, et caractérisation en logique du second ordre monadique. Nous établissons un lien étroit entre les automates à pile d'ordre supérieur et les ensembles rationnels de piles d'ordre supérieur. Notre seconde contribution est l'étude structurelle des graphes associés à ces automates. Nous en donnons différentes caractérisations qui montrent la robustesse de ces familles de graphes infinis.

Thèse de doctorat : Informatique : Paris 12 : 2005. Thèse de doctorat : Informatique : Oldenburg, Carl v. Ossietzky Universität : 2005. / Thèse soutenue en co-tutelle. Titre provenant de l'écran-titre. Bibliogr. p. 166173. Index.

Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <> nousentendons la prose que le mathématicien utilise tous les jours dansses articles et ses livres. C'est une langue naturelle avec desexpressions symboliques et des notations spécifiques. Cette langue està la fois flexible et structurée mais reste sémantiquementintelligible par tous les mathématiciens.Cependant, il est très difficile de formaliser automatiquement cettelangue. Les raisons principales sont: la complexité et l'ambiguïté deslangues naturelles en général, le mélange inhabituel entre languenaturelle et notations symboliques tout aussi ambiguë et les sautsdans le raisonnement qui sont pour l'instant bien au-delà descapacités des prouveurs de théorèmes automatiques ou interactifs.Pour contourner ce problème, les assistants de preuves actuelsutilisent des langages formels précis dans un système logique biendéterminé, imposant ainsi de fortes restrictions par rapport auxlangues naturelles. En général ces langages ressemblent à des langagesde programmation avec un nombre limité de constructions possibles etune absence d'ambiguïté.Ainsi, le monde des mathématiques est séparé en deux, la vastemajorité qui utilise la langue naturelle et un petit nombre utilisantaussi des méthodes formelles. Cette seconde communauté est elle-mêmesubdivisée en autant de groupes qu'il y a d'assistants de preuves. Onperd alors l'intelligibilité des preuves pour tous les mathématiciens.Pour résoudre ce problème, on peut se demander:est-il possible d'écrire un programme qui comprend la langue naturellemathématique et qui la traduit vers un langage formel afin depermettre sa validation?Ce problème se subdivise naturellement en deux sous-problèmes tous lesdeux très difficiles:1. l'analyse grammaticale des textes mathématiques et leur traductiondans un langage formel,2. la validation des preuves écrites dans ce langage formel.Le but du projet MathNat (Mathematics in controlled Natural languages)est de faire un premier pas pour répondre à cette question trèsdifficile, en se concentrant essentiellement sur la première question.Pour cela, nous développons CLM (Controlled Language for Mathematics)qui est un sous-ensemble de l'anglais avec une grammaire et un lexiquerestreint, mais qui inclut tout de même quelques ingrédientsimportants des langues naturelles comme les pronoms anaphoriques, lesréférences, la possibilité d'écrire la même chose de plusieursmanières, des adjectifs distributifs ou non, ...Le second composant de MathNath est MathAbs (Mathematical Abstractlanguage). C'est un langage formel, indépendant du choix d'un systèmelogique permettant de représenter la sémantique des textes enpréservant leur structure et le fil du raisonnement. MathAbs est conçucomme un langage intermédiaire entre CLM et un système logique formelpermettant la vérification des preuves.Nous proposons un système qui permet de traduire CLM vers MathAbsdonnant ainsi une sémantique précise à CLM. Nous considèrons que cetravail est déjà un progrès notable, même si pour l'instant on estloin de pouvoir vérifier formellement toutes les preuves en MathAbsainsi générées.Pour le second problème, nous avons réalisé une petite expérience entraduisant MathAbs vers une liste de formules en logique du premierordre dont la validité garantit la correction de la preuve. Nous avonsensuite essayé de vérifier ces formules avec des prouveurs dethéorèmes automatiques validant ainsi quelques exemples.

Nous étudions dans cette thèse la notion de quasipériodicité,introduite par Apostolico et Ehrenfeucht au début des années 1990,puis étendue aux mots infinis par Solomon Marcus au début des années2000. Un mot (fini ou infini) w est quasipériodique s'il peut êtrecouvert par des occurrences, éventuellement chevauchantes, d'un autremot, fini, appelé sa quasipériode. En 2006, Monteil etMarcus ont introduit la notion plus forte de quasipériodicitémulti-échelles : le fait d'avoir une infinité de quasipériodes.Dans un premier temps, nous étudions la quasipériodicité des motsinfinis bidimensionnels. Nous montrons que, contrairement au casunidimensionnel où la quasipériodicité ne force aucune propriété fortedes mots infinis, il existe des quasipériodes q qui forcent les mots2D q-quasipériodiques à être d'entropie nulle. Nous montrons égalementque la quasipériodicité multi-échelles en deux dimensions forcel'existence de fréquences uniformes pour les facteurs.Dans un deuxième temps, nous donnons des résultats sur les motsinfinis en une dimension. Nous donnons notament une approchepermettant de déterminer les quasipériodes d'un mot infini à partir deses facteurs carrés et de ses facteurs spéciaux. Nous montrons ensuiteque la famille des mots périodiques, ainsi que celle des mots standardsturmiens, peuvent être caractérisées en termes de quasipériodicitémulti-échelles. / We study the notion of quasiperiodicity, introduced by Apostolico and Ehrenfeucht at the beginning of the 1990's, then extended to infinite words by Solomon Marcus at the beginning of the 2000's. A (finite or infinite) word w is quasiperiodic if it can be covered by occurrences, possibly overlapping, of another finite word, call its quasiperiod. In 2006, Monteil and Marcus introduced a stronger notion: multi-scale quasiperiodicity, the property of having infinitely many quasiperiods.First we study quasiperiodicity of two-dimensional infinite words. We show that, by contrast with the one-dimensional case where quasiperiodicity do not force any property on infinite words, there exist quasiperiods q which force 2D q-quasiperiodic words to have zero entropy. We also show that multi-scale quasiperiodicity in two dimension force the existence of uniform frequencies for factors.Then we give results on infinite words in one dimension. Most notably we give a method to determine the quasiperiods of an infinite words from its square and special factors. We show that the family of periodic words and standard Sturmian words are characterizable in terms of multi-scale quasiperiodicity.

La vérification automatique de preuves consiste à faire vérifier par un ordinateur la validité de démonstrations d'énoncés mathématiques. Cette vérification étant purement calculatoire, elle offre un haut degré de confiance. Elle est donc particulièrement utile pour vérifier qu'un logiciel critique, c'est-à-dire dont le bon fonctionnement a un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens, correspond exactement à sa spécification. DEDUKTI est l'un de ces vérificateurs de preuves. Il implémente un système de type, le lambda-Pi-Calcul Modulo, qui est une extension du lambda-calcul avec types dépendants avec des règles de réécriture du premier ordre. Suivant la correspondance de Curry-Howard, DEDUKTI implémente à la fois un puissant langage de programmation et un système logique très expressif. Par ailleurs, ce langage est particulièrement bien adapté à l'encodage d'autres systèmes logiques. On peut, par exemple, importer dans DEDUKTI des théorèmes prouvés en utilisant d'autres outils tels que COQ, HOL ou encore ZENON, ouvrant ainsi la voie à l'interopérabilité entre tous ces systèmes. Le lambda-Pi-Calcul Modulo est un langage très expressif. En contrepartie, certaines propriétés fondamentales du système, telles que l'unicité des types ou la stabilité du typage par réduction, ne sont pas garanties dans le cas général et dépendent des règles de réécriture considérées. Or ces propriétés sont nécessaires pour garantir la cohérence des systèmes de preuve utilisés, mais aussi pour prouver la correction et la complétude des algorithmes de vérification de types implémentés par DEDUKTI. Malheureusement, ces propriétés sont indécidables. Dans cette thèse, nous avons donc cherché à concevoir des critères garantissant la stabilité du typage par réduction et l'unicité des types et qui soient décidables, de manière à pouvoir être implémentés par DEDUKTI. Pour cela, nous donnons une nouvelle définition du lambda-Pi-Calcul Modulo qui rend compte de l'aspect itératif de l'ajout des règles de réécriture dans le système en les explicitant dans le contexte. Une étude détaillée de ce nouveau calcul permet de comprendre qu'on peut ramener le problème de la stabilité du typage par réduction et de l'unicité des types à deux propriétés plus simples, qui sont la compatibilité du produit et le bon typage des règles de réécriture. Nous étudions donc ces deux propriétés séparément et en donnons des conditions suffisantes effectives. Ces idées ont été implémentées dans DEDUKTI, permettant d'augmenter grandement sa généralité et sa fiabilité. / Automatic proof checking is about using a computer to check the validity of proofs of mathematical statements. Since this verification is purely computational, it offers a high degree of confidence. Therefore, it is particularly useful for checking that a critical software, i.e., a software that when malfunctioning may result in death or serious injury to people, loss or severe damage to equipment or environmental harm, corresponds to its specification. DEDUKTI is such a proof checker. It implements a type system, the lambda-Pi-Calculus Modulo, that is an extension of the dependently-typed lambda-calculus with first-order rewrite rules. Through the Curry-Howard correspondence, DEDUKTI implements both a powerful programming language and an expressive logical system. Furthermore, this language is particularly well suited for encoding other proof systems. For instance, we can import in DEDUKTI theorems proved using other tools such as COQ, HOL or ZENON, a first step towards creating interoperability between these systems.The lambda-Pi-Calculus Modulo is a very expressive language. On the other hand, some fundamental properties such as subject reduction (i.e., the stability of typing by reduction) and uniqueness of types are not guaranteed in general and depend on the rewrite rules considered. Yet, these properties are necessary for guaranteeing the coherence of the proof system, but also for provingthe soundness and completeness of the type-checking algorithms implemented in DEDUKTI. Unfortunately, these properties are undecidable. In this thesis, we design new criteria for subject reduction and uniqueness of types that are decidable in order to be implemented in DEDUKTI.For this purpose, we give a new definition of the lambda-Pi-Calculus Modulo that takes into account the iterative aspect of the addition of rewrite rules in the typing context. A detailed study of this new system shows that the problems of subject reduction and uniqueness of types can be reduced to two simpler properties that we call product compatibility and well-typedness of rewrite rules.Hence, we study these two properties separately and give effective sufficient conditions for them to hold.These ideas have been implemented in DEDUKTI, increasing its generality and reliability.

Cette thèse adresse les problèmes d'universalité et de complétude computationelle pour plusieurs modèles de calcul inspirés par la biologie. Il s'agit principalement des systèmes d'insertion/effacement, réseaux de processeurs évolutionnaires, ainsi que des systèmes de réécriture de multi-ensembles. Les résultats décrits se classent dans deux catégories majeures : l'étude de la puissance de calcul des opérations d'insertion et d'effacement avec ou sans mécanismes de contrôle, et la construction des systèmes de réécriture de multi-ensembles universels de petite taille. Les opérations d'insertion et d'effacement consistent à rajouter ou supprimer une sous-chaîne dans une chaîne de caractères dans un contexte donné. La motivation pour l'étude de ces opérations vient de la biologie, ainsi que de la linguistique et de la théorie des langages formels. Dans la première partie de ce manuscrit nous examinons des systèmes d'insertion/effacement correspondant à l'édition de l'ARN, un processus qui insère ou supprime des fragments de ces molécules. Une particularité importante de l'édition de l'ARN est que le endroit auquel se font les modifications est déterminé par des séquences de nucléotides se trouvant toujours du même côté du site de modification. En termes d'insertion et d'effacement, ce phénomène se modéliserait par des règles possédant le contexte uniquement d'un seul côté. Nous montrons qu'avec un contexte gauche de deux caractères il est possible d'engendrer tous les langages rationnels. D'autre part, nous prouvons que des contextes plus longs n'augmentent pas la puissance de calcul du modèle. Nous examinons aussi les systèmes d’insertion/effacement utilisant des mécanismes de contrôle d’application des règles et nous montrons l'augmentation de la puissance d'expression. Les opérations d'insertion et d'effacement apparaissent naturellement dans le domaine de la sécurité informatique. Comme exemple on peut donner le modèle des grammaires gauchistes (leftist grammar), qui ont été introduites pour l'étude des systèmes critiques. Dans cette thèse nous proposons un nouvel instrument graphique d'analyse du comportement dynamique de ces grammaires. La deuxième partie du manuscrit s'intéresse au problème d'universalité qui consiste à trouver un élément concret capable de simuler le travail de n'importe quel autre dispositif de calcul. Nous commençons par le modèle de réseaux de processeurs évolutionnaires, qui abstrait le traitement de l'information génétique. Nous construisons des réseaux universels ayant un petit nombre de règles. Nous nous concentrons ensuite sur les systèmes de réécriture des multi-ensembles, un modèle qui peut être vu comme une abstraction des réactions biochimiques. Pour des raisons historiques, nous formulons nos résultats en termes de réseaux de Petri. Nous construisons des réseaux de Petri universels et décrivons des techniques de réduction du nombre de places, de transitions et d'arcs inhibiteurs, ainsi que du degré maximal des transitions. Une bonne partie de ces techniques repose sur une généralisation des machines à registres introduite dans cette thèse et qui permet d'effectuer plusieurs tests et opérations en un seul changement d'état / The present thesis considers the problems of computational completeness and universality for several biologically-inspired models of computation: insertion-deletion systems, networks of evolutionary processors, and multiset rewriting systems. The presented results fall into two major categories: study of expressive power of the operations of insertion and deletion with and without control, and construction of universal multiset rewriting systems of low descriptional complexity. Insertion and deletion operations consist in adding or removing a subword from a given string if this subword is surrounded by some given contexts. The motivation for studying these operations comes from biology, as well as from linguistics and the theory of formal languages. In the first part of the present work we focus on insertion-deletion systems closely related to RNA editing, which essentially consists in inserting or deleting fragments of RNA molecules. An important feature of RNA editing is the fact that the locus the operations are carried at is determined by certain sequences of nucleotides, which are always situated to the same side of the editing site. In terms of formal insertion and deletion, this phenomenon is modelled by rules which can only check their context on one side and not on the other. We show that allowing one-symbol insertion and deletion rules to check a two-symbol left context enables them to generate all regular languages. Moreover, we prove that allowing longer insertion and deletion contexts does not increase the computational power. We further consider insertion-deletion systems with additional control over rule applications and show that the computational completeness can be achieved by systems with very small rules. The motivation for studying insertion-deletion systems also comes from the domain of computer security, for the purposes of which a special kind of insertion-deletion systems called leftist grammars was introduced. In this work we propose a novel graphical instrument for visual analysis of the dynamics of such systems. The second part of the present thesis is concerned with the universality problem, which consists in finding a fixed element able to simulate the work any other computing device. We start by considering networks of evolutionary processors (NEPs), a computational model inspired by the way genetic information is processed in the living cell, and construct universal NEPs with very few rules. We then focus on multiset rewriting systems, which model the chemical processes running in the biological cell. For historical reasons, we formulate our results in terms of Petri nets. We construct a series of universal Petri nets and give several techniques for reducing the numbers of places, transitions, inhibitor arcs, and the maximal transition degree. Some of these techniques rely on a generalisation of conventional register machines, proposed in this thesis, which allows multiple register checks and operations to be performed in a single state transition

Dans cette thèse nous étudions le pouvoir d'expression de plusieurs logiques sur les arbres finis. En particulier, nous cherchons à obtenir une compréhension précise du pouvoir d'expression de la logique du premier ordre sur les arbres finis. Nous étudions un nombre important de logiques- pour cette raison nous procédons par comparaison avec une logique qui les contient et nous sert de référence: la logique monadique du second-ordre. Chaque logique que nous considérons est un fragment de la logique monadique du second ordre. MSO est liée à la théorie des langages formels. A chaque formule logique correspond un langage d'arbre: celui des arbres satisfaisant la formule. De plus, étant donné une logique nous pouvons lui associer une classe de langages d'arbres: la classe des langages définissables par une formule de cette logique. Dans le cadre des arbres finis, MSO correspond exactement à la classe des langages réguliers. Étant donné une logique, nous cherchons en fait à obtenir une caractérisation décidable de la classe de langages définissable par celle-ci. Par caractérisation décidable nous entendons un algorithme résolvant le problème suivant: pour un automate d'arbre finis, décider si le langage appartient à la classe en question. Nos caractérisations décidables sont en fait obtenue en exhibant pour chaque classe un ensemble de propriétés de clôture vérifiées par un langage si et seulement si celui-ci appartient à la classe en question. Nous montrons ensuite que chaque propriété de clôture est décidable. Énoncer et prouver de telles propriétés de clôture permet généralement d'obtenir une bonne compréhension du pouvoir de la logique correspondante. Le problème ouvert principal de ce domaine de recherche est l'obtention d'une caractérisation décidable pour la logique du premier ordre. Nous présentons des caractérisation décidables pour plusieurs fragment de FO. Nous commençons par la présentation de trois caractérisations décidable pour des classes de langages d'arbres de rang borné. La première classe que nous considérons est celle des langages définissables par la logique EF + F-1. Cette logique permet de naviguer dans l'arbre en se déplaçant soit vers un ancêtre, soit vers un descendant. La second classe est celle des arbres de rang borné définissables par la logique du premier ordre en n'utilisant qu'une seule alternance de quantificateurs. La dernière classe est celle des langages définissables par une combinaison booléenne de formules existentielles du premier ordre. Dans le cadre des forêts, nous étudions la classe des langages définissable par la logique du premier ordre à deux variables et deux prédicats correspondants respectivement à la relation ancêtre et la relation frère suivant. Nous présentons une caractérisation pour cette logique. La dernière classe pour laquelle nous présentons une caractérisation décidable est celle des langages localement testables (LT). UN langage est dans LT si l'appartenance d'un arbre à celui-ci ne dépends que des voisinages d'une certaine taille fixée dans l'arbre. / In this thesis we investigate the expressive power of several logics over finite trees. In particular we want to understand precisely the expressive power of first-order logic over finite trees. Because we study many logics, we proceed by comparison to a logic that subsumes them all and serves as a yardstick: monadic second-order logic. Each logic we consider is a fragment of monadic second-order logic. MSO is linked to the theory of formal languages. To each logical formula corresponds a tree language, which is the language of trees satisfying this formula. Furthermore, given a logic we can associate a class of tree languages: the class of languages definable by a formula of this logic. In the setting of finite trees MSO corresponds exactly to the class of regular tree languages. Given a logic, we actually look for a decidable characterization of the class of languages defined in this logic. By decidable characterization, we mean an algorithm for solving the following problem: given as input a finite tree automaton, decide if the recognized language belongs to the class in question. We will actually obtain our decidable characterizations by exhibiting for each class a set of closure properties such that a language is in the class under investigation if and only if it satisfies these closure properties. Each such closure property is then shown to be decidable. Stating and proving such closure properties usually yields a solid understanding of the expressive power of the corresponding logic. The main open problem in this research area is to obtain a decidable characterization for the class of tree languages that are definable in first-order logic. We provide decidable characterizations for several fragments of FO. First we provide three decidable characterizations for classes of regular languages of trees of bounded rank. The first class we consider is the class of languages definable in the temporal logic EF+F^-1. It essentially navigates the trees using two modalities for moving to a descendant node or an ancestor node. The second class we consider is the class of trees of bounded rank definable using one quantifier alternation. The last class, is the class of languages definable using a boolean combination of existential first order formulas. In the setting of forests, we investigate the class of languages definable in first-order logic using only two variables and two prediactes corresponding respectively to the ancestor and following sibling relations. We provide a characterization for this logic. The last class for which we provide a decidable characterization is the class of locally testable language (LT). A language L is in LT if membership in L depends only on the presence or absence of neighborhoods of a certain fixed size in the tree. We define notions of LT for both unranked trees and trees of bounded rank by adapting the definition of neighborhood to each setting. Then we provide a decidable characterization for both notions of LT.

L’analyse examina l’impact des relations tonales, des fonctions et des types formels transformés sur l’unité compositionnelle dans les œuvres orchestrales de Max Reger. Le contexte théorique est celui de nouvelles Formenlehre et Harmonielehre. La forme conçue comme une succession des fonctions fut analysée sur la base de la théorie des fonctions formelles de Caplin. Son apparatus analytique a été combiné avec le modèle sophistiqué de ponctuation et le concept de la déformation de la théorie de la sonate de Hepokoski et Darcy. En examinant les relations et la structure tonales, l’analyse adhère au concept de la monotonalité de Schoenberg. L’attention analytique fut focalisée sur les motifs harmoniques dérivés des accords, des progressions et de la ligne de basse. La Grundgestalt (une configuration fondamentale) fut perçue comme une structure motivique ou un contour intervallique quasi-arythmique. L’analyse montra comment Reger avait confirmé la clarté de l’unité tonale du mouvement ou de l’œuvre. / The analysis examined the impact of tonal relations and transformed formal types and functions on the compositional unity in Max Reger’s orchestral works. The theoretical background consisted of New Formenlehre and Harmonielehre. The form conceived as a succession of functions, was analyzed on the basis of Caplin’s formal function theory. His analytical apparatus was combined with the sophisticated punctuation model and the concept of “deformation” developed in the competing sonata theory of Hepokoski and Darcy. In consideration of tonal relationships and structure, the analysis adhered to Schoenberg’s concept of monotonality. The analytical attention was focused on harmonic motives derived from chords, progressions and the bass line. The Grundgestalt (basic configuration) was perceived as a motivic structure or quasi-arrhythmic interval contour. The analysis showed how Reger has confirmed the clarity of the tonal unity of a movement or work in whole.

La plupart des métriques de qualité logicielle mesurables sont actuellement basées sur des mesures bas niveau, telles que la complexité cyclomatique, le nombre de lignes de commentaires ou le nombre de blocs dupliqués. De même, la qualité de l'ingénierie logicielle est davantage liée à des facteurs techniques ou de gestion, et devrait fournir des indicateurs utiles pour les exigences de qualité. Actuellement, l'évaluation de ces exigences de qualité n'est pas automatisée, elle n'est pas validée empiriquement dans des contextes réels et l'évaluation est définie sans tenir compte des principes de la théorie de la mesure. Par conséquent, il est difficile de comprendre où et comment améliorer le logiciel suivant le résultat obtenu. Dans ce domaine, les principaux défis consistent à définir des métriques adéquates et utiles pour les exigences de qualité, les documents de conception de logiciels et autres artefacts logiciels, y compris les activités de test.Les principales problématiques scientifiques abordées dans cette thèse sont les suivantes: définir des mesures et des outils de support pour mesurer les activités d'ingénierie logicielle modernes en termes d'efficacité et de qualité. La seconde consiste à analyser les résultats de mesure pour identifier quoi et comment s'améliorer automatiquement. Le dernier consiste en l'automatisation du processus de mesure afin de réduire le temps de développement. Une telle solution hautement automatisée et facile à déployer constituera une solution révolutionnaire, car les outils actuels ne le prennent pas en charge, sauf pour une portée très limitée. / Most of the measurable software quality metrics are currently based on low level metrics, such as cyclomatic complexity, number of comment lines or number of duplicated blocks. Likewise, quality of software engineering is more related to technical or management factoid, and should provide useful metrics for quality requirements. Currently the assessment of these quality requirements is not automated, not empirically validated in real contexts, and the assessment is defined without considering principles of measurement theory. Therefore it is difficult to understand where and how to improve the software following the obtained result. In this domain, the main challenges are to define adequate and useful metrics for quality requirements, software design documents and other software artifacts, including testing activities.The main scientific problematic that are tackled in this proposed thesis are the following : defining metrics and its supporting tools for measuring modern software engineering activities with respect to efficiency and quality. The second consists in analyzing measurement results for identifying what and how to improve automatically. The last one consists in the measurement process automation in order to reduce the development time. Such highly automated and easy to deploy solution will be a breakthrough solution, as current tools do not support it except for very limited scope.