面向传值进程的谓词μ—演算与FO（HML）的完备推演系统

来源 :计算机学报 | 被引量 : 0次 | 上传用户：www6331758

【摘要】

：

作者提出一个谓词μ-演算系统,目的在于描述传值进程的性质.该系统的公式和谓词相互递归定义,谓词中含有抽象式、谓词变元以及最大和最小不动点.其语义模型是带赋值的符号迁

【作者】

：

薛锐林惠民

【机构】

：

中国科学院软件研究计算机科学实验室

【出处】

：

计算机学报

【发表日期】

：

2002年6期

【关键词】

：

传值进程谓词μ-演算 FO 完备推演系统计算机 valuepassing processes μcalculus model checking tab

【基金项目】

：

国家自然科学基金，山西省留学回国人员科研项目，中国科学院软件研究所开放实验室基金

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

作者提出一个谓词μ-演算系统,目的在于描述传值进程的性质.该系统的公式和谓词相互递归定义,谓词中含有抽象式、谓词变元以及最大和最小不动点.其语义模型是带赋值的符号迁移图所诱导的迁移系统.并且该系统包含Hennessy-Milner逻辑的一阶扩充FO(HML)作为子系统.作者用例子说明了本演算系统在表达传值进程性质方面的优越性.该文后半部分主要给出了FO(HML)的一个推演系统,并运用判定树(Tableau)的方法,证明了所给的推演系统是完备的.

其他文献

基于线性表出的非奇异循环变换局部性优化方法

开发程序的局部性是当今并行编译优化研究的重点之一,而程序变换是开发程序时间局部性和空间局部性的重要手段之一.该文提出了一种新的利用非奇异循环变换来优化程序局部性的

期刊

并行编译优化非奇异循环变换局部性优化方程序变换数据变换parallel compiling optimization temporal localit

面向HDL描述基于路径覆盖的模拟矢量自动生成方法研究

提出和实现了一种面向HDL描述基于路径覆盖的模拟矢量自动生成方法.该方法在约束生成时只考虑控制语句的条件表达式,可有效避免生成冗余约束;利用扩展的决策图模型解决了中间

期刊

HDL描述路径覆盖模拟矢量自动生成约束逻辑求解VLSIVLSI automatic simulation vectors generation DD

基于锁集合的动态数据竞争检测方法

数据竞争使得共享存储程序难于调试.以前大部分针对共享存储程序的动态数据竞争检测工作都是通过维护发生序来实现.这种方法有一个重要缺点,即针对程序的一种输入,对程序的一

期刊

编程技巧动态数据竞争检测方法锁集合软件分布式共享存储系统域一致性模型程序并行性software distributed shared memory

基于广义细胞自动机的网络信息自组织利用方法

目前的网络信息利用模式存在着严重缺陷,它将网络上发生的海量、随机、分布、并行的信息利用行为当作是没有后效的和彼此无关的.该文提出一种新的基于网络信息自组织的信息利

期刊

计算机网络网络信息自组织广义细胞自动机信息利用模式细胞神经网络network information exploitation generalized

面向传值进程的谓词μ—演算与FO（HML）的完备推演系统

与本文相关的学术论文