Efficient Abstraction and Refinement for Behavioral Description Based Web Service Composition

1 Introduction

Web services are software systems designed to support machine to machine interoperation over the Internet. When a single web service does not satisfy a given requirement entirely, one needs to use a composition of web services. In particular, the Web Service Composition (WSC) problem that we focus on is, given a set of (behavioral descriptions of) web services, W, and a reachability goal, G, to automatically synthesize a coordinator web service, c, that controls W to satisfy G. In this paper, a behavioral description of a web service is a formal specification on what the web service executes internally and externally with interacting with users; e.g., describing what output value it returns for a given input and its state, and how it changes its internal state.

Despite abundant researches on the WSC problem, only a few (e.g., [Traverso and Pistore, 2004; Pistore et al., 2005a; 2005b]) employ realistic models with partial observation. Our previous work [Kil et al., 2008] investigated the computational complexity (i.e., lower bound) of the WSC problem: (1) solving the WSC problem for a restricted case (when the synthesized coordinator web service, c, has full observation for all variables of the given web services) is EXP-hard, and (2) solving the WSC problem for a general case (when c has partial observation) is 2-EXP-hard. These results suggest studying efficient approximation solutions to the WSC problem. Toward this challenge, in this paper, we propose two approximation-based algorithms using "abstraction and refinement" [Clarke et al., 1994]. To the best of our knowledge, it is the first attempt to apply an abstraction technique to the WSC problem. Even, in planning under partial observation which has a strong connection with WSC, no study has attempted to apply abstraction techniques.

The first step is to reduce the original web services to the abstract ones with less variables. If we identify a coordinator that controls the abstract web services to satisfy a given goal, the coordinator can control the original web services to satisfy the goal since the abstract web services over-approximate the concrete ones. Otherwise, we refine the abstract web services by adding variables, and repeat to find a solution. For abstraction, we propose two methods-signature-preserving abstraction and signature-subsuming abstraction. We report on the performance of our tool on 3 sets of realistic problems (8 instances), comparing with a basic algorithm [Traverso and Pistore, 2004] without abstraction/refinement. Our experiment shows that our technique outperforms the basic algorithm. Finally, it is worth pointing out that our approach can be readily adopted for other WSC techniques such as knowledge-level composition [Pistore et al., 2005b].

2 Web Service Composition &Lower Bounds

Example 1 (Travel agency system). Clients want to reserve both a flight ticket and a hotel room for a particular destination and a period. However, there exist only an airline reservation (AR) web service and a hotel reservation (HR) web service separately. Clearly, we want to combine these web services rather than implementing a new one. One way to combine them is to automatically construct a coordinator web service which communicates with them to book up both a flight ticket and a hotel room. Figure 1 illustrates this example. AR service receives a request including departing/returning dates, an origin and a destination, and then checks if the number of available seats for flights is greater than 0. If so, it returns the flight information and its price; otherwise, it returns "Not Available". Once offering the price, it waits for "Accept" or "Refuse" from its environment (in this case, a coordinator to be constructed). According to the answer, it processes the reservation. Likewise, HR service is requested with check-in/check-out dates and a location, and then checks the number of available rooms. If there is an available accommodation, it returns the room information and its price; otherwise, it returns "Not Available". AR then processes a reply "Accept" or "Refuse" from its environment. ✷

Definition 1 (Web service) A (behavioral description of) web service w is a 5-tuple (X , XI , XO , Init , T ) where:

• X is a finite set of variables that w controls. A state s of w is a valuation for every variable in X . We denote a set of all states as S.
• XI is a finite set of input variables that w reads from its environment; X ∩ XI = ∅, and every variable x ∈ X ∪ XI has a finite domain (e.g., Boolean, bounded integers, or enumerated types). A state in for inputs is a valuation for every variable in XI . We denote a set of all input states as S I .
• XO ⊆ X is a finite set of output variables that its environment can read. Let us denote a set of input and output variables by XIO (i.e., XIO = XI ∪XO ), and a set of all variables by XA (i.e., XA = X ∪ XI ).
• Init(X) is an initial predicate over X. Init(s) = true if and only if s is an initial state.
• T(X,XI ,X ′ ) is a transition predicate over X ∪XI ∪ X ′ . For a set X of variables, we denote the set of primed variables of X as X′ = {x′ | x ∈ X}, which represents a set of variables encoding successor states. T(s, in, s ′ ) is true if and only if s ′ can be a next state when the input in ∈ S I is received at the state s. T can define a non-deterministic transition relation. ✷

