Skip to Main content Skip to Navigation
New interface

Logiques de Ressources Dynamiques : Modèles, Propriétés et Preuves

Jean-René Courtault 1 
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In computer science, the notion of resource is a central concern. We consider as a resource, any entity that can be composed or decomposed into sub-entities. Many logics were proposed to model and express properties on these resources, like BI logic, a logic about sharing and separation of resources. As the computer systems manipulate resources, a crucial issue consists in providing new models that capture the dynamics of resources, and also in verifying and proving properties on these models. In this context, we define new logics with new models and new languages allowing to respectively capture and express new properties on the dynamics of resources. Moreover, for all these logics, we also study the foundations of proof search and provide tableau methods and counter-model extraction methods. After defining new Petri nets we propose a new semantics based on such nets for BI logic, that allows us to show that BI is able to capture a kind of dynamics of resources. After observing that it is necessary to introduce new modalities in BI logic, we study successively different modal extensions of BI. We define a logic, called DBI, that allows us to model resources having dynamic properties, meaning that they evolve during the iterations of a system. Then, we define a logic, called DMBI, that allows us to model systems that manipulate/produce/consume resources. Moreover, we define a new modal logic, called LSM, having new multiplicative modalities, that deals with resources. Finally, we introduce the notion of separation in Epistemic Logic, obtaining a new logic, called ESL, that models and expresses new properties on agent knowledge.
Document type :
Complete list of metadata

Cited literature [100 references]  Display  Hide  Download
Contributor : Didier Galmiche Connect in order to contact the contributor
Submitted on : Wednesday, January 27, 2016 - 2:44:09 PM
Last modification on : Saturday, October 8, 2022 - 12:05:27 PM
Long-term archiving on: : Thursday, April 28, 2016 - 11:21:16 AM


  • HAL Id : tel-01263165, version 2



Jean-René Courtault. Logiques de Ressources Dynamiques : Modèles, Propriétés et Preuves . Logique en informatique [cs.LO]. Université de Lorraine 2015. Français. ⟨NNT : 2015LORR0033⟩. ⟨tel-01263165v2⟩



Record views


Files downloads