• Langue : Français
• Discipline : Sciences mathématiques. Informatique
• Identifiant : Inconnu
• Type de mémoire : Habilitation à diriger des recherches
• Date de soutenance : 01/01/2005

Résumé en langue originale

Le problème de model-checking pour une logique L et une classe de structures C est de savoir si une formule (close) donnée de L est vraie pour une certaine structure de C. Ce problème revêt différentes formes selon la thématique dans laquelle il est étudié: dans le cadre de la vérification, il s'agit de tester si un système (ou une abstraction de celui-ci) vérifie une spécification logique. Dans le cadre des bases de données relationnelles ou semi-structurées, ce problème, appelé également requêtes booléennes, consiste à vérifier que la base de données satisfait un certain nombre de contraintes, comme, par exemple, la conformité vis-à-vis d'un schéma XML. Dans tous les cas, lorsqu'on considère un problème de model-checking, la décidabilité de celui-ci et le cas échéant, sa complexité sont des questions cruciales. Dans ce mémoire, nous résumons nos activités de recherches sur le problème de model-checking, problème que nous avons étudié dans le cadre restreint du calcul des ambients. Cette étude a été effectuée avec une double approche, d'un côté, dans l'optique "programmation - vérification pour les algèbres de processus" et de l'autre, dans celle de "base de données - interrogation de données semi-structurées". Le calcul des ambients est une algèbre de processus visant à modéliser l'informatique mobile; ce calcul est basé sur une notion de domaines hiérarchiquement organisés, hiérarchie qui évolue au cours de l'exécution du système. Nous nous sommes intéressés au problème de vérification du calcul des ambients pour des spécifications écrites dans une logique dédiée appelée logique des ambients. Pour divers fragments du calcul et de la logique, nous avons établi des bornes fines concernant la décidabilité et la complexité du problème de model-checking. Nous montrons en particulier qu'en présence de réplication, le problème de model-checking est indécidable, y compris pour des petits fragments de la logique et du calcul. Débarrassés de leurs mécanismes d'exécution, les processus des ambients se résument à leurs structures hiérarchiques correspondant à des données arborescentes. Cette vision du calcul et de la logique associée a donné naissance au langage TQL (Tree Query Language) d'interrogation de données semi-structurées. Nous avons mené une étude formelle de cette logique TQL, en particulier concernant les problèmes de model-checking et de satisfiabilité (l'existence d'une structure de la classe C qui est modèle d'une formule donnée de la logique L). Nous avons également mesuré l'expressivité de cette logique en la comparant notamment à la logique monadique du second-ordre et à certaines de ses extensions. Ces travaux ont été menés au sein de l'équipe STC du LIFL. De plus, les recherches sur la validation et l'interrogation de données semi-structurées s'inscrivent dans la thématique du projet MOSTRARE de l'INRIA Futurs.