论文标题
计划在纯past线性时间逻辑中的时间扩展目标:多项式减少到标准计划
Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic: A Polynomial Reduction to Standard Planning
论文作者
论文摘要
我们研究以纯Past LTL(PPLTL)表达的时间扩展目标。 PPLTL对于表达目标特别有趣,因为它允许表达复杂的任务,就像在正式方法文献中一样,而确定性和非确定性域(FOND)中规划的最差计算复杂性仍然与经典可及性目标相同。但是,尽管对PPLTL目标的计划理论有充分的理解,但尚未对实用工具进行专门研究。在本文中,我们在构建实际工具来处理PPLTL目标方面取得了重大飞跃。我们设计一种技术,将PPLTL目标的计划转化为标准计划。我们通过一些比较实验显示了翻译,复杂性及其实际有效性的正式正确性。结果,我们的翻译使最新的工具(例如FD或MYND)能够无缝处理PPLTL目标,从而保持了他们对经典可及性目标的令人印象深刻的表现。
We study temporally extended goals expressed in Pure-Past LTL (PPLTL). PPLTL is particularly interesting for expressing goals since it allows to express sophisticated tasks as in the Formal Methods literature, while the worst-case computational complexity of Planning in both deterministic and nondeterministic domains (FOND) remains the same as for classical reachability goals. However, while the theory of planning for PPLTL goals is well understood, practical tools have not been specifically investigated. In this paper, we make a significant leap forward in the construction of actual tools to handle PPLTL goals. We devise a technique to polynomially translate planning for PPLTL goals into standard planning. We show the formal correctness of the translation, its complexity, and its practical effectiveness through some comparative experiments. As a result, our translation enables state-of-the-art tools, such as FD or MyND, to handle PPLTL goals seamlessly, maintaining the impressive performances they have for classical reachability goals.