Dottorato in INGEGNERIA INFORMATICA

Titolo della tesi: 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), have 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 logics 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 with respect to the infinite traces setting, and this open new avenues for algorithms that work well in practice. This thesis aims to take some of these avenues, and to open new ones, both in the theory and the applications of temporal logics 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 on this direction, as well as a ready-to-use tool for several applications in AI. Then, we studied new problems in applying temporal logics 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 have 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 to engineer restraining specifications in order 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, is able to 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 efficiently explore the search graph. The experimental results are very promising. This contribution is the starting point for a cross-fertilization between the Synthesis and Planning community, and in particular for the development of a science of heuristics for LTLf synthesis, as has happened in Planning.