智能规划是当前人工智能的热点领域，具有突出的理论和应用价值。基于模型检测的规划方法是最近发展起来的新方法，它可以处理带有不确定性的规划问题，例如涉及可达性目标的、限于部分可观察的或者面向扩展的规划目标的规划问题，这种方法的关键思想是利用模型理论来解决规划问题。 本文重点介绍了使用基于模型检测的方法来处理带有不确定性的规划问题。介绍了对可达性目标、对扩展目标和在部分可观察领域作规划的思想方法。回顾了对可达性目标作规划的弱规划算法、强规划算法和强循环规划算法，研究了这三个算法的思想，指出了它们各自的特点和不足之处。对在有向图中用邻接矩阵求可达性关系进行了研究，提出了不确定状态转移系统的超图、不确定状态转移系统的超图的邻接矩阵和不确定状态转移系统中的状态之间的可达性关系等概念。设计了用不确定状态转移系统的超图的邻接矩阵求不确定状态转移系统中的状态之间的可达性关系的方法。利用不确定状态转移系统的超图、不确定状态转移系统的超图的邻接矩阵和不确定状态转移系统中的状态之间的可达性关系得到了关于弱规划解、强规划解和强循环规划解的一些重要性质和定理。这些性质和定理是关于一些状态动作序偶是否不可能参与构成弱规划解、强规划解和强循环规划解的结论，通过这些性质和定理可以将很多状态动作序偶直接去掉，从而大大简化求解过程。分别设计了对求弱规划解、强规划解和强循环规划解的问题中的状态进行分层的方法，分别获得了求弱规划解、强规划解和强循环规划解时状态被分层后的一些重要性质和定理，这些性质和定理是关于一些状态动作序偶是否可以不参与构成弱规划解、强规划解和强循环规划解的结论，通过所获得的这些性质和定理可以将很多状态动作序偶直接去掉，从而减少问题规模，大幅度提高求规划解的效率。本文还将不确定状态转移系统中的状态之间的可达性关系和不确定状态转移系统中的状态分层的方法用于对可达性目标求弱规划、强规划和强循环规划的算法设计中，重新设计了对可达性目标求弱规划、强规划和强循环规划的算法。实际上，本文提出了在用模型检测方法求不确定状态转移系统中的规划问题的规划解时先采用正向搜索技术对规划问题进行化简的思想并设计了采用正向搜索技术对规划问题进行化简的方法。