The resulting BDD, APPLICABLE( ), represents the set of state-action pairs such that the action is applicable in the state. The BDD representing the states reachable from Q in one step is obtained with the following computation.

## =X (R(X, Α, X')^Q(X'/X]

Notice that, with this single operation, we symbolically simulate the effect of the application of any applicable action in A to any of the states in Q . Similarly, the following transformation allows to symbolically compute the SPreImage of a set of states Q under all possible actions in one single computation:

## Vx' (R(X, Α, X') → Q(X)[X/X']) ∧ Applicable(X, Α)

The resulting BDD represents all the state-action pairs ( x . α ) such that α is applicable in x and the execution of α in x results in states in Q .

## 5.3  Symbolic Search In The Space Of Belief States

The main strength of the symbolic approach is that it allows to perform a symbolic breadthfirst search, and it provides a way for compactly representing and efficiently expanding the frontier. For instance, plans can be constructed by symbolic breadth-first search in the space of states, repeatedly applying the strong pre-image to the goal states (Cimatti et al.,
1998b). However, the machinery presented in the previous section cannot be directly applied to tackle conformant planning. The basic difference is that with conformant planning we are searching in the space of belief states 3 , and therefore the frontier of the search is basically a set of sets of states. We introduce a way to symbolically represent BsP tables. Basically, this can be seen as a construction on demand, based on the algorithm steps, of increasingly large portions of the space of beliefstates. The key intuition is that a BsP table

$\{\langle\{s^{1}_{1},\ldots,s^{1}_{n_{1}}\}\cdot\pi_{1}\rangle,\ldots,\langle\{s^{k}_{1},\ldots,s^{k}_{n_{k}}\}\cdot\pi_{k}\rangle\}$
is represented as a relation between plans (of the same length) and states, by associating the plan directly with each state in the belief state indexed by the plan, as follows:

$$\left\{\left\langle s_{1}^{1}\ ,\ \pi_{1}\right\rangle,\ldots,\left\langle s_{n_{1}}^{1}\ ,\ \pi_{1}\right\rangle,\ldots,\left\langle s_{1}^{k}\ ,\ \pi_{k}\right\rangle,\ldots,\left\langle s_{n_{k}}^{k}\ ,\ \pi_{k}\right\rangle\right\}$$
$$\left({2}\right)$$

We use additional variables to represent the plans in the BsP tables. In order to represent plans of increasing length, at each step of the algorithm, a vector of new BDD variables, called plan variables , is introduced. The vector of plan variables introduced at the i-th step of the algorithm is written π |||, with | π ||| = | α || , and is used to encode the i-th to last action in the plan 4 . At step one of the algorithm, we introduce the vector of plan variables π 11 to represent the action corresponding to each 1-length possible conformant plan. The BsP