Graph rewriting for model construction in modal logic

Réécriture de graphes pour la construction de modèles en logique modale

Bilal Said (1)

1 IRIT-LILaC - Logique, Interaction, Langue et Calcul

To model the functioning of a system, to describe a situation or to represent ideas, we intuitively begin to draw bubbles and connect them by arrows as labeled graphs. Modal logics offer a formal and expressive framework to define these graphs as “models”, and to express certain properties of these graphs as “formulas”. They allow then to reason about these graphs and properties: model-checking, satisfiability or validity check, etc. 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. I brought new extensions and the new implementation techniques that were needed to handle new logics (such as K.alt1, universal modality, Hybrid Logic HL(@),Intuitionistic logic, Public Announcement Logic, ...). On the other hand, I examined the origins of LoTREC in the world of graph rewriting and specified the semantics of its rewriting engine.

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 et extensible 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: model checking, test de satisfiabilité ou de validité, etc. 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. D'autre part, j'ai examiné les origines de LoTREC dans le monde de réécriture de graphes et j'ai spécifié la sémantique de son moteur de réécriture. 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.

Mots clés: modal logic; satisfiability; tableaux methods; graph rewriting

Mots clés: Logique modale; réécriture de graphes; satisfiabilité; model-checking; méthodes de tableaux

Domaines: Informatique [cs]

Bilal Said. Graph rewriting for model construction in modal logic. Computer Science [cs]. Université Paul Sabatier - Toulouse III, 2010. English. ⟨NNT : ⟩. ⟨tel-00466115⟩