Abstract:Planning by model checking is an approach to planning under uncertainty that deals with nondeterminism. Three ways which obtain hierarchical states for searching weak planning, strong planning, andstrong cyclic planning are respectively designed. Based on hierarchical states, some important conclusions on aweak solution, a strong solution, and a strong cyclic solution are obtained. What can be eliminated directly are allfound when a weak solution, a strong solution, and a strong cyclic solution are in turn searched. Therefore manystate-action pairs can be eliminated directly before starting planning. In fact, a way has been given which is basedon a search proceeding forwards from the initial states towards the goal states.