摘要
Chocs and π-calculus are two extensions of CCS where, respectively, processes and channels are transmissible values. In previous work we have proposed a formalization of the notion of bisimulation for Chocs. In this paper we suggest a more effective way to reason about this notion by means of an embedding of Chocs into a richer calculus endowed with a notion of ‘activation’ channel which we christen Chocst. is the name of a new internal action which is produced by a synchronization on an activation channel, such a synchronization has the effect of forcing the execution of an idle process. In first approximation transitions in Chocst may be understood as sequences of synchronizations along activation channels followed by an ‘observable’ transition. There is a simple definition of bisimulation for Chocst which satisfies natural laws and congruence rules, moreover the synchronization trees associated to Chocst processes are finitely branching. We propose Chocst as an intermediate step towards the definition of a tool for the verification of Chocs bisimulation.
摘要译文
Choc和π演算分别是CCS的两个扩展,其中进程和通道分别是可传输的值。在之前的工作中,我们提出了巧克力互模拟的概念的正式化。在本文中,我们建议通过将巧克力嵌入到更丰富的演算中来推断这一概念的更有效方法,该演算赋予了我们引导Chocst的“激活”频道概念。是由激活通道上的同步产生的新内部动作的名称,这样的同步具有强制执行空闲过程的效果。在一次近似中,Chocst中的过渡可以被理解为沿着激活信道的同步序列,随后是可观察的过渡。Chocst的互模拟有一个简单的定义,它满足自然法则和同余规则,而且与Chocst过程相关的同步树是有限分支的。我们建议Chocst作为确定Chocs互模拟验证工具定义的中间步骤。
Roberto M. Amadio1. On the reduction of chocs bisimulation to π-calculus bisimulation. CONCUR'93[M].DE: Springer, 1993: 112-126