Return to search

Algèbres de Processus Réversibles

Nous présentons un système de retour arrière distribué basé sur le Calcul des Systèmes Communicants de Robin Milner. L'algèbre de pro- cessus réversible ainsi définie (RCCS) nous permet de poser les fondements théoriques du retour arrière dans un calcul concurrent. En particulier, étant donné un processus et un passé, nous montrons que RCCS permet de re- venir en arrière dans tout passé causalement équivalent. Nous exprimons aussi l'équivalence comportementale associée aux processus réversibles en utilisant une notion de bisimulation mettant en relation les traces causales des processus. Il en résulte une méthode de programmation déclarative de systèmes transactionnels qui peuvent être efficacement vérifiés à l'aide d'un algorithme basé sur des structures d'événements. Par l'intermédiaire d'une construction catégorique, nous montrons que cette méthode peut être géné- ralisée à une large classe de calculs concurrents.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00519528
Date16 November 2006
CreatorsKrivine, Jean
PublisherUniversité Pierre et Marie Curie - Paris VI
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0019 seconds