Abstract
Linear Temporal Logic on process traces (or LTLp) is a logic introduced to specify and reason over the temporal properties of (the traces generated by) business processes. So far, its relation with finite-state automata has not been explored and researchers resorted to more expressive logics and the corresponding automata construction algorithms. In this paper, we present a tool, named LTLp2DFA, to automatically construct the automata associated with LTLp specifications and show how, by considering process traces as first-class citizens, this results in simpler automata and better construction algorithms.