Document Open Access Logo

A Verified and Compositional Translation of LTL to Deterministic Rabin Automata

Authors Julian Brunner , Benedikt Seidl , Salomon Sickert

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.11.pdf
  • Filesize: 0.59 MB
  • 19 pages

Document Identifiers

Author Details

Julian Brunner
  • Technische Universität München, Germany
Benedikt Seidl
  • Technische Universität München, Germany
Salomon Sickert
  • Technische Universität München, Germany

Funding

This work was partially funded and supported by the German Research Foundation (DFG) project "Verified Model Checkers" (317422601).

Acknowledgements

The authors want to thank Manuel Eberl, Javier Esparza, Lars Hupel, Peter Lammich, and Tobias Nipkow for their helpful comments and technical expertise.

Cite As Get BibTex

Julian Brunner, Benedikt Seidl, and Salomon Sickert. A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.11

Abstract

We present a formalisation of the unified translation approach from linear temporal logic (LTL) to omega-automata from [Javier Esparza et al., 2018]. 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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Interactive proof systems
Keywords
  • Automata Theory
  • Automata over Infinite Words
  • Deterministic Automata
  • Linear Temporal Logic
  • Model Checking
  • Verified Algorithms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

  • The described Isabelle/HOL development is archived in the "Archive of Formal Proofs" and is split into the entries [Julian Brunner, 2017] and [Benedikt Seidl and Salomon Sickert, 2019].

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. 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 Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings, volume 7976 of Lecture Notes in Computer Science, pages 81-98. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39176-7_6.
  3. 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. URL: https://doi.org/10.1007/978-3-319-21690-4_31.
  4. 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. URL: https://doi.org/10.1007/978-3-319-02444-8_4.
  5. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  6. Clemens Ballarin. Locales: A Module System for Mathematical Theories. J. Autom. Reasoning, 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  7. 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. URL: https://doi.org/10.1007/978-3-319-08970-6_7.
  8. 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. URL: https://doi.org/10.1007/978-3-642-14128-7_5.
  9. Julian Brunner. Büchi complementation. Archive of Formal Proofs, 2017, 2017. URL: https://www.isa-afp.org/entries/Buchi_Complementation.html.
  10. Julian Brunner. Transition Systems and Automata. Archive of Formal Proofs, 2017, 2017. URL: https://www.isa-afp.org/entries/Transition_Systems_and_Automata.html.
  11. Julian Brunner. Partial Order Reduction. Archive of Formal Proofs, 2018, 2018. URL: https://www.isa-afp.org/entries/Partial_Order_Reduction.html.
  12. 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. URL: https://doi.org/10.1007/s10817-017-9418-4.
  13. Janusz A. Brzozowski. Derivatives of Regular Expressions. J. ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  14. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8.
  15. Costas Courcoubetis and Mihalis Yannakakis. The Complexity of Probabilistic Verification. J. ACM, 42(4):857-907, 1995. URL: https://doi.org/10.1145/210332.210339.
  16. 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. URL: https://doi.org/10.1007/978-3-319-46520-3_8.
  17. 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. URL: https://doi.org/10.1007/s10703-016-0259-2.
  18. 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. URL: https://doi.org/10.1007/978-3-319-08867-9_13.
  19. 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. URL: https://doi.org/10.1145/3209108.3209161.
  20. 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. URL: https://doi.org/10.1007/978-3-642-39799-8_31.
  21. 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.
  22. 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. URL: https://doi.org/10.1007/3-540-44585-4_6.
  23. 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. Google Scholar
  24. 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. URL: https://doi.org/10.1007/978-3-319-03545-1_9.
  25. 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. URL: https://doi.org/10.1007/978-3-319-94821-8_18.
  26. Peter Lammich. Refinement for Monadic Programs. Archive of Formal Proofs, 2012, 2012. URL: https://www.isa-afp.org/entries/Refine_Monadic.shtml.
  27. Peter Lammich. Automatic Data Refinement. Archive of Formal Proofs, 2013, 2013. URL: https://www.isa-afp.org/entries/Automatic_Refinement.shtml.
  28. Peter Lammich. The CAVA Automata Library. Archive of Formal Proofs, 2014, 2014. URL: https://www.isa-afp.org/entries/CAVA_Automata.shtml.
  29. 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. URL: https://doi.org/10.1007/978-3-319-08970-6_21.
  30. 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.
  31. 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.
  32. 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. URL: https://doi.org/10.1145/2676724.2693165.
  33. Peter Lammich and René Neumann. A Framework for Verifying Depth-First Search Algorithms. Archive of Formal Proofs, 2016, 2016. URL: https://www.isa-afp.org/entries/DFS_Framework.shtml.
  34. 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 Lecture Notes in Computer Science, pages 424-441. Springer, 2000. URL: https://doi.org/10.1007/3-540-44659-1_26.
  35. Tobias Nipkow. Boolean Expression Checkers. Archive of Formal Proofs, 2014, 2014. URL: https://www.isa-afp.org/entries/Boolean_Expression_Checkers.shtml.
  36. 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. URL: https://doi.org/10.1007/3-540-45949-9.
  37. 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. URL: https://doi.org/10.1007/978-3-319-08970-6_29.
  38. 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. URL: https://doi.org/10.1007/978-3-642-03359-9_29.
  39. 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.
  40. 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.
  41. Salomon Sickert. Linear Temporal Logic. Archive of Formal Proofs, 2016, 2016. URL: https://www.isa-afp.org/entries/LTL.shtml.
  42. Salomon Sickert. A Unified Translation of Linear Temporal Logic to ω-Automata. PhD thesis, Technical University Munich, Germany, 2019. Google Scholar
  43. 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. URL: https://doi.org/10.1007/978-3-319-41540-6_17.
  44. 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. URL: https://doi.org/10.1109/SFCS.1985.12.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact