In progression we can handle both causative effects and observations, so in general, progressing the action over the belief state generates the set of successor belief states . The set of belief states is empty when the action is not applicable to ( ).
Progression of a belief state over an action is best understood as the union of the result of applying to each model of but we in fact implement it as BDD images, as in the MBP planner . 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 is found by progressing the belief state over the causative effects of the action . If the action is applicable, the causative successor is the disjunction of causative progression (Progress ) for each state in over :
The progression of an action over a state 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).
Applying the observations of an action results in the set of successors . The set is found (in Progress ) by individually taking the conjunction of each sensor reading with the causative successor . Applying the observations to a belief state results in a set of belief states, defined as:
The full progression is computed as:
= Progress( ) = Progress Progress .