La conduite de systèmes autonomes nécessite de prendre des décisions en fonction des observations et des objectifs courants : cela implique des tâches à effectuer en ligne, avec les moyens de calcul embarqués. Cependant, il s'agit généralement de tâches combinatoires, gourmandes en temps de calcul et en espace mémoire. Réaliser ces tâches intégralement en ligne dégrade la réactivité du système ; les réaliser intégralement hors ligne, en anticipant toutes les situations possibles, nuit à son embarquabilité. Les techniques de compilation de connaissances sont susceptibles d'apporter un compromis, en déportant au maximum l'effort de calcul avant la mise en situation du système. Ces techniques consistent à traduire un problème dans un certain langage, fournissant une forme compilée de ce problème, dont la résolution est facile et la taille aussi compacte que possible. L'étape de traduction peut être très longue, mais elle n'est effectuée qu'une seule fois, hors ligne. Il existe de nombreux langages-cible de compilation, notamment le langage des diagrammes de décision binaires (BDDs), qui ont été utilisés avec succès dans divers domaines de l'intelligence artificielle, tels le model-checking, la configuration ou la planification. L'objectif de la thèse était d'étudier l'application de la compilation de connaissances à la conduite de systèmes autonomes. Nous nous sommes intéressés à des problèmes réels de planification, qui impliquent souvent des variables continues ou à grand domaine énuméré (temps ou mémoire par exemple). Nous avons orienté notre travail vers la recherche et l'étude de langages-cible de compilation assez expressifs pour permettre de représenter de tels problèmes. Dans la première partie de la thèse, nous présentons divers aspects de la compilation de connaissances ainsi qu'un état de l'art de l'utilisation de la compilation dans le domaine de la planification. Dans une seconde partie, nous étendons le cadre des BDDs aux variables réelles et énumérées, définissant le langage-cible des " interval automata " (IAs). Nous établissons la carte de compilation des IAs et de certaines restrictions des IAs, c'est-à-dire leurs propriétés de compacité et leur efficacité vis-à-vis d'opérations élémentaires. Nous décrivons des méthodes de compilation en IAs pour des problèmes exprimés sous forme de réseaux de contraintes continues. Dans une troisième partie, nous définissons le langage-cible des " set-labeled diagrams " (SDs), une autre généralisation des BDDs, permettant de représenter des IAs discrétisés. Nous établissons la carte de compilation des SDs et de certaines restrictions des SDs, et décrivons une méthode de compilation de réseaux de contraintes discrets en SDs. Nous montrons expérimentalement que l'utilisation de IAs et de SDs pour la conduite de systèmes autonomes est prometteuse.

Dans le cadre des évolutions du bâtiment, il est de plus en plus nécessaire d'interconnecter des objets communicants. Cette démarche est cependant freinée du fait de l'absence d'un protocole de communication standard. La maison intelligente n'est pas un nouveau concept, et l'automatisation de la maison est devenue un sujet de recherche à la mode ces dernières années. La problématique de cette thèse se focalise sur l'interopérabilité de systèmes communicants. Plus précisément, nous nous intéressons à la manière de créer une coopération entre différents dispositifs d'un environnement, afin de masquer la complexité à l'usager. Dans un premier temps, l'interopérabilité entre ces objets est réalisée par la mise en place d'un écosystème virtuel où les dispositifs peuvent communiquer leurs états ou l'état de l'environnement. C'est l'abstraction des systèmes. Dans ce mémoire, nous abordons comment et pourquoi les systèmes sont nécessairement abstraits lorsque l'on s'intéresse à la prise en compte du contexte de l'installation. L'étude de la prise en compte du contexte à permis de procurer les données scientifiques à l'entreprise Overkiz afin qu'elle puisse réaliser l'abstraction des dispositifs domotiques. Ensuite, la coopération entre les objets communicants est mise en œuvre par un outil mathématique permettant de modéliser le comportement d'un environnement composé d'actionneurs, de capteurs et d'interfaces utilisateurs. Le comportement est formalisé au moyen de la théorie des automates étendus et plus particulièrement par la théorie des systèmes de transitions symboliques à entrées/sorties (IOSTS). Nous synthétisons alors le pilotage par un "contrôleur" du comportement global d'une installation, à partir de règles de contraintes ou de règles d'action.

