Efficient Techniques for Automated Planning for Goals in Linear Temporal Logics on Finite Traces

Simple item page
dc.contributor.advisorGiacomo, Giuseppe De
dc.contributor.advisorLespérance, Yves
dc.contributor.authorFuggitti, Francesco
dc.date.accessioned2023-12-08T14:45:49Z
dc.date.available2023-12-08T14:45:49Z
dc.date.issued2023-12-08
dc.date.updated2023-12-08T14:45:49Z
dc.degree.disciplineElectrical Engineering & Computer Science
dc.degree.levelDoctoral
dc.degree.namePhD - Doctor of Philosophy
dc.description.abstractOne 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.
dc.identifier.urihttps://hdl.handle.net/10315/41760
dc.languageen
dc.rightsAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.
dc.subjectArtificial intelligence
dc.subjectComputer science
dc.subject.keywordsArtificial intelligence
dc.subject.keywordsComputer science
dc.subject.keywordsAutomated planning
dc.subject.keywordsAI planning
dc.subject.keywordsSequential decision-making
dc.subject.keywordsClassical planning
dc.subject.keywordsDeterministic planning
dc.subject.keywordsFond planning
dc.subject.keywordsNondeterministic planning
dc.subject.keywordsPlanning domain definition language
dc.subject.keywordsFormal methods
dc.subject.keywordsFormal languages
dc.subject.keywordsFinite automata
dc.subject.keywordsAlternating automata
dc.subject.keywordsNondeterministic automata
dc.subject.keywordsDeterministic automata
dc.subject.keywordsBusiness process management
dc.subject.keywordsBusiness automation
dc.subject.keywordsLinear temporal logics
dc.subject.keywordsPure-past linear temporal logics
dc.subject.keywordsTemporally extended goals
dc.subject.keywordsPlanning for temporally extended goals
dc.subject.keywordsTrace alignment
dc.subject.keywordsDeclarative trace alignment
dc.subject.keywordsConformance checking
dc.subject.keywordsNatural language understanding
dc.subject.keywordsAutomatic workflow construction
dc.subject.keywordsAI safety
dc.subject.keywordsTrustworthy AI
dc.subject.keywordsLarge language models
dc.titleEfficient Techniques for Automated Planning for Goals in Linear Temporal Logics on Finite Traces
dc.typeElectronic Thesis or Dissertation

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Fuggitti_Francesco_2023_PhD.pdf
Size:
1.43 MB
Format:
Adobe Portable Document Format
Download
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
license.txt
Size:
1.87 KB
Format:
Plain Text
Description:
Download
No Thumbnail Available
Name:
YorkU_ETDlicense.txt
Size:
3.39 KB
Format:
Plain Text
Description:
Download

Collections

Electrical and Computer Engineering

All items in the YorkSpace institutional repository are protected by copyright, with all rights reserved except where explicitly noted.