Efficient techniques for automated planning for goals in linear temporal logics on finite traces

One of the greatest challenges of the modern era is to empower AI systems with the ability to deliberate and act autonomously while mitigating the risks that arise from granting such power. To address this challenge, a promising approach is to incorporate behavioral specifications within AI systems using formal languages, especially linear temporal logics. We are interested in efficiently combining temporal logics on finite traces with automated planning, which is an AI model-based approach to producing autonomous behavior and solving the problem of sequential decision-making. Despite the ample literature on the application of linear temporal logics on finite traces, LTLf and LDLf, in planning and related fields, limited attention has been given to the study and use of the pure-past linear temporal logics and their potential for specifying temporal goals in planning. Furthermore, the application of temporal logics to other related research areas where planning techniques have been successfully employed, such as business process management and business automation, has been given relatively little focus, and there is a lack of principled research on the topic. In this dissertation, we propose (i) an in-depth study of the pure-past linear temporal logics, (ii) their effective applicability as formal languages to specify temporally extended goals in deterministic and nondeterministic planning, and (iii) the application of planning techniques to solve the declarative trace alignment in business process management while envisioning new methods to solve workflow construction from natural language in business automation. More specifically, we first review the pure-past linear temporal logics, PPLTL and PPLDL, and we show how we can exploit a foundational result on reverse languages to get an exponential improvement over LTLf/LDLf, when computing the corresponding deterministic automata. Given this key result, we introduce an efficient technique to cleverly evaluate the truth of pure-past formulas given the truth value of a small set of subformulas, thus enabling the development of more efficient algorithms. Consequently, in the context of deterministic and nondeterministic planning for pure-past temporally extended goals, we present a novel efficient encoding into standard planning for final-state goals with minimal overhead, and that is at most linear in the size of the goal formula and does not add additional spurious actions. As for declarative trace alignment, we extend process model specifications to full LTLf/LDLf, provide a reduction to cost-optimal planning, and devise new practical encodings. Finally, focusing on the enterprise use of business automation, we look into the latest techniques in natural language understanding and large language models to translate English instructions to LTL formulas, bridging the gap between the end user and reasoning engines used to construct automatic workflows.