Cette thèse aborde des sujets liés à la théorie des automates, à la logique et à la théorie des jeux. Ces thèmes sont au cœur de l'informatique théorique depuis de nombreuses décennies. Les travaux de recherche dans ces domaines sont motivés entre autres par des questions de modélisation et de vérification de systèmes. La première partie de la thèse considère les automates finis et la logique temporelle sur des ordres linéaires arbitraires. On y donne une procédure (doublement exponentielle en espace) pour décider la satisfaisabilité d'une formule LTL, utilisant une étape de transformation d'une formule logique en un transducteur synchrone. La seconde partie s'intéresse à des jeux de longueur ordinale. On propose un modèle de jeux à deux joueurs sur des graphes finis, et on montre que la question du vainqueur pour ces jeux peut être résolue en espace polynomial. De plus, on montre qu'il existe des stratégies gagnantes à mémoire finie.

L'espérance de vie a augmenté dans les dernières décennies et devrait continuer à croître dans les prochaines années. Cette augmentation entraîne de nouveaux défis concernant l'autonomie et l'indépendance des personnes âgées. Le développement d'habitats intelligents est une piste pour répondre à ces défis et permettre aux personnes de vivre plus longtemps dans un environnement sûr et confortable. Rendre un habitat intelligent consiste à y installer des capteurs, des actionneurs et un contrôleur afin de pouvoir prendre en compte le comportement de ses habitants et agir sur leur environnement, pour améliorer leur sécurité, leur santé et leur confort. La plupart de ces approches s'appuient sur la localisation en temps réel des habitants dans leur habitat. Dans cette thèse, une nouvelle approche complète permettant la localisation d'un nombre a priori inconnu d'habitants basée sur le modèle est proposée. Cette approche tire parti des paradigmes, de la théorie et des outils des Systèmes à Événements Discrets. L'utilisation des automates à états finis pour modéliser le mouvement détectable des habitants ainsi que des méthodes permettant de construire ces modèles ont été développées. A partir de ces modèles automates finis, plusieurs algorithmes permettant de localiser de manière efficace les habitants ont été définis. Enfin, plusieurs approches pour l'évaluation des performances de l'instrumentation d'un habitat intelligent pour un objectif de localisation ont été proposées. La méthode a également été totalement implémentée et mise à l'épreuve. Tout au long de cette thèse, les différentes contributions sont illustrées à l'aide de cas d'étude. / Life expectancy has continuously increased in most countries over the last decades and will probably continue to increase in the future. This leads to new challenges relative to the autonomy and the independence of elderly. The development of Smart Homes is a direction to face these challenges and to enable people to live longer in a safe and comfortable environment. Making a home smart consists in placing sensors, actuators and a controller in the house in order to take into account the behavior of their inhabitants and to act on their environment to improve their safety, health and comfort. Most of these approaches are based on the real-time indoor Location Tracking of the inhabitants. In this thesis, a whole new approach for model-based Location Tracking of an a priori unknown number of inhabitants is proposed. This approach is based on Discrete Event Systems paradigms, theory and tools. The usage of Finite Automata (FA) to model the detectable motion of the inhabitants as well as different methods to create such FA models have been developed. Based on these models, algorithms to perform efficient Location Tracking are defined. Finally, several approaches aiming at evaluating the relevance of the instrumentation of a Smart Home with the objective of Location Tracking are proposed. The approach has also been fully implemented and tested. Throughout the thesis, the different contributions are illustrated on case studies. / In den meisten Industrieländern ist die Lebenserwartung in den letzten Jahrzehnten fortlaufend gestiegen und wird höchstwahrscheinlich noch weiter steigen. Dieser Anstieg führt zu neuen Herausforderungen hinsichtlich der Autonomie und Unabhängigkeit von älteren Menschen. Die Entwicklung von intelligenten Wohnungen ist ein Weg diesen Herausforderungen zu begegnen und es den Menschen zu ermöglichen länger in einer sicheren und komfortablen Umgebung zu leben. Dazu stattet man solcheWohnungen mit Sensoren, Aktoren sowie einem Controller aus. Dies erm öglicht es, in Abhängigkeit vom Verhalten der Bewohner, dieWohnumgebung so zu beein_ussen, dass sich Sicherheit, Gesundheit und Komfort verbessern. Ansätze, die dies zum Ziel haben, basieren meistens auf Methoden, die es ermöglichen Menschen innerhalb ihrer Wohnung in Echtzeit zu lokalisieren. In dieser Dissertation wird daher ein neuer Ansatz für eine modellbasierte Lokalisierung einer a priori unbekannten Anzahl von Bewohnern vorgestellt. Dieser Ansatz fuÿt auf der Theorie, den Paradigmen und den Werkzeugen aus dem Gebiet der ereignisdiskreten Systeme. Es werden endliche Automaten eingesetzt, um die von den Sensoren erfassbaren Bewohnerbewegungen zu modellieren. Verschiedene Verfahren zur Erzeugung solcher Automaten werden gezeigt. Basierend auf diesen Modellen warden Algorithmen de_niert, mittels derer die Bewohner wirksam lokalisiert werden können. Abschlieÿend werden Methoden vorgeschlagen, die dazu dienen die Relevanz der Sensorinstrumentierung für die Lokalisierung zu bewerten. Die entwickelten Verfahren werden in der Dissertation durchgehend anhand von Fallbeispielen erläutert. Der gesamte Ansatz wurde implementiert und erprobt.

