[Thèse TYPES] Preuves et réfutations en logiques de ressources

Contexte général, approche et enjeux

Un défi majeur pour appréhender les problèmes posés par la complexité des systèmes actuels est de proposer de nouveaux cadres formels et de nouvelles méthodes d’analyse et de conception (au sens large incluant aussi bien des aspects de spécification, de modélisation et de vérification), qui intègrent dès l’origine, de manière globale et intrinsèque, les liens et interactions qui existent entre les aspects statiques et dynamiques d’un système. Nous souhaitons proposer des cadres formels et des méthodes adaptées selon trois axes complémentaires : un premier lié à des propriétés de nature spatiale (distribution, mobilité dans l’espace), un deuxième lié à des propriétés de nature temporelle (par exemple, l’évolution du système vers un état stable, l’exécution infiniment répétée d’une suite d’opérations), et enfin, un troisième pour rendre compte de problèmes (éventuellement soulevés dans les deux autres) en termes quantitatifs et pas uniquement qualitatifs (par exemple, toutes les trois opérations de lecture, le système vérifie la présence d’une opération d’écriture en attente).

La notion de ressource et les problématiques liées à leur gestion sont au cœur de notre approche. Nous entendons ici par ressources aussi bien des entités physiques (un circuit électronique, une imprimante, un processeur) que des entités abstraites (une fonction mathématique, une structure de données, un processus). Nous nous intéressons plus particulièrement à des phénomènes de production/consommation (jetons dans un réseau de Petri), de partage/séparation (zones de mémoire dans un ordinateur, de contrôle d’accès, distribution spatiale et de mobilité (processus mobiles, systèmes embarqués). Presque tout objet présentant des propriétés de ressources, les logiques et modèles de ressources suscitent depuis quelques années un vif intérêt dans le domaine de l’analyse et la conception de systèmes complexes.

Description du sujet

Dans le contexte des logiques de ressources, on s’intéressera plus particulièrement à la logique BI (« The Logic of Bunched Implications ») et ses variantes qui incluent un opérateur de composition s’interprétant en termes de partage et de séparation de ressources. La logique BI se décline en une version intuitionniste [13] et une version booléenne [7] qui se distinguent par les propriétés de leurs opérateurs additifs. Dans sa version booléenne, appelée Boolean BI (BBI), elle constitue le noyau autour duquel sont construites les logiques spatiales [2, 3] et les logiques de séparation [9, 10].

Plusieurs systèmes de preuves existent pour BI, notamment pour sa version intuitionniste, un calcul des séquents avec « bunch » purement syntaxique appelé LBI [13] et une méthode de tableaux avec labels et contraintes sémantiques appelée TBI [6]. Si on sait très bien comment transformer directement toute preuve de TBI en une preuve de LBI [6], la transformation duale reste un problème ouvert. Pour le cas plus restreint de la logique intuitionniste, des résultats récents montrent que la transformation de preuves en séquents avec labels vers des preuves en séquents sans labels n’est pas triviale et nécessite le passage intermédiaire par la logique bi-intuitionniste [12].

La logique bi-intuitionniste [4, 14] est une extension de la logique intuitionniste dans laquelle on ajoute un connecteur dual de l’implication additive appelé co-implication ou exclusion. C’est un mélange entre la logique intuitionniste, qui privilégie la notion de vérification constructive (et donc de preuve), et la logique intuitionniste duale qui met plutôt l’accent sur la notion de falsification constructive (et donc de réfutation) [15]. Des formalismes à base de jeux dialogiques à la Lorenzen permettent de mieux appréhender cette dualité preuve/réfutation en opposant deux joueurs sur une même formule, l’un tentant de la prouver tandis que l’autre tente de la réfuter [5]. Dans le cadre de BI, il semble intéressant également de définir une implication multiplicative duale, appelée septraction [1]. Ainsi, plusieurs types d’extension bi-intuitionnistes (additives et/ou multiplicatives) de BI peuvent être considérées.

Dans nos travaux sur les tableaux pour BI nous avons mis en évidence l’importance de structures, appelées graphes de ressources, qui représentent la validité d’une formule à l’aide de contraintes de connexité, d’accessibilité entre nœuds et d’acyclicité. Les graphes de ressources permettent de guider à la fois un processus de recherche de preuves ou un processus de construction de contre-modèles [6]. La construction de contre-modèles est centrale dans notre approche car il est crucial en pratique de comprendre rapidement et précisément les raisons pour lesquelles une spécification échoue. Si un contre-modèle est un objet sémantique établissant la non-validité d’une formule (dans une certaine sémantique), il est également intéressant de savoir construire des réfutations, c’est à dire, des objets syntaxiques établissant la non-prouvabilité d’une formule (dans un système de preuve). Par exemple, CRIP est un système de réfutation pour la logique intuitionniste propositionnelle [11]. En l’absence de théorème de complétude, les notions de réfutations et de contre-modèles ne coïncident pas forcément.

L’objectif de ce sujet de thèse est d’étudier les notions de graphe de ressources, de contre-modèles et/ou réfutations et de transformation de preuves entre calculs internes (purement syntaxiques) et externes (avec labels et contraintes sémantiques) dans le contexte d’extensions de BI. Pour le moment les graphes de ressources pour BI et ses variantes sont construits à partir de systèmes de déduction avec labels sans variables libres, sauf dans le cas particulier de la logique bi-intuitionniste [8].

Plusieurs pistes seront explorées :

  • la généralisation de la structure de graphes de ressources aux cas des systèmes de déduction avec variables libres ;
  • la proposition de structures de données et d’algorithmes spécialisés, permettant la représentation et la résolution efficace des contraintes de validité dans un ensemble de graphes de
    ressources donné ;
  • la transformation de preuves obtenues dans des systèmes avec labels (à partir de graphes de ressources dont les contraintes de validité ont été résolues) en preuves purement syntaxiques
    (lorsque les calculs internes correspondant existent) ;
  • la reconnaissance, par exemple à l’aide de techniques d’appariement ou de bisimulation, de motifs de graphes caractérisant les mêmes ensembles de formules valides ;
  • la caractérisation à base de jeux dialogiques de la validité dans diverses extensions bi-intuitionnistes de BI en termes de stratégies gagnantes ;
  • la mise en œuvre de la méthode des tableaux pour BI et ses extensions bi-intuitionnistes.

Le sujet s’inscrit dans le développement des travaux actuels de l’équipe TYPES sur les logiques et modèles de ressources, à partir des logiques de séparation, avec l’étude de nouveaux modèles et sémantiques et la conception de systèmes et méthodes de preuve efficaces dans ce contexte.

Environnement de la thèse

Lieu : Nancy, LORIA, Equipe TYPES
Directeur de thèse : Didier Galmiche (didier.galmiche@loria.fr)
Co-encadrement : Daniel Méry (daniel.mery@loria.fr)
Mots clés : preuves, réfutations, logiques de ressources.
Compétences et profil : un master en informatique ou équivalent. Compétences en logique, sémantique, théorie de la preuve et programmation.

Références

[1] R. Brochenin, S. Demri, and E. Lozes. On the almighty wand. In 17th EACSL Annual Conference on Computer Science Logic, CSL 2008, LNCS 5213, pages 323–338, Bertinoro, Italy, 2008.
[2] L. Caires and E. Lozes. Elimination of quantifiers and undecidability in spatial logics for concurrency. Theoretical Computer Science, 358(2-3) :293–314, 2006.
[3] C. Calcagno, L. Cardelli, and A. Gordon. Deciding Validity in a Spatial Logic for Trees. Journal of Functional Programming, 15(4) :543–572, 2005.
[4] T. Crolard. Subtractive logic. In Theoretical Computer Science, 254(1-2) :151–185.
[5] W. Felscher. Dialogues, strategies, and intuitionistic provability. In Annals of Pure and Applied Logic, 28(3) :217–254, 1985.
[6] D. Galmiche, D. Méry, and D. Pym. The semantics of BI and Resource Tableaux. Mathematical Structures in Computer Science, 15(6) :1033–1088, 2005.
[7] D. Galmiche and D. Larchey-Wendling. Expressivity properties of Boolean BI through relational models. In Int. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006, LNCS 4337, pages 357–368, Kolkata, India, 2006.
[8] D. Galmiche and D. Méry. A connection-based characterization of bi-intuitionistic validity. In Int. Conference on Automated Deduction, CADE 23, LNCS 6803, pages 268–282, Wroclaw, Poland, 2011.
[9] S. Ishtiaq and P.W. O’Hearn. BI as an assertion language for mutable data structures. In 28th ACM Symposium on Principles of Programming Languages, POPL 2001, pages 14–26, London, UK, 2001.
[10] P.W. O’Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In 15th Int. Workshop on Computer Science Logic, CSL 2001, LNCS 2142, pages 1–19, Paris, France, 2001.
[11] L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Symposia Gaussiana, Conference A, pages 226–232, 1995.
[12] L. Pinto and T. Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic. In 3rd Workshop on Classical Logic and Compution, CL&C 2010, EPTCS 47, pages 57–72, Brno, Czech Republic, 2010.
[13] D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series. Kluwer Academic Publishers, 2002.

Logo d'Inria