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:
- Always ship frozen food in a refrigerated truck.
- Prefer to deliver priority packages before regular packages.
- If the customer is a preferred customer, then always apply a 15% discount to the final bill.
- Prefer to deliver domestic packages within 24 hours of receipt.
- While a truck is at a location and not full, load all packages bound for a different destination on the truck; drive to the next destination; unload all packages to be delivered to this destination.
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 |
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.