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.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00519528 |
| Date | 16 November 2006 |
| Creators | Krivine, Jean |
| Publisher | Université Pierre et Marie Curie - Paris VI |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds