We study planning for temporally extended goals expressed in Pure-Past Linear Temporal Logic ( ppltl ) in the context of deterministic (i.e., classical) and fully observable nondeterministic (FOND) domains. ppltl is the variant of Linear-time Temporal Logic on finite traces ( ltl f ) that refers to the past rather than the future. Although ppltl is as expressive as ltl f , we show that it is computationally much more effective for planning. In particular, we show that checking the validity of a plan for a ppltl formula is Markovian. This is achieved by introducing a linear number of additional propositional variables that capture the validity of the entire formula in a modular fashion. The solution encoding introduces only a linear number of new fluents proportional to the size of the ppltl goal and does not require any additional spurious action. We implement our solution technique in a system called Plan4Past , which can be used alongside state-of-the-art classical and FOND planners. Our empirical analysis demonstrates the practical effectiveness of Plan4Past in both classical and FOND problems, showing that the resulting planner performs overall better than other planning approaches for ltl f goals.

We present Lemming – a visualization tool for the interactive selection of plans for a given problem, allowing the user to efficiently whittle down the set of plans and select their plan(s) of choice. We demonstrate four different user experiences for this process, three of them based on the principle of using disjunctive action landmarks as guidance to cut down the set of choice points for the user, and one on the use of linear temporal logic (LTL) to impart additional constraints into the plan set using natural language (NL) instruction.

Abstract Goal Recognitionis the task of discerning the intended goal that an agent aims to achieve, given a set of goal hypotheses, a domain model, and a sequence of observations (i.e., a sample of the plan executed in the environment). Existing approaches assume that goal hypotheses comprise a single conjunctive formula over a single final state and that the environment dynamics are deterministic, preventing the recognition of temporally extended goals in more complex settings. In this paper, we expand goal recognition totemporally extended goalsinFully Observable Non-Deterministic(fond) planning domain models, focusing on goals on finite traces expressed inLinear Temporal Logic(ltl $$_f$$ f ) andPure-Past Linear Temporal Logic(ppltl). We develop the first approach capable of recognizing goals in such settings and evaluate it using differentltl $$_f$$ f andppltlgoals over sixfondplanning domain models. Empirical results show that our approach is accurate in recognizing temporally extended goals in different recognition settings.

This is a demonstration of our newly released Python package NL2LTL which leverages the latest in natural language understanding (NLU) and large language models (LLMs) to translate natural language instructions to linear temporal logic (LTL) formulas. This allows direct translation to formal languages that a reasoning system can use, while at the same time, allowing the end-user to provide inputs in natural language without having to understand any details of an underlying formal language. The package comes with support for a set of default LTL patterns, corresponding to popular DECLARE templates, but is also fully extensible to new formulas and user inputs. The package is open-source and is free to use for the AI community under the MIT license. Open Source: https://github.com/IBM/nl2ltl. Video Link: https://bit.ly/3dHW5b1

Recently, Pure-Past Temporal Logic (PPLTL) has proven highly effective in specifying temporally extended goals in deterministic planning domains. In this paper, we show its effectiveness also for fully observable nondeterministic (FOND) planning, both for strong and strong-cyclic plans. We present a notably simple encoding of FOND planning for PPLTL goals into standard FOND planning for final-state goals. The encoding only introduces few fluents (at most linear in the PPLTL goal) without adding any spurious action and allows planners to lazily build the relevant part of the deterministic automaton for the goal formula on-the-fly during the search. We formally prove its correctness, implement it in a tool called Plan4Past, and experimentally show its practical effectiveness.

We review PLTLf and PLDLf, the pure-past versions of the well-known logics on finite traces LTLf and LDLf, respectively. PLTLf and PLDLf are logics about the past, and so scan the trace backwards from the end towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, over LTLf /LDLf , for computing the corresponding DFA. This exponential improvement is reflected in several forms of sequential decision making involving temporal specifications, such as planning and decision problems in non-deterministic and non-Markovian domains. Interestingly, PLTLf (resp., PLDLf ) has the same expressive power as LTLf (resp., LDLf ), but transforming a PLTLf (resp., PLDLf ) formula into its equivalent LTLf (resp.,LDLf) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLDLf .