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