APPLICATIONS OF ANSWER SET PROGRAMMING TO LINEAR TEMPORAL LOGIC OVER FINITE TRACES

Abstract

Linear Temporal Logic over Finite Traces (LTLf) is a popular logic to express high level specifications that require reasoning about time. It was introduced in the seminal work of De Giacomo and Vardi, motivated by the fact that many Artificial Intelligence applications that require temporal reasoning are more intuitively described as finite execution sequences, rather than infinite execution sequences as in Linear Temporal Logic. Due to the high complexity that characterizes LTLf-related problems, efficienty systems are required. Reasoning tasks in LTLf are usually tackled by automata theoretic techniques or by SAT-based approaches. This thesis proposes an alternative approach to LTLf-related reasoning problems that is based on Answer Set Programming (ASP). Answer Set Programming is a declarative logic programming paradigm that stems from research in stable model semantics for logic programs and knowledge representation and reasoning. ASP is more expressive than SAT, thus, the solutions we obtain are more compact, intuitive and readable than SAT counterparts; moreover the usage of ASP does not result in a compromise on efficiency and effectiveness. Indeed, the approach presented in this thesis often obtains better performance with respect to existing SAT-based solutions; also, ASP enabled the development of novel solutions for unsatisfiable core enumeration and query checking in declarative process mining contexts.