While the formalism for web services by Traverso et al. [Traverso and Pistore, 2004] is based on an explicit statetransition system using a set of states, we define symbolically web services by a set of variables, which is more compact.

Example 2. Consider a simple version of a web service w for the airline reservation in Example 1, and assume that clients can request (reserve or refuse) a flight ticket by an action req1 or req2 (accept or refuse, respectively). The web service w can be represented as (X , XI , XO , Init , T ) where:

• X = {state, avail, reply, confirm, f num, tr num} where state has the domain {q1 , q2}, avail is boolean, reply has the domain {undecided, offer, notAvail}, confirm has the domain {undecided, reserve, cancel}, f num (flight number) has the domain {f1 , f2}, and tr num (transaction number) has the domain {t1 , t2 }.
• XI = {action} where action has the domain {req 1 , req 2 , accept, refuse}.
• XO = {reply, confirm, f num}.
• Init(X) ≡ (state = q1 ) ∧ (reply = undecided) ∧(confirm = undecided ).

· T(X,XI , X ′ ) ≡ (((state = q1 )∧(action = req 1 )∧(avail = true)) → ((state′ = q2 ) ∧ (reply′ = offer ) ∧ (tr num′ = t1 ))) ∧ (((state = q1 ) ∧ (action = req 1 )) → (f num′ = f1 )) ∧ · · · ∧ (((state = q2 ) ∧ (action = accept )) → ((state′ = q1 ) ∧ (confirm′ = reserve))) ∧ (((state = q2 ) ∧ (action = refuse)) → ((state′ = q1 ) ∧ (confirm′ = cancel ))). ✷

Note that the process model for any web service described in semantic web languages (e.g., WS-BPEL or OWL-S) can be easily transformed into our representation above without any information loss if it has only finite domain variables and no recursion. In the WSC problem in this paper, given a set of available web services, W, every web service in W communicates only with their coordinator but not with each other.

Definition 2 (Set of web services) Based on the assumption above, given a set W = {w1, · · · , wn} of web services where each wi is (Xi,XI i ,XO i , Initi,Ti), and Xi and XI i are disjoint with each other Xj and XI j , respectively, W also can be represented by a 5-tuple (X,XI , XO , Init , T ) where X = X1 ∪ · · · ∪ Xn, XI = XI 1 ∪ · · · ∪ XIn , XO = XO 1 ∪ · · · ∪ XO n , Init(X) = Init1 ∧ · · · ∧ Initn, and T (X , XI , X ′ ) = T1 ∧ · · · ∧ Tn. ✷

Since a coordinator web service is also a web service, it is a 5-tuple c(Xc,XI c , XO c , Initc,Tc). In what follows, sc denotes a state of a coordinator web service, and Sc denotes a set of all states of a coordinator. Although Tc can define a non-deterministic transition relation, in this problem we want only a deterministic transition relation for c; i.e., for every coordinator state sc and input in, there exists only one next coordinator state s ′c such that Tc(sc, in, s ′c ) = true.

For a state s over X and a set of variables Y ⊆ X, let s[Y ] denote the valuation over Y obtained by restricting s to Y .

Definition 3 (Execution tree) Given a set W(X, XI , XO , Init, T) of web services and a coordinator c(Xc, XI c , XO c , Initc, Tc) where XI = XO c and XO = XI c , we can define an execution tree, denoted by W||c, which represents the composition of W and c as follows:

• Each node inW||c is in S ×Sc.
• The root node is (s, sc) such that Init(s) = true and Init c(sc) = true.
• For each node (s, sc), it has a set of child nodes, {(s ′ , s ′c ) | T(s, in, s ′ )=true, in=sc[XI ], Tc(sc, inc, s ′c )=true, inc=s ′ [XO ]}. ✷

In the above, intuitively, the web services W, by receiving the input in from the current state sc of the coordinator, collectively proceeds from s to the next state s ′ , and then the coordinator, by receiving the input inc from the new state s ′ of the web services, proceeds from sc to the next state s ′c . Even though the composition of W and c is defined as synchronous communication, we can easily extend this model for asynchronous communication using τ-transition [Pistore et al., 2005a]. A goal G ⊆ S is a set of states to reach, and specified as a predicate. Given a set W of web services, a coordinator c, and a goal G, we define W||c |= G if for every path (s 0 , s 0 c )(s 1 , s 1 c ) · · · in the execution tree W||c, there exists i ≥ 0 such that s i ∈ G; namely, every path from the initial node (s 0 , s 0 c ) reaches a goal state eventually.

