3. 状态遍历
　　模型检验的基本思想就是对有限状态机模型进行状态空间的遍历，其最基本的操作是前向遍历（Forward Traversal）和逆向遍历（Backward Traversal），分别称为转换关系的image操作和inverse_image操作。给定用BDD表示的状态集合S以及转换关系N，则可用下述方法求得S的image和inverse_image：
　　　　　　imageV'(S) = V.[N(V, V')∧S(V)]
　　　　　　inverse_imageV(S) = V'.[N(V, V')∧S(V')]
其中imageV'(S)表示用V' 中的变量表示的image(S)的BDD结果，而inverse_imageV(S)则表示用V中的变量表示的inverse_image(S) 的BDD结果。
　　Image的意思是映像，即根据S(V) 中的每个现态和转换关系N (V, V')，求次态。而inverse_image则表示逆向映像，是从次态求现态，或者说，从现在求前面的状态。

　　4. 有限状态机模型的BDD表示
　　通用的有限状态机模型M是一个六元组：<I, O, S, δ, λ, s₀>，其中：
　　· I，O，S分别是M的输入域，输出域以及状态域；
　　· s₀∈S是M的初始状态；
　　· δ：I×S -> S 是M 的状态转换函数；
　　· λ：I×S -> O 是M 的输出函数。
　　对于这样一个有限状态机模型，我们可以分别用BDD来表示其I，O，S，以及状态转换函数以及输出函数。
　　给定有限状态机模型M = (I, O, S, δ, λ, s₀)，令用BDD表示的有限状态机为M^*=(I^*, O^*, S^*,δ^*,λ^*, s₀^*)，则具体过程如下:
　　首先，对输入集合I、输出集合O以及状态集合S进行二进制编码。令B = {0，1}，则编码后：
　　I^* = Bⁿⁱ，其中ni = [log |I|]。令i₁, i₂, …, i_ni为相应的输入变量；
　　O^* = B^no，其中no = [log |O|]。令o₁, o₂, …, o_no为相应的输出变量；
　　S^* = B^ns，其中ns = [log |S|]。令s₁, s₂, …, s_ns为相应的状态变量；
　　然后, 将状态转换函数δ和输出函数λ重新定义如下：
　　δ^*：I^*′S^*′S^*→B。对于任一输入i = ( i₁, i₂, …, i_ni)和两个状态sc = ( s_c1, s_c2, …, s_cns) 和sn = ( s_n1, s_n2, …, s_nns)，如果 δ(i, s_c) = s_n, 则δ*(i, s_c, s_n)= 1，否则δ^*(i,s_c, s_n) = 0。
　　λ^*：I^*′S^*′O^*→B。对于任一输入i = ( i₁, i₂, …, i_ni)、状态sc = ( s_c1, s_c2, …, s_cns)和输出o = ( o₁, o₂, …, o_no)，如果λ( i, s_c) = o, 则λ^*( i, s_c, o) = 1，否则λ^*( i, s_c, o) = 0。
　　这样，有限状态机模型M的状态转换函数和输出函数均变成布尔函数表示方式，也就可以采用BDD来表示。
　　这里符号很多，其实所表达的事实和前面说的一样，就是原来关于状态的关系，变成关于状态变量的关系，即输出函数和状态转换函数都转换成状态变量之间的关系，这些关系是都是布尔表达式，而这些布尔表达式用BDD表示。