Réécriture de graphes pour la construction de modèles en logique modale
Institution:
Toulouse 3Disciplines:
Directors:
Abstract EN:
To model the functioning of a system, to describe a situation or to represent ideas, we begin to intuitively draw bubbles and connect them by arrows as labeled graphs. Modal logics offer a formal, expressive and scalable framework to define these graphs as "models", and to express certain properties of these graphs as "formulas". They allow then to reason on these graphs and properties: wether a model satisfies a certain formula or not (model-checking), or wether there is a model satisfying a given formula or not (satisfiability / validity). For formulas and models of large sizes, these tasks become complicated, and thus, we need a tool to achieve these reasoning tasks automatically. LoTREC is an example of such tools. It allows the user to create his own proof method, through a simple and high level language without any need to a specific expertise in programming. During my Ph. D. , I revisited the work that has been already done in LoTREC and I have brought new extensions that were needed to offer the users new implementation techniques. This allowed to handle new logics (such as K. Alt1, universal modality, Hybrid Logic HL(@),Intuitionistic logic, Public Announcement Logic,. . . ). This achievement required the development and the expansion of the software core of LoTREC, its language and its user interface. With the new version we can experiment in a step-by-step mode or use other options to debug our method, while visualizing and analyzing the models (and / or counter-models) generated and displayed in an pretty-print layout. When we define a semi-automatic procedure, we can also start with partial models and intervene during the execution. . .
Abstract FR:
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. . .