TY  - JOUR
AU  - Esparza, Javier
AU  - Rubio Cuéllar, Rubén Rafael
AU  - Salomon Sickert
PY  - 2024
DO  - 10.1145/3651152
SN  - 0004-5411
SN  - 1557-735X
UR  - https://hdl.handle.net/20.500.14352/103063
T2  - Journal of the ACM
AB  - In the mid 1980s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of Linear Temporal Logic (LTL) with past operators) is equivalent to a formula of the form ⋀<sup>n</sup><sub>i=1</sub>GF...
LA  - eng
M2  - 16:1
PB  - ACM
KW  - Linear temporal logic
KW  - Normal form
KW  - Weak alternating automata
KW  - Deterministic automata
TI  - Efficient Normalization of Linear Temporal Logic
TY  - journal article
VL  - 71
ER  -