Quantitative Analysis of Concurrent Reversible Computations

Reversible computing is a paradigm of computation that extends the standard forward-only programming to reversible programming, so that programs can be executed both in the standard, forward direction, and backward, going back to past states. In this paper we present novel quantitative stochastic model for concurrent and cooperating computations. More precisely, we introduce the class of ρ-reversible stochastic automata and define a semantics for the synchronization ensuring that this class of models is closed under composition. For this class of automata we give an efficient way of deriving the equilibrium distribution. Moreover, we prove that the equilibrium distribution of the composition of reversible automata can be derived as the product of the equilibrium distributions of each automaton in isolation.