随着计算机软硬件系统日益复杂,保证系统的正确性和可靠性日显重要,为此提出的许多理论和方法中,模型检测以其简洁明了和自动化程度高而引人注目。论文介绍了二元决策图的基本原理与研究现状,针对影响二元决策图结构的因素——变量排序进行了深入分析;给出了节点规模优化的排序算法的改进思想;研究了利用动态交换来完成路径数量优化的方法,提出了OSMNP排序优化算法。该算法通过对节点路径的定义和记录,实现了在变量交换中局部路径改变量向全局改变量的转移,从而实现路径数量的优化。论文还研究了基于二元决策图的故障树分析的排序和转化问题,提出一种快速有效的LNPC方法,该方法采用逐渐分解的策略直接完成子事件的排序与组合,一次性地实现故障树到二元决策图的转化与优化,并通过实例验证了其有效性。OSMNP算法利用相邻变量交换的有效性能获取最少路径的排序;LNPC算法通过按定义的规则遍历故障树不仅完成底事件的优化排序,同时也有效地实现了故障树向二元决策图的转化,这些研究成果对二元决策图应用的深入有较好的理论意义和一定的实用价值。