Presburger arithmetic is the first-order theory of the integers with addition and ordering, but without multiplication. This theory is decidable and the sets it defines admit several different representations, including formulas, generators, and finite automata, the latter being the focus of this thesis. Finite-automata representations of Presburger sets work by encoding numbers as words and sets by automata-defined languages. With this representation, set operations are easily computable as automata operations, and minimized deterministic automata are a canonical representation of Presburger sets. However, automata-based representations are somewhat opaque and do not allow all operations to be performed efficiently. An ideal situation would be to be able to move easily between formula-based and automata-based representations but, while building an automaton from a formula is a well understood process, moving the other way is a much more difcult problem that has only attracted attention fairly recently. The main results of this thesis are new algorithms for extracting information about Presburger-definable sets represented by finite automata. More precisely, we present algorithms that take as input a finite-automaton representing a Presburger definable set S and compute in polynomial time the affine hull over Q or over Z of the set S, i.e., the smallest set defined by a conjunction of linear equations (and congruence relations in Z) which includes S. Also, we present an algorithm that takes as input a deterministic finite-automaton representing the integer elements of a polyhedron P and computes a quantifier-free formula corresponding to this set. The algorithms rely on a very detailed analysis of the scheme used for encoding integer vectors and this analysis sheds light on some structural properties of finite-automata representing Presburger definable sets. The algorithms presented have been implemented and the results are encouraging : automata with more than 100000 states are handled in seconds.

Le travail présenté dans ce mémoire propose une méthodologie de synthèse de la commande pour des systèmes hybrides, qui permet de calculer l'ensemble de toutes les lois de commande telles que le fonctionnement du système respecte les spécifications imposées par le cahier des charges. Notre approche consiste à représenter la dynamique continue par un système linéaire discrétisé et la dynamique événementielle par un automate à états finis. L'ensemble donne un automate hybride sur lequel les techniques d'analyse d'atteignabilité sont appliquées. Ces techniques permettent d'obtenir l'automate atteignable, qui ne contient que les trajectoires possibles du système pour une condition initiale donnée. En quelque sorte, nous avons ici une généralisation de la méthode clock translation. L'utilisation du temps discrétisé permet d'obtenir un automate à états finis modélisant le système hybride. Ce modèle est obtenu par le dépliage temporel de la dynamique continue du système dans chaque sommet de l'automate hybride. La technique est similaire avec celle proposée par Brandin et Wonham pour les systèmes temporisés. Par ce modèle les trajectoires du système hybride seront explicitement représentées. L'approche de synthèse de la commande présentée dans ce mémoire est basée sur une extension de la théorie classique de la commande supervisée. Le modèle de commande synthétisé est représenté par un automate temporisé. Celui-ci indique les dates d'occurrence auxquelles les événements contrôlables intervenant dans le fonctionnement du système doivent être exécutés. On notera que l'on s'affranchit ici de l'aspect hybride du système. Les résultats de la synthèse sont optimaux. Les résultats de recherche de ce travail peuvent s'appliquer aussi bien au pilotage des systèmes de production qu'au contrôle des flux dans un procédé batch.

Les travaux de recherche présentés dans cette thèse proposent une méthodologie de synthèse de la commande des systèmes à événements discrets temporisés permettant de calculer l'ensemble de toutes les lois de commande telles que le fonctionnement du système respecte les spécifications imposées par le cahier des charges. Notre approche associe la capacité de modélisation de l'outil réseau de Petri T-temporel à la puissance d'analyse des automates temporisés. Dans un premier temps, le système à commander est modélisé par un réseau de Petri T-temporel. Ensuite on construit l'automate temporisé qui modélise le comportement de ce réseau de Petri T-temporel. Les comportements non-désirés sont modélisés par des sommets interdits. La synthèse de la commande est basée sur des techniques d'analyse d'atteignabilité spécifiques aux automates temporisés. La méthode proposée consiste à calculer des nouvelles gardes des transitions de l'automate telles que les sommets interdits ne soient jamais atteints. L'approche de synthèse de la commande présenté dans cette thèse s'adresse aux systèmes à événements discrets temporisés modélisés par des réseaux de Petri T-temporels bornés avec des contraintes temporelles spécifiées par des nombres rationnels.

