La thèse se situe à la charnière de l'informatique théorique et de la logique mathématique. Elle se concentre en particulier sur les aspects mathématiques de la vérification et du contrôle. La thèse se focalise sur l'étude de deux sous-classes d'automates hybrides: les
automates temporisés pondérés et les automates hybrides o-minimaux.
Concernant les automates temporisés pondérés, en
introduisant un nouvel algorithme, nous donnons une caractérisation exacte de la complexité du problème d'atteignabilité optimal en prouvant qu'il est PSpace-complet. Nous prouvons que le model-checking de la logique WCTL est en général
indécidable. Nous nous intéressons alors à une
restriction de la logique WCTL. Nous montrons que
la décidabilité du model-checking de WCTL restreint dépend de la dimension de l'automate et du fait que le temps soit discret ou dense. Finalement pour, nous prouvons que le
problème de contrôle optimal est en général
indécidable. Nous prouvons cependant que ce même problème est décidable pour les automates temporisés pondérés de dimension 1.
En ce qui concerne les automates hybrides o-minimaux, à l'aide d'un encodage symbolique des trajectoires par des mots, nous sommes parvenus à prouver l'existence d'une bisimulation finie pour ces automates. De plus (toujours en utilisant nos encodages des trajectoires par des mots), nous avons obtenu des résultats de décidabilité pour des problèmes de jeux sur ces mêmes automates hybrides o-minimaux. Pour une classe d'automates hybrides o-minimaux, nous avons prouvé (i) que l'existence de stratégie gagnante pouvait être décidée et (ii) que ces stratégies gagnantes pouvaient être synthétisées.
| Identifer | oai:union.ndltd.org:BICfB/oai:umh.ac.be:ETDUMH:UMHetd-01302009-134458 |
| Date | 02 June 2006 |
| Creators | Brihaye, Thomas |
| Contributors | Bruyère, Véronique, Bouyer, Patricia, Michaux, Christian, Point, Françoise, Raskin, Jean-François, Roy, Marie-Françoise, Steinhorn, Charles, Thomas, Wolfgang, Troestler, Christophe, Wijsen, Jef |
| Publisher | Universite de Mons Hainaut |
| Source Sets | Bibliothèque interuniversitaire de la Communauté française de Belgique |
| Language | English |
| Detected Language | French |
| Type | text |
| Format | application/pdf |
| Source | http://theses.umh.ac.be/ETD-db/collection/available/UMHetd-01302009-134458/ |
| Rights | unrestricted, J'accepte que le texte de la thèse (ci-après l'oeuvre), sous réserve des parties couvertes par la confidentialité, soit publié dans le recueil électronique des thèses UMH. A cette fin, je donne licence à UMH : - le droit de fixer et de reproduire l'oeuvre sur support électronique : logiciel ETD/db - le droit de communiquer l'oeuvre au public Cette licence, gratuite et non exclusive, est valable pour toute la durée de la propriété littéraire et artistique, y compris ses éventuelles prolongations, et pour le monde entier. Je conserve tous les autres droits pour la reproduction et la communication de la thèse, ainsi que le droit de l'utiliser dans de futurs travaux. Je certifie avoir obtenu, conformément à la législation sur le droit d'auteur et aux exigences du droit à l'image, toutes les autorisations nécessaires à la reproduction dans ma thèse d'images, de textes, et/ou de toute oeuvre protégés par le droit d'auteur, et avoir obtenu les autorisations nécessaires à leur communication à des tiers. Au cas où un tiers est titulaire d'un droit de propriété intellectuelle sur tout ou partie de ma thèse, je certifie avoir obtenu son autorisation écrite pour l'exercice des droits mentionnés ci-dessus. |
Page generated in 0.0056 seconds