摘要

提出一种基于模型检测的多Agent交互策略验证方法,首先通过责任政策语言建模多Agent的交互策略,基于责任政策语言的操作语义将政策模型转换为模型检测器Nu SMV的输入,利用时态逻辑声明表征策略冲突的系统性质,然后利用模型检测器Nu SMV自动验证政策模型对性质的可满足性,并根据模型检测器产生的反例分析交互策略中的各种错误。该方法可提高交互策略的验证效率,确保多Agent系统设计的正确性。