摘要： 将Web服务组合建模为多智能体系统，采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例，并验证相关的时态知识规范。在同一实验环境下，采用另一种时态知识逻辑模型检测工具MCMAS进行建模，并验证该实例。实验结果表明，基于MCTK的Web服务模型检测方法比基于MCMAS的方法更有效。

关键词: 模型检测, 时态知识逻辑, 多智能体系统, Web服务

Abstract: A Web service composition is modeled as a multi-agent system. The MCTK, a symbolic model checker for temporal logic of knowledge, is used to model a Web service example of loan approval and verify some related temporal epistemic specifications. Within the same experimental environment, the example is also modeled and verified via MCMAS, which is another model checker for temporal logic of knowledge. Experimental results show the presented model checking approach for Web services based on MCTK is more efficient than the approach based on MCMAS.

Key words: model checking, temporal logics of knowledge, multi-agent system, Web service

中图分类号: 

• N945