Definition 4 (Web service composition problem) The web service composition (WSC) problem that we focus on in this paper is, given a set W of web services and a goal G, to construct a coordinator web service c such that W||c |= G. ✷ Example 3. In Example 1, we wish to reserve both a flight ticket and a hotel room. This can be represented as G ≡ (flightConfirm = reserve) ∧ (hotelConfirm = reserve). Now, given a set W = {wAR, wHR} of web services and the goal G above, a WSC problem is to construct a coordinator web service c such that W||c |= G. ✷

To study the computational complexity (i.e., lower bound) for WSC, we define two WSC problems as follows:

• WSC with full observation: a special case of WSC problems where W(X,XI , XO , Init,T) such that X = XO ; i.e., W contains no internal variable.
• WSC with partial observation: a general WSC problem where there is no restriction for XO . That is, a coordinator can read only the output variables in XO .

Theorem 1. The WSC problem with full observation is exponential in the number of variables inW.

The proof is to simulate an alternating Turing machine (ATM) [Papadimitriou, 1994] with a polynomial space bound. That is, for any ATM A and any input string σ, we can construct a WSC problem in polynomial time such that A accepts σ if and only if there exists a coordinator to satisfy a goal. Theorem 2. The WSC problem with partial observation is doubly-exponential in the number of variables inW.

The proof is to simulate an ATM with exponential space bound. For the details of both proofs, see [Kil et al., 2008].

3 Basic Algorithm forWSC Problem

In this section, we study a basic algorithm for the general WSC problem defined in Section 2. Several researches [Traverso and Pistore, 2004; Pistore et al., 2005a] have successfully applied a planning technique with partial observation [Bertoli et al., 2006] to WSC problems. Thus, we also employ the same method for our baseline algorithm; Algorithm 1 for the WSC problem is based on the automated planning algorithm on partial observation [Bertoli et al., 2006]. In a general case of WSC, a coordinator web service is not able to identify the exact state of target web services. Hence, we model this uncertainty by using a belief state, which is a set of possible states of target web services but indistinguishable. The underlying idea of Algorithm 1 is to construct an and-or searching tree from initial belief states to goal belief states. That is, from any node (a belief state) of the tree, for non-determinism of output values of web services, we extend the tree with a set of child nodes via andedges. In this case, all the child nodes should reach a goal belief state. For coordinator's selecting input values, we construct a set of child nodes via or-edges. In this case, at least one child is required to reach a goal belief state.

To initialize the and-or searching tree, Algorithm 1 first constructs a root node (a belief state) corresponding to the given initial predicate, Init, and assigns "undecided" to the result value for the root (lines 1-2). If the states corresponding to Init are already included in goal states, we assign "true" to the result value for the root. Next (lines 5-12), until

Algorithm 1: WSC with partial observation

Input : A set W of web services and a goal G.

Output: A coordinate web service c. tree := InitializeSearchingTree(Init); 1 tree.root.result := undecided; 2 if (States(Init) ⊆ States(G)) then 3 tree.root.result := true; 4 while (tree.root .result = undecided) do 5 node := SelectNode(tree); 6 childNodes := ExtendTree(tree, node); 7 if (CheckSuccess(childNodes)) then 8 node.result := true; 9 else if (CheckFailure(childNodes)) then 10 node.result := false; 11 PropagateResult (tree , node); 12 if (tree.root.result = true) then 13 return ConstructCoordinator (tree); 14 else return null ; 15

determining the result value for the root, we repeat: (1) to select a node which is not determined yet as "true" or "false", (2) to extend the tree from the selected node by computing a set of possible successor nodes, and (3) to check if the node can reach a goal state based on the and-or constraint. Once we identify the result of each node, we propagate the result to its ancestor node. Finally, if the algorithm identifies the result of root node as true, it constructs a coordinator web service from the tree, and returns the coordinator. Otherwise, it returns null. The complexity of the algorithm is O(22n ) where n is the number of variables in W, since the number of states of W is 2n and thus the number of belief states is 22n (recall Theorem 2).

4 Signature-preserving Abstraction and Refinement

Theorems 1 and 2 imply that the WSC problem is computationally hard. Hence, more efforts to devise efficient approximation solutions to the WSC problem are needed. In addition, the complexity of Algorithm 1 also provides the same implication. Therefore, we propose two approximation-based methods using abstraction and refinement in Sections 4 and 5.

