A planner fully based on linear time logic

摘要

This work aims at verifying the effective possibility of using Linear Time Logic (LTL) as a planning language. The main advantage of such a rich and expressive language is the possibility of encoding problem specific information, that can be of help both in reducing the search space and finding a better plan. To this purpose, we have implemented a planning system, PADOK (Planning with Domain Knowledge), where the whole planning domain is modeled in LTL and planning is reduced to model search. We briefly describe the components of problem specifications accepted by PADOK, that may include knowledge about the domain and control knowledge, in a declarative format. Some experiments are then reported, comparing the performances of PADOK with some well established existing planners (IPP, BLACKBOX and STAN) on some sample problems. In most cases, our system is guided by additional knowledge that cannot be stated in the languages accepted by the other planners. In general, when the complexity of the problem instances increases, the behaviour of PADOK improves, with respect to the other planners, and it can solve problem instances that other systems cannot.