LTL and Past LTL on Finite Traces for Planning and Declarative Process Mining This is my master's thesis with presentation slides. For the slides, many thanks to @manuelcoppotelli for the Beamer Roma theme.