×
Brunner, Julian; Seidl, Benedikt; Sickert, Salomon

A verified and compositional translation of LTL to deterministic Rabin automata. (English) Zbl 07649960

Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 11, 19 p. (2019).
Summary: We present a formalisation of the unified translation approach from linear temporal logic (LTL) to \(\omega\)-automata from [J. Esparza et al., in: Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 384–393 (2018; Zbl 1497.68259)]. This approach decomposes LTL formulas into “simple” languages and allows a clear separation of concerns: first, we formalise the purely logical result yielding this decomposition; second, we develop a generic, executable, and expressive automata library providing necessary operations on automata to re-combine the “simple” languages; third, we instantiate this generic theory to obtain a construction for deterministic Rabin automata (DRA). We extract from this particular instantiation an executable tool translating LTL to DRAs. To the best of our knowledge this is the first verified translation of LTL to DRAs that is proven to be double-exponential in the worst case which asymptotically matches the known lower bound.
For the entire collection see [Zbl 1423.68027].

Cited in 2 Documents

MSC:

68Q45 Formal languages and automata

Keywords:

automata theory; automata over infinite words; deterministic automata; linear temporal logic; model checking; verified algorithms

Citations:

Zbl 1497.68259

Software:

Isabelle/HOL; Autoref; Archive Formal Proofs; Transfer; Lifting; Refinement Monadic; SPOT; Boolean_Expression_Checkers; LTL2BA; Transition_Systems_and_Automata; Locales; LTL_to_DRA; CAVA Automata Library; Gabow SCC; Regex_Equivalence; Program-Conflict-Analysis; CAVA; CAVA LTL Modelchecker
Cite Review PDF
Full Text: DOI

References:

