论文标题
可逆的早期内部Pi-Calculus的事件结构
Event structures for the reversible early internal Pi-calculus
论文作者
论文摘要
Pi-Calculus是一种广泛使用的过程演算，它在过程之间进行通信并允许通过通信链接进行通信。已经提出了PI-Calculus的各种操作语义，可以根据过渡是未标记的（所谓的减少）或标记的。通过标记的过渡，我们可以区分早期和晚期语义。早期版本允许一个过程从环境中接收名称，而后期语义和简化语义则没有。尽管（仅远期）Pi-Calculus的早期语义比晚期更广泛使用，但PI-Calculus的所有现有可逆版本都使用降低或晚期语义。我们定义了PIIH，这是第一个可逆的早期Pi-calculus，并就可逆的捆绑捆绑事件结构赋予了它的典型语义。新的演算是内部pi-calculus的可逆形式，这是PI-Calculus的一个子集，其中每个由输出发送的每个链接都是私有的，在输入和输出之间产生更大的对称性。
The pi-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the pi-calculus have been proposed, which can be classified according to whether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a process to receive names it already knows from the environment, while the late semantics and reduction semantics do not. All existing reversible versions of the pi-calculus use reduction or late semantics, despite the early semantics of the (forward-only) pi-calculus being more widely used than the late. We define piIH, the first reversible early pi-calculus, and give it a denotational semantics in terms of reversible bundle event structures. The new calculus is a reversible form of the internal pi-calculus, which is a subset of the pi-calculus where every link sent by an output is private, yielding greater symmetry between inputs and outputs.