4.1 Signature-preserving abstraction

Given a set W of web services, we define signaturepreserving abstract web services that have the same signature

(i.e., the same I/O variables) but less variables thanW. Definition 5 (Signature-preserving abstract web services) Given a set of web services W(X, XI , XO , Init, T) and a set Y of variables such that XIO ⊆ Y ⊆ XA, the signature-preserving abstraction of W with respect to Y is WY (XY , XIY , XO Y , InitY , TY ) where:

• XY = Y \XI , XIY =XI , and XO Y =XO .
• For every sY ∈ SY , InitY (sY ) = true iff ∃s ∈ S. (Init(s) = true) ∧ (sY = s[XY ]).
• For every sY , s′Y ∈ SY , TY (sY , in, s′Y ) = true iff ∃s, s′ ∈ S. (T(s, in, s′ ) = true) ∧ (sY = s[XY ]) ∧ (s′Y = s′ [XY ]). ✷

(c) Abstract states for {state}

Figure 2: Abstraction

Since WY preserves the signature of W, once we construct a coordinator c which can be composed with WY based on Definition 3, c also can be composed with W. Moreover, since the abstraction WY over-approximates the concrete web services W (i.e., WY contains all the behaviors of W), WY satisfies the following property.

Theorem 3 (Soundness). Given a set W of web services and a goal G, if a coordinator web service c satisfies W ′ ||c |= G where W ′ is a signature-preserving abstraction of W (e.g., WY in Definition 5), then c also satisfies W||c |= G.

Example 4 (Abstraction). Figure 2(a) illustrates the concrete state space with 6 states, where there are three internal variables-state, avail, tr num. Symbols above arrows represent a value of an input variable. In this example, from the state s1, we have a strategy to guarantee to reach GOAL-invoking req and order. Figure 2(b) shows an abstract state space with respect to {state, avail}. s1 and s4 in the original space are mapped to s7 and s9, respectively. Two states, s2 and s3, (s5 and s6) collapse into s8 (s10, respectively). Although the number of states decreases, every path in the original state space is mapped to one of paths in the abstract space. Moreover, from the state s7 corresponding to s1, we still have a strategy to guarantee to reach GOAL. Figure 2(c) shows a coarser abstraction. However, from the state s11 corresponding to s1, we no longer have a strategy to guarantee to reach GOAL since we abstract out too much. ✷

4.2 Abstraction and refinement algorithm

Algorithm 2 presents a high-level description of our method based on signature-preserving abstraction. In a nutshell, we abstract a given web services W into W ′ and try to find a solution for the abstraction W ′ . If we identify such a coordinator, it can indeed control the original web services W to

Input : A set W of web services and a goal G. Output: A coordinate web service c. Y :=XI ∪XO ; 1 WY := Abstraction(W, Y ); // WY has only XI and XO . 2 if ((c :=WSCFullObs(WY ,G)) ̸= null) then 3 return c; 4 ConstructDependencyGraph(W , G); 5 while ((newVars := SelectNewVars(W,G)) ̸= null) do 6 Y := Y ∪ newVars; 7 WY := Abstraction(W, Y ); 8 if ((c :=WSCPartialObs(WY ,G)) ̸= null) then 9 return c; 10 return null ; 11

satisfy a given goal. Otherwise, we repeat the search with more accurate abstraction.

First, we abstract W with only input and output variables, i.e., Y = XI ∪ XO (lines 1-2). Since, at this point, WY does not include any internal variable (i.e., XY = XO Y ), we can exploit, in this case, the algorithm for WSC with full observation, WSCFullObs, which is more efficient algorithm (EXP-hard). For the sake of space, we do not show the details of WSCFullObs. If we find a coordinator c such that WY ||c |= G, then c also satisfies W||c |= G by Theorem 3. Otherwise, we refine our current abstraction WY by adding more variables, and try to find c for the new abstraction (lines 6-10). How to select additional variables will be elaborated in Section 4.3. We repeat the abstration/refinement step until we identify a coordinator c satisfying WY ||c |= G or the variable set used for abstraction equals to the original variable set. The latter case implies that no solution exists for the given problem. Although from the second loop, we should employ the algorithm for WSC with partial observation, WSCPartialObs, with O(22n ) complexity, once we identify a coordinator using small abstract web services, searching space is shrunken (double-)exponentially in the number of variables that we save.

4.3 Automatic refinement