Le problème de la combinaison des services, autrement appelé problème de la composition, constitue le foyer d'une intense activité de recherche. Composer les services entre eux, c'est entrelacer leurs séquences d'actions, de manière à obtenir des séquences qui satisfassent les exigences des clients. Le problème de la composition de services est difficile à résoudre en général. Dans cette thèse nous considérons des services qui peuvent à la fois exécuter des actions de communications ainsi que des actions internes. De plus, des conditions peuvent être exigées et des effets peuvent être appliqués sur les transitions. Formellement, les services sont représentés par des automates communicants conditionnels. Nous définissons, pour ce modèle, le problème de la composition et nous étudions sa décidabilité pour différentes relations d'équivalence et de préordre à savoir : l'inclusion de traces, l'équivalence de traces, la simulation et la bisimulation. Suite aux résultats de décidabilité obtenus, nous proposons trois variantes pour le modèle initial. Pour chacune d'elles, nous définissions le problème de la composition et nous étudions sa complexité pour les relations citées ci-dessus.

Les transferts de chaleur et de masse sont deux phénomènes physiques à la base de nombreux systèmes thermiques employés dans des secteurs variés tels que l'industrie, le bâtiment ou encore les énergies renouvelables. Les présents travaux de recherche envisagent différentes méthodologies d'optimisation de configurations assurant le transfert de flux de chaleur, couplé ou non à un écoulement fluide, au sens topologique du terme. Les équations aux dérivées partielles décrivant les phénomènes physiques sont discrétisées avec la méthode des volumes finis. La première partie du manuscrit examine successivement trois classes différentes de méthodes: la théorie constructale, les automates cellulaires et les méthodes par pénalisation. Le même cas académique, portant sur le refroidissement d'un volume fini générant de la chaleur, est résolu au moyen de ces trois méthodes, ce qui permet ainsi de comparer les performances de chaque algorithme. Cette comparaison démontre l'ascendant des méthodes par pénalisation sur les deux premiers types, tant structurellement que quantitativement, et permet également d'établir des solutions basées sur des compromis dans le cadre d'optimisations multi-objectifs. Par conséquent, la seconde partie envisage l'application de cette approche à des configurations réalisant des transferts de chaleur conducto-convectifs en régime laminaire. L'utilisation de paramètres de pénalisation en conjonction avec les volumes finis requiert une régularisation de la dissipation visqueuse le long de l'interface fluide/solide. Une approche bi-objectif est développée visant à minimiser la puissance dissipée par le fluide, tout en maximisant l'énergie thermique récupérée sur le système. Les solutions obtenues adoptent des configurations non-triviales qui sont divisibles en quatre classes topologiques différentes. La thèse ouvre ainsi un nouveau champ d'investigation pour l'optimisation d'écoulements couplés à la problématique du transport de chaleur.

Les transferts de chaleur et de masse sont deux phénomènes physiques à la base de nombreux systèmes thermiques employés dans des secteurs variés tels que l'industrie, le bâtiment ou encore les énergies renouvelables. Les présents travaux de recherche envisagent différentes méthodologies d'optimisation de configurations assurant le transfert de flux de chaleur, couplé ou non à un écoulement fluide, au sens topologique du terme. Les équations aux dérivées partielles décrivant les phénomènes physiques sont discrétisées avec la méthode des volumes finis. La première partie du manuscrit examine successivement trois classes différentes de méthodes: la théorie constructale, les automates cellulaires et les méthodes par pénalisation. Le même cas académique, portant sur le refroidissement d'un volume fini générant de la chaleur, est résolu au moyen de ces trois méthodes, ce qui permet ainsi de comparer les performances de chaque algorithme. Cette comparaison démontre l'ascendant des méthodes par pénalisation sur les deux premiers types, tant structurellement que quantitativement, et permet également d'établir des solutions basées sur des compromis dans le cadre d'optimisations multi-objectifs. Par conséquent, la seconde partie envisage l'application de cette approche à des configurations réalisant des transferts de chaleur conducto-convectifs en régime laminaire. L'utilisation de paramètres de pénalisation en conjonction avec les volumes finis requiert une régularisation de la dissipation visqueuse le long de l'interface fluide/solide. Une approche bi-objectif est développée visant à minimiser la puissance dissipée par le fluide, tout en maximisant l'énergie thermique récupérée sur le système. Les solutions obtenues adoptent des configurations non-triviales qui sont divisibles en quatre classes topologiques différentes. La thèse ouvre ainsi un nouveau champ d'investigation pour l'optimisation d'écoulements couplés à la problématique du transport de chaleur.

