多智体系统时序认知规范的SPIN模型检测
Multi-Agent System SPIN Model Checking Based on the Temporal Logic of Knowledge作者机构:贵州大学计算机科学与信息学院贵州贵阳550025
出 版 物:《计算机工程与科学》 (Computer Engineering & Science)
年 卷 期:2011年第33卷第12期
页 面:12-16页
核心收录:
学科分类:08[工学] 0839[工学-网络空间安全] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术(可授工学、理学学位)]
基 金:国家自然科学基金资助项目(61163001 60963023)
摘 要:SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。