TY - GEN
T1 - An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
AU - Sickert, Salomon
AU - Esparza, Javier
N1 - Publisher Copyright:
© 2020 Owner/Author.
PY - 2020/7/8
Y1 - 2020/7/8
N2 - 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 formula of the form nu=1 GF† v FGψi, where † and ψ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.
AB - 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 formula of the form nu=1 GF† v FGψi, where † and ψ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.
KW - Deterministic Automata
KW - Linear Temporal Logic
KW - Normal Form
KW - Weak Alternating Automata
UR - http://www.scopus.com/inward/record.url?scp=85085912053&partnerID=8YFLogxK
U2 - 10.1145/3373718.3394743
DO - 10.1145/3373718.3394743
M3 - Conference contribution
AN - SCOPUS:85085912053
T3 - ACM International Conference Proceeding Series
SP - 831
EP - 844
BT - Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
PB - Association for Computing Machinery
T2 - 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Y2 - 8 July 2020 through 11 July 2020
ER -