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].
Cerrito, S., Cialdea, M. (1998). Using Linear Temporal Logic to Model and Solve Planning Problems. In Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'98) (pp.141-152). BERLIN HEIDELBERG : Springer-Verlag [10.1007/BFb0057441].
Using Linear Temporal Logic to Model and Solve Planning Problems
CIALDEA, Marta
1998-01-01
Abstract
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].I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
