Projet ANR-12-IS02-0001 – PACE : Processus non-standard: Analyse, Coinduction, Expressivité
Programme : Blanc International II - SIMI 2 - Science informatique et applications (Blanc Inter II - SIMI 2) 2012
Année de financement : 2012
Coordinateur du projet : Monsieur Daniel Hirschkoff (Laboratoire de l'Informatique du Parallélisme, École Normale Supérieure de Lyon)
Partenaires : Inria Centre Paris - Rocquencourt; Inria Centre Sophia Antipolis - Méditerranée; Laboratoire d'Informatique du Parallélisme; Shanghai Communications University
Montant : 338416.0 euros
Date de début : 2013
Durée : 48 mois
Résumé : La coinduction, l'expressivité et les techniques d'analyse sont trois
ingrédients centraux dans la sémantique de la concurrence. La
coinduction permet de spécifier des processus et d'en prouver des
propriétés. L'application la plus répandue de la coinduction est la
bisimulation: la bisimilarité sert à étudier des équivalences
comportementales, et la bisimulation permet d'établir ce type
d'égalité. L'expressivité permet d'établir des relations formelles au
sein de la variété des modèles existants pour les processus, des
primitives que l'on peut définir sur les processus, et des
équivalences. Ce faisant, on peut en particulier distinguer entre
primitives essentielles et primitives dérivées; on peut également
étudier des questions d'implémentation, en mettant en relation un
aspect d'un langage avec des primitives se prêtant à une
implémentation directe. Enfin, les techniques d'analyse introduisent
des méthodes et des outils permettant d'établir des propriétés
comportementales des systèmes.
Ces trois notions -- coinduction, expressivité, techniques d'analyse -- sont au cœur du projet PACE. 
    Notre objectif est d'enrichir et d'adapter ces méthodes, au-delà des processus "traditionnels". 
En l'occurrence, nous nous intéressons à des modèles exhibant une combinaison parmi les traits
suivants: la présence de probabilités, l'ordre supérieur (la
communication de code), le quantique, les contraintes, la connaissance partagée,
et la confidentialité. Il s'agit là d'aspects dont l'importance est grandissante pour les
applications. Des formalismes ont déjà été introduits pour rendre
compte de certains de ces traits. Ceux-ci engendrent cependant des phénomèenes bien plus
complexes que dans la concurrence "traditionnelle", et nombreux sont les
aspects fondamentaux qui doivent encore être étudiés. Nous nous
attendons à ce que la coinduction joue un rôle central dans le
projet. En particulier, nous nous concentrerons sur une étude de
l'expressivité se fondant sur des équivalences coinductives, et sur
des techniques d'analyse exploitant des notions coinductives.
Les objectifs en lien avec la coinduction se déclinent suivant deux
axes. D'une part, nous souhaitons nous concentrer sur des propriétés
basiques de la coinduction dans des modèles comportant les traits
susmentionnés. Nous examinerons également une approche quantitative,
permettant d'analyser la "distance comportementale" entre deux
processus. D'autre part, nous souhaitons développer une théorie
générale et unificatrice pour les techniques "modulo", rendant compte
de leur application aux divers paradigmes étudiés au sein de PACE. La
nature algébrique de notre théorie devra permettre de combiner
diverses techniques afin d'en définir de nouvelles. Nous étudierons
aussi des applications de la coinduction à des questions de sécurité
et de confidentialité.
Nos travaux sur l'expressivité exploiteront les travaux fondateurs
dans ce domaine dûs à des membres du projet. Nous souhaitons
construire une théorie générale pour les traits pris en compte dans le
projet. Nous comptons également étudier des applications de ce cadre
général. En particulier, nous comparerons l'expressivité de divers
opérateurs permettant de décrire la connaissance partagée
distribuée. Nous voulons aussi exprimer des critères d'expressivité
dans des scenarii en lien avec la sécurité, où l'on souhaite garantir
des formes de protection de l'information.
Les travaux portant sur les techniques et les algorithmes pour
l'analyse des processus consisteront à développer des méthodes
permettant de valider de façon automatique ou semi-automatique des
équivalences coinductives développées au sein du projet PACE. Nous
souhaitons en particulier exploiter des techniques de preuve pour la
bisimulation, ainsi que des caractérisations symboliques ou des
approximations des bisimulations.