基于智能体的OWL-S过程模型验证

摘要

The atomic process as agent and the semantic web service composition as multi-agent were abstracted) a formal model OWL-S2FSM for modeling OWL-S was proposed to ensure the correctness and reliability of the semantic web service composition. The proposed method supports temporal properties and epistemic properties. Two algorithms OWL-S2FSM and FSM2M were developed and implemented to translate OWL-S into FSM and FSM into the input language of MCTK. The experimental results show the MCTK is effective.%为保证基于OWL-S的web服务组合的正确性和可靠性,对OWL-S过程模型进行时态和认知属性的验证.将原子过程视为单个服务作为Agent,将组合过程抽象为多智能体系统,把对OWL-S过程模型的验证转换成对多智能体系统的验证.提出了OWL-S语言的形式化模型OWL-S2FSM,设计从OWL-S2FSM到模型检测工具MCTK输入语言之间的转换算法,并应用MCTK对多智能体系统的规范进行验证.实验结果表明,该方法可以有效地验证多智能体系统的时态属性和认知属性.