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, and abstract models such as 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 various reversibility properties. In particular, we show how all properties we consider 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 properties related to causal consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.

翻译：对并发系统的计算进行撤销在许多场景中是有益的，例如多线程程序的可逆调试，以及由于乐观执行导致的并行离散事件模拟错误恢复。已有多种方法提出用于逆转并发计算的形式化模型，包括CCS这样的进程演算、Erlang等语言，以及诸如主事件结构和发生网之类的抽象模型。然而，可逆系统应具备何种性质，以及所提出的各种性质（如抛物线引理和因果一致性）之间的关系尚未明确。我们通过使用一个配备表示变迁是否独立的关系的通用带标号变迁系统，探索各种可逆性质之间的蕴含关系，从而为这些问题的解决做出贡献。特别地，我们展示了如何从一组公理中推导出所有考虑的性质。我们的意图是，在建立某种形式体系的性质时，验证这些公理将比直接证明抛物线引理等性质更为简便。我们还引入了与因果一致可逆相关的两个新性质，即因果活性和因果安全性，分别表明：当且仅当一个动作与所有后续动作独立时，该动作可被撤销（因果活性对应“若”条件，因果安全性对应“仅当”条件）。这些性质具有三种形式：基于独立变迁定义、基于独立事件定义，或通过事件上的序关系定义。因果活性和因果安全性均可从我们的公理中推导得出。