%0 Conference Paper %1 10.1145/3373718.3394743 %A Sickert, Salomon %A Esparza, Javier %B Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science %C New York, NY, USA %D 2020 %I Association for Computing Machinery %K conference %P 831–844 %R 10.1145/3373718.3394743 %T An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata %U https://doi.org/10.1145/3373718.3394743 %X 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 Λni =1 GFφi ∨FGψi, where φi and ψi 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. %@ 9781450371049

@inproceedings{10.1145/3373718.3394743, abstract = {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 Λni =1 GFφi ∨FGψi, where φi and ψi 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.}, added-at = {2020-10-01T16:07:41.000+0200}, address = {New York, NY, USA}, author = {Sickert, Salomon and Esparza, Javier}, biburl = {https://www.bibsonomy.org/bibtex/2c09db65740da893a1dc64b277f1c0d56/paves}, booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science}, doi = {10.1145/3373718.3394743}, interhash = {2e629a11a01b41f712b522ddbb62c4fd}, intrahash = {c09db65740da893a1dc64b277f1c0d56}, isbn = {9781450371049}, keywords = {conference}, location = {Saarbr\"{u}cken, Germany}, note = {Preprint: <a href="https://arxiv.org/abs/2005.00472">Link</a><br>#conference}, numpages = {14}, pages = {831–844}, publisher = {Association for Computing Machinery}, series = {LICS '20}, timestamp = {2023-09-24T19:43:55.000+0200}, title = {An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata}, url = {https://doi.org/10.1145/3373718.3394743}, year = 2020 }