Processus non-standard: Analyse, Coinduction, Expressivité – PACE

L'application de techniques coinductives pour représenter et analyser le comportement de processus non standard est au cœur du projet PACE.
C'est à partir de celles-ci que nous développerons de nouvelles méthodes algorithmiques pour raisonner sur les propriétés des systèmes, en nous appuyant sur des résultats d'expressivité. Ces trois éléments, la coinduction, l'expressivité et les techniques pour l'analyse de propriétés comportementales, structurent le projet PACEet agencent nos travaux.

Le projet PACE débouchera sur les résultats suivants:
- l'étude de notions coinductives d'équivalences et préordres pour les processus non standard, et la définition de techniques de preuve pertinentes pour ces relations;
- une perspective unificatrice sur diverses formes d'interaction à l'œuvre dans les processus non standard, du point de vue de leur expressivité;
- la définition de techniques d'analyse des processus non standard se fondant sur les résultats ci-dessus.

Les perspectives ouvertes par le projet PACE sont essentiellement de
deux sortes:
- d'une part, une meilleure compréhension de diverses formes d'interaction non standard: leur pouvoir expressif, la notion de comportement qu'elles déterminent, et les méthodes qui peuvent être mises en œuvre pour en analyser les propriétés;
- d'autre part, et ce faisant, une extension du domaine d'applicabilité de l'approche coinductive pour l'analyse des systèmes.

Nous comptons publier nos résultats dans des actes de conférences
internationales et des journaux. Le cas échéant, nous pourrons
développer des implémentations prototypes permettant d'illustrer et
d'évaluer les méthodes algorithmiques proposées dans PACE.
Nous n'envisageons pas que nos travaux débouchent sur des dépôts de
brevets.

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.