Extensions modales des logiques de ressources : expressivité et calculs

Pierre Kimmel 1
1 TYPES - Logic, proof Theory and Programming
LORIA - FM - Department of Formal Methods
Abstract : The design of new logical formalisms is at the heart of several problems in formal methods. Those formalisms must respond to requirements both concerning modelling (they must be able to describe certain systems) and computing (they must provide complete and sound calculus methods). In this context, we look at resource logics, and in particular BI and BBI logics, that deal with the separation and sharing of resources and have led to several separation logics whose applications to software verification have been widely developped recently. We propose in this thesis, starting from BI and BBI logics, to study some modal and epistemic separation logics by focusing on their modelling capacities and their expresiveness, as well as on the new proof calculi for those logics. A first study deals with the modelling of dynamic resource properties through new logic LTBI, which is a temporal separation logic, based on BI logic and temporal modalities. This logic notably offers interesting perspectives in temporal branching modelling, allowing for instance to characterize multi-thread processes. A complementary study concerns the modelling of access by agents to properties under the conditions of posessing some resources, through a new logic ERL, which is an epistemic separation logic, based on BBI logic and epistemic modalities. This logic allows many modellings of access control systems. In order to extend the expressivity of such separation logics, like BBI logic and its variants, a study on the internalization of resources symbols in the logic’s syntax has been developed through the new logics HRL and HBBI (hybrid version of BBI). Internalization allows both the extension of the expressivity of logics and the axiomatisation of BBI logic and some of its variants. In addition to the conception of those logics, the study of their semantics and their modelling capacities, a part of this thesis is dedicated to the definition of proof calculs, here tableaux calculus, for those new logics, as well as their proof of soundness and completeness
Complete list of metadatas

Cited literature [157 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-02096099
Contributor : Thèses Ul <>
Submitted on : Thursday, April 11, 2019 - 9:49:26 AM
Last modification on : Saturday, April 13, 2019 - 1:23:54 AM

File

DDOC_T_2018_0299_KIMMEL.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02096099, version 1

Citation

Pierre Kimmel. Extensions modales des logiques de ressources : expressivité et calculs. Logique en informatique [cs.LO]. Université de Lorraine, 2018. Français. ⟨NNT : 2018LORR0299⟩. ⟨tel-02096099⟩

Share

Metrics

Record views

26

Files downloads

41