Temporalising Separation Logic for Planning with Search Control Knowledge

Temporalising Separation Logic for Planning with Search Control Knowledge

Xu Lu, Cong Tian, Zhenhua Duan

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 1167-1173. https://doi.org/10.24963/ijcai.2017/162

Temporal logics are widely adopted in Artificial Intelligence (AI) planning for specifying Search Control Knowledge (SCK). However, traditional temporal logics are limited in expressive power since they are unable to express spatial constraints which are as important as temporal ones in many planning domains. To this end, we propose a two-dimensional (spatial and temporal) logic namely PPTL^SL by temporalising separation logic with Propositional Projection Temporal Logic (PPTL). The new logic is well-suited for specifying SCK containing both spatial and temporal constraints which are useful in AI planning. We show that PPTL^SL is decidable and present a decision procedure. With this basis, a planner namely S-TSolver for computing plans based on the spatio-temporal SCK expressed in PPTL^SL formulas is developed. Evaluation on some selected benchmark domains shows the effectiveness of S-TSolver.
Keywords:
Knowledge Representation, Reasoning, and Logic: Geometric, Spatial, and Temporal Reasoning
Planning and Scheduling: Other approaches to planning
Knowledge Representation, Reasoning, and Logic: Logics for Knowledge Representation
Constraints and Satisfiability: Satisfiability