Efficient Normalization of Linear Temporal Logic

Javier Esparza, Rubén Rubio, Salomon Sickert

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formu…