Modèles d'automates d'arbres étendus pour la vérification de systèmes infinis

This document presents the study of several models of state machines, all of them extending the same formalism: the classical tree automata, and their application in various reasoning tasks, such as static analysis of programs or systems, typing, verification of the consistency of specifications, model checking... Trees are a natural data structure, widespread in computer science, for instance for the representation of hierarchical or nested data structures, e.g. filesystems, for specific algorithms (binary search trees, distributed algorithms), for an abstract model for semi-structured data used for information exchange in the Web, for an algebraic presentation of recursive processes, as terms in logic... When it comes to reasoning on systems manipulating trees, or modeled by trees, it is crucial to have finite representation of infinite sets of trees. Tree automata are finite state machines providing such a representation, acknowledged as suitable for a use in reasoning tasks: they are a well established theoretical model, in close relationship with logic, they enjoy good compositional properties and efficient decision algorithms. In particular, tree automata are used at the core of systems for software and hardware verification and theorem proving. However, tree automata have also some severe limitations in expressiveness. For instance, they are unable of non-linear pattern matching or of expressing integrity constraints such as keys. Some extensions have been proposed in order to improve the model while trying to preserve good properties. We present in this document several such extensions, their properties and the advents of their use in symbolic verification of systems and programs.Ce document présente l'étude de plusieurs modèles de machines à états finis qui étendent tous le même formalisme: les automates d'arbres classiques, et leur application dans différentes tâches telles que l'analyse statique de programmes ou de systèmes, la typage, la vérification de la cohérence de spécifications, le model checking... Les arbres sont une structure naturelle de données, très répandue en informatique, par exemple pour la représentation des structures de données hiérarchiques ou imbriquées, pour des algorithmes spécifiques (arbres binaires de recherche, algorithmes distribués), comme modèle abstrait pour des données semi-structurées utilisées pour l'échange d'information dans le Web, pour une présentation algébrique de processus récursifs, comme les termes en logique... Lorsqu'il s'agit de raisonner sur des systèmes manipulant des arbres, ou modelisés par des arbres, il est crucial d'avoir une représentation finie d'ensembles infinis d'arbres. Les automates d'arbres sont des machines à états finis permettant une telle représentation. Ils ont fait la preuve de leur adéquation à des tâches de raisonnement: ils ont un modèle théorique bien établi, en étroite relation avec la logique, ils bénéficient de bonnes propriétés de composition et d'algorithmes de décision efficaces. En particulier, les automates d'arbres sont utilisées au coeur de systèmes de vérification formelle d'outils de déduction automatique. Toutefois, les automates d'arbres ont des limitations sévères en expressivité. Par exemple, ils sont incapables de faire du filtrage non-linéaire ou d'exprimer des contraintes d'intégrité tels que les clés dans les bases de données. Certaines extensions ont été proposées afin d'améliorer le modèle en essayant de conserver de bonnes propriétés. Nous présentons dans ce document de plusieurs de telles extensions, leurs propriétés et leur utilisation en vérification symbolique de systèmes et de programmes