Logiques de séparation : complexité, expressivité, calculs

Cette thèse propose une étude approfondie de problèmes de décision classiques, tels que la satisfaisabilité et la validité pour des logiques de séparation, langages d'assertion bien connus développés pour la vérification de programmes avec structures dynamiques. La première partie de la thèse s'intéresse à la notion d'accessibilité pour les logiques de séparation. Notre motivation est double: d'une part, il s'agit de comprendre les frontières de la décidabilité de fragments de la logique de séparation du premier ordre connue pour être indécidable; d'autre part l'intention est de concevoir une logique de séparation aussi expressive que possible qui contienne des prédicats d'accessibilité, et dont le problème de satisfaisabilité soit décidable avec une complexité algorithmique relativement modeste (PSpace).Dans la seconde partie de la thèse, nous tirons profit des techniques développées dans la première partie pour définir une axiomatisation à la Hilbert de logiques de séparation et d'autres logiques spatiales. En particulier, nous définissons le premier calcul interne correct et complet pour la logique de séparation sans quantification. En utilisant la même approche, nous définissons une axiomatisation pour une logique modale enrichie d'un opérateur de composition issu d'une logique des ambients, formalisme logique dédié à la vérification de systèmes distribués. Les deux systèmes de preuves mettent en lumière des relations intéressantes entre les logiques de séparation et les logiques des ambients.Dans la troisième partie de la thèse, nous approfondissons encore davantage les relations entre les logiques de séparation et les logiques des ambients. Des similarités et des différences sont établies en termes de pouvoir d'expression et de complexité algorithmique, en comparant la conjonction séparante des logiques de séparation avec l'opérateur de composition des logiques des ambients. Afin de mener à bien nos comparaisons, nous nous plaçons dans une cadre uniforme issu de la logique modale, ce qui permet de partir d'une base commune pour étudier ces deux logiques.