Le but de la thèse est de développer une nouvelle approche de surveillance des systèmes à événements discrets. La méthode proposée est basée sur la surveillance du temps de service en utilisant l'automate temporisé comme outil de modélisation.<br />Partant d'un système commandé, le premier objectif est la surveillance des différentes activités de ce système afin d'améliorer sa disponibilité. Ceci se traduit par la minimisation du nombre d'arrêts qui pénalisent la production, en suivant en temps réel, l'état de fonctionnement des différents capteurs du système. Ainsi pour chaque tâche, la surveillance du temps écoulé entre deux événements (l'instant où la commande a donné l'ordre de démarrer une tâche et l'instant où le capteur indique la fin d'exécution de la tâche) permet de détecter au plutôt d'éventuelles défaillances. La deuxième phase correspond au diagnostic qui consiste en la détermination des causes du problème observé.<br />Jusqu'à présent les approches de surveillance utilisent un modèle de référence basé sur la connaissance à priori de toutes les situations interdites du système. Le modèle de surveillance proposé présente un réel avantage. En effet, la détection d'éventuelles défaillances ne nécessite pas une liste exhaustive de toutes les défaillances possibles du système. En fonction de la catégorie du système de production et de la nature des tâches à surveiller nous introduisons une tolérance sur la durée de la tâche à surveiller. Ainsi, la notion de fonctionnement en ‘ mode dégradé' est introduite. Au-delà de cette tolérance, le système sera effectivement dans un état de ‘défaillance'. Différents exemples illustrent la démarche proposée. Ils permettent de montrer la puissance d'une telle approche. De plus, un algorithme permettant le calcul du seuil optimal de tolérance est proposé, ainsi que l'évaluation des performances du système de surveillance.

Les jeux à deux joueurs sur des graphes finis ou infinis permettent de modéliser de nombreux problèmes liés à la vérification des systèmes. Le système spécifié dépend de la nature du graphe de jeu considéré tandis que la propriété à vérifier est décrite par la condition de gain. Le premier joueur, Eve, représente un programme qui évolue dans un environnement hostile représenté par le second joueur, Adam. Dans ce formalisme, Eve possède une stratégie gagnante si et seulement si le programme peut être contrôlé de sorte à satisfaire la propriété spécifiée par la condition de gain. On souhaite alors décider si Eve possède une stratégie gagnante et si oui la déterminer, afin de synthétiser ensuite un contrôleur. <br /><br />Dans cette thèse, les graphes de jeu considérés sont des graphes de processus à pile qui offrent une représentation finie simple de systèmes infinis relativement complexes. Sur de tels graphes, on peut considérer des conditions de gain classiques (accessibilité, Büchi ou parité) mais aussi des conditions plus spécifiques au modèle comme celles portant sur le bornage de la pile. On peut également combiner ces dernières entre elles. <br /><br />Une première contribution a été de fournir une représentation des ensembles de positions gagnantes pour les jeux de parité ainsi qu'une nouvelle présentation des résultats connus pour ces derniers. On a alors pu étendre de façon naturelle les techniques de preuves à d'autres conditions de gain, notamment à celles portant sur le bornage de la pile. <br /><br />Une autre contribution a été la description d'une famille de conditions de gain de complexité borélienne arbitraire finie pour lesquelles les jeux (sur des graphes finis ou sur des graphes de processus à pile) restent décidables. <br /><br />L'étude des jeux sur les graphes de BPA et sur les graphes de processus à compteur a permis de proposer des techniques propres à ces modèles qui fournissent alors des bornes de complexité meilleures que celles obtenues dans le cas général des graphes de processus à pile. <br /><br />Enfin, une dernière contribution a été de proposer une solution pour les jeux sur des graphes de processus à pile munis de conditions combinant des conditions régulières et des conditions sur la hauteur de pile et pour des conditions décrites par des automates à pile avec visibilité.

