Document Open Access Logo

A Naturally-Colored Translation from LTL to Parity and COCOA

Authors Rüdiger Ehlers , Ayrat Khalimov

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.39.pdf
  • Filesize: 1.16 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Linear logic
  • Theory of computation → Logic and verification
Keywords
  • Temporal Logic
  • Automata over Infinite Words
  • Canonical Automata
  • Automaton Minimization
  • Parity Automata
  • Determinization

Metrics

Abstract

Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical representation of omega-regular languages. The co-Büchi automata in a chain assign each omega-word its natural color, which depends only on the language itself and not on the chosen automaton representation. Automata in such a chain can be minimized in polynomial time and are good-for-games, making this representation attractive for verification and reactive synthesis. However, in these applications, specifications are usually given in linear temporal logic (LTL). To make COCOA useful, an LTL specification must first be translated into the chain of automata. The only translation currently known proceeds via deterministic parity automata (LTL→DPA→COCOA), where the first step ignores natural colors and requires involved constructions due to Safra or Esparza et al. This raises the question of whether, by exploiting the definition of the natural color of words, one can avoid such constructions and obtain a direct translation from LTL to COCOA.
In this paper, we present a simple yet optimal translation from LTL to COCOA, as well as a variant that translates LTL into DPA. The translation represents a new path from LTL to DPA and exploits the definition of natural colors. It relies on standard operations on weak alternating automata, the Miyano-Hayashi breakpoint construction, the subset construction, and simple graph algorithms. Starting from weak alternating automata, the procedure also applies to specifications in linear dynamic logic. The procedure runs in asymptotically optimal doubly exponential time and produces automata of asymptotically optimal size.

Cite As Get BibTex

Rüdiger Ehlers and Ayrat Khalimov. A Naturally-Colored Translation from LTL to Parity and COCOA. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 39:1-39:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.39

Author Details

Rüdiger Ehlers
  • Clausthal University of Technology, Germany
Ayrat Khalimov
  • Clausthal University of Technology, Germany

Funding

  • Ehlers, Rüdiger: Funded by Volkswagen Foundation within its Momentum framework under project no. 9C283.
  • Khalimov, Ayrat: Funded by Volkswagen Foundation within its Momentum framework under project no. 9C283.

Acknowledgements

We thank anonymous reviewers for numerous constructive suggestions.

References

  1. Dana Angluin and Dana Fisman. Learning regular omega languages. Theoretical Computer Science, 650:57-72, 2016. Algorithmic Learning Theory. URL: https://doi.org/10.1016/j.tcs.2016.07.031.
  2. Dana Angluin and Dana Fisman. Constructing concise characteristic samples for acceptors of omega regular languages. Logical Methods in Computer Science, 20, 2024. URL: https://doi.org/10.46298/LMCS-20(4:10)2024.
  3. Hugues Calbrix, Maurice Nivat, and Andreas Podelski. Ultimately periodic words of rational ω-languages. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics, pages 554-566, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-58027-1_27.
  4. Rüdiger Ehlers and Ayrat Khalimov. Fully generalized reactivity(1) synthesis. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 83-102. Springer Nature Switzerland, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_6.
  5. Rüdiger Ehlers and Sven Schewe. Natural colors of infinite words. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, pages 36:1-36:17, 2022. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2022.36.
  6. Rüdiger Ehlers. Rerailing automata, 2025. URL: https://doi.org/10.48550/arXiv.2503.08438.
  7. Javier Esparza, Jan Kretínský, Jean-François Raskin, and Salomon Sickert. From linear temporal logic and limit-deterministic büchi automata to deterministic parity automata. Int. J. Softw. Tools Technol. Transf., 24(4):635-659, 2022. URL: https://doi.org/10.1007/s10009-022-00663-1.
  8. Peter Faymonville and Martin Zimmermann. Parametric linear dynamic logic. Inf. Comput., 253:237-256, 2017. URL: https://doi.org/10.1016/j.ic.2016.07.009.
  9. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 854-860. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
  10. Swen Jacobs, Guillermo A. Pérez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaëtan Staquet, Clément Tamines, Leander Tentrup, and Adam Walker. The reactive synthesis competition (syntcomp): 2018-2021. International Journal on Software Tools for Technology Transfer, June 2024. URL: https://doi.org/10.1007/s10009-024-00754-1.
  11. Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming, pages 299-310, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. Google Scholar
  12. Orna Kupferman and Adin Rosenberg. The blow-up in translating ltl to deterministic automata. In Ron van der Meyden and Jan-Georg Smaus, editors, Model Checking and Artificial Intelligence, pages 85-94, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  13. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of LNCS, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  14. Yong Li, Sven Schewe, and Qiyi Tang. A novel family of finite automata for recognizing and learning ω-regular languages. In Étienne André and Jun Sun, editors, Automated Technology for Verification and Analysis, pages 53-73, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-45329-8_3.
  15. Oded Maler and Ludwig Staiger. On syntactic congruences for ω-languages. Theoretical Computer Science, 183(1):93-112, 1997. Formal Language Theory. URL: https://doi.org/10.1016/S0304-3975(96)00312-X.
  16. Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification, pages 578-586, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-96145-3_31.
  17. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32(3):321-330, 1984. Google Scholar
  18. David E Muller, Ahmed Saoudi, and Paul E Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings Third Annual Symposium on Logic in Computer Science, pages 422-423. IEEE Computer Society, 1988. Google Scholar
  19. Bader Abu Radi and Orna Kupferman. Minimization and canonization of GFG transition-based automata. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/lmcs-18(3:16)2022.
  20. Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, and Adrien Pommellet. Dissecting ltlsynt. Formal Methods in System Design, 2023. Available online since 14 July 2023. URL: https://doi.org/10.1007/s10703-022-00407-6.
  21. Shmuel Safra. On the complexity of omega-automata. In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 319-327. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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