具有行为观察的移动界程演算空间逻辑

• 作者: 林荣德 陈江
• 来源期刊: 南京师范大学学报：工程技术版
• 学科: 工学
• 关键词: 移动界程演算 界程逻辑 空间和行为观察 模型检测
• 年，卷（期）: 2011,（4）
• 页码范围: 70-76
• 分类号: TP311
• 字数: 7078字
• 语种: 中文
• DOI: 10.3969/j.issn.1672-1292.2011.04.015

摘要

界程逻辑中的并发模态副词是观察进程交互行为的关键因素之一,但引入并发模态副词又会导致模型检测的不可判定性.针对这一问题,提出了可判定的、描述移动界程演算进程的空间结构和行为性质的应用界程逻辑.该逻辑定义了空间模态词和行为模态词来直接观察移动进程的空间性质和潜在交互行为性质,并定义了不动点公式来刻画进程的递归性质.为了证明逻辑公式的指称语义的正确性,引入了性质集的概念并证明两者之间的一致性.最后给出了使用应用界程逻辑公式来描述一个资源传输系统在时间和空间上的行为性质的实例.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	林荣德	华侨大学网络信息中心	13	14	2.0	2.0
2	陈江	华侨大学网络信息中心	13	25	3.0	4.0