Document Open Access Logo

A Direct Translation from LTL with Past to Deterministic Rabin Automata

Authors Shaun Azzopardi , David Lidell , Nir Piterman

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2024.13.pdf
  • Filesize: 0.71 MB
  • 15 pages

Document Identifiers

Author Details

Shaun Azzopardi
  • University of Malta, Msida, Malta
David Lidell
  • University of Gothenburg, Sweden
Nir Piterman
  • University of Gothenburg, Sweden

Funding

This research is supported by the Swedish research council (VR) project (No. 2020-04963) and the ERC Consolidator grant DSynMA (No. 772459).

Acknowledgements

We are grateful to Gerardo Schneider and the reviewers for their very useful feedback.

Cite As Get BibTex

Shaun Azzopardi, David Lidell, and Nir Piterman. A Direct Translation from LTL with Past to Deterministic Rabin Automata. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.MFCS.2024.13

Abstract

We present a translation from linear temporal logic with past to deterministic Rabin automata. The translation is direct in the sense that it does not rely on intermediate non-deterministic automata, and asymptotically optimal, resulting in Rabin automata of doubly exponential size. It is based on two main notions. One is that it is possible to encode the history contained in the prefix of a word, as relevant for the formula under consideration, by performing simple rewrites of the formula itself. As a consequence, a formula involving past operators can (through such rewrites, which involve alternating between weak and strong versions of past operators in the formula’s syntax tree) be correctly evaluated at an arbitrary point in the future without requiring backtracking through the word. The other is that this allows us to generalize to linear temporal logic with past the result that the language of a pure-future formula can be decomposed into a Boolean combination of simpler languages, for which deterministic automata with simple acceptance conditions are easily constructed.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Modal and temporal logics
Keywords
  • Linear temporal logic
  • ω-automata
  • determinization

Metrics

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

Related Versions

References

  1. Shaun Azzopardi, David Lidell, and Nir Piterman. A Direct Translation from LTL with Past to Deterministic Rabin Automata, 2024. URL: https://arxiv.org/abs/2405.01178.
  2. Shaun Azzopardi, David Lidell, Nir Piterman, and Gerardo Schneider. ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae. In Étienne André and Jun Sun, editors, Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part II, volume 14216 of Lecture Notes in Computer Science, pages 276-287. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-45332-8_15.
  3. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of Reactive(1) Designs. J. Comput. Syst. Sci., 78(3):911-938, 2012. URL: https://doi.org/10.1016/J.JCSS.2011.08.007.
  4. Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, and Stefano Tonetta. Reactive Synthesis from Extended Bounded Response LTL Specifications. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 83-92. IEEE, 2020. URL: https://doi.org/10.34727/2020/ISBN.978-3-85448-042-6_15.
  5. Javier Esparza, Jan Křetínský, and Salomon Sickert. A Unified Translation of Linear Temporal Logic to ω-Automata. J. ACM, 67(6), October 2020. URL: https://doi.org/10.1145/3417995.
  6. Dov M. Gabbay. The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In Behnam Banieqbal, Howard Barringer, and Amir Pnueli, editors, Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings, volume 398 of Lecture Notes in Computer Science, pages 409-448, New York, NY, USA, 1987. Springer. URL: https://doi.org/10.1007/3-540-51803-7_36.
  7. Paul Gastin and Denis Oddoux. LTL with Past and Two-Way Very-Weak Alternating Automata. In Branislav Rovan and Peter Vojtás, editors, Mathematical Foundations of Computer Science 2003, 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings, volume 2747 of Lecture Notes in Computer Science, pages 439-448, New York, NY, USA, 2003. Springer. URL: https://doi.org/10.1007/978-3-540-45138-9_38.
  8. Jan Kretínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A Library for ω-Words, Automata, and LTL. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 543-550. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_34.
  9. Orna Lichtenstein, Amir Pnueli, and Lenore Zuck. The Glory of the Past. In Rohit Parikh, editor, Logics of Programs, pages 196-218, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg. Google Scholar
  10. Zohar Manna and Amir Pnueli. A Hierarchy of Temporal Properties. In Cynthia Dwork, editor, Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22-24, 1990, pages 377-410. ACM, 1990. URL: https://doi.org/10.1145/93385.93442.
  11. Nicolas Markey. Temporal Logic with Past is Exponentially More Succinct. Bulletin- European Association for Theoretical Computer Science, 79:122-128, 2003. URL: https://hal.science/hal-01194627.
  12. Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit Reactive Synthesis Strikes Back! In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 578-586. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_31.
  13. Nir Piterman. From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS '06, pages 255-264, USA, 2006. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2006.28.
  14. Nir Piterman and Amir Pnueli. Temporal Logic and Fair Discrete Systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 27-73. Springer, New York, NY, USA, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_2.
  15. Amir Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS '77, pages 46-57, USA, 1977. IEEE Computer Society. URL: https://doi.org/10.1109/SFCS.1977.32.
  16. S. Safra. On the Complexity of Omega-Automata. In Proceedings of the 29th Annual Symposium on Foundations of Computer Science, SFCS '88, pages 319-327, USA, 1988. IEEE Computer Society. URL: https://doi.org/10.1109/SFCS.1988.21948.
  17. A. P. Sistla and E. M. Clarke. The Complexity of Propositional Linear Temporal Logics. J. ACM, 32(3):733-749, July 1985. URL: https://doi.org/10.1145/3828.3837.
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