Dipartimento di Ingegneria informatica, automatica e gestionale

The translation from temporal logics to automata is the workhorse algorithm of several techniques in computer science and AI, such as reactive synthesis, reasoning about actions, FOND planning with temporal specifications, and reinforcement learning with non-Markovian rewards, just to name a few. Unfortunately, the problem is computationally intractable, requiring the implementation of several heuris- tics to make it usable in practice. In this paper, following the recent interest in temporal logic formalisms over finite traces, we present a compositional approach for dealing with translations of Linear Temporal Logic and Linear Dynamic Logic (LDLf) on finite traces into Deterministic Finite Automata DFA.That is, we inductively transform each LTLf/LDLf subformula into a DFA, and combine them through automata operators. By relying on efficient semi-symbolic automata rep- resentations, we empirically show the effectiveness of our ap- proach and the competitiveness with similar tools. Moreover, this is the first work that provides a scalable and practical tool supporting the translation to DFA not only for LTLf but also for full LDLf .