An epistemic model checking approach for OWL-S web services

The verification of Web service compositions is mainly based on model checking techniques for temporal logics. Little attention is paid to the epistemological perspectives. In this paper, we abstract an OWL-S web service composition as a multi-agent system, propose an intermediate formal model OWL-S2FSM for modeling OWL-S process models, based on which we further develop a transformation method to convert the OWL-S language to the input language of the epistemic model checker MCTK developed by us. The proposed verification approach enables us to check not only temporal properties, but also temporal-epistemic properties of OWL-S web services. The experimental results show the validity of the proposed verification approach.