This work presents an approach to artificial intelligence planning based on linear temporal logic (LTL). The language PDDL-K (Planning Domain Description Language with control Knowledge), a simple and easy-to-use planning language, is described. This language allows one to specify a planning problem together with heuristic information that can be of help for both pruning the search space and find better plans. The semantics of the language is given in terms of a translation into a set of LTL formulae. Planning is then reduced to ``executing'' the LTL encoding, i.e. to model search in LTL. The choice of LTL is due to two main reasons. First of all, it allows a simple and natural representation of a world that changes over time. Secondly, it is decidable. These two features together free planning in LTL from the above mentioned inconveniences of planning in (either propositional or first-order) classical logic. Moreover, domain dependent knowledge as well as intermediate tasks can be easily expressed both in LTL The feasibility of the approach has been successfully tested by means of the system Pdk, an implementation of the proposed method. Since expressing control knowledge correctly as LTL formulae can be quite a delicate task, Pdk has equipped by tools supporting the domain expert in the specification task, in particular debugging tools, and the language PDDL-K.
Linear Temporal Logic as An executable semantics for planning languages
POGGIONI, VALENTINA;
2007
Abstract
This work presents an approach to artificial intelligence planning based on linear temporal logic (LTL). The language PDDL-K (Planning Domain Description Language with control Knowledge), a simple and easy-to-use planning language, is described. This language allows one to specify a planning problem together with heuristic information that can be of help for both pruning the search space and find better plans. The semantics of the language is given in terms of a translation into a set of LTL formulae. Planning is then reduced to ``executing'' the LTL encoding, i.e. to model search in LTL. The choice of LTL is due to two main reasons. First of all, it allows a simple and natural representation of a world that changes over time. Secondly, it is decidable. These two features together free planning in LTL from the above mentioned inconveniences of planning in (either propositional or first-order) classical logic. Moreover, domain dependent knowledge as well as intermediate tasks can be easily expressed both in LTL The feasibility of the approach has been successfully tested by means of the system Pdk, an implementation of the proposed method. Since expressing control knowledge correctly as LTL formulae can be quite a delicate task, Pdk has equipped by tools supporting the domain expert in the specification task, in particular debugging tools, and the language PDDL-K.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
