This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such ...

Linear temporal logic (LTL) is a popular language in formal verification, especially in the domains of model checking and reactive synthesis. Because its semantics is defined in terms of infinite sequences of symbols ...