Automaton

Heuristics

Mathematics

Operating system

Algorithm

Deterministic finite automaton

Artificial intelligence

Finite-state machine

Rotation formalisms in three dimensions

Programming language

Temporal logic

Geometry

Computer science

Theoretical computer science

Linear temporal logic

Proceedings of the International Conference on Automated Planning and Scheduling

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, to name a few. Unfortunately, the problem is computationally intractable, requiring the implementation of several heuristics 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 (LTLf) and Linear Dynamic Logic (LDLf) on finite traces into Deterministic Finite Automata (DFA). We inductively transform each LTLf/LDLf subformula into a DFA and combine them through automata operators. By relying on efficient semi-symbolic automata representations, we empirically show our approach's effectiveness and 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.

Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata