Bridging Causal Consistent and Time Reversibility: A Stochastic Process Algebraic Approach

Causal consistent reversibility blends causality and reversibility. For a concurrent system, it says that an action can be undone provided that this has no consequences, thereby making it possible to bring the system back to a past consistent state. Time reversibility is instead considered in the performance evaluation field, mostly for efficient analysis purposes. A continuous-time Markov chain is time reversible if its stochastic behavior remains the same when the direction of time is reversed. We study how to bridge these two theories of reversibility by showing the conditions under which both causal consistent reversibility and time reversibility can be ensured by construction. This is done in the setting of a stochastic process calculus, which is then equipped with a notion of stochastic bisimilarity accounting for both forward and backward directions.