Progression

In progression we can handle both causative effects and observations, so in general, progressing the action $a$ over the belief state $BS$ generates the set of successor belief states $B$ . The set of belief states $B$ is empty when the action is not applicable to $BS$ ( $BS \not\models \rho^e(a)$ ).

Progression of a belief state $BS$ over an action $a$ is best understood as the union of the result of applying $a$ to each model of $BS$ but we in fact implement it as BDD images, as in the MBP planner [3]. Since we compute progression in two steps, first finding a causative successor, and second partitioning the successor into observational classes, we explain the steps separately. The causative successor $BS'$ is found by progressing the belief state $BS$ over the causative effects of the action $a$ . If the action is applicable, the causative successor is the disjunction of causative progression (Progress$_c$ ) for each state in $BS$ over $a$ :

$$BS' = {\tt Progress}_c(BS, a) = \left\{ \begin{array} {c @{\qua... ...\cal M}(BS)} {\tt Progress}_c(S, a) & {\tt otherwise}\ \end{array} \right.$$

The progression of an action $a$ over a state $S$ is the conjunction of every literal that persists (no applicable effect consequent contains the negation of the literal) and every literal that is given as an effect (an applicable effect consequent contains the literal).

$$S' = {\tt Progress}_c(S, a) = \bigwedge\limits_{\substack{l:l \in... ...k{l: \exists_j\; S \models \rho^j(a) \;{\tt and} \ l \in \varepsilon^j(a)}} l$$

Applying the observations of an action results in the set of successors $B$ . The set is found (in Progress$_s$ ) by individually taking the conjunction of each sensor reading $o^j(a)$ with the causative successor $BS'$ . Applying the observations $\Theta(a)$ to a belief state $BS'$ results in a set $B$ of belief states, defined as:

$$B = {\tt Progress}_s(BS', a) = \left\{ \begin{array}{l @{\quad:\... ...' \vert BS'' = o^j(a) \wedge BS'\}& {\tt otherwise}\ \end{array} \right.\$$

The full progression is computed as:

$B$ = Progress($BS, a$ ) = Progress$_s($ Progress $_c(BS, a),a)$ .