Adversarial Planning Via Symbolic Model Checking

Intelligent planning is an important field in AI. In classical planning, the planning problems must satisfy the following assumptions: the initial state is completely specified, the effects of the action are deterministic, and environmental changes are completely predictable and well known, which make the scope of the problems handled by the resulting classical planners very limited. To solve real problems, nowadays, people have attached importance to the research on incomplete information and uncertain effects. The remarkable fruits have been made: the improvements on Graphplan including CGP, SGP, the different class of universal plan via model checking.Model checking is a formal verification by exhaustive search to finite state automata. And efficient search techniques have been developed in model checking. Planning problems can be translated as finite state automata. So it is natural and reasonable to apply model checking to planning problem. Due to large state space of real world, the method of model checking has brought state explosion problem. Ordered Binary Decision Diagram has been applied to represent finite state automata, which is a compact representation of propositional formula. This representation can save large space, by which large state space problems can be solved successfully.In this paper, the theory of planning via OBDD-based symbolic model checking is employed. And the contributions are in the following:An adversarial planning algorithm based on symbolic model checking is proposed, which combines hill-climbing and weak universal planning algorithm in model checking, and senses the behavior of environment agents by means of sensing actions.An adversarial planning system has been developed based on UMOP, in which heuristic search strategy is applied to speed up the problem-solving;NADL domain description language is applied, which has powerful expressiveness and can handle non-deterministic and multi-agent domains;the system can solve complex adversarial planning problems, hence, it has wide application in reality.