ExpandBspTABLE($BspPT$)$\doteq\bigcup\limits_{\langle\,Bs\,\,,\,\pi\rangle\in BspT}$ExpandBspPAIR($\langle\,Bs\,\,,\,\pi\rangle$)
$$B\,s^{I}\,=\,S P r e\,I m a\,g e\,[\,\alpha](B\,s)\,\neq\,\varnothing\}$$
$$(\langle B\,s\ ,\ \pi\,\rangle)\,\doteq\,\{\langle B$$
$$s^{\prime}\quad.$$
EXPANDBSPPAIR( \B s . π ⟩ ) = { ⟨ B s . α ; π ⟩ | such that B s ′ = SPreImage[α ]( B s ) ̸ = ∅}
PRUNEBSPTABLE(BsPT, BsPTables, i) = { ( Bs . π ) E BsPT | for all j < i, there is no { Bs . π ′ } E BsPTables[j] such that ( Bs ′ = Bs )}
E XTRACTS OLUTION (I, BsPT) = { π | there exists ⟨ Bs . π ⟩ ∈ BsPT such that I ⊆ Bs }
Figure 5: The primitives used by the conformant planning algorithm.

## 5. Conformant Planning Via Symbolic Model Checking

Model checking is a formal verification technique based on the exploration of finite state automata (Clarke, Emerson, & Sistla, 1986). Symbolic model checking (McMillan, 1993) is a particular form of model checking using Binary Decision Diagrams to compactly represent and efficiently analyze finite state automata. The introduction of symbolic techniques into model checking led to a breakthrough in the size of model which could be analyzed (Burch et al., 1992), and made it possible for model checking to be routinely applied in industry, especially in logic circuits design (for a survey see Clarke & Wing, 1996).

In the rest of this section, we will provide an overview of Binary Decision Diagrams, and we will describe the representation of planning domains, based on the BDD-based representation of finite state automata used in model checking. Then, we will discuss the extension which allows to symbolically represent BsP tables and their transformations, thus allowing for an efficient implementation of the algorithm described in the previous section.

## 5.1  Binary Decision Diagrams

A Reduced Ordered Binary Decision Diagram (Bryant, 1992, 1986) (improperly called Bdd)
is a directed acyclic graph (DAG). The terminal nodes are either True or False. Each nonterminal node is associated with a boolean variable, and two BDDs, called left and right branches. Figure 6 (a) depicts a Bdd for ( a 1 ↔ b 1 ) ∧ ( a 2 ↔ b 2 ) ∧ ( a 3 ↔ b 3 ). At each non-terminal node, the right [left, respectively] branch is depicted as a solid [dashed, resp.]
line, and represents the assignment of the value True [ False, resp.] to the corresponding variable.  A BDD represents a boolean function.  For a given truth assignment to the variables in the BDD, the value of the function is determined by traversing the graph from the root to the leaves, following each branch indicated by the value assigned to the variables 1 . The