these

Informations

• Publié par: Zyof
• Nombre de lectures: 23
• Langue: Français

Extrait

UNIVERSITE DE GRENOBLE
Nattribue par la bibliotheque
THESE
pour obtenir le grade de
DOCTEUR DE l’UNIVERSITE DE GRENOBLE
Specialite : Informatique
preparee au laboratoire LIG, projet SARDES,
dans le cadre de l’Ecole Doctorale
Mathematiques Sciences et Technologies de l’Information, Informatique
presentee et soutenue publiquement par
Sergue Lenglet
le 15 Janvier 2010
Bisimulations dans les calculs avec
passivation
Directeur de these :
Jean-Bernard Stefani
JURY
M. Pierre-Louis Curien President
M. Matthew Hennessy Rapporteur
M. Davide Sangiorgi Rapp
M. Jean-Fran cois Monin Examinateur
M. Francesco Zappa Nardelli
M. Jean-Bernard Stefani Directeur de these
M. Alan Schmitt Co-Directeur de thesea AndrianRemerciements
Je remercie Alan Schmitt et Jean-Bernard Stefani pour la presence et le soutien dont
ils ont fait preuve tout au long de cette these. Nos echanges m’ont permis de me poser les
bonnes questions et de corriger mes erreurs. Merci pour toutes ces discussions, scienti ques
ou non, qui ont participe a rendre agreables ces annees de these.
Merci a l’ensemble des membres du jury, en particulier a Pierre-Louis Curien, qui
a accepte d’en ^etre le president, ainsi qu’ a Matthew Hennessy et Davide Sangiorgi, qui
ont bien voulu relire cette these, et dont les commentaires m’ont permis de sensiblement
ameliorer ce document.
Merci a Daniel Hirschko et Tom Hirschowitz, comme enseignants d’abord, pour
m’avoir donne le gout^ de la recherche en informatique theorique, mais egalement pour
s’^etre interesses a mes travaux et pour m’avoir force a m’exprimer autrement que par
monosyllabes.
Merci au projet Sardes de m’avoir accueilli et pour l’ambiance qui regne au sein de
l’equipe. Merci pour les seminaires et les tablees de vingt personnes a midi qui participent
a la bonne humeur generale. Merci a Beno^ t, Fabien 2, Jean, Michael, Stephane, Syl-
vain, Willy, etc. pour les parties de Tetrinet, Diplomacy, Wormux (bien que Worms soit
meilleur), Can’t Stop, etc. Merci a Thomas pour son niveau a Starcraft, et a Damien pour
la technique du mass dropships. Merci a tous les membres de l’equipe que j’ai pu c^otoyer,
joueurs ou non.
Merci a Aurelien et Romain, ma^ tres en humour potache.
En n, merci a la ville de Grenoble, son air pur, son climat tempere, et ses prix de
l’immobilier abordables. Merci a l’INRIA de s’^etre installe a Montbonnot, un site parti-
culierement bien desservi par les transports publics, surtout pour ceux qui, comme moi,
partent au travail des l’aube.Table des matieres
1 Introduction 1
1.1 Calculs de processus et passivation . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Equivalences comportementales . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.4 Organisation du document . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2 Bisimulations dans les calculs d’ordre superieur 5
2.1 Le calcul HO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.1.1 Syntaxe et semantique informelle . . . . . . . . . . . . . . . . . . . . 5
2.1.2 Systeme de transitions etiquetees . . . . . . . . . . . . . . . . . . . . 7
2.2 Theorie comportementale pour HO . . . . . . . . . . . . . . . . . . . . . . 9
2.2.1 Congruence barbue . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2.2 Bisimilarite d’ordre superieur . . . . . . . . . . . . . . . . . . . . . . 10
2.2.3e contextuelle . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.4 Bisimilarite normale . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Equivalences dans les calculs avec passivation . . . . . . . . . . . . . . . . . 16
2.3.1 Syntaxe et semantique de HOP . . . . . . . . . . . . . . . . . . . . 16
2.3.2 Bisimilarite contextuelle . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.4 Etat de l’art et conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.4.1 Le calcul minimal HOcore . . . . . . . . . . . . . . . . . . . . . . . 19
2.4.2 Les calculs CHOCS et Plain CHOCS . . . . . . . . . . . . . . . . . . 20
2.4.3 Les Ambients . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.4.4 Le Seal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.4.5 Les calculs avec passivation . . . . . . . . . . . . . . . . . . . . . . . 21
2.4.6 Bisimilarite environnementale . . . . . . . . . . . . . . . . . . . . . . 22
2.4.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3 Bisimulation normale 25
3.1 Bisimulation pour HOP . . . . . . . . . . . . . . . . . . . . . . . . 25
3.1.1 Bisimulation d’ordre superieur . . . . . . . . . . . . . . . . . . . . . 25
3.1.2 Bisimilarite normale . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.2 Equivalence de fonctions pour HOP . . . . . . . . . . . . . . . . . . . . . . 31
3.2.1 Les processus sans reception . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.2 Processus nis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.2.3 Contre-exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4 Preuves de congruence 37
4.1 Preuve classique pour HO . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2e par progression . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4.3 Methode de Howe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.3.1 Resume de la methode . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3.2 Probleme avec la communication d’ordre superieur . . . . . . . . . . 444.4 Autres methodes et conclusions . . . . . . . . . . . . . . . . . . . . . . . . . 45
5 Semantique a complement 47
5.1 Semantique a complement pour HO . . . . . . . . . . . . . . . . . . . . . . 47
5.1.1 Systeme de transitions etiquetees a complement . . . . . . . . . . . . 47
5.1.2 Bisimulation associee . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5.2 Application a HOP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.2.1 Systeme de transitions etiquetees a complement . . . . . . . . . . . . 51
5.2.2 Bisimulation a complement . . . . . . . . . . . . . . . . . . . . . . . 53
5.3 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
6 Application au Kell-calcul 57
6.1 Recepteurs joints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
6.1.1 Le calcul HOJ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
6.1.2 Semantique a complement . . . . . . . . . . . . . . . . . . . . . . . . 59
6.1.3 Bisimilarite aement . . . . . . . . . . . . . . . . . . . . . . . . 63
6.2 Semantique a complement du Kell . . . . . . . . . . . . . . . . . . . . . . . 64
6.2.1 Presentation du Kell . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
6.2.2 Syntaxe et semantique contextuelle . . . . . . . . . . . . . . . . . . . 65
6.2.3 Semantique a complement : principe . . . . . . . . . . . . . . . . . . 68
6.2.4 Transitions inferieures . . . . . . . . . . . . . . . . . . . . . . . . . . 69
6.2.5 T sup . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.2.6 Actions internes et jugements d’observation . . . . . . . . . . . . . . 75
6.2.7 Bisimilarite a complement . . . . . . . . . . . . . . . . . . . . . . . . 77
6.3 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
7 Conclusions et perspectives 81
A Semantique a complement 89
A.1 Resultats generaux sur la methode de Howe . . . . . . . . . . . . . . . . . . 89
A.2 Preuves pour HO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
A.2.1 Correspondance des systemes de transitions . . . . . . . . . . . . . . 90
A.2.2 Congruence de la bisimilarite a complement . . . . . . . . . . . . . . 92
A.2.3 Correspondance deses . . . . . . . . . . . . . . . . . . . . 94
A.3 Preuves pour HOP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
A.3.1 Correspondance des systemes de transitions . . . . . . . . . . . . . . 95
A.3.2 Congruence de la bisimilarite a complement . . . . . . . . . . . . . . 98
A.3.3 Correspondance deses . . . . . . . . . . . . . . . . . . . . 101
A.3.4 Completude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
A.4 Preuves pour HOJ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
A.5es pour le Kell . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
A.5.1 Systeme de transitions a complement . . . . . . . . . . . . . . . . . . 111
A.5.2 Congruence de la bisimilarite a complement . . . . . . . . . . . . . . 115
B Preuves pour HOP 121
B.1 Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
B.2 Bisimilarite normale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
C Equivalences de fonctions en HOP 127Chapitre 1
Introduction
1.1 Calculs de processus et passivation
Les systemes distribues sont constitues de nombreuses entites, de natures di erentes,
qui peuvent evoluer independamment et interagir entre elles, et dont la con guration peut
changer dynamiquement. Decrire et raisonner sur les comportements de tels systemes
necessite une modelisation qui fasse abstraction le plus possible de la nature des com-
posants p