La fiabilité des logiciels est un facteur critique de notre société~: toute panne, tout bogue, tout dysfonctionnement, perturbe la bonne marche de nos activités avec parfois des conséquences humaines, financières ou morales importantes. Contrairement à d'autres domaines industriels plus anciens, la démarche qualité en informatique n'en est encore qu'à ses débuts. Il est couramment convenu comme normal qu'un ordinateur perde un fichier ou que l'installation d'un nouveau logiciel en rende un autre inutilisable. Cependant, dans des domaines précis (banque, systèmes embarqués, médecine, etc.), dits critiques, on ne peut se permettre d'avoir un système défaillant~: une phase importante du développement logiciel est celle de la validation durant laquelle le système est analysé afin de garantir qu'il respecte certaines exigences de fiabilité. Cette phase de validation fait appel à deux approches complémentaires, le test et la vérification. Les travaux présentés dans cette habilitation concernent majoritairement la verification par la technique dite de "model-checking". Une première partie montre des techniques originales pour la vérification de protocoles de sécurité. D'autres travaux, plus théoriques, portent sur l'accélération de relations de semi-commutation ainsi que sur la vérification de propriétés non fonctionnelles. Enfin, des résultats sur la génération aléatoire de structures complexes sont développés dans le contexte du test à partir de modèles et du test de performances.

Nous mettons en évidence un certain nombre de liens entre la théorie des nombres et celle des automates :<br>- étude de sous-suites de la suite "somme des chiffres", étude des itérées de cette suite ;<br>- utilisation de suites automatiques particulières (baptisées q-miroirs) dans le problème de l'itération des fonctions continues unimodales réelles ;<br>- étude d'un curieux ensemble de répartition modulo 1 de nombres réels ; <br>- propriétés arithmétiques d'un automate cellulaire ;<br>- répartition modulo 1 des puissances de séries formelles à coefficients automatiques (donc algébrique sur le corps des fractions rationnelles sur un corps fini).

Les expressions rationnelles et les automates finis sont des objets mathématiques permettant de représenter les langages rationnels. Le lien entre ces structures est le sujet de nombreux thèmes de recherche. Chacun de ces modèles présentent avantages et inconvénients. Nous nous proposons d'établir de nouveaux opérateurs, les multi-tildes-barres, permettant de créer un modèle d'expression se situant entre la structure d'automate et celle d'expression rationnelle simple, utilisant l'union, la concaténation, et l'étoile de Kleene. Les multi-tildes-barres sont basées sur des opérations relativement simples sur les langages, l'ajout et l'élimination du mot vide. Nous étendons les méthodes de conversion classiques entre expressions rationnelles simples et automates finis aux expressions utilisant ces nouveaux opérateurs. Nous montrons également que le pouvoir de factorisation de ces nouvelles expressions est exponentiellement plus grand que celui des expressions rationnelles simples.