De nombreux sytèmes critiques comportent des aspects temporisés, où interviennent de manière cruciale des contraintes quantitatives sur les délais séparant certaines actions. Un automate programmable industriel (API) constitue un composant fondamental d'un système souvent critique destiné à réagir et à communiquer en temps réel avec son environnement. Ma thèse se situe dans le contexte de la vérification de propriétés temporisées des APIS. Plus précisement, on propose une sémantique formelle à base d'automates temporisés pour la modélisation d'une sous classe de programmes Ladder comportant des blocs TON. On fournie une logique temporisée dont la sémantique permet de considérer seulement les événements "signifcatifs" (c'est à dire les événements qui durent suffisamment longtemps). On propose deux sémantiques différentes pour cette logique: sémantique "locale" et sémantique "globale". Pour la sémantique "locale", on a obtenu plusieurs résultats d'expressivité et grâce à une nouvelle relation d'équivalence, on montre que son model checking reste décidable sans modifier la complexité théorique. En revanche, pour la sémantique "globale", le model checking devient indécidable.

Les travaux de cette thèse s'inscrivent dans la théorie des automates et des langages formels. ils peuvent se diviser en deux parties qui donnent également deux visions différentes de manipuler les langages dans la théorie des automates. La première partie s'intéresse à la notion de dérivation des expressions qui permet de faire passer le formalisme des quotients de langages au niveau des expressions rationnelles. en particulier cette thèse étudie les termes dérivés cassés d'une expression rationnelle. ces termes dérivés cassés permettent, sous certaines circonstances, et à l'aide d'autres opérations, une réversibilité de la transformation d'un automate en une expression rationnelle. Dans la seconde partie, la théorie des automates est utilisée pour traiter des problèmes sur les systèmes de numération. les systèmes de numération représentent des nombres par des mots. il est possible d'utiliser des automates et des transducteurs afin d'être capable de 'compter' sur un langage rationnel représentant les entiers. plus précisément ces automates sont étudiés pour le cas des systèmes de numération abstraits qui associent à chaque entier un mot d'un langage rationnel, ordonné par l'ordre radiciel. dans un tel système, la fonction qui permet de calculer le mot suivant est une fonction co-séquentielle par morceaux, c'est-à-dire qu'il suffit de lire deux fois le mot d'entrée de la droite vers la gauche pour qu'une machine calcule son image.

