Reversibility in Process Calculi with Nondeterminism and Probabilities

A reversible system features not only forward computations, but also backward computations along which the effects of forward ones can be undone by starting from the last performed action. According to causal reversibility, an executed action can be undone provided that all the actions it caused have been undone already. We investigate causal reversibility in a nondeterministic and probabilistic setting by adapting the framework of Phillips and Ulidowski to define a reversible calculus in which action transitions and probabilistic transitions alternate in the style of Hansson and Jonsson. We show that the calculus meets causal reversibility through a suitable variant of the technique of Lanese, Phillips, and Ulidowski that ensures the proper forward and backward interplay of nondeterminism and probabilities. The use of the calculus is illustrated on a quantum computing example.