If we fail to identify a coordinator for abstract web services (line 3 or 9 in Algorithm 2), it is caused either by too coarse abstraction or by the fact that a coordinator for the original web services does not exist. For the latter case, since we check it with the original web services in the worst case, Algorithm 2 will correctly conclude that there is no solution.

Theorem 4 (Completeness). Given a set of web services W and a goal G, if there does not exist a coordinator c to satisfy W ||c |= G, Algorithm 2 eventually returns null .

However, in the former case, although there exists a coordinator for the original web services W , WSCFullObs or WSCPartialObs returns null for the abstraction WY . The reason is that removing too many variables, including ones with significant information to reach a goal, gives too much freedom to the abstraction. It induces some infeasible paths to states not satisfying the goal. For instance, in Figure 2(c), since we remove the variable avail, s1 (s2 and s3) is indistinguishable from s4 (s5 and s6, respectively). Thus, an infeasible edge from s12 to s11 by order is introduced, by which we no longer have a strategy to guarantee to reach a goal. Therefore, we have to refine the current abstraction to find a solution by adding more variables. Since the infeasible paths to states not satisfying the goal prevent us from identifying a solution coordinator, it is important to accurately keep track of the values of variables appearing in the given goal predicate. With this reason, the most significant criterion for selecting variables to be added is the relevance to variables in the goal predicate. To evaluate each variable's relevance to the goal variables, we construct a variable dependency graph.

Definition 6 (Variable dependency graph) Given a set of web services W and a goal G, a variable dependency graph is a directed graph G(V, E) where a set V of vertexes is {x | x ∈ X ∪ XI } and a set E of directed edges is {(x ▷ y) | x, y ∈ V, the value of y depends on the value of x}. ✷

For instance, the pseudo-codes "y := x" and "if (x = true) then y :=0" imply that the value of y depends on x. Figure 3 illustrates a fraction of the variable dependency graph for W and G in Example 3. It shows only variables of wAR. For example, since the values of state, reply and tr num depend on the values of state, action and avail (see the first part of T in Example 2), we have corresponding directed edges (state▷state), (action▷state), (avail▷ state), · · · , and (action ▷ tr num) in Figure 3. In the dependency graph, it is clear that variables with stronger dependency to the variables in the goal predicate locate closer to the goal variables. Thus, in each iteration of Algorithm 2, the procedure SelectNewVars returns a set of variables that have the closest hop to the variables in the goal predicate (i.e., 1hop, 2-hop, and so on). For instance, since confirm is a variable in the goal predicate, the set of variables that have 1-hop dependency is {action, avail, state}.

5 Signature-subsuming Abstraction

In Section 4, we restricted the target of abstraction to internal variables; namely, abstract web services have the same I/O variables with original ones. However, in many cases, we have observed that some of output variables do not provide any important information for a coordinator to decide its move. For instance, the airline reservation web service in Example 2 simply copies the request value (i.e., req1 and req2 ) to the flight number (i.e., f1 and f2 ), and returns it to clients for reference. In this case, even without this output, the coordinator can successfully control given web services to satisfy the goal. Hence, in this section, we consider, as the target of abstraction, output variables as well as internal variables.

First, we define signature-subsuming abstract web services for given web services, which have the same input variables, but less internal variables and output variables.

Definition 7 (Signature-subsuming abstract web services) Given a set of web services W(X , XI , XO , Init, T), and a set Y of variables such that XI ⊆ Y ⊆ XA, the signaturesubsuming abstraction of W with respect to Y is WY (XY , XIY , XO Y , InitY , TY ) where XY = Y \ XI , XIY = XI , XO Y = Y ∩XO , and InitY and TY are defined as the same as Definition 5. ✷

Since signature-subsuming abstract web services WY have less output variables than the original web services W, any coordinator c which can be composedwithWY is also able to be composed with W by ignoring redundant output variables ofW (i.e., ignoringXO \XO Y ). Moreover, sinceWY contains all the behaviors of W, Theorem 3 is still valid.

For selecting output variables to be used in abstraction, we again employ the variable dependency graph in Section 4.3. In general, output variables that depend on internal variables that in turn depend on variables in a goal predicate, tend to provide important information on the state of web services for the coordinator to control the web services. For instance, in Figure 3, reply has a dependency on state and avail that have a dependency on the goal variable confirm, and reply is an important output by which a coordinator infer whether a flight seat is available. On the other hand, f num that represents a flight number has dependency only on an input variable, action, and it does not provide any information to help a coordinator. Therefore, we find such a set X SO ⊆ XO of significant output variables which have a dependency on internal variables with a dependency on variables in a goal predicate, and then use XSO for the initial abstraction. That is, in signature-subsuming abstraction, we start Y := XI ∪ X SO as line 1 in Algorithm 2. The rest of output variables (i.e., XO \XSO ) are used in the last iteration.

