Ressources and spatial logic, tree models and applications
Logiques spatiales de ressources, modèles d'arbres et applications
Résumé
Modelling and specifying distributed systems require an adaptation of logical model habitually used to represent those systems. The notions of location and resource are one of the key points for representing such systems. We begin with a first proposition of logic, the Distributed and Concurrent Linear Logic (DMLL), which integrates notions of distribution and of mobility. We also propose a Kripke's semantic and a sequent calculus that supports cut-elimination. This first study emphasizes the central role of semantics in the modelling of distributed systems. We propose then a new structure, the resource trees, which are labelled trees containing resources from a partial monoid inside their nodes and a new logic, BI-Loc, to reason about these trees. We also propose a language to transform these trees and its correct and complete logical axiomatisation using Hoare's triples. Concerning BI-Loc, we determine sufficient condition to decide satisfaction and validity and we develop a correct and complete proof-search method using semantic labelled tableaux. This method is inspired of the one developed for BI. Then we show some application of the partial tree model. Firstly, we show how the resource trees can be used to reason about the heap of pointers and a refinement of this model, the permission model. Then, we focus on semi-structured data, and show how we can represent and specify such data using resource trees and how it can be used to reason about transformation of these data.
La modélisation et la spécification de systèmes distribués nécessitent une adaptation des modèles logiques utilisés pour leur représentation. Les notions d'emplacements et de ressources jouent notamment un rôle centrale dans la représentation de ces systèmes. Dans ce cadre, on propose tout d'abord une première logique, la logique linéaire distribuée et mobile (DMLL) qui integre les notions de distribution et de mobilité. On propose également une sémantique à la Kripke et un calcul des séquents supportant l'élimination des coupures pour cette logique. Cette première étude a mis en avant le rôle centrale de la sémantique pour la modélisation de systèmes distribués. On propose alors la structure des arbres de ressources, des arbres dont les noeuds possèdent des labels et contiennent des ressources appartenant à mono?ide partiel de ressources et BI-Loc, une logique pour raisonner sur ces arbres, un langage permettant de modifier les arbres et son axiomatisation correcte et complète sous forme de triplets de Hoare. Concernant \acronym{BI-Loc}, on détermine des conditions suffisantes pour décider de la satisfaction et de la validité par model-checking et on développe une méthode de preuves fondée sur les tableaux sémantiques correcte et complète. On montre comment on peut raisonner sur les tas de pointeurs grâce aux arbres de ressources. Enfin, on détermine comment le modèle des arbres partiel peut être utilisé pour représenter et spécifier les données semi-structurées et raisonner sur la transformation de ce type de données.