LogoLogo

Said, Bilal. Réécriture de graphes pour la construction de modèles en logique modale

Said, Bilal (2010) Réécriture de graphes pour la construction de modèles en logique modale.

[img]PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
2765Kb

Résumé en francais

Pour modéliser le fonctionnement d'un système, décrire une situation ou représenter des idées, on se met intuitivement à dessiner des bulles et les lier par des flèches sous forme de graphes étiquetés. Les logiques modales constituent un cadre formel expressif, extensible et toujours d'actualité qui permet de définir ces graphes sous forme de " modèles ", et d'exprimer certaines propriétés de ces graphes sous forme de " formules " afin de pouvoir raisonner là-dessus: vérifier si un modèle satisfait une certaine formule ou non (model checking), ou bien s'il existe un modèle satisfaisant une formule donnée ou non (satisfiabilité / validité). Pour des formules et modèles de tailles importantes, ces tâches deviennent compliquées. De ce fait, un outil permettant de les réaliser automatiquement s'avère nécessaire. LoTREC en est un exemple. Il permet à son utilisateur de créer sa propre méthode de preuve, grâce à un langage simple et de haut niveau, sans avoir besoin d'aucune expertise spécifique en programmation. Durant ma thèse, j'ai revu le travail qui était déjà accompli dans LoTREC et j'ai apporté de nouvelles extensions qui s'avéraient nécessaires pour pouvoir traiter de nouvelles logiques (K.alt1, universal modality, Hybrid Logic HL(@),Intuitionistic logic, Public Announcement Logic, ...) et offrir à l'utilisateur certaines nouvelles techniques. Cela a exigé le développement et l'extension du noyau logiciel de LoTREC, ainsi que du langage et de l'interface qu'il offre à ses utilisateurs. Avec la nouvelle version on peut expérimenter avec ses formules afin de déboguer sa méthode en l'exécutant pas-à-pas, tout en visualisant et analysant les modèles (et/ou contre-modèles) générés d'une façon ludique. Quand on définit une procédure semi-automatique, on peut aussi démarrer avec des modèles partiels et intervenir durant l'exécution. D'autre part, je me suis donné l'objectif d'examiner les origines de LoTREC dans le monde de réécriture de graphes et de spécifier la sémantique de son moteur de réécriture. Ce travail a permis de bien présenter le mécanisme événementiel qui gère le processus de " pattern matching " d'une façon optimisée. Mon travail a permis de clarifier la sémantique de ce mécanisme, et de montrer son avantage par rapport aux techniques existantes par des résultats empiriques. En plus, ce travail a permis d'établir un lien entre le système de réécriture de LoTREC et l'une des approches théoriques bien fondées et connues chez la communauté de réécriture de graphes. Cela a permis d'éclaircir comment l'on peut hériter dans nos méthodes de preuve des résultats et des propriétés théoriques déjà bien établies dans le domaine de la réécriture de graphes.

Sous la direction du :
Directeur de thèse
Gasquet, Olivier
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Logique modale - Construction de modèles - Méthode de tableaux - Satisfiabilité - Réécriture de graphes
Sujets :Informatique
Déposé le :03 Sep 2010 14:05