Cette thèse a pour but d’étudier des propriétés structurelles d’automates étendant celle du déterminisme, et les langages pouvant être dénotés par une expression rationnelle dont l’automate des positions présente l’une de ces propriétés. Si Book et al. ont montré que tous les langages rationnels peuvent être reconnus par un automate des positions non-ambigu, Brüggemann-Klein et Wood ont montré que ceux pouvant l’être par un automate des positions déterministe forment une famille strictement incluse dans celle des rationnels. Nous nous intéressons aux extensions de cette famille, en cherchant à caractériser leurs langages, et à étudier leur hiérarchie interne et leur inclusion entre elles. / This thesis aims to study structural properties of automata extending determinism, and the languages that can be denoted by a regular expression of which the position automaton has one such property. If Book et al. showed that all regular languages can be recognized by an unambiguous position automaton, Brüggemann-Klein and Wood showed that only a proper subset of them can be recognized by a deterministic position automaton. We focus on extensions of this subfamily, by seeking to characterize their languages, and to study their internal hierarchy and how they relate to each other.

Cette thèse porte sur l'étude de la combinatoire énumérative, plus particulièrement autour des partitions d'entiers et des groupes de Coxeter. Dans une première partie, à l'instar de Han et de Nekrasov-Okounkov, nous étudions des développements combinatoires des puissances de la fonction êta de Dedekind, en termes de longueurs d'équerres de partitions d'entiers. Notre approche, bijective, utilise notamment les identités de Macdonald en types affines (en particulier le type C), généralisant l'approche de Han en type A. Nous étendons ensuite avec de nouveaux paramètres ces développements, grâce à de nouvelles propriétés de la décomposition de Littlewood vis-à-vis des partitions et statistiques considérées. Cela nous permet de déduire des formules des équerres symplectiques, ainsi qu'une connexion avec la théorie des représentations. Dans une seconde partie, nous étudions les éléments cycliquement pleinement commutatifs dans les groupes de Coxeter introduits par Boothby et al., qui forment une sous famille des éléments pleinement commutatifs. Nous commençons par développer une construction, la clôture cylindrique, donnant un cadre théorique qui est aux éléments CPC ce que les empilements de Viennot sont aux éléments PC. Nous donnons une caractérisation des éléments CPC en terme de clôtures cylindriques pour n'importe quel système de Coxeter. Celle-ci nous permet de déterminer en termes d'expressions réduites les éléments CPC dans tous les groupes de Coxeter finis ou affines, et d'en déduire dans tous ces groupes l'énumération de ces éléments. En utilisant la théorie des automates finis, nous montrons aussi que la série génératrice de ces éléments est une fraction rationnelle / This thesis focuses on enumerative combinatorics, particularly on integer partitions and Coxeter groups. In the first part, like Han and Nekrasov-Okounkov, we study the combinatorial expansion of power of the Dedekind's eta function, in terms of hook lengths of integer partitions. Our approach, bijective, use the Macdonald identities in affine types, generalizing the study of Han in the case of type A. We extend with new parameters the expansions that we obtained through new properties of the Littlewood decomposition. This enables us to deduce symplectic hook length formulas and a connexion with representation theory. In the second part, we study the cyclically fully commutative elements in Coxeter groups, introduced by Boothby et al., which are a sub family of the fully commutative elements. We start by introducing a new construction, the cylindrical closure, which give a theoretical framework for the CPC elements analogous to the Viennot's heaps for fully commutative elements. We give a characterization of CPC elements in terms of cylindrical closures in any Coxeter groups. This allows to deduce a characterization of these elements in terms of reduced decompositions in all finite and affine Coxeter and their enumerations in those groups. By using the theory of finite state automata, we show that the generating function of these elements is always rational, in all Coxeter groups

