A proof system for communicating processes with value-passing

A proof system for a version of CCS with value-passing is proposed in which the reasoning about data is factored out from that about the structure of processes. The system is shown to be sound and complete for finite terms with respect to a denotational semantics based on Acceptance Trees.     

Communicating processes with value-passing and assignments

A semantic theory of an imperative language which allows value-passing and assignments as a simple action prefixing is described. Three different semantic approaches are given: denotational based on the mathematical model Acceptance Trees, axiomatic based on inequations and behavioural in terms of testing. The equivalence of these different approaches is shown. The results are compared with similar results for other languages such asCSP andOccam.This work has partly been supported by the ESPRIT/BRA project Concur     

嵌套谓词等式系与弱互模拟

带赋值符号迁移图是一般传值进程的语义模型,其强互模拟等价可以归结为谓词等式系的最大解.该文将这一结果推广到弱互模拟等价,为此,引入嵌套谓词等式系的概念,并提出算法,将带赋值符号迁移图的弱互模拟等价归结为形如E₂μE₁的嵌套谓词等式系的最大解.     

传值系统的互模拟与谓词等式系

本文引入描述传值并系统的新模型“带赋值符号迁移图（ＳＴＧＡ）”推广了Ｈｅｎｎｅｓｓｙ和Ｌｉｎ提出的“符号迁移图”的概念，允许迁移上带有赋值，从而能将更大的一类传值系统表示为有穷状态图，ＳＴＧＡ的中车优点是在并行运算不封闭，文中给给ＳＴＧＡ的操作语义，在此基础上定义了ＳＴＧＡ的互模拟等价关系，为了刻划ＳＴＧＡ的互模拟，以谓词等式系的形式在一阶逻辑的正子集中扩充了最大和最小不动点，并设计了一个算法将Ｓ     

递归数据传送进程的证明系统

本文提出了递归数据传送进程互模拟的证明系统，并证明了其可靠性和相对于数据推理的完备性，其中关键的推理规则是唯一不动点归纳法，这个结果一方面将Ｍｉｌｎｅｒ关于正则基本ＣＣＳ的公理系统推广到数据传送进程，另一方面将Ｈｅｎｎｅｓｓｙ与Ｌｉｎ关于有穷数据传送进程的证明系统推广到无穷进程。