多智体系统时序认知规范的SPIN模型检测

• 作者: 王扣武 龙士工
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: SPIN 模型检测 时序认知逻辑 线性时序逻辑
• 年，卷（期）: 2011,（12）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 12-16
• 分类号: TP309
• 字数: 4319字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2011.12.003

摘要

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便.本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑.本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	龙士工	贵州大学计算机科学与信息学院	39	110	5.0	9.0
2	王扣武	贵州大学计算机科学与信息学院	3	4	1.0	1.0