论文部分内容阅读
状态爆炸是模型检验需解决的一个关键问题．基于GPVW算法，以及从LTL公式导出识别该公式的Bachi自动机，用OBDD符号表示，通过符号操作求解自动机乘积．采用符号方法求解出含有初始状态或接受状态的最大连通图，判断自动机是否存在初始状态能否到达含有接收状态的最大连通分支，从而判定所接受的语言是否非空来模型检验LTL公式．采用本文所提出模型检验LTL公式的方法，能在一定程度上解决空间爆炸问题．