6.4 符号模型检验
6.4.2 用BDD隐式表示有限状态机
要在模型检验中使用BDD，首先需要将模型检验问题映射到布尔域。这就意味着需要将状态集合、转换关系以及状态遍历等都映射为布尔函数。
3. 状态遍历
4. 有限状态机模型的BDD表示