Planning Based On Model Checking

Planning in artificial intelligence is concerned with developing methods that reason about the consequences of actions to determine how best to achieve given objectives. Planning is a key technology for building intelligent systems in areas such as manufacturing, space systems, software engineering, robotics, education, and entertainment. In this paper, we at first introduce briefly the familiar method of solving planning problems, and point out their advantages and disadvantages, then introduce model checking, ordered binary decision diagraph, the representation and computation of transition relation, the partition of transition relation, and a planning domain description language defined by myself ADL. At last, introduce the planner based on the model checking, we name it MYPLANNER. Model checking is an automation verification method used in finite state concurrence systems. In this verification method, temporal logic specifications are checked through exploration state space. Boolean functions can represent state space using symbols, which we call symbol model checking. Because the state space is represented implicitly, we often can explore very large state space. Model checking has already been applied in electro circuit control and communication protocols to find micro errors. Usually, the consumers provide high level representation and specifications needed being checked. The model checking arithmetic either return true and end that is to say the model satisfies the specification, or give a counterexample, that means the specification are not satisfied. Reduced Ordered Binary Decision Diagrams, are also called OBDD or BDD for short. It can representation Boolean functions completely specification. In essence, it is a compact truth table. For a non-constant Boolean function, OBDD is a directed acyclic diagraph. The operation about Boolean functions can be implemented to diagraph arithmetic of OBDD. OBDD is a compact and strong data structure for describing Boolean functions, is a very important tool in many research fields such as model checking, verification and compose of hardware circuit. The state Q of automaton M is represented by all possible assignments of variables assignments. The input Σof M is all actions of agent. We use transition relations to represent the relation of all current state and input. T ?S×A×S is a transition relation, T(s,a,s′) is true if action a is applicable in state s and can cause state s transiting to s′. We can describe automaton using Boolean functions. Image computation: For a state set R, its image is a state set that state machine can arrive from the current state(set) through one step transition. Preimage computation: For a state set R, its preimage is a state set that state machine can from any one state of the set can reach one state in state set R through one step transition. Using model checking method to find a plan of planning problem equals finding a state path that connects the initial state and the goal set in the automaton representing the planning domain. Using model checking method to solute planning problem is based on translating planning problems to the exploration of finite state machine. Every transition of automaton represents executing an action in a given state. We use OBDD and symbol model checking technology encoding representation and exploring automaton. It starts from the initial state, according actions applicable, traverse width first, until reach the goal or a fixed point namely at that point, there is no newly produced state. The main principle in the exploration is that the operated object is state set, not a single state. There are several planner developed based on model checking. But, all of them do not make use of the up to date research products in model checking such as partition and abstraction. In MYPLANNER, the special data structure OBDD is used. According the characters of computation of relation product and quantification of quantifiers, transition relation is partitioned and quantifiers are quantified early, so the complex of relation product is reduced greatly. For the ordering of OBDD variables, we use dynamic ordering and improve according to the system character. We at first give a very reasonable initial ordering, then using sieving method to improve the ordering. Partition is a very famous method in model checking. The basic idea is partitioning the transition relation to the disjunction or conjunction of smaller expressions, being referred to as disjunction partition or conjunction partition. We in chief discuss conjunction partition. There are three advantages through partitioning. (1) It can reduce the complex of computing the transition relation; (2) it can reduce the total node number of OBDD; (3) it is the most important, it can reduce the computation complex of image and preimage.