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.

Traditional planning assumes reachability goals and/or full observability. In this paper, we propose a novel solution for safety and reachability planning with partial observability. Given a planning domain, a safety property, and a reachability goal, we automatically learn a safe permissive plan to guide the planning domain so that the safety property is not violated and that can force the planning domain to eventually reach states that satisfy the reachability goal, regardless of how the planning domain behaves. Our technique is based on the active learning of regular languages and symbolic model checking. The planning method first learns a safe plan using the L (*) algorithm, which is an efficient active learning algorithm for regular languages. We then check whether the safe plan learned is also permissive by Alternating-time Temporal Logic (ATL) model checking. If the plan is permissive, it is indeed a safe permissive plan. Otherwise, we identify and add a safe string to converge a safe permissive plan. We describe an implementation of the proposed technique and demonstrate that our tool can efficiently construct safe permissive plans for four sets of examples.

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.

While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In this paper, we propose a novel solution for automatically extracting such temporal specifications for Java classes. Given a Java class, and a safety property such as “the exception E should not be raised”, the corresponding (dynamic) interface is the most general way of invoking the methods in the class so that the safety property is not violated. Our synthesis method first constructs a symbolic representation of the finite state-transition system obtained from the class using predicate abstraction. Constructingthe interface then corresponds to solving a partial-information two-player game on this symbolic graph. We present a sound approach to solve this computationally-hard problem approximately using algorithms for learning finite automata and symbolic model checking for branching-time logics. We describe an implementation of the proposed techniques in the tool JIST — Java Interface Synthesis Tool—and demonstrate that the tool can construct interfaces accurately and efficiently for sample Java2SDK library classes. Categories and Subject Descriptors: D.2.4 [Software Engineering] Software/Program Verification-formal methods, model checking; D.2.1 [Software Engineering] Requirements/Specification-methodologies, tools; D.2.2 [Software