该文主要研究利用知识逻辑进行协议验证的问题.一直以来,高效无二意的通信协议是人们进行有效的远距离通信交流的基础,设计高效无二意的通信协议是一项极具挑战性的工作.通信协议的效率可以通过设计高效的编码方案或发明新型高速传输媒质来提高;而无二意的通信协议必须满足在一定的执行环境中,所有可能发生的情况下,协议执行的结果唯一确定.该文集中讨论了如何验证一个设计好的通信协议是无二意的,即协议验证问题.这一问题也是一个极具挑战性的问题,并且至今还没有一个完美的解决方案.传统的协议验证方法多基于时态逻辑,主要考察系统在执行协议时在时间序列上所具有的性质.引入多智能体系统后,协议的执行不仅受时间的影响,还与智能体的知识状态有关.在多智能体系统中考察协议的执行,不仅可以从时间序列上考虑,还可以从系统中的智能体执行协议后,所具有的知识发生变化这个角度去考虑.这正是该文讨论的切入点,该文在传统的基于时态逻辑的协议验证方法基础上,引入知识逻辑,借助多智能体系统的知识模型,以新的视角研究协议,并利用模型检测技术实现了对有限知识模型的多智能体系统的协议验证.作为研究成果,我们定义了一个有限状态多智能体系统框架,并研究了在采用不同观察策略的多智能体系统中如何计算智能体的知识.以此为理论基础,我们实现了基于知识的协议验证系统KMAS,并利用模型检测技术成功验证了几个协议实例.同时,作为研究的一个附加成果,我们实现了基于知识的程序设计工具LKBL.