Skip to Main content Skip to Navigation

Logiques de ressources dynamiques : modèles, propriétés et preuves

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, called ß-PN, we propose a new semantics based on ß-PN 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 metadatas

Cited literature [107 references]  Display  Hide  Download
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 1:20:29 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:06 PM


Files produced by the author(s)


  • HAL Id : tel-01751493, version 1



Jean-René Courtault. Logiques de ressources dynamiques : modèles, propriétés et preuves. Autre [cs.OH]. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0033⟩. ⟨tel-01751493⟩



Record views


Files downloads