非对称χ<'≠>-演算的公理化系统

来源 :上海交通大学 | 被引量 : 0次 | 上传用户:shiqingfang
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
该文的主要研究内容和成果包括:1.非对称χ<≠>-演算的语法和语义 定义了非对称χ<≠>-演算的语法和语义:在语法上,给出了一组算子用以构造进程,其中就有不等名算子[x≠y];语义上,引入了一个标号转移系统来定义操作语义,强调非对称通信,即区分输入和输出动作,例如形如ax的动作是输出动作,而形如ax的动作则为输入动作.2.非对称χ<≠>-演算的互模拟格 在类χ-演算中,一般用L-互模拟来研究各互模拟关系之间的相关性.L-互模拟的基本思想是,不同的观察者所能看到的进程行为是不同的,因此所能区别的进程对也是不一样的.L-互模拟试图将所有不同的观察行为进行分类,定义出相应的进程间的等价关系.根据这些L-互模拟关系之间的序关系,我们可以构造互模拟格.3.非对称χ<≠>-演算中barbed互模拟的操作性质和代数性质 Barbed互模拟定义简单,可以有效地生成一个合理的观察等价关系,而且对标号转移系统和归约语义均适用,所以在研究一个新进程演算的普适性时,通常要研究barbed互模拟.对通道类的进程演算来说,这种方法通常会得到该演算的最弱的互模拟等价关系.另外,由于barbed互模拟可以应用于各种进程演算中,所以也可用来研究各演算之间的关系.该论文定义了强、弱barbed互模拟关系,并确定了barbed互模拟在互模拟格中处于顶元的位置;研究了barbed互模拟的操作性质,可以看到由于不等名算子和非对称通信结构的存在,其性质相当复杂.Barbed互模拟关系对上下文的依赖性使其难以理解,因此该论文给出了barbed互模拟关系的开形式等价定义,根据该定义可以清楚地了解barbed互模拟进程对的行为方式.开互模拟关系是一个在替换下封闭的互模拟关系,是移动进程最自然的互模拟关系.开barbed互模拟关系既给出了barbed互模拟关系的上下文无关刻划,又有助于建立相应的barbed同余关系的公理化系统.4.非对称χ<≠>-演算的其他L-互模拟关系的性质和公理化研究 该论文最后研究了互模拟格中其他L-互模拟关系的性质.首先,给出了L-互模拟关系的定义及其开形式刻划,并证明了二者的一致性;然后在开L-互模拟关系的基础上定义L-同余关系;最后根据开L-互模拟关系的定义并不是通过对开barbed互模拟关系的定义进行简单地删减而获得的,它们的定义充分体现了相应的L-互模拟关系的性质.另外,L-同余关系的定义也不尽相同,而它们的公理化系统则各具特点.
其他文献
论文的主要内容是研究使用Web Services技术和面向服务的体系结构设计、实现经营信息服务的方法和过程.在现有的、以数据仓库为核心的经营信息系统的基础上,论文设计并实现了
软件系统的成功极大依赖软件需求工程的质量,而软件的可靠性难以保证和开发效率低一直是困扰软件产业的两大难题。而用形式化方法开发软件始终被认为是提高软件可靠性和软件生
计算机支持的协同工作(Computer Supported Collaborative Work,CSCW)是计算机理论和应用的一个重要领域。它利用了计算机的交互性、网络的分布性以及多媒体的综合性,支持不
随着人们对视频点播等视频服务的需求迅猛增长,视频服务器得到广泛应用。集群视频服务器具有较好的扩展性、可靠性和高性价比越来越受到关注。高质量的视频服务需要持续的高
基于互联网的信息管理已经成为现代化管理中人们关注的技术焦点和信息系统的一个发展方向.本课题的任务就是要建立一个基于网络环境的人类精子库信息管理系统,为我国生殖医学
近年来主动数据库已经成为数据库研究领域的热点。主动数据库技术是为实现对于数据完整性和一致性的自动维护和满足实时信息处理的需要应运而生的,是数据库理论发展的一个重
传统的Internet中没有服务质量的保证,网络只提供最大努力的数据传输服务,如何在互联网中为多媒体应用提供服务质量的保证是当前网络研究中的热点问题。本文主要讨论互联网中提
网格试图实现互联网上所有资源的全面连通,包括计算资源、存储资源、通信资源、软件资源、信息资源、知识资源等。服务网格研究的目标是智能信息处理,它侧重在如何消除信息孤
随着软交换技术和各种相关的软件、硬件方面的发展,下一代网络(NGN,Next Generation Network)的发展已经进入试商用运行的阶段.广东电信目前在全省进行下一代网络的试商用运
单机家庭影院(Home Theater in a Box)是把MPEG编解码、多通道音频编解码、声音处理DSP、功放、喇叭、单芯片AM/FM以及音频DAC等功能有效地整合在一起、以一个DVD播放器为基