Smaller to Sharper: Efficient Web Service Composition and Verification Using On-the-fly Model Checking and Logic-Based Clustering

Model checking (MC) is an emerging approach recently suggested for the problem of Web Service Composition (WSC), since it can ensure both the soundness and completeness once verifying if an WSC solution fulfills a goal formally described or not. However, as the number of web services to be considered in practice is often very large, the MC-based approach suffers from the state space explosion problem. Clustering has been naturally considered reducing the number of candidates for the WSC problem. However, as typical clustering techniques are mostly semi-formal in terms of cluster representation, it poses a dilemma of maintaining both soundness and completeness. In this paper, we handle this problem by suggesting a logic-based approach for clustering. This work makes twofold contributions. We propose a logic-based similarity between web services, which results in more reasonable clustering results; and we represent the generated clusters as logical formula and enjoy a seamless integration between web service clustering and MC. This approach eventually brings significant improvement of WSC performance when applied on real and relatively large repository of web services.