I. Motivation

Automated planning is a subfield of Artificial Intelligence that concerns the generation of a set of actions and orderings – a plan – for execution by agents to realize a goal. While significant advances have been made in automated planning involving final-state goals, most real-world planning problems involve complex goals that are temporally extended, necessitate the optimization of preferences or other quality measures, require adherence to safety constraints and directives, and/or may require or benefit from following a prescribed high-level script that specifies how the task is to be realized. By way of illustration, consider a logistics company that transports packages. Package delivery may be governed by the following types of (possibly inconsistent) goals:

Such goals are typically specified in the subset of Linear Temporal Logic (LTL) found in the Planning Domain Description Language, PDDL3.0 [3].

In a series of well-received lectures between 2011 and 2013, Moshe Vardi advocated convincingly for the benefits of LTL, but also discussed its limitations in the context of industry-driven verification tasks (e.g., [5]). In response to LTL’s limitations, Vardi advocated Linear Dynamic Logic (LDL)), a temporal logic that combines LTL and Regular Expressions (REs) in a manner that avoids the exponential increase in size that typically plagues REs in such a context. Subsequently, De Giacomo and Vardi [2], proposed LDLf, which defines LDL over finite traces, citing automated planning among the applications for the logic.

In brief, LDL is semantically a very powerful language that can serve as a goal specification vehicle for a myriad of applications in automated planning and beyond, ranging from business process management/monitoring and Internet of Things, to high-level robot control. However, we believe that despite the great mathematical power of LDL, its syntax is not very intuitive. To mend this, we propose LTL-RE: a language with a user-friendly syntax whose expressive power is no less than that of LDL. We also propose a means of efficiently planning with LTL-RE, and thus LDL, by exploiting highly optimized classical planning technology. The critical question of how to efficiently generate plans with goals specified in LDL (or LTL-RE) has not yet been explored in the literature.

II. Contributions

We propose LTL-RE, a high-level language that supports the specification of a wide variety of temporal goals, not only using LTL but also using REs. LTL- RE derives its formal foundation from finite Linear Dynamic Logic (LDLf), and its expressive power is no less than that of regular expressions. LTL- RE augments LDLf with planning-friendly syntax including LTL and typical programming language constructs. It is also designed for use with AI automated planning transition systems, supporting state-, action-, and path-oriented temporal goal specification. Further, we propose a translation of LTL-RE goals into classical planning domains for use with state-of-the-art classical planners. Unlike previous reformulation approaches that exploited Non-deterministic Finite State Automata (NFAs) (e.g., [1]), we exploit an approach based on Alternating Automata following Torres and Baier [4] that avoids the worst-case exponential increase in size inherent to NFAs. We evaluated the behavior of our translator and the resultant planning problems, with comparison to alternative LTL translators.

III. Analysis

We have implemented the translator for LTL-RE. Since realistic benchmarks exist only in limited ways and only for the LTL fragment of LTL- RE, the comparative experimental analysis reported here is solely for the LTL fragment of LTL-RE.

We compared the performance of our LTL-RE translator both to a Non-Deterministic Finite state Automata (NFA)-based LTL translator initially introduced in [1], and to an Alternating Automata (AA)-based LTL translator [4], similar to ours. The NFA-based LTL translator is highly optimized to avoid, in most cases, the exponential increase in the size of the automata characteristic of NFA-based representations of LTL. The AA translator exists in two versions: a naive one without engineering optimizations, and an optimized version. In order to fairly compare against our LTL-RE translator, which currently lacks the implementation of analogous optimizations, we compared against the similarly unoptimized AA-based LTL translator. Even this comparison is not entirely appropriate. The LTL-RE translator is designed to translate all of LDLf, including REs, LTL, and additional programming language constructors. We expected that a special-purpose translator that is tuned exclusively to LTL would be more efficient than the LTL portion of a more general LTL-RE translator at least before implementation of optimizations.

NFA translator AA-LTL LTL-RE
TT PL PT PS TT PL WPL PT PS TT PL WPL PT PS
p01 0.051 2 0.00 3 0.108 15 2 0.00 73 0.112 15 2 0.00 48
p02 0.044 3 0.00 4 0.093 22 3 0.00 139 0.110 22 3 0.00 96
p03 0.051 7 0.00 16 0.113 50 7 0.00 719 0.113 53 7 0.00 547
p04 0.058 10 0.00 27 0.112 75 10 0.01 3351 0.115 83 10 0.01 2959
p05 0.049 14 0.00 43 0.115 104 13 0.03 15575 0.139 121 13 0.04 16672
p06 0.303 14 0.00 43 0.117 99 13 0.04 16213 0.135 110 13 0.04 17153
p07 0.077 4 0.00 6 0.095 32 4 0.00 1555 0.115 32 4 0.00 1454
p08 3.568 7 0.00 11 0.116 55 6 0.04 20920 0.125 62 6 0.09 33262
p09 72.556 9 0.02 20 0.113 67 7 0.18 74360 0.133 78 7 0.57 156892
p10 72.614 9 0.02 20 0.119 68 7 0.22 89464 0.144 79 7 1.01 227686
Table 1: Results for domain Blocksworld, depicting translation time (TT), plan length (PL), total planning time (PT), number of planning states that were evaluated before the goal was reached (PS), and world plan length (WPL), which denotes the number of planning actions in PL (excluding the actions that are responsible for the automaton synchronization).

References

[1] Baier, J., and McIlraith, S. 2006. Planning with first-order temporally extended goals using heuristic search. In Proceedings of the 21st National Conference on Artificial Intelligence (AAAI06), 788–795.

[2] De Giacomo, G., and Vardi, M. Y. 2013. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI).

[3] Gerevini, A.; Haslum, P.; Long, D.; Saetti, A.; and Dimopoulos, Y. 2009. Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artificial Intelligence 173(5-6):619–668.

[4] Torres, J., and Baier, J. A. 2015. Polynomial-time reformulations of ltl temporally extended goals into final-state goals. In Proceedings of the Workshop on Model-Checking and Automated Planning (MOCHAP) at ICAPS-2015.

[5] Vardi, M. Y. 2012. The rise and fall of temporal logic. Keynote, 13th International Conference on Principles of Knowledge Representation and Reasoning.