Normal view MARC view ISBD view

Axiomatisations et types pour des processus probabilistes et mobiles / par Yuxin Deng ; sous la direction de Davide Sangiorgi

Auteur principal : Deng, Yuxin, 1978-...Auteur secondaire : : Sangiorgi, Davide, 1964-...., Directeur de thèseAuteur secondaire collectivité : École nationale supérieure des mines, Paris, Organisme de soutenancePublication :2005Description : 1 vol. ( 168 p.) ; 30 cmClassification : 530Résumé : Cette thèse se concentre sur des bases théoriques utiles pour l’analyse d’algorithmes et de protocoles pour des systèmes répartis modernes. Deux caractéristiques importantes des modèles pour ces systèmes sont les probabilités et la mobilité typée : des probabilités peuvent être utilisées pour quantifier des comportements incertains ou imprévisibles, et des types peuvent être utilisés pour garantir des comportements sˆurs dans des systèmes mobiles. Dans cette thèse nous développons des techniques algébriques et des techniques basées sur les types pour l’étude comportementale des processus probabilistes et mobiles. Dans la première partie de la thèse nous étudions la théorie algébrique d’un calcul de processus qui combine les comportements non-déterministe et probabiliste dans le modèle des automates probabilistes proposés par Segala et Lynch. Nous considérons diverses équivalences comportementales fortes et faibles, et nous fournissons des axiomatisations complètes pour des processus à états finis, limitées à la récursion gardée dans le cas des équivalences faibles. Dans la deuxième partie de la thèse nous étudions la théorie algébrique du n-calcul en présence des types de capacités, qui sont très utiles dans les calculs de processus mobiles. Les types de capacités distinguent la capacité de lire sur un canal, la capacité d’écrire sur un canal, et la capacité de lire et d’écrire à la fois. Ils introduisent également une relation de sous-typage naturelle et puissante. Nous considérons deux variantes de la bisimilarité typée, dans leurs versions retardées et anticipées. Pour les deux variantes, nous donnons des axiomatisations complètes pour les termes fermés. Pour une des deux variantes, nous fournissons une axiomatisation complète pour tous les termes finis. Dans la dernière partie de la thèse nous développons des techniques basées sur les types pour vérifier la propriété de terminaison de certains processus mobiles..Bibliographie: Bibliogr. 110 réf..Thèse : .Sujet - Nom d'actualité : Maîtrise statistique des processus -- Thèses et écrits académiques ;Théorie des types -- Thèses et écrits académiques ;Probabilités -- Thèses et écrits académiques Sujet : axiomatisation ;Système réparti ;bisimilarité ;maîtrise statistique des processus ;calcul de processus ;types, théorie des ;mobilité typée
Current location Call number Status Notes Date due Barcode
Bib. Paris
EMP 153.273 CCL.TH.1133 Perdu Thèse en ligne. Manquant au 07/03/2018 LR EMP46634D
Bib. Paris
EMP 153.272 CCL.TH.1133 Available Thèse en ligne. EMP46635D
Sophia Antipolis
EMS T-CMA-059 Sur demande Thèse en ligne

Thèse en ligne sur pastel

Publication autorisée par le jury

Bibliogr. 110 réf.

Thèse de doctorat Sciences et génie des matériaux Paris, ENMP 2005

Cette thèse se concentre sur des bases théoriques utiles pour l’analyse d’algorithmes et de protocoles pour des systèmes répartis modernes. Deux caractéristiques importantes des modèles pour ces systèmes sont les probabilités et la mobilité typée : des probabilités peuvent être utilisées pour quantifier des comportements incertains ou imprévisibles, et des types peuvent être utilisés pour garantir des comportements sˆurs dans des systèmes mobiles. Dans cette thèse nous développons des techniques algébriques et des techniques basées sur les types pour l’étude comportementale des processus probabilistes et mobiles. Dans la première partie de la thèse nous étudions la théorie algébrique d’un calcul de processus qui combine les comportements non-déterministe et probabiliste dans le modèle des automates probabilistes proposés par Segala et Lynch. Nous considérons diverses équivalences comportementales fortes et faibles, et nous fournissons des axiomatisations complètes pour des processus à états finis, limitées à la récursion gardée dans le cas des équivalences faibles. Dans la deuxième partie de la thèse nous étudions la théorie algébrique du n-calcul en présence des types de capacités, qui sont très utiles dans les calculs de processus mobiles. Les types de capacités distinguent la capacité de lire sur un canal, la capacité d’écrire sur un canal, et la capacité de lire et d’écrire à la fois. Ils introduisent également une relation de sous-typage naturelle et puissante. Nous considérons deux variantes de la bisimilarité typée, dans leurs versions retardées et anticipées. Pour les deux variantes, nous donnons des axiomatisations complètes pour les termes fermés. Pour une des deux variantes, nous fournissons une axiomatisation complète pour tous les termes finis. Dans la dernière partie de la thèse nous développons des techniques basées sur les types pour vérifier la propriété de terminaison de certains processus mobiles.

Powered by Koha