Salomon Sickert
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.
- Julian Brunner, Benedikt Seidl, and Salomon Sickert. 2019. A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9--12, 2019, Portland, OR, USA (LIPIcs, Vol. 141), John Harrison, John O'Leary, and Andrew Tolmach (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 11:1--11:19. https://doi.org/10.4230/LIPIcs.ITP.2019.11Google Scholar
- Ivana Černá and Radek Pelánek. 2003. Relating Hierarchy of Temporal Properties to Model Checking. In Mathematical Foundations of Computer Science 2003, 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2747), Branislav Rovan and Peter Vojtás (Eds.). Springer, 318--327. https://doi.org/10.1007/978-3-540-45138-9_26Google Scholar
- Edward Y. Chang, Zohar Manna, and Amir Pnueli. 1992. Characterization of Temporal Property Classes. In Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings (Lecture Notes in Computer Science, Vol. 623), Werner Kuich (Ed.). Springer, 474--486. https://doi.org/10.1007/3-540-55719-9_97Google Scholar
- Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. 1998. Property specification patterns for finite-state verification. In FMSP. 7--15. https://doi.org/10.1145/298595.298598Google Scholar
- Javier Esparza, Jan Kretínský, and Salomon Sickert. 2018. One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 384--393. https://doi.org/10.1145/3209108.3209161Google ScholarDigital Library
- Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, and Moshe Y. Vardi. 2003. On Complementing Nondeterministic Büchi Automata. In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2860), Daniel Geist and Enrico Tronci (Eds.). Springer, 96--110. https://doi.org/10.1007/978-3-540-39724-3_10Google Scholar
- Jan Kretínský, Tobias Meggendorfer, and Salomon Sickert. 2018. Owl: A Library for ω-Words, Automata, and LTL. In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11138), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 543--550. https://doi.org/10.1007/978-3-030-01090-4_34Google Scholar
- Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. 1985. The Glory of the Past. In Logics of Programs, Conference, Brooklyn College, New York, NY, USA, June 17-19, 1985, Proceedings (Lecture Notes in Computer Science, Vol. 193), Rohit Parikh (Ed.). Springer, 196--218. https://doi.org/10.1007/3-540-15648-8_16Google Scholar
- Christof Löding and Wolfgang Thomas. 2000. Alternating Automata and Logics over Infinite Words. In Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, International Conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000, Proceedings (Lecture Notes in Computer Science, Vol. 1872), Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito (Eds.). Springer, 521--535. https://doi.org/10.1007/3-540-44929--9_36Google Scholar
- Oded Maler and Amir Pnueli. 1990. Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II. IEEE Computer Society, 672--682. https://doi.org/10.1109/FSCS.1990.89589Google Scholar
- Zohar Manna and Amir Pnueli. 1990. A Hierarchy of Temporal Properties. In Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22-24, 1990, Cynthia Dwork (Ed.). ACM, 377--410. https://doi.org/10.1145/93385.93442Google Scholar
- Zohar Manna and Amir Pnueli. 1992. The temporal logic of reactive and concurrent systems - specification. Springer.Google Scholar
- Satoru Miyano and Takeshi Hayashi. 1984. Alternating Finite Automata on omega-Words. Theor. Comput. Sci. 32 (1984), 321--330. https://doi.org/10.1016/0304-3975(84)90049-5Google ScholarCross Ref
- David E. Muller, Ahmed Saoudi, and Paul E. Schupp. 1988. Weak Alternating Automata Give a Simple Explanation of Why Most Temporal and Dynamic Logics are Decidable in Exponential Time. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988. IEEE Computer Society, 422--427. https://doi.org/10.1109/LICS.1988.5139Google ScholarCross Ref
- Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer. https://doi.org/10.1007/3-540-45949-9Google ScholarDigital Library
- Radek Pelánek and Jan Strejcek. 2005. Deeper Connections Between LTL and Alternating Automata. In Implementation and Application of Automata, 10th International Conference, CIAA 2005, Sophia Antipolis, France, June 27-29, 2005, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 3845), Jacques Farré, Igor Litovsky, and Sylvain Schmitz (Eds.). Springer, 238--249. https://doi.org/10.1007/11605157_20Google Scholar
- Nir Piterman and Amir Pnueli. 2018. Temporal Logic and Fair Discrete Systems. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer, 27--73. https://doi.org/10.1007/978-3-319-10575--8_2Google Scholar
- Klaus Schneider. 2004. Verification of Reactive Systems - Formal Methods and Algorithms. Springer. https://doi.org/10.1007/978-3-662-10778-2Google Scholar
- Benedikt Seidl and Salomon Sickert. 2019. A Compositional and Unified Translation of LTL into ω-Automata. Archive of Formal Proofs 2019 (2019). https://www.isa-afp.org/entries/LTL_Master_Theorem.htmlGoogle Scholar
- Salomon Sickert. 2016. Linear Temporal Logic. Archive of Formal Proofs 2016 (2016). https://www.isa-afp.org/entries/LTL.shtmlGoogle Scholar
- Salomon Sickert. 2019. A Unified Translation of Linear Temporal Logic to ω-Automata. Ph.D. Dissertation. Technical University of Munich, Germany. http://nbn-resolving.de/urn:nbn:de:bvb:91-diss-20190801-1484932-1-4Google Scholar
- Salomon Sickert. 2020. An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation. Archive of Formal Proofs 2020 (2020). https://www.isa-afp.org/entries/LTL_Normal_Form.htmlGoogle Scholar
- Salomon Sickert and Javier Esparza. 2020. An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata. CoRR abs/2005.00472 (2020). http://arxiv.org/abs/2005.00472Google Scholar
- Moshe Y. Vardi. 1994. Nontraditional Applications of Automata Theory. In Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings (Lecture Notes in Computer Science, Vol. 789), Masami Hagiya and John C. Mitchell (Eds.). Springer, 575--597. https://doi.org/10.1007/3-540-57887-0_116Google Scholar
- Lenore D. Zuck. 1986. Past Temporal Logic. Ph.D. Dissertation. The Weizmann Institute of Science, Israel.Google Scholar
Index Terms
- An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
Recommendations
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceWe present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, ...
A Unified Translation of Linear Temporal Logic to ω-Automata
We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). The translations yield automata of asymptotically ...
Weak alternating automata are not that weak
Automata on infinite words are used for specification and verification of nonterminating programs. Different types of automata induce different levels of expressive power, of succinctness, and of complexity. Alternating automata have both existential ...
Comments