π -calcul - π-calculus

En informatique théorique , le π- calcul (ou pi-calcul ) est un calcul de processus . Le π -calcul permet aux noms de canaux d'être communiqués le long des canaux eux-mêmes, et de cette manière, il est capable de décrire des calculs concurrents dont la configuration du réseau peut changer au cours du calcul.

Le π -calcul a peu de termes et est un langage petit mais expressif (voir § Syntaxe ). Programmes fonctionnels peuvent être codés dans le π -calcul, et le codage souligne la nature du dialogue de calcul, en établissant des liens avec la sémantique de jeu . Extensions du π -calcul, comme le calcul et appliqué spi π , ont réussi à raisonner sur des protocoles cryptographiques . Outre l'utilisation originale pour décrire les systèmes concurrents, le π- calcul a également été utilisé pour raisonner sur les processus commerciaux et la biologie moléculaire .

Définition informelle

Le π -calcul appartient à la famille des calculs de processus , formalismes mathématiques permettant de décrire et d'analyser les propriétés du calcul concurrent. En fait, le π- calcul, comme le λ-calcul , est si minimal qu'il ne contient pas de primitives telles que des nombres, des booléens, des structures de données, des variables, des fonctions, ou même les instructions de flux de contrôle habituelles (telles que if-then-else, while).

Constructions de processus

Au cœur du π -calcul se trouve la notion de nom . La simplicité du calcul réside dans le double rôle que jouent les noms en tant que canaux de communication et variables .

Les constructions de processus disponibles dans le calcul sont les suivantes (une définition précise est donnée dans la section suivante) :

• concurrency , écrit , où et sont deux processus ou threads exécutés simultanément.${\displaystyle P\mid Q}$${\style d'affichage P}$${\style d'affichage Q}$
• communication , où
  • le préfixe d'entrée est un processus attendant un message qui a été envoyé sur un canal de communication nommé avant de procéder comme , liant le nom reçu au nom x . Typiquement, cela modélise soit un processus attendant une communication du réseau, soit une étiquette utilisable une seule fois par une opération.${\style d'affichage c\gauche(x\droit).P}$${\style d'affichage c}$${\style d'affichage P}$cgoto c
  • le préfixe de sortie décrit que le nom est émis sur le canal avant de procéder comme . Typiquement, cela modélise soit l'envoi d'un message sur le réseau, soit une opération.${\displaystyle {\overline {c}}\langle y\rangle .P}$${\style d'affichage y}$${\style d'affichage c}$${\style d'affichage P}$goto c
• réplication , écrite , qui peut être considérée comme un processus qui peut toujours créer une nouvelle copie de . En règle générale, cela modélise soit un service réseau, soit une étiquette en attente d'un nombre quelconque d' opérations.${\style d'affichage !\,P}$${\style d'affichage P}$cgoto c
• création d'un nouveau nom , écrit , qui peut être vu comme un processus attribuant une nouvelle constante x à l' intérieur . Les constantes du π -calcul sont définies par leurs noms uniquement et sont toujours des canaux de communication. La création d'un nouveau nom dans un processus est également appelée restriction .${\style d'affichage \gauche(\nu x\droit)P}$${\style d'affichage P}$
• le processus nil, écrit , est un processus dont l'exécution est terminée et s'est arrêtée.${\style d'affichage 0}$

Bien que le minimalisme du π -calcul nous empêche d'écrire des programmes au sens normal, il est facile d'étendre le calcul. En particulier, il est facile de définir à la fois des structures de contrôle telles que la récursivité, les boucles et la composition séquentielle et des types de données tels que les fonctions du premier ordre, les valeurs de vérité , les listes et les entiers. De plus, les extensions du π -calcul ont été proposées qui prennent en compte la distribution de la cryptographie à clé publique. La appliquée π -calcul en raison de Abadi et Fournet [1] a mis ces différentes extensions sur une base formelle en étendant le π -calcul avec des types de données arbitraires.

Un petit exemple

Vous trouverez ci-dessous un petit exemple d'un processus composé de trois composants parallèles. Le nom de canal x n'est connu que par les deux premiers composants.

${\displaystyle {\begin{aligned}(\nu x)&\;(\;{\overline {x}}\langle z\rangle .\;0\\&\;|\;x(y).\ ;{\overline {y}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\ langle v\rangle .0\end{aligned}}}$

Les deux premiers composants sont capables de communiquer sur le canal x , et le nom y devient lié à z . La prochaine étape du processus est donc

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;{\overline {z}}\langle x\rangle .\;x(y).\ ;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .\;0\end{aligned}}}$

Notez que le y restant n'est pas affecté car il est défini dans une portée interne. Les deuxième et troisième composants parallèles peuvent maintenant communiquer sur le nom de canal z , et le nom v devient lié à x . La prochaine étape du processus est maintenant

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;x(y).\;0\\&\;|\;{\overline {x }}\langle x\rangle .\;0\;)\end{aligned}}}$

