Causal Reversibility for Timed Process Calculi with Lazy/Eager Durationless Actions and Time Additivity

A reversible computing system features backward computations along which the effects of forward ones are undone when needed. This is accomplished by reverting executed actions from the last one. Since the last performed action may not be uniquely identifiable in a concurrent system, causal reversibility is considered: an executed action can be undone provided that all of its consequences have been undone already. We investigate causal reversibility in a timed setting by defining a reversible calculus in the style of Phillips and Ulidowski in which action execution is separated from time passing, actions can be lazy or eager, and time is described via numeric delays subject to time additivity. We show that the calculus meets causal reversibility through an adaptation of the technique of Lanese, Phillips, and Ulidowski that ensures a proper treatment of action laziness/eagerness as well as time-additive delays.