La modélisation dans le domaine de l'agro-écologie est importante car elle permet de mieux comprendre les interactions entre l'environnement et les activités humaines. Des travaux basés sur la simulation ont été développés depuis des années. Cependant, non seulement ces outils restent difficiles à utiliser par les utilisateurs non experts, mais aussi le coût des modèles rend leur utilisation difficile à case de la complexité élevée en cas d'application réelle. Nous proposons une approche qui consiste à représenter le système étudié dans un formalisme de système à événements discrets qui est bien adapté quand la dynamique du système est liée à des interactions entre les entités concernés. Ceci permet de profiter l'efficacité du model-checking pour étudier le comportement du système modélisé et d'utiliser la synthèse de contrôleur pour générer automatiquement des stratégies optimales. Nous présentons deux contributions dans cette thèse. La première contribution concerne le projet EcoMata. Cette modélisation qualitative en automates temporisés pour un réseau trophique marin de type proie-prédateur permet d'analyser l'écosystème à l'aide de model-checking sans avoir à faire des simulations. Des scénarios de requête prédéfinis ont été développés dans un langage naturel pour que les utilisateurs non expert puissent faire des requêtes sur les réseaux trophiques sans avoir des connaissances sur la langage TCTL. Nous avons amélioré la génération automatique d'automates temporisés à partir d'une description des équation Lotka-Votera. Nous avons aussi proposé une approche de synthèse de contrôleur pour générer automatiquement des stratégies optimales de gestion de pêche. Le prototype logiciel EcoMata implémente l'ensemble des propositions incluant la recherche de stratégies optimales. Dans la seconde contribution, nous proposons une modélisation hybride en automates temporisés d'une exploitation de pâturage. Cette modélisation hybride combine un modèle numérique de la croissance d'herbe et un modèle qualitatif des activités de pâturage. Une structure hiérarchique organise les modèles dans quatre couches: la couche biologique, la couche activité, la couche décisionnelle et la couche d'horloge. Nous proposons quatre méthodes pour générer des stratégies optimales des activités de pâturage. La première méthode est appliquée à la recherche de stratégies optimales de la mise au pâturage. Trois méthodes sont dédiées à la recherche de stratégies optimales de la fertilisation. Une d'entre elles utilise la synthèse de contrôleur alors que les deux autres combinent la synthèse de contrôleur et l'apprentissage supervisé pour générer des stratégies génériques par type d'exploitation. Un prototype logiciel PaturMata a été développé implémentant cette modélisation, permettant aux utilisateurs de simuler des scénarios de pâturage et rechercher des stratégies optimales de mise au pâturage.

Les avancées des dernières décennies dans le domaine de l'électronique ont permis l'intégration plus facile des dispositifs de commande à base de convertisseur sur un plus grand nombre d'applications. L'utilisation de ces dispositifs de commande offre des avantages importants au niveau du dimensionnement et de l'efficacité énergétique, mais, en contrepartie, leur modèle dynamique présente une complexité accrue en particulier à cause des dynamiques hétérogènes des différents composants. Ainsi, en général, on retrouve une dynamique très rapide liée au changement de fonctionnement des composants et une dynamique du reste du système plus lente par rapport à la première.<br />Les travaux de cette thèse abordent les problèmes de la modélisation hybride de ce type de systèmes. Un des points importants des travaux effectués est la mise en place d'en ensemble d'outils et de méthodes permettant d'obtenir un modèle automate hybride équivalent d'un système physique avec des interrupteurs. Dans l'approche proposée l'automate hybride est obtenu par la composition des équations du système issues de l'approche bond-graph commuté et des contraintes introduites par les interrupteurs.<br />La méthodologie proposée est ensuite utilisée pour définir un modèle de simulation sous Simulink.<br />Le problème de la commande est abordé dans le cadre particulier du démarrage d'un convertisseur à double résonance issu d'une application en imagerie médicale.

Dans le cadre de ce sujet de thèse, on s'intéresse à la surveillance des systèmes hybrides à forte dynamique événementielle. L'objectif est de détecter les défauts permanents et intermittents qui causent l'accélération et le ralentissement des tâches des systèmes. C'est dans ce contexte que se situent les principales contributions suivantes des travaux consignés dans la présente thèse : - Le développement d'une méthode de surveillance des processus basée sur les automates hybrides linéaires (AHL). Cette méthode consiste en premier lieu à l'établissement du modèle AHL du système dynamique en tenant compte des contraintes physiques et dynamiques de celui-ci. - La réalisation d'une analyse d'atteignabilité qui consiste à définir toutes les trajectoires pouvant amener le système à son objectif tout en respectant le cahier des charges qui lui est imposé. L'extension de l'approche en utilisant les automates hybrides rectangulaires. Cette sous-classe d'automates nous a permis de modéliser des systèmes plus complexes donc une modélisation hybride riche et a permis également une analyse formelle. Cette partie a été ponctuée par l'implémentation du système de surveillance qui consiste à déterminer les équations caractérisant chaque sommet de l'automate qui modélise le système.