Notez que puisque le nom local x a été affiché, la portée de x est étendue pour couvrir également le troisième composant. Enfin, le canal x peut être utilisé pour envoyer le nom x . Après cela, tous les processus en cours d'exécution se sont arrêtés

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;0\\&\;|\;0\;)\end{aligned}}}$

Définition formelle

Syntaxe

Soit Χ un ensemble d'objets appelés noms . La syntaxe abstraite du π -calcul est construite à partir de la grammaire BNF suivante (où x et y sont des noms quelconques de Χ) :

${\displaystyle {\begin{aligned}P,Q::=&\;x(y).P\,\,\,\,\,&{\text{Recevoir sur le canal }}x{\text{, lier le résultat à }}y{\text{, puis exécuter }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,& {\text{Envoyez la valeur }}y{\text{ sur le canal }}x{\text{, puis exécutez }}P\\&\;|\;P|Q\,\,\,\,\, \,\,\,\,&{\text{Exécuter }}P{\text{ et }}Q{\text{ simultanément}}\\&\;|\;(\nu x)P\,\, \,&{\text{Créez un nouveau canal }}x{\text{ et exécutez }}P\\&\;|\;!P\,\,\,&{\text{Faire des copies répétées de }} P\\&\;|\;0&{\text{Terminer le processus}}\end{aligned}}}$

Dans la syntaxe concrète ci-dessous, les préfixes se lient plus étroitement que la composition parallèle (|), et les parenthèses sont utilisées pour lever l'ambiguïté.

Les noms sont liés par les constructions de restriction et de préfixe d'entrée. Formellement, l'ensemble des noms libres d'un processus en π -calcul sont définis de manière inductive par le tableau ci - dessous. L'ensemble des noms liés d'un processus est défini comme les noms d'un processus qui ne figurent pas dans l'ensemble des noms libres.

Construction	Noms libres
${\style d'affichage 0}$	Rien
${\displaystyle {\overline {a}}\langle x\rangle .P}$	un ; x ; tous les noms libres de P
${\style d'affichage a(x).P}$	un ; noms libres de P sauf pour x
${\style d'affichage P|Q}$	Tous les noms libres de P et Q
${\style d'affichage (\nu x).P}$	Noms libres de P à l' exception de x
${\style d'affichage !P}$	Tous les noms libres de P

Congruence structurelle

Au centre de la sémantique de réduction et de la sémantique de transition étiquetée se trouve la notion de congruence structurelle . Deux processus sont structurellement congrus, s'ils sont identiques à structure près. En particulier, la composition parallèle est commutative et associative.

Plus précisément, la congruence structurelle est définie comme la relation de moindre équivalence conservée par les construits du processus et satisfaisant :

Alpha-conversion :

• ${\displaystyle P\équiv Q}$if peut être obtenu en renommant un ou plusieurs noms liés dans .${\style d'affichage Q}$${\style d'affichage P}$${\style d'affichage P}$

Axiomes pour la composition parallèle :

• ${\style d'affichage P|Q\équiv Q|P}$
• ${\style d'affichage (P|Q)|R\équiv P|(Q|R)}$
• ${\displaystyle P|0\équiv P}$

Axiomes de restriction :

• ${\style d'affichage (\nu x)(\nu y)P\equiv (\nu y)(\nu x)P}$
• ${\style d'affichage (\nu x)0\équiv 0}$

Axiome pour la réplication :

• ${\displaystyle !P\équiv P|!P}$

Axiome reliant restriction et parallèle :

• ${\style d'affichage (\nu x)(P|Q)\equiv (\nu x)P|Q}$si x n'est pas un nom libre de .${\style d'affichage Q}$

Ce dernier axiome est connu sous le nom d'axiome "d'extension de portée". Cet axiome est central, car il décrit comment un nom lié x peut être extrudé par une action de sortie, provoquant l'extension de la portée de x . Dans les cas où x est un nom libre de , la conversion alpha peut être utilisée pour permettre à l'extension de continuer. ${\style d'affichage Q}$

Sémantique de réduction

Nous écrivons si peut effectuer une étape de calcul, à la suite de laquelle c'est maintenant . Cette relation de réduction est définie comme la moindre relation fermée sous un ensemble de règles de réduction. ${\style d'affichage P\flèche droite P'}$${\style d'affichage P}$${\style d'affichage P'}$ ${\displaystyle \rightarrow }$

La principale règle de réduction qui capture la capacité des processus à communiquer via des canaux est la suivante :

• ${\displaystyle {\overline {x}}\langle z\rangle .P|x(y).Q\rightarrow P|Q[z/y]}$

où désigne le processus dans lequel le nom libre a été substitué aux occurrences libres de . Si une occurrence libre de se produit dans un emplacement où ne serait pas libre, une conversion alpha peut être requise.${\style d'affichage Q[z/y]}$${\style d'affichage Q}$${\style d'affichage z}$${\style d'affichage y}$${\style d'affichage y}$${\style d'affichage z}$

Il y a trois règles supplémentaires :

• Si alors aussi .${\displaystyle P\rightarrow Q}$${\displaystyle P|R\rightarrow Q|R}$

Cette règle dit que la composition parallèle n'empêche pas le calcul.

• Si , alors aussi .${\displaystyle P\rightarrow Q}$${\style d'affichage (\nu x)P\rightarrow (\nu x)Q}$

Cette règle garantit que le calcul peut se dérouler sous une restriction.

• Si et et , alors aussi .${\displaystyle P\équiv P'}$${\displaystyle P'\rightarrow Q'}$${\displaystyle Q'\équiv Q}$${\displaystyle P\rightarrow Q}$

Cette dernière règle stipule que les processus qui sont structurellement congruents ont les mêmes réductions.

L'exemple revisité

Considérez à nouveau le processus

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)| z(v).{\overline {v}}\langle v\rangle .0}$

En appliquant la définition de la sémantique de réduction, on obtient la réduction

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)| z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)| z(v).{\overline {v}}\langle v\rangle .0}$

Notez comment, en appliquant l'axiome de substitution de réduction, les occurrences libres de sont maintenant étiquetées comme . ${\style d'affichage y}$${\style d'affichage z}$

Ensuite, on obtient la réduction

${\displaystyle (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle . 0\rightarrow (\nu x)(0|x(y).0|{\overline {x}}\langle x\rangle .0)}$

Notez que puisque le nom local x a été affiché, la portée de x est étendue pour couvrir également le troisième composant. Cela a été capturé en utilisant l'axiome d'extension de portée.

Ensuite, en utilisant l'axiome de substitution de réduction, nous obtenons

${\style d'affichage (\nu x)(0|0|0)}$

Enfin, en utilisant les axiomes de composition parallèle et de restriction, nous obtenons

${\style d'affichage 0}$

Sémantique étiquetée

Alternativement, on peut donner au pi-calcul une sémantique de transition étiquetée (comme cela a été fait avec le calcul des systèmes communicants ).
Dans cette sémantique, une transition d'un état à un autre état après une action est notée comme : ${\style d'affichage P}$${\style d'affichage P'}$${\style d'affichage \alpha }$

• ${\displaystyle P\,{\xrightarrow {\overset {}{\alpha }}}P'}$

Lorsque les États et représentent des processus et est soit une action d'entrée , une action de sortie , ou une action silencieuse τ . ${\style d'affichage P}$${\style d'affichage P'}$${\style d'affichage \alpha }$ ${\style d'affichage a(x)}$ ${\displaystyle {\overline {a}}\langle x\rangle }$

Un résultat standard concernant la sémantique étiquetée est qu'elle s'accorde avec la sémantique de réduction jusqu'à la congruence structurelle, en ce sens que si et seulement si ${\style d'affichage P\flèche droite P'}$${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$

Extensions et variantes

La syntaxe donnée ci-dessus est minimale. Cependant, la syntaxe peut être modifiée de diverses manières.

Un opérateur de choix non déterministe peut être ajouté à la syntaxe. ${\style d'affichage P+Q}$

Un test d' égalité des noms peut être ajouté à la syntaxe. Cet opérateur de correspondance peut procéder comme si et seulement si x et étaient le même nom. De même, on peut ajouter un opérateur de non - concordance pour l' inégalité de nom . Les programmes pratiques qui peuvent transmettre des noms (URL ou pointeurs) utilisent souvent une telle fonctionnalité : pour modéliser directement une telle fonctionnalité à l'intérieur du calcul, cette fonctionnalité et les extensions associées sont souvent utiles. ${\style d'affichage [x=y]P}$${\style d'affichage P}$${\style d'affichage y}$

Le π -calcul asynchrone ne permet que des sorties sans suffixe, c'est-à-dire des atomes de sortie de la forme , ce qui donne un calcul plus petit. Cependant, tout processus du calcul d'origine peut être représenté par le plus petit π -calcul asynchrone utilisant un canal supplémentaire pour simuler un accusé de réception explicite du processus de réception. Puisqu'une sortie sans continuation peut modéliser un message en transit, ce fragment montre que le π -calcul original , qui est intuitivement basé sur la communication synchrone, a un modèle de communication asynchrone expressif dans sa syntaxe. Cependant, l'opérateur de choix non déterministe défini ci-dessus ne peut pas être exprimé de cette manière, car un choix non gardé serait converti en un choix gardé ; ce fait a été utilisé pour démontrer que le calcul asynchrone est strictement moins expressif que le synchrone (avec l'opérateur de choix). ${\displaystyle {\overline {x}}\langle y\rangle }$

Le polyadique π -calcul permet de communiquer plus d'un nom dans une seule action: (sortie polyadique) et (entrée polyadique) . Cette extension polyadique, qui est particulièrement utile lors de l'étude des types pour les processus de passage de noms, peut être encodée dans le calcul monadique en passant le nom d'un canal privé par lequel les multiples arguments sont ensuite passés en séquence. L'encodage est défini récursivement par les clauses ${\displaystyle {\overline {x}}\langle z_{1},...,z_{n}\rangle .P}$ ${\style d'affichage x(z_{1},...,z_{n}).P}$

${\displaystyle {\overline {x}}\langle y_{1},\cdots ,y_{n}\rangle .P}$ est codé comme ${\displaystyle (\nu w){\overline {x}}\langle w\rangle .{\overline {w}}\langle y_{1}\rangle .\cdots .{\overline {w}}\langle y_ {n}\rangle .[P]}$

${\displaystyle x(y_{1},\cdots ,y_{n}).P}$ est codé comme ${\displaystyle x(w).w(y_{1}).\cdots .w(y_{n}).[P]}$

Toutes les autres constructions de processus sont laissées inchangées par le codage.

Dans ce qui précède, désigne le codage de tous les préfixes de la suite de la même manière. ${\style d'affichage [P]}$${\style d'affichage P}$

La pleine puissance de réplication n'est pas nécessaire. Souvent, on ne considère que l'entrée répliquée , dont l'axiome de congruence structurelle est . ${\style d'affichage !P}$ ${\style d'affichage !x(y).P}$${\style d'affichage !x(y).P\équiv x(y).P|!x(y).P}$

Processus d'entrée répliqué tel qu'il peut être compris comme des serveurs, attendant sur le canal x d'être appelé par les clients. L'invocation d'un serveur génère une nouvelle copie du processus , où a est le nom passé par le client au serveur, lors de l'invocation de ce dernier. ${\style d'affichage !x(y).P}$${\displaystyle P[a/y]}$

Un π -calcul d' ordre supérieur peut être défini où non seulement les noms mais les processus sont envoyés via des canaux. La règle de réduction clé pour le cas d'ordre supérieur est

${\displaystyle {\overline {x}}\langle R\rangle .P|x(Y).Q\rightarrow P|Q[R/Y]}$

Ici, désigne une variable de processus qui peut être instanciée par un terme de processus. Sangiorgi a établi que la capacité de passer des processus n'augmente pas l'expressivité du π -calcul : passer un processus P peut être simulé en passant simplement un nom qui pointe vers P à la place. ${\style d'affichage Y}$

Propriétés

Complétude de Turing

Le π- calcul est un modèle de calcul universel . Cela a été observé pour la première fois par Milner dans son article "Functions as Processes", dans lequel il présente deux codages du lambda-calcul dans le π -calcul. Un encodage simule la stratégie d'évaluation impatiente (appel par valeur) , l'autre encodage simule la stratégie d' ordre normal (appel par nom). Dans ces deux cas, l'idée cruciale est la modélisation des liaisons d'environnement - par exemple, " x est lié au terme " - en tant qu'agents de réplication qui répondent aux demandes de leurs liaisons en renvoyant une connexion au terme . ${\styletexte M}$${\style d'affichage M}$

Les caractéristiques du π -calcul qui rendent ces codages possibles sont le passage de noms et la réplication (ou, de manière équivalente, des agents définis de manière récursive). En l'absence de réplication / récursion, le π -calcul cesse d'être Turing -complete. Cela peut être vu par le fait que l' équivalence de bisimulation devient décidable pour le calcul sans récursivité et même pour le π -calcul à contrôle fini où le nombre de composants parallèles dans tout processus est limité par une constante.

Bisimulations dans le π -calcul

Comme pour les calculs de processus, le π -calcul permet une définition de l'équivalence de bisimulation. Dans le π -calcul, la définition de l'équivalence de bisimulation (également connue sous le nom de bisimilarité) peut être basée soit sur la sémantique de réduction, soit sur la sémantique de transition étiquetée.

Il existe (au moins) trois manières différentes de définir l' équivalence de bisimulation étiquetée dans le π -calcul : Bisimilarité précoce, tardive et ouverte. Cela vient du fait que le π -calcul est un calcul de processus de passage de valeur.

Dans le reste de cette section, nous laissons et désignons les processus et désignons les relations binaires sur les processus. ${\style d'affichage p}$${\style d'affichage q}$${\style d'affichage R}$

Bisimilarité précoce et tardive

La bisimilarité précoce et tardive ont toutes deux été formulées par Milner, Parrow et Walker dans leur article original sur le π -calcul.

Une relation binaire sur les processus est une bisimulation précoce si pour chaque paire de processus , ${\style d'affichage R}$${\style d'affichage (p,q)\dans R}$

• chaque fois qu'alors pour chaque nom il en existe tel que et ;${\displaystyle p\,{\xrightarrow {a(x)}}\,p'}$${\style d'affichage y}$${\style d'affichage q'}$${\displaystyle q\,{\xrightarrow {a(x)}}\,q'}$${\style d'affichage (p'[y/x],q'[y/x])\in R}$
• pour toute action sans entrée , s'il existe alors une telle que et ;${\style d'affichage \alpha }$${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$${\style d'affichage q'}$${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$${\style d'affichage (p',q')\dans R}$
• et exigences symétriques avec et échangées.${\style d'affichage p}$${\style d'affichage q}$

Les processus et sont dits bissimilaires précoces, écrits si la paire pour une bisimulation précoce . ${\style d'affichage p}$${\style d'affichage q}$${\displaystyle p\sim _{e}q}$${\style d'affichage (p,q)\dans R}$${\style d'affichage R}$

En cas de bisimilarité tardive, la correspondance de transition doit être indépendante du nom transmis. Une relation binaire sur les processus est une bisimulation tardive si pour chaque paire de processus , ${\style d'affichage R}$${\style d'affichage (p,q)\dans R}$

• chaque fois qu'alors pour certains, il détient cela et pour chaque nom y ;${\displaystyle p{\xrightarrow {a(x)}}p'}$${\style d'affichage q'}$${\displaystyle q{\xrightarrow {a(x)}}q'}$${\style d'affichage (p'[y/x],q'[y/x])\in R}$
• pour toute action de non-entrée , si implique qu'il existe un tel que et ;${\style d'affichage \alpha }$${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$${\style d'affichage q'}$${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$${\style d'affichage (p',q')\dans R}$
• et exigences symétriques avec et échangées.${\style d'affichage p}$${\style d'affichage q}$

Les processus et sont dits bissimilaires tardifs, écrits si la paire pour une bisimulation tardive . ${\style d'affichage p}$${\style d'affichage q}$${\displaystyle p\sim _{l}q}$${\style d'affichage (p,q)\dans R}$${\style d'affichage R}$

Les deux et souffrent du problème qu'ils ne sont pas des relations de congruence dans le sens où ils ne sont pas préservés par toutes les constructions de processus. Plus précisément, il existe des procédés et tels que mais . On peut remédier à ce problème en considérant les relations de congruence maximale incluses dans et , appelées respectivement congruence précoce et congruence tardive . ${\displaystyle \sim _{e}}$${\displaystyle \sim _{l}}$${\style d'affichage p}$${\style d'affichage q}$${\displaystyle p\sim _{e}q}$${\displaystyle a(x).p\pas \sim _{e}a(x).q}$${\displaystyle \sim _{e}}$${\displaystyle \sim _{l}}$

Bisimilarité ouverte

Heureusement, une troisième définition est possible, qui évite ce problème, à savoir celle de la bissimilarité ouverte , due à Sangiorgi.

Une relation binaire sur les processus est une bisimulation ouverte si pour chaque paire d'éléments et pour chaque substitution de nom et chaque action , chaque fois qu'il en existe un tel que et . ${\style d'affichage R}$${\style d'affichage (p,q)\dans R}$${\style d'affichage \sigma }$${\style d'affichage \alpha }$${\displaystyle p\sigma {\xrightarrow {\overset {}{\alpha }}}p'}$${\style d'affichage q'}$${\displaystyle q\sigma {\xrightarrow {\overset {}{\alpha }}}q'}$${\style d'affichage (p',q')\dans R}$

Les processus et sont dits bissimilaires ouverts, écrits si la paire pour une bisimulation ouverte . ${\style d'affichage p}$${\style d'affichage q}$${\displaystyle p\sim _{o}q}$${\style d'affichage (p,q)\dans R}$${\style d'affichage R}$

Bisimilarité précoce, tardive et ouverte sont distinctes

Les bisimilarités précoces, tardives et ouvertes sont distinctes. Les confinements sont corrects, donc . ${\displaystyle \sim _{o}\subsetneq \sim _{l}\subsetneq \sim _{e}}$

Dans certains sous-calculs tels que le pi-calcul asynchrone, la bisimilarité tardive, précoce et ouverte est connue pour coïncider. Cependant, dans ce contexte, une notion plus appropriée est celle de bisimilarité asynchrone . Dans la littérature, le terme bisimulation ouverte fait généralement référence à une notion plus sophistiquée, où les processus et les relations sont indexés par des relations de distinction ; les détails sont dans l'article de Sangiorgi cité ci-dessus.

Équivalence barbelée

Alternativement, on peut définir l'équivalence de bisimulation directement à partir de la sémantique de réduction. Nous écrivons si le processus autorise immédiatement une entrée ou une sortie sur name . ${\displaystyle p\Downarrow a}$${\style d'affichage p}$${\style d'affichage a}$

Une relation binaire sur les processus est une bisimulation barbelée si c'est une relation symétrique qui satisfait que pour chaque paire d'éléments nous avons que ${\style d'affichage R}$${\style d'affichage (p,q)\dans R}$

(1) si et seulement si pour chaque nom${\displaystyle p\Downarrow a}$${\displaystyle q\Downarrow a}$${\style d'affichage a}$

et

(2) pour chaque réduction il existe une réduction${\displaystyle p\rightarrow p'}$${\displaystyle q\rightarrow q'}$

tel que . ${\style d'affichage (p',q')\dans R}$

On dit que et sont bisimilaires barbelés s'il existe une bisimulation barbelée où . ${\style d'affichage p}$${\style d'affichage q}$${\style d'affichage R}$${\style d'affichage (p,q)\dans R}$

En définissant un contexte comme un terme π avec un trou [], nous disons que deux processus P et Q sont barbelés congrus , écrits , si pour chaque contexte nous avons cela et sont barbelés bissimilaires. Il s'avère que la congruence barbelée coïncide avec la congruence induite par la bissimilarité précoce. ${\displaystyle P\sim _{b}Q\,\!}$${\style d'affichage C[]}$${\style d'affichage C[P]}$${\style d'affichage C[Q]}$

Applications

Le π -calcul a été utilisé pour décrire de nombreux types de systèmes concurrents. En fait, certaines des applications les plus récentes se situent en dehors du domaine de l'informatique traditionnelle.

En 1997, Martin Abadi et Andrew Gordon ont proposé une extension du π -calcul, le Spi-calcul, en tant que notation formelle pour décrire et raisonner sur les protocoles cryptographiques. Le spi-calcul étend le π -calcul avec des primitives pour le chiffrement et le déchiffrement. En 2001, Martin Abadi et Cédric Fournet ont généralisé la manipulation des protocoles cryptographiques pour produire le calcul π appliqué . Il existe maintenant un grand nombre de travaux consacrés aux variantes du calcul π appliqué , y compris un certain nombre d'outils de vérification expérimentale. Un exemple est l'outil ProVerif [2] de Bruno Blanchet, basé sur une traduction du π -calcul appliqué dans le cadre de programmation logique de Blanchet. Un autre exemple est Cryptyc [3] , dû à Andrew Gordon et Alan Jeffrey, qui utilise la méthode d'assertions de correspondance de Woo et Lam comme base pour les systèmes de types qui peuvent vérifier les propriétés d'authentification des protocoles cryptographiques.

Vers 2002, Howard Smith et Peter Fingar se sont intéressés au fait que le π -calcul deviendrait un outil de description pour la modélisation des processus métier. En juillet 2006, il y a une discussion dans la communauté sur l'utilité de cela. Plus récemment, le π -calcul a constitué la base théorique du langage de modélisation des processus métier (BPML) et du XLANG de Microsoft.

Le π -calcul a également suscité l'intérêt en biologie moléculaire. En 1999, Aviv Regev et Ehud Shapiro ont montré que l'on peut décrire une voie de signalisation cellulaire (la cascade dite RTK / MAPK ) et en particulier le « lego » moléculaire qui met en œuvre ces tâches de communication dans une extension du π -calcul. À la suite de cet article fondateur, d'autres auteurs ont décrit l'ensemble du réseau métabolique d'une cellule minimale. En 2009, Anthony Nash et Sara Kalvala ont proposé un cadre de calcul π pour modéliser la transduction du signal qui dirige l' agrégation de Dictyostelium discoideum .

Histoire

Le π- calcul a été développé à l'origine par Robin Milner , Joachim Parrow et David Walker en 1992, sur la base des idées d'Uffe Engberg et de Mogens Nielsen. Il peut être vu comme une continuation des travaux de Milner sur le calcul des processus CCS ( Calculus of Communicating Systems ). Dans sa conférence de Turing, Milner décrit le développement du π -calcul comme une tentative de capturer l'uniformité des valeurs et des processus chez les acteurs.

Implémentations

Les langages de programmation suivants implémentent le π -calcul ou l'une de ses variantes :

• Langage de modélisation des processus métier (BPML)
• occam-π
• Pict
• JoCaml (basé sur le Join-calcul )
• RhoLang

Remarques

Les références

• Milner, Robin (1999). Systèmes communicants et mobiles : le π-calcul . Cambridge, Royaume-Uni : Cambridge University Press. ISBN 0-521-65869-1.
• Milner, Robin (1993). "Le π-Calcul polyadique : Un Tutoriel" . Dans FL Hamer; W. Brauer ; H. Schwichtenberg (éd.). Logique et algèbre de spécification . Springer-Verlag.
• Sangiorgi, Davide ; Walker, David (2001). Le π-calcul : une théorie des processus mobiles . Cambridge, Royaume-Uni : Cambridge University Press. ISBN 0-521-78177-9.

Liens externes

• PiCalculus sur le wiki C2
• FAQ sur π-Calculus par Jeannette M. Wing