Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between these properties. In particular, we show how they are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new notions related to causal consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if and only if it is independent from all the following ones. We show that both causal liveness and causal safety are derivable from our axioms.

翻译：撤销并发系统中的计算在许多情况下非常有用，例如多线程程序的可逆调试以及并行离散事件模拟中因乐观执行导致的错误恢复。目前已有多种方法被提出用于反转并发计算的正式模型，包括进程演算（如CCS）、Erlang语言、原始事件结构以及发生网。然而，关于可逆系统应具备哪些性质，以及已提出的各种性质（如抛物线引理和因果一致性）之间的关系，尚未有明确结论。我们通过使用一个泛化的带标记迁移系统（配备捕捉变迁是否独立的二元关系），探索这些性质之间的蕴含关系，从而为这些问题提供解决方案。特别地，我们展示了这些性质如何从一组公理中推导得出。我们的意图是，在建立某种形式体系的性质时，验证这些公理将比直接证明抛物线引理等性质更为容易。此外，我们引入了与因果一致可逆性相关的两个新概念，即因果活性与因果安全性，分别表明：一个动作当且仅当与所有后续动作独立时方可被撤销。我们证明，因果活性与因果安全性均可从我们的公理中推导得出。