The Alternating-time Temporal Logic (ATL) is a temporal logic for formal verification of open systems, which supports selective quantification over paths. The open system can be represented as a game where the system and the environment pick their moves in turn or simultaneously. The ATL model checker Mocha has been developed by using Binary Decision Diagrams (BDDs), and successfully employed for open system verification. However, since Mocha symbolically manipulates a set of states by a BDD, it is hard to generate a winning strategy as a witness or a counter-example. In this paper, we propose a novel algorithm to efficiently construct a winning strategy tree and report that our technique has been successfully implemented on Mocha.

The behavioral description based Web Service Composition (WSC) problem aims at the automatic construction of a coordinator web service that controls a set of web services to reach a goal state. However, solving the WSC problem exactly with a realistic model is doubly-exponential in the number of variables in web service descriptions. In this paper, we propose a novel efficient approximation-based algorithm using automatic abstraction and refinement to dramatically reduce the number of variables needed to solve the problem.

The Web service composition (WSC) problem on behavioral descriptions deals with the automatic construction of a coordinator web service to control a set of web services to reach the goal states. As such, WSC is one of the fundamental techniques to enable the Service Oriented Architecture on the Web. Despite its importance and implications, however, very few studies exist on the computational complexities of the WSC problem. In this paper, we present two novel theoretical findings on WSC problems: (1) Solving the WSC problem with "complete" information is EXP-hard, and (2) Solving the WSC problem with "incomplete" information is 2-EXP-hard. These findings imply that more efforts to devise efficient approximate solutions to the WSC problem be needed.

A novel benchmark, WSBen, for testing web services discovery and composition is presented. WSBen includes: (1) A collection of synthetic web services (WSDL) files with diverse characteristics and sizes; (2) Test discovery and composition queries and solutions; and (3) External files for statistical analysis and AI planners. Users can fine-tune the generated WSDL files using various parameters such as skewness or matching type. It is our hope that WSBen will provide useful insights for researchers evaluating the performance of web services discovery and composition algorithms and softwares.