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.
A Reversible Perspective on Petri Nets and Event Structures
ICC - Universidad de Buenos Aires, Conicet（布宜诺斯艾利斯大学计算机研究所（CONICET））；Dipartimento di Scienze Pure e Applicate, Università di Urbino（乌尔比诺大学纯科学与应用科学系）；Dipartimento di Matematica e Informatica, Università di Cagliari（卡利亚里大学数学与信息科学系）
Axiomatic approach to the theory of algorithms and relativized computability
众所周知，递归论中的许多定理都可以“相对化”。这意味着，如果部分递归函数被相对于某个固定的Oracle集是部分递归的函数所替换，则它们仍然为真。乌斯彭斯基制定了三个“公理”，称为“计算记录公理”、“程序公理”和“算术性公理”。然后，使用这些公理（更确切地说，前两个），他证明了基本结果的递归论。这两个公理对于相对于某个固定的预言集是部分递归的函数类也是正确的。这个类在替换、原始递归式和最小化（$μ$ -运算符）下也是封闭的;这些（直观上显而易见的）封闭性也用于证明中。这一观察所作出的乌斯彭斯基解释了为什么许多定理的递归论可以相对化。事实证明，相反的陈述也是正确的：所有可相对化的结果都遵循前两个公理和封闭性。没错，就是\emph{every class of partial functions that is closed under substitution, primitive recursion and minimization that satisfies the first two axioms is the class of functions that are partial recursive relative to some oracle set $A$}。这是本文的主要结果。