6 Empirical Validation

We have implemented automatic tools for signaturepreserving/signature-subsuming abstraction and refinement, using a state-of-the-art planning tool, MBP [Bertoli et al., 2006]. Given a set of web service descriptions in WS-BPEL files, and a goal predicate, our tools automatically construct a coordinator web service which can control the given web services to achieve the goal. To demonstrate that our tools efficiently synthesize coordinators, we compared the basic algorithm [Traverso and Pistore, 2004] and our methods with 3 sets of realistic examples (8 instances); Travel agency system (TAS), Producer and shipper (P&S), and Virtual online shop (VOS). Since there are no public benchmark test sets, we have selected web service examples popularly used in web service composition researches. TAS was explained in Example 1. We have three instances, TAS-a, TAS-b, and TASc, where we have 4, 9, and 16 options, respectively, for input values for flight reservation and hotel reservation each. Producer and shipper (P&S) [Traverso and Pistore, 2004; Pistore et al., 2005a] includes two web services, Producer and Shipper. Producer produces furniture items, and Shipper delivers an item from an origin to a destination. We have three instances, P&S-a, P&S-b, and P&S-c where there are 4, 6, and 8 options, respectively, for furniture order and delivery order each. Virtual online shop (VOS) [Barbon et al., 2006] includes Store and Bank web services where Store sells items and Bank transfers money from one account to another account. This example includes two instances, VOS-a and VOS-b where there are 3 and 4 options, respectively, for item orders and money transfer each.

All experiments have been performed on a PC using a 2.4GHz Pentium processor, 2GB memory and a Linux operating system. Table 1 presents the number of total variables (Total var) and input/output variables (I/O var) in boolean. It also shows the total execution time in seconds for the basic algorithm (Basic) and our methods (Signature-preserving and Signature-subsuming), and the number of boolean variables that we saved (Saved var). In the signature-subsuming case, the table presents the number of internal variables/IO variables which we saved. Our experiment shows that our technique outperforms the basic algorithm in terms of execution time. The numbers of iterations in our experiments were around 2-3, since variable dependency graphs were relatively shallow. In WSC literature, in general, behavior descriptions in WS-BPEL or OWL-S tend not to be complex, which usually yields to shallow variable dependency graphs.

Although we have employed modest size of examples, our abstraction technique can be useful even for larger size examples since in general, the number of variables which have relevance with goal variables is limited. For instance, with 100 web services with 10 variables each (total 1,000 variables), a goal that users want is often associated with only a fraction of available web services and variables (say 5%, 50 variables). In such a case, our techniques can eliminate 95% of irrelevant variables, improving the convergence speed considerably.

7 RelatedWork and Conclusion

In web service compositions, many researches [Traverso and Pistore, 2004; Pistore et al., 2005a; 2005b; Nam et al., 2008] have been carried out, but only a few ones employ realistic models with partial observability. [Traverso and Pistore, 2004; Pistore et al., 2005a; 2005b] have defined web service compositions with partial observability, and presented algorithms and tools using their automated planning techniques. However, to the best of our knowledge, there is no study for WSC problems or planning on partial observation using abstraction and refinement.

The WSC problem has a strong connection with automated planning under partial observation. In [Bertoli et al., 2006], a fully automatic planning tool MBP has been developed for this setting based on belief-states. On the other hand, several researches have been performed in planning using abstraction. Huang et al. [Huang et al., 2007] propose an algorithm to reduce observation variables for strong plans. This technique, however, cannot identify such a variable until a plan is constructed. Thus, it cannot be applied to our problem. Armano et al. [Armano et al., 2003] employ abstraction techniques for a hierarchical planner. Smith et al. [Smith et al., 2007] present an abstraction technique to generate exponentially smaller POMDP.

In this paper, we proposed approximation based techniques for WSC problems based on abstraction and refinement. Our preliminary experiment showed promising results. Several directions are ahead for future work. First, we plan to study other abstraction methods and refinement techniques to early converge the conclusion. Second, we will extend our technique for the WSC problem with more expressive goals (e.g., goals specified in temporal logics). Third, we want to study a tight bound for variables required to solve this problem.