Algèbres de Processus Réversibles

We propose a notion of distributed backtracking built on top of Milner's Calculus of Communicating Systems. This reversible process al- gebra (RCCS) offers a clear-cut theoretical characterisation of reversibility. In particular, given a process and a past, we show that RCCS allows to backtrack along any causally equivalent past. We express behavioural equi- valence of reversible processes in terms of simple bisimimulation of causal transition systems. This results in a declarative way of programming dis- tributed transactional systems that can be efficiently model-checked using an event structure based algorithm. Using a categorical abstraction we then show that this method can be generalised for a wide range of concurrent calculus.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