On s'intéresse dans ce travail aux automates cellulaires unidimensionnels qui ont été largement étudiés mais où il reste beaucoup à faire. La théorie spectrale des automates cellulaires a notamment été peu abordée à l'exception de quelques résultats indirects. On cherche a mieux comprendre les cadres topologiques et ergodiques en étudiant l'existence de valeurs propres en particulier celles irrationnelles c'est à dire de la forme e^{2Iπα} où α est un irrationnel et I la racine carrée de l'unité. Cette question ne semble pas avoir été abordée jusqu'à présent. Dans le cadre topologique les résultats sur l'équicontinuité de Kůrka et Blanchard et Tisseur permettent de déduire directement que tout automate cellulaire équicontinu possède des valeurs propres topologiques rationnelles. La densité des points périodiques pour le décalage empêche l'existence de valeurs propres topologiques irrationnelles. La densité des points périodiques pour l'automate cellulaire semble être liée à la question des valeurs propres. Dans le cadre topologique, si l'automate cellulaire possède des points d'équicontinuité sans être équicontinu, la densité des points périodiques a comme conséquence le fait que le spectre représente l'ensemble des racines rationnelles de l'unité c'est à dire tous les nombres de la forme e^{2Iπα} avec α∈Q .Dans le cadre mesuré, la question devient plus difficile, on s'intéresse à la dynamique des automates cellulaires surjectifs pour lesquels la mesure uniforme est invariante en vertu du théorème de Hedlund. La plupart des résultats obtenus demeurent valable dans un cadre plus large. Nous commençons par montrer que les automates cellulaires ayant des points d'équicontinuité ne possèdent pas de valeurs propres mesurables irrationnelles. Ce résultat se généralise aux automates cellulaires possédant des points μ-équicontinu selon la définition de Gilman. Nous démontrons finalement que les automates cellulaires possédant des points μ-équicontinu selon la définition de Gilman possèdent des valeurs propres rationnelles

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.

Ce travail propose une méthode pour l'analyse de systèmes temps-reél. <br />Cette méthode est basée sur la compilation des spécifications<br />vers des graphes temporisés, à partir desquels il est possible<br />de vérifier des propriétés et de générer du code exécutable.<br /><br />Les graphes temporisés sont des automates étendus avec des<br />variables, appelées horloges, qui permettent de décrire les<br />contraintes temporelles. <br /><br />Un algorithme de compilation est développé pour l'algèbre<br />de processus temporisés ATP, qui est une extension des <br />algèbres de processus avec des opérateurs temporels comme <br />le ``timeout'' et le ``watchdog''. L'intérêt de l'algorithme est <br />que la taille du graphe obtenu est indépendante des valeurs <br />des paramètres des opérateurs temporels.<br /><br />Les propriétés temps-reél sur les graphes temporisés sont <br />décrites par des formules de la logique TCTL. <br />Il est montré que les opérateurs temporels<br />de TCTL s'expriment en termes de points fixes à l'aide d'un <br />opérateur ``d'état suivant'' défini de façon appropriée.<br />De plus, ce travail propose un algorithme de vérification qui<br />consiste à évaluer symboliquement l'ensemble caractéristique<br />d'une formule comme une disjonction de contraintes linéaires<br />sur les horloges.<br /><br />Les algorithmes de compilation et de vérification développés <br />ont été implémentés dans l'outil KRONOS, <br />utilisé pour analyser des applications temps-reél <br />significatives. Les résultats obtenus confirment l'intérêt<br />pratique de l'approche proposée.

Reproduction de : Thèse doctorat : Informatique : Reims : 2008. / Titre provenant de l'écran titre. Bibliogr. p. 301-320.

Cette thèse porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes temps-réel. La thèse est constituée de trois parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (sur-approximation, sous-approximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes temps-réel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure non-déterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles forçant la convergence d'horloges. Finalement, nous étudions le problème de l'accessibilité des états acceptants dans des réseaux d'automates temporisés qui communiquent via des files FIFO. Nous considérons tout d'abord des automates temporisés à temps discret, et caractérisons les topologies de réseaux pour lesquelles l'accessibilité est décidable. Cette caractérisation est ensuite étendue aux automates temporisés à temps continu.