table BsPT 1 at level 1 is built by EXPANDBSPTABLE by performing the following BDD computation starting from the BsP table at level 0, i.e. G( x ):

## (Vx' (R(X, A, X') -> G(X)[X/])  A  Applicable(X, A))[A/X/]]

The computation collects those state-action pairs ( x . α ) such that (the action represented by) α is applicable in (the state represented by) x, and such that all the resulting (states represented by) x' are goal states. Then we replace the vector of action variables α with the first vector of plan variables π [1]. The resulting BDD, BsPT( x, π [1]), represents a BsP
table containing plans of length one in the form of a relation between states and plans as in (2). In the general case, after step i - 1, the BsP table BsPT i –1, associating belief states to plans of length i - 1, is represented by a BDD in the state variables i and in the plan variables 711implemented as the following BDD transformation on BsPT i - 1
(VI'.(R(x, a, x') → BsPTi-1(x, π |i-1|i , . . , π |i|)[x, x'])   ∧   Applicable(x, α))[α/π |i|(3)
The next state variables in R and in BsPT i –1 (resulting from the forward shifting) disappear because of the universal quantification. The action variables are renamed to the newly introduced plan variables π iji, so that in the next step of the algorithm the construction can be repeated.

EXTRACTS OLUTIO N extracts the assignments to plan variables such that the corresponding set contains the initial states. In terms of BDD transformations, EXTRACTS O LUTION is implemented as follows:

Vxx (I(x) -> BsPTi(x, 71i1, . . . , 711))
(4)
The result is a BDD in the plan variables 71 no solutions of length i.  Otherwise, each of the satisfying assignments to the resulting BDD
represents a conformant solution to the problem.

To guarantee the termination of the algorithm, at each step the BsP table returned by E X P A N D B S P  T A B L E  is simplified by  P R U N E B S P  T A B L E  by  removing  all the  belief states which do not deserve further expansion. This requires the comparison of the belief states contained in the BsP table with the belief states contained in each of the BsP tables built at previous levels.  This is one of the crucial steps in terms of efficiency.  An earlier implementation of this step with logical Bdd transformations, following directly from the set-theoretical definition of PRUNEBSPTABLE, was extremely inefficient (Cimatti & Roveri, 1999). Furthermore, we noticed that the serial encoding could yield BsP tables containing a large nmber of equivalent plans, all indexing exactly the same belief state. Often these equivalent plans only differ in the order of some independent actions, and this is a potential source of combinatorial explosion.  This occurs even in the simple version of the BTUC (in Figure 3, two equivalent conformant plans are associated with Bss). Therefore, we developed a new implementation which could tackle these two problems by operating directly on the BsP
table. The idea is depicted in Figure 7. Initially, the cache contains Bs 1 , Bs 2 and Bs 3 . The simplification performs a traversal of the BDD, by accumulating the subtrees representing belief states, comparing them with the ones built at previous levels, and inserting the new ones in the cache (in Figure 7, Bs 4 , Bs 5 and Bs 6 ). Each time a path is identified which