Skip to Main content Skip to Navigation
Theses

Logiques spatiales de ressources, modèles d'arbres et applications

Abstract : 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.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_2005_0137_BIRI.pdf
Complete list of metadata

https://hal.univ-lorraine.fr/tel-01746669
Contributor : Thèses Ul Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 10:42:23 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM

Identifiers

  • HAL Id : tel-01746669, version 1

Collections

Citation

Nicolas Biri. Logiques spatiales de ressources, modèles d'arbres et applications. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2005. Français. ⟨NNT : 2005NAN10137⟩. ⟨tel-01746669⟩

Share

Metrics

Record views

43