Dottorato in INGEGNERIA INFORMATICA

Titolo della tesi: 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 potentials 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 \myi an in-depth study of the pure-past linear temporal logics, \myii their effective applicability as formal languages to specify temporally extended goals in deterministic and nondeterministic planning, and \myiii 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, \PLTLf and \PLDLf, 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.