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 :
Theses
Complete list of metadatas

Cited literature [107 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01751493
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

File

DDOC_T_2015_0033_COURTAULT.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01751493, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

61

Files downloads

40