Automata-theoretic techniques for reasoning and learning in linear-time temporal logics on finite traces

The use of temporal logics on finite traces, like Linear Temporal Logic (LTLf) and Linear Dynamic Logic (LDLf), has shown to be very powerful for AI. In particular, they have been successfully applied in several AI fields, such as temporal synthesis, FOND planning, the theory of Markov Decision Processes, Reinforcement Learning, and Business Process Management. Almost all the techniques developed in recent years rely on the well-known connection between temporal logic and automata theory. In particular, the size of a deterministic finite automaton equivalent to an LTLf/LDLf formula is, in the worst case, doubly exponentially larger than the formula. Nevertheless, such transformation is much better behaved in the infinite traces setting, which opens new avenues for algorithms that work well in practice. This thesis aims to take some of these avenues and open new ones in the theory and the applications of temporal logic in AI. As a first contribution, we present a novel compositional technique for transforming an LDLf formula into a minimal DFA and propose an efficient symbolic implementation that is competitive with state-of-the-art tools. The impressive results obtained open new possibilities for further research in this direction and provide a ready-to-use tool for several AI applications. Then, we studied new problems in applying temporal logic in the context of Reinforcement Learning and Markov Decision Processes. In particular, we study the novel problem of Restraining Bolts, in which an authority imposes a restraining specification, written in LTLf/LDLf, to the acting of a reinforcement learning agent. Despite the authority and the learning agent having different representations of the world, we can show that, under general circumstances, the agent can learn its goals to suitably conform (as much as possible) to the restraining bolt specifications. We also studied variants of this problem and methods for engineering restraining specifications to improve the learning process. In the area of LTLf synthesis, we develop the theory and the implementation of a forward technique that, in many cases, can cope with the costly translation to automata by building the automaton on the fly. We drastically improve related works on the topic by using an AND/OR graph search algorithm and Knowledge Compilation techniques to explore the search graph efficiently. The experimental results are very promising. This contribution is the starting point for cross-fertilization between the Synthesis and Planning community, particularly for developing a science of heuristics for LTLf synthesis, as has happened in Planning.