Using Linear Temporal Logic to Model and Solve Planning Problems

In this work we investigate the use of propositional linear temporal logic LTL as a specification language for planning problems and the use of analytic tableaux as a tool for plan search, following the “planning as satisfiability” approach [11]. We claim that LTL can be a good specification language for planning problems, because of its rich expressive power and the underlying simple model of time and actions. We propose the use of Tabplan, a tableau calculus for bounded model search in LTL (fully described in [7]), as a system for plan synthesis. We show how to code a given planning problem by means of different LTL theories, each encoding making the model construction procedure simulate a different search strategy, namely planning by progression and partial order regression planning in the style of [14]