Causal Reversibility in Nondeterministic Process Calculi Extended with Time or Probabilities

In addition to forward computations, a reversible system also features backward computations along which the effects of forward ones can be undone. This is accomplished by reverting executed actions starting from the last one. Since the last performed action may not be uniquely identifiable in a concurrent setting, Danos and Krivine proposed causal reversibility: an executed action can be undone provided that all of its consequences have been undone already. Phillips and Ulidowski then showed how to define nondeterministic process calculi that meet causal reversibility by construction. Lanese, Phillips, and Ulidowski subsequently classified the basic properties that ensure causal reversibility. In this paper we investigate the extent to which those techniques apply to reversible nondeterministic process calculi that include quantitative aspects. Firstly, we consider the introduction of time described via numeric delays with action execution separated from time passing like in the calculus of Moller and Tofts, where actions can be lazy or eager and time is subject to time determinism and time additivity. Secondly, we address the introduction of probabilities like in the calculus of Hansson and Jonsson, in which action execution and probabilistic choices alternate. We show that both resulting reversible calculi satisfy causal reversibility provided that suitable variants of the aforementioned techniques are developed to guarantee the proper forward and backward interplay of nondeterminism and quantitative aspects. The use of the former calculus is illustrated on a timeout mechanism, whereas the use of the latter is exemplified on quantum teleportation.