[1] Romain Aïssat, Frédéric Voisin, and Burkhart Wolff. Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths. Archive of Formal Proofs, 2016, 2016. URL: https://www.isa-afp.org/entries/InfPathElimination.shtml.
[2] J. Brunner, B. Seidl, and S. Sickert 11:17
[3] Tomás Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, and Jan Strejcek. Compositional Approach to Suspension and Other Improvements to LTL Translation. In Ezio Bartocci and C. R. Ramakrishnan, editors, Model Checking Software -20th International Sym-posium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings, volume 7976 of Lecture Notes in Computer Science, pages 81-98. Springer, 2013. doi:10.1007/978-3-642-39176-7_6. · doi:10.1007/978-3-642-39176-7_6
[4] Tomás Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejcek. The Hanoi Omega-Automata Format. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification -27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 479-486. Springer, 2015. doi:10.1007/978-3-319-21690-4_31. · doi:10.1007/978-3-319-21690-4_31
[5] Tomás Babiak, Frantisek Blahoudek, Mojmír Křetínský, and Jan Strejcek. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis -11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 24-39. Springer, 2013. doi: 10.1007/978-3-319-02444-8_4. · Zbl 1414.03003 · doi:10.1007/978-3-319-02444-8_4
[6] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. · Zbl 1179.68076
[7] Clemens Ballarin. Locales: A Module System for Mathematical Theories. J. Autom. Reasoning, 52(2):123-153, 2014. doi:10.1007/s10817-013-9284-7. · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7
[8] Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly Modular (Co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving -5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 93-110. Springer, 2014. doi:10.1007/978-3-319-08970-6_7. · Zbl 1416.68151 · doi:10.1007/978-3-319-08970-6_7
[9] Maksym Bortin and Christoph Lüth. Structured Formal Development with Quotient Types in Isabelle/HOL. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings, volume 6167 of Lecture Notes in Computer Science, pages 34-48. Springer, 2010. doi:10.1007/978-3-642-14128-7_5. · Zbl 1286.68391 · doi:10.1007/978-3-642-14128-7_5
[10] Julian Brunner. Büchi complementation. Archive of Formal Proofs, 2017, 2017. URL: https://www.isa-afp.org/entries/Buchi_Complementation.html.
[11] Julian Brunner. Transition Systems and Automata. Archive of Formal Proofs, 2017, 2017. URL: https://www.isa-afp.org/entries/Transition_Systems_and_Automata.html.
[12] Julian Brunner. Partial Order Reduction. Archive of Formal Proofs, 2018, 2018. URL: https://www.isa-afp.org/entries/Partial_Order_Reduction.html.
[13] Julian Brunner and Peter Lammich. Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. J. Autom. Reasoning, 60(1):3-21, 2018. doi:10.1007/ s10817-017-9418-4. · Zbl 1426.68162 · doi:10.1007/s10817-017-9418-4
[14] Janusz A. Brzozowski. Derivatives of Regular Expressions. J. ACM, 11(4):481-494, 1964. doi:10.1145/321239.321249. · Zbl 0225.94044 · doi:10.1145/321239.321249
[15] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. doi:10.1007/978-3-319-10575-8. · Zbl 1390.68001 · doi:10.1007/978-3-319-10575-8
[16] Costas Courcoubetis and Mihalis Yannakakis. The Complexity of Probabilistic Verification. J. ACM, 42(4):857-907, 1995. doi:10.1145/210332.210339. · Zbl 0885.68109 · doi:10.1145/210332.210339
[17] Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 -A Framework for LTL and ω-Automata Manipulation. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis -14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 122-129, 2016. doi:10.1007/978-3-319-46520-3_8. · doi:10.1007/978-3-319-46520-3_8
[18] Javier Esparza, Jan Křeínský, and Salomon Sickert. From LTL to deterministic automata -A safraless compositional approach. Formal Methods in System Design, 49(3):219-271, 2016. doi:10.1007/s10703-016-0259-2. · Zbl 1368.68233 · doi:10.1007/s10703-016-0259-2
[19] Javier Esparza and Jan Křetínský. From LTL to Deterministic Automata: A Safraless Compositional Approach. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification -26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 192-208. Springer, 2014. doi:10.1007/978-3-319-08867-9_13. · doi:10.1007/978-3-319-08867-9_13
[20] Javier Esparza, Jan Křetínský, and Salomon Sickert. One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 384-393. ACM, 2018. doi:10.1145/3209108.3209161. · Zbl 1497.68259 · doi:10.1145/3209108.3209161
[21] Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A Fully Verified Executable LTL Model Checker. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification -25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 463-478. Springer, 2013. doi:10.1007/978-3-642-39799-8_31. · doi:10.1007/978-3-642-39799-8_31
[22] Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A Fully Verified Executable LTL Model Checker. Archive of Formal Proofs, 2014, 2014. URL: https://www.isa-afp.org/entries/CAVA_LTL_Modelchecker.shtml.
[23] Paul Gastin and Denis Oddoux. Fast LTL to Büchi Automata Translation. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings, volume 2102 of Lecture Notes in Computer Science, pages 53-65. Springer, 2001. doi:10.1007/3-540-44585-4_6. · Zbl 0991.68044 · doi:10.1007/3-540-44585-4_6
[24] Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Piotr Dembinski and Marek Sredniawa, editors, Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995, volume 38 of IFIP Conference Proceedings, pages 3-18. Chapman & Hall, 1995.
[25] Brian Huffman and Ondrej Kuncar. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs -Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, volume 8307 of Lecture Notes in Computer Science, pages 131-146. Springer, 2013. doi:10.1007/978-3-319-03545-1_9. · Zbl 1426.68284 · doi:10.1007/978-3-319-03545-1_9
[26] Simon Jantsch and Michael Norrish. Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving -9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, pages 306-323. Springer, 2018. doi:10.1007/ 978-3-319-94821-8_18. · Zbl 1511.68335 · doi:10.1007/978-3-319-94821-8_18
[27] Peter Lammich. Refinement for Monadic Programs. Archive of Formal Proofs, 2012, 2012. URL: https://www.isa-afp.org/entries/Refine_Monadic.shtml.
[28] Peter Lammich. Automatic Data Refinement. Archive of Formal Proofs, 2013, 2013. URL: https://www.isa-afp.org/entries/Automatic_Refinement.shtml.
[29] Peter Lammich. The CAVA Automata Library. Archive of Formal Proofs, 2014, 2014. URL: https://www.isa-afp.org/entries/CAVA_Automata.shtml.
[30] Peter Lammich. Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving -5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 325-340. Springer, 2014. doi:10.1007/978-3-319-08970-6_21. 11:19 · Zbl 1416.68168 · doi:10.1007/978-3-319-08970-6_21
[31] Peter Lammich. Verified Efficient Implementation of Gabow’s Strongly Connected Components Algorithm. Archive of Formal Proofs, 2014, 2014. URL: https://www.isa-afp.org/entries/ Gabow_SCC.shtml.
[32] Peter Lammich and Markus Müller-Olm. Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors. Archive of Formal Proofs, 2007, 2007. URL: https://www.isa-afp.org/entries/Program-Conflict-Analysis.shtml.
[33] Peter Lammich and René Neumann. A Framework for Verifying Depth-First Search Algorithms. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 137-146. ACM, 2015. doi:10.1145/2676724.2693165. · doi:10.1145/2676724.2693165
[34] Peter Lammich and René Neumann. A Framework for Verifying Depth-First Search Al-gorithms. Archive of Formal Proofs, 2016, 2016. URL: https://www.isa-afp.org/entries/ DFS_Framework.shtml.
[35] Stephan Merz. Weak Alternating Automata in Isabelle/HOL. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, volume 1869 of Lec-ture Notes in Computer Science, pages 424-441. Springer, 2000. doi:10.1007/3-540-44659-1_26. · Zbl 0974.68090 · doi:10.1007/3-540-44659-1_26
[36] Tobias Nipkow. Boolean Expression Checkers. Archive of Formal Proofs, 2014, 2014. URL: https://www.isa-afp.org/entries/Boolean_Expression_Checkers.shtml.
[37] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL -A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-45949-9. · Zbl 0994.68131 · doi:10.1007/3-540-45949-9
[38] Tobias Nipkow and Dmitriy Traytel. Unified Decision Procedures for Regular Expression Equivalence. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving -5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 450-466. Springer, 2014. doi:10.1007/978-3-319-08970-6_29. · Zbl 1416.68175 · doi:10.1007/978-3-319-08970-6_29
[39] Alexander Schimpf, Stephan Merz, and Jan-Georg Smaus. Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 424-439. Springer, 2009. doi: 10.1007/978-3-642-03359-9_29. · Zbl 1252.68196 · doi:10.1007/978-3-642-03359-9_29
[40] Benedikt Seidl and Salomon Sickert. A Compositional and Unified Translation of LTL into ω-Automata. Archive of Formal Proofs, 2019, 2019. URL: https://isa-afp.org/entries/ LTL_Master_Theorem.html.
[41] Salomon Sickert. Converting Linear Temporal Logic to Deterministic (Generalised) Rabin Automata. Archive of Formal Proofs, 2015, 2015. URL: https://www.isa-afp.org/entries/ LTL_to_DRA.shtml.
[42] Salomon Sickert. Linear Temporal Logic. Archive of Formal Proofs, 2016, 2016. URL: https://www.isa-afp.org/entries/LTL.shtml.
[43] Salomon Sickert. A Unified Translation of Linear Temporal Logic to ω-Automata. PhD thesis, Technical University Munich, Germany, 2019.
[44] Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetínský. Limit-Deterministic Büchi Automata for Linear Temporal Logic. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification -28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 312-332. Springer, 2016. doi:10.1007/978-3-319-41540-6_17. · Zbl 1411.68054 · doi:10.1007/978-3-319-41540-6_17
[45] Moshe Y. Vardi. Automatic Verification of Probabilistic Concurrent Finite-State Programs. In 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21-23 October 1985, pages 327-338. IEEE Computer Society, 1985. doi:10.1109/SFCS.1985.12. · doi:10.1109/SFCS.1985.12
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.