Extensions modales des logiques de ressources : expressivité et calculs

Le développement de nouveaux formalismes logiques est au cœur de nombreuses problématiques de méthodes formelles. Ces formalismes doivent répondre à la fois à des impératifs de modélisation (ils doivent permettre de décrire certains systèmes) et de calcul (ils doivent fournir des méthodes de calcul correctes et complètes). Dans ce contexte, nous nous intéressons aux logiques de ressources, en particulier les logiques BI et BBI qui traitent du partage et de la séparation de ressources et qui ont conduit aux diverses logiques de séparation dont les applications à la vérification de programmes se sont développées fortement ces dernières années. Nous proposons dans cette thèse d’étudier, à partir des logiques BI et BBI, des logiques de séparation modales et épistémiques en se focalisant sur leurs capacités de modélisation et leur expressivité mais aussi les nouveaux calculs de preuve pour ces logiques. Une première étude a porté sur la modélisation de propriétés dynamiques de ressources au travers d’une nouvelle logique LTBI, qui est une logique de séparation temporelle, fondée sur la logique BI et des modalités temporelles. Cette logique offre notamment des perspectives intéressantes de modélisation temporelle branchante, permettant par exemple de caractériser les processus multi-thread. Une étude complémentaire a porté sur la modélisation de l’accès par des agents à des propriétés sous conditions de posséder certaines ressources, au travers d’une nouvelle logique ERL, qui est une logique de séparation épistémique, fondée sur la logique BBI et des modalités épistémiques. Cette logique permet de nombreuses modélisations de systèmes de contrôle d’accès. En vue d’étendre l’expressivité de telles logiques de séparation, comme la logique BBI et ses variantes, une étude sur l’internalisation des symboles de ressources dans la syntaxe de la logique a été développée au travers des nouvelles logiques HRL et HBBI (version hybride de BBI). L’internalisation permet à la fois d’étendre l’expressivité des logiques et d’axiomatiser la logique BBI et certaines de ses variantes. Outre la conception de ces logiques, l’étude de leur sémantique et aussi de leurs capacités de modélisation, une partie de cette thèse a été consacrée à la définition de calculs de preuve, ici de tableaux, pour ces nouvelles logiques ainsi qu’à leurs preuves de correction et de complétude