This thesis studies the properties of finite automata recognizing sets of real vectors encoded in positional notation using an integer base. We consider both general infinite-word automata, and the restricted class of weak deterministic automata, used, in particular, as symbolic data structures for representing the sets of vectors definable in the first order additive theory of real and integer numbers. <br><br> In previous work, it has been established that all sets definable in the additive theory of reals and integers can be handled by weak deterministic automata regardless of the chosen numeration base. In this thesis, we address the reciprocal property, proving that the sets of vectors that are simultaneously recognizable in all bases, by either weak deterministic or Muller automata, are those definable in the additive theory of reals and integers. <br><br> Precisely, for weak deterministic automata, we establish that the sets of real vectors simultaneously recognizable in two multiplicatively independent bases are necessarily definable in the additive theory of reals and integers. For general automata, we show that the multiplicative independence is not sufficient, and we prove that, in this context, the sets of real vectors that are recognizable in two bases that do not share the same set of prime factors are exactly those definable in the additive theory of reals and integers. <br><br> Those results lead to a precise characterization of the sets of real vectors that are recognizable in multiple bases, and provide a theoretical justification to the use of weak automata as symbolic representations of sets. <br><br> As additional contribution, we also obtain valuable insight into the internal structure of automata recognizing sets of vectors definable in the additive theory of reals and integers.

Le concept d’automate, central en théorie des langages, est l’outil d’appréhension naturel et efficace de nombreux problèmes concrets. L’usage intensif des automates finis dans un cadre algorithmique s ’illustre par de nombreux travaux de recherche. La correction et l’ évaluation sont les deux questions fondamentales de l’algorithmique. Une méthode classique d’ évaluation s’appuie sur la génération aléatoire contrôlée d’instances d’entrée. Les travaux d´écrits dans cette thèse s’inscrivent dans ce cadre et plus particulièrement dans le domaine de la génération aléatoire uniforme d’automates finis.L’exposé qui suit propose d’abord la construction d’un générateur aléatoire d’automates à pile déterministes, real time. Cette construction s’appuie sur la méthode symbolique. Des résultats théoriques et une étude expérimentale sont exposés.Un générateur aléatoire d’automates non-déterministes illustre ensuite la souplesse d’utilisation de la méthode de Monte-Carlo par Chaînes de Markov (MCMC) ainsi que la mise en œuvre de l’algorithme de Metropolis - Hastings pour l’ échantillonnage à isomorphisme près. Un résultat sur le temps de mélange est donné dans le cadre général .L’ échantillonnage par méthode MCMC pose le problème de l’évaluation du temps de mélange dans la chaîne. En s’inspirant de travaux antérieurs pour construire un générateur d’automates partiellement ordonnés, on montre comment différents outils statistiques permettent de s’attaquer à ce problème. / The concept of automata, central to language theory, is the natural and efficient tool to apprehendvarious practical problems.The intensive use of finite automata in an algorithmic framework is illustrated by numerous researchworks.The correctness and the evaluation of performance are the two fundamental issues of algorithmics.A classic method to evaluate an algorithm is based on the controlled random generation of inputs.The work described in this thesis lies within this context and more specifically in the field of theuniform random generation of finite automata.The following presentation first proposes to design a deterministic, real time, pushdown automatagenerator. This design builds on the symbolic method. Theoretical results and an experimental studyare given.This design builds on the symbolic method. Theoretical results and an experimental study are given.A random generator of non deterministic automata then illustrates the flexibility of the Markov ChainMonte Carlo methods (MCMC) as well as the implementation of the Metropolis-Hastings algorithm tosample up to isomorphism. A result about the mixing time in the general framework is given.The MCMC sampling methods raise the problem of the mixing time in the chain. By drawing on worksalready completed to design a random generator of partially ordered automata, this work shows howvarious statistical tools can form a basis to address this issue.