pith. sign in

arxiv: 2606.26768 · v2 · pith:NSJMQGJJnew · submitted 2026-06-25 · 💻 cs.FL · cs.LO

Complementing Emerson-Lei Elevator Automata (Technical Report)

Ondrej Alexaj , Vojt\v{e}ch Havlena , Ond\v{r}ej Leng\'al , Yong Li , Nicolas Mazzocchi This is my paper

Pith reviewed 2026-06-30 01:33 UTC · model grok-4.3

classification 💻 cs.FL cs.LO
keywords Emerson-Lei automataelevator automataautomata complementationBuchi automataformal verificationmodel checking
0
0 comments X

The pith

Emerson-Lei elevator automata admit a complementation algorithm with significantly better asymptotic complexity than the best known algorithm for unrestricted Emerson-Lei automata.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines Emerson-Lei elevator automata by extending the elevator property from Buchi automata to Emerson-Lei acceptance conditions, where every strongly connected component remains either deterministic or inherently weak. It then supplies a complementation procedure that exploits this structure to achieve improved asymptotic complexity compared with existing methods for arbitrary Emerson-Lei automata. The motivation is that the elevator subclass already covers most automata arising in LTL model checking and hyperproperty verification, so the same restriction should support practical algorithms once acceptance conditions become richer.

Core claim

Emerson-Lei elevator automata, obtained by lifting the elevator structural restriction to Emerson-Lei acceptance, admit a complementation algorithm whose asymptotic complexity is significantly lower than that of the best algorithm known for general Emerson-Lei automata.

What carries the argument

The elevator structural restriction (every strongly connected component is deterministic or inherently weak), preserved under the move from Buchi to Emerson-Lei acceptance and used to derive the improved complementation construction.

If this is right

  • The algorithm supplies the first practical route to complementation, determinization, universality, and inclusion testing for Emerson-Lei automata with rich acceptance conditions.
  • Experimental runs against the Spot tool confirm that the complexity improvement translates to observable runtime gains on instances drawn from model-checking and hyperproperty tasks.
  • Because the elevator property already covers the majority of automata generated in practice for Buchi conditions, the same coverage is expected to hold for Emerson-Lei conditions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the elevator property continues to appear frequently under Emerson-Lei acceptance, the same structural restriction could be reused for determinization and inclusion algorithms beyond complementation.
  • Tools that currently convert LTL or hyperproperty specifications to Emerson-Lei automata may obtain immediate speed-ups by detecting and exploiting the elevator form during construction.

Load-bearing premise

The elevator restriction on strongly connected components remains both common and exploitable for complementation once acceptance conditions are extended beyond Buchi.

What would settle it

A concrete family of Emerson-Lei elevator automata on which the new algorithm produces a complement whose size matches or exceeds the size produced by the best general-purpose algorithm.

read the original abstract

B\"uchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of B\"uchi automata where every strongly connected component is either deterministic or inherently weak. It was shown that this class contains the majority of B\"uchi automata generated in practical applications, including LTL model-checking and verification of hyperproperties. Moreover, the elevator subclass enables more efficient complementation and determinization algorithms than unrestricted B\"uchi automata. In this paper, we introduce Emerson-Lei elevator automata, which is a generalization of B\"uchi elevator automata to richer acceptance conditions. We provide a complementation algorithm with a significantly better asymptotic complexity than the best known algorithm for unrestricted Emerson-Lei automata. The practical efficiency of our algorithm is demonstrated by an experimental comparison with the popular state-of-the-art tool Spot. Our work is, to the best of our knowledge, the first step towards practical algorithms for complementing, determinizing, and testing universality and inclusion of Emerson-Lei automata with rich acceptance conditions.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 4 minor

Summary. The paper defines Emerson-Lei elevator automata by directly generalizing the elevator structural restriction (every SCC is deterministic or inherently weak) from Büchi automata to Emerson-Lei acceptance. It presents a complementation construction that exploits this structure to obtain strictly better asymptotic complexity than the best known algorithm for unrestricted Emerson-Lei automata, together with an experimental comparison against Spot demonstrating practical gains.

Significance. If the complexity bound and correctness of the construction hold, the result supplies the first non-trivial algorithmic improvement for complementation (and, by extension, determinization and inclusion testing) of Emerson-Lei automata with rich acceptance conditions. Because elevator automata already capture the majority of practical Büchi instances arising in LTL model checking and hyperproperty verification, the generalization offers a concrete route toward scalable algorithms for the richer acceptance setting.

minor comments (4)
  1. [§2] §2, Definition 3: the formal statement of the elevator property under Emerson-Lei acceptance should explicitly record whether the deterministic/inherently-weak partition is required to be uniform across all acceptance sets or may vary per set.
  2. [§4] §4, Theorem 12: the complexity analysis cites an O(2^{O(n log n)}) bound for the general case; the corresponding bound for the elevator subclass should be stated in the same asymptotic notation for direct comparison.
  3. [Table 2] Table 2: several rows report only the number of states after complementation; adding the number of acceptance sets produced by each construction would clarify whether the elevator algorithm also reduces acceptance complexity.
  4. [§5.3] §5.3: the experimental section should state the precise timeout and memory limits used when comparing against Spot, as well as the benchmark suite provenance (e.g., whether the EL automata were obtained by direct translation or by conversion from Büchi instances).

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work and the recommendation for minor revision. The assessment correctly captures the contribution of generalizing the elevator restriction to Emerson-Lei automata and the resulting improvement in complementation complexity. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity; derivation is a constructive algorithm

full rationale

The paper introduces Emerson-Lei elevator automata by direct structural generalization of the Buchi case and supplies an explicit complementation construction whose complexity bound is derived from the algorithm itself. No step equates a claimed prediction or result to a fitted parameter, self-defined quantity, or load-bearing self-citation chain. Prior citations on Buchi elevator automata serve only as motivation; the new algorithm and its analysis stand independently. The experimental comparison with Spot is external validation, not part of any internal reduction. This is the normal case of a self-contained theoretical construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract; no information is available on free parameters, axioms, or invented entities.

pith-pipeline@v0.9.1-grok · 5722 in / 1071 out tokens · 58693 ms · 2026-06-30T01:33:01.716070+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 33 canonical work pages

  1. [1]

    In: Dawar, A., Gr¨ adel, E

    2 Joël D. Allred and Ulrich Ultes-Nitsche. A simple and optimal complementation algorithm for Büchi 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 46–55. ACM, 2018.doi:10.1145/3209108.3209138. 3 František Blahoudek, Matthias He...

    work page doi:10.1145/3209108.3209138 2018

  2. [2]

    4 Udi Boker

    URL: https://doi.org/10.1007/978-3-662-49674-9_49,doi:10.1007/978-3-662-49674-9_49. 4 Udi Boker. Why these automata types? In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors,LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, volume 57 ofEPiC Series in Co...

    work page doi:10.1007/978-3-662-49674-9_49 2018

  3. [3]

    5 Stefan Breuers, Christof Löding, and Jörg Olschewski

    URL:https://doi.org/10.29007/c3bj, doi:10.29007/C3BJ. 5 Stefan Breuers, Christof Löding, and Jörg Olschewski. Improved Ramsey-based Büchi comple- mentation. In Lars Birkedal, editor,Foundations of Software Science and Computational Struc- tures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Con- ferences on Theory and Pr...

    work page doi:10.29007/c3bj 2012

  4. [4]

    URL: https://doi.org/10.1007/978-3-642-28729-9_10,doi:10.1007/978-3-642-28729-9_10. 6 J. Richard Büchi. On a decision method in restricted second order arithmetic. InProc. of International Congress on Logic, Method, and Philosophy of Science

    work page doi:10.1007/978-3-642-28729-9_10

  5. [5]

    A tight lower bound for Streett complementation

    7 Yang Cai and Ting Zhang. A tight lower bound for Streett complementation. In Supra- tik Chakraborty and Amit Kumar, editors,IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 ofLIPIcs, pages 339–350. Schloss Dagstuhl - Leibniz- Zentrum für Informatik,

    2011

  6. [6]

    8 Yang Cai and Ting Zhang

    URL:https://doi.org/10.4230/LIPIcs.FSTTCS.2011.339, doi:10.4230/LIPICS.FSTTCS.2011.339. 8 Yang Cai and Ting Zhang. Tight upper bounds for Streett and parity complementation. In Marc Bezem, editor,Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, volume 1...

    work page doi:10.4230/lipics.fsttcs.2011.339 2011

  7. [7]

    9 Krishnendu Chatterjee, Andreas Gaiser, and Jan Křetínský

    URL: https://doi.org/10.4230/LIPIcs.CSL.2011.112,doi:10.4230/LIPICS.CSL.2011.112. 9 Krishnendu Chatterjee, Andreas Gaiser, and Jan Křetínský. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In Natasha Sharygina and Helmut Veith, editors,Computer Aided Verification - 25th International Conference, CAV 2013, Saint P...

    work page doi:10.4230/lipics.csl.2011.112 2011

  8. [8]

    10 Yu-Fang Chen, Vojtěch Havlena, and Ondřej Lengál

    URL:https://doi.org/10.1007/978-3-642-39799-8_37, doi:10.1007/978-3-642-39799-8_37. 10 Yu-Fang Chen, Vojtěch Havlena, and Ondřej Lengál. Simulations in rank-based Büchi automata complementation. In Anthony Widjaja Lin, editor,Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, v...

    work page doi:10.1007/978-3-642-39799-8_37 2019

  9. [9]

    URL: https://doi.org/10.1007/978-3-030-34175-6_23,doi:10.1007/978-3-030-34175-6_23. O. Alexaj, V. Havlena, O. Lengál, Y. Li, and N. Mazzocchi 19 11 Yu-Fang Chen, Matthias Heizmann, Ondřej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, and Lijun Zhang. Advanced automata-based algorithms for program termination checking. In Jeffrey S. Foster and Dan Gros...

    work page doi:10.1007/978-3-030-34175-6_23 2018

  10. [10]

    Clarkson and B

    URL:https://doi.org/10.1007/978-3-642-54792-8_15, doi:10.1007/978-3-642-54792-8_15. 13 Costas Courcoubetis and Mihalis Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 338–345. IEEE Computer Society, 1988.doi:...

    work page doi:10.1007/978-3-642-54792-8_15 1988

  11. [11]

    URL:https://is.muni.cz/th/xu3iz/. 15 Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexan- dre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: What’s new? In Sharon Shoham and Yakir Vizel, editors,Computer Aided Verifica...

    2022

  12. [12]

    URL: https://doi.org/10.1007/978-3-031-13188-2_9,doi:10.1007/978-3-031-13188-2_9. 16 E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back.Sci. Comput. Program., 8(3):275–306, 1987.doi:10.1016/0167-6423(87) 90036-0. 17 Javier Esparza, Jan Křetínský, and Salomon Sickert. From LTL to deterministic automata - A...

    work page doi:10.1007/978-3-031-13188-2_9 1987

  13. [13]

    18 Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y

    URL: https://doi.org/10.1007/s10703-016-0259-2,doi:10.1007/S10703-016-0259-2. 18 Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi, and Lijun Zhang. On the power of finite ambiguity in Büchi complementation.Inf. Comput., 292:105032,

    work page doi:10.1007/s10703-016-0259-2

  14. [14]

    19 Vojtěch Havlena and Ondřej Lengál

    URL:https: //doi.org/10.1016/j.ic.2023.105032,doi:10.1016/J.IC.2023.105032. 19 Vojtěch Havlena and Ondřej Lengál. Reducing (to) the ranks: Efficient rank-based Bü- chi automata complementation. In Serge Haddad and Daniele Varacca, editors,32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 o...

    work page doi:10.1016/j.ic.2023.105032 2023

  15. [15]

    In: Haddad, S., Varacca, D

    URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.2, doi:10.4230/LIPICS.CONCUR.2021.2. 20 Vojtěch Havlena, Ondřej Lengál, Yong Li, Barbora Šmahlíková, and Andrea Turrini. Modular mix-and-match complementation of Büchi automata. In Sriram Sankaranarayanan and Natasha Sharygina, editors,Tools and Algorithms for the Construction and Analysis of Systems - 29th ...

    work page doi:10.4230/lipics.concur.2021.2 2021

  16. [16]

    1007/978-3-031-30823-9_13

    URL:https://doi.org/10.1007/978-3-031-30823-9_13, doi:10. 1007/978-3-031-30823-9_13. 21Vojtěch Havlena, Ondřej Lengál, and Barbora Šmahlíková. Complementing Büchi automata with Ranker. In Sharon Shoham and Yakir Vizel, editors,Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, 20 ...

    work page doi:10.1007/978-3-031-30823-9_13 2022

  17. [17]

    In: Shoham, S., Vizel, Y

    URL: https://doi.org/10.1007/978-3-031-13188-2_10,doi:10.1007/978-3-031-13188-2_10. 22 Vojtěch Havlena, Ondřej Lengál, and Barbora Šmahlíková. Sky is not the limit: Tighter rank bounds for elevator automata in Büchi automata complementation. In Dana Fis- man and Grigore Rosu, editors,Tools and Algorithms for the Construction and Analysis of Systems - 28th...

    work page doi:10.1007/978-3-031-13188-2_10 2022

  18. [18]

    In: Fisman, D., Rosu, G

    URL:https://doi.org/10.1007/978-3-030-99527-0_7, doi:10.1007/978-3-030-99527-0_7. 23 Vojtěch Havlena, Ondřej Lengál, and Barbora Šmahlíková. Complementation of Emerson- Lei automata. In Parosh Aziz Abdulla and Delia Kesner, editors,Foundations of Soft- ware Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of t...

    work page doi:10.1007/978-3-030-99527-0_7 2025

  19. [19]

    URL:https://doi.org/10.1007/ 978-3-031-90897-2_5,doi:10.1007/978-3-031-90897-2_5. 24 Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski. Ultimate Automizer and the search for perfect interpolants (competition contribution). In ...

    work page doi:10.1007/978-3-031-90897-2_5 2018

  20. [20]

    1007/978-3-319-89963-3_30

    URL:https://doi.org/10.1007/978-3-319-89963-3_30, doi:10. 1007/978-3-319-89963-3_30. 25 Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software model checking for people who love automata. In Natasha Sharygina and Helmut Veith, editors,Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19,

    work page doi:10.1007/978-3-319-89963-3_30 2013

  21. [21]

    26 Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski

    URL: https://doi.org/10.1007/978-3-642-39799-8_2,doi:10.1007/978-3-642-39799-8_2. 26 Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Termination analysis by learning terminating programs. In Armin Biere and Roderick Bloem, editors,Computer Aided Verifica- tion - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic,...

    work page doi:10.1007/978-3-642-39799-8_2 2014

  22. [22]

    27 Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey O

    URL:https://doi.org/10.1007/978-3-319-08867-9_53, doi:10.1007/978-3-319-08867-9_53. 27 Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey O. Shallit. Decidability for Sturmian words.Log. Methods Comput. Sci., 20(3),

    work page doi:10.1007/978-3-319-08867-9_53

  23. [23]

    28 TobiasJohn, SimonJantsch, ChristelBaier, andSaschaKlüppelholz

    URL: https://doi.org/10.46298/lmcs-20(3:12)2024,doi:10.46298/LMCS-20(3:12)2024. 28 TobiasJohn, SimonJantsch, ChristelBaier, andSaschaKlüppelholz. Determinizationandlimit- determinization of Emerson-Lei automata. In Zhe Hou and Vijay Ganesh, editors,Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QL...

    work page doi:10.46298/lmcs-20(3:12)2024 2024

  24. [24]

    29 Detlef Kähler and Thomas Wilke

    URL:https://doi.org/10.1007/978-3-030-88885-5_2, doi: 10.1007/978-3-030-88885-5_2. 29 Detlef Kähler and Thomas Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors,Automata, Languages and Programming,...

    work page doi:10.1007/978-3-030-88885-5_2 2008

  25. [25]

    In: Aceto, L., Damg˚ ard, I., Goldberg, L.A., Halld´ orsson, M.M., Ing´ olfsd´ ottir, A., Walukiewicz, I

    URL:https://doi.org/10.1007/ 978-3-540-70575-8_59,doi:10.1007/978-3-540-70575-8_59. 30 Yonit Kesten and Amir Pnueli. A complete proof systems for QPTL. InProceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 2–12. IEEE Computer Society, 1995.doi:10.1109/LICS.1995.523239. 31 Orna Kupferman...

    work page doi:10.1007/978-3-540-70575-8_59 1995

  26. [26]

    33 Orna Kupferman and Moshe Y

    URL:https://doi.org/10.1007/ 978-3-540-31980-1_14,doi:10.1007/978-3-540-31980-1_14. 33 Orna Kupferman and Moshe Y. Vardi. From complementation to certification.Theor. Comput. Sci., 345(1):83–100, 2005.doi:10.1016/j.tcs.2005.07.021. 34 Robert P. Kurshan. Complementing deterministic Büchi automata in polynomial time.J. Comput. Syst. Sci., 35(1):59–71, 1987....

    work page doi:10.1007/978-3-540-31980-1_14 2005

  27. [27]

    36 Ondřej Lengál et al

    URL:https://doi.org/10.1007/ 978-3-642-31424-7_7,doi:10.1007/978-3-642-31424-7_7. 36 Ondřej Lengál et al. Automata benchmarks. https://github.com/ondrik/ automata-benchmarks,

    work page doi:10.1007/978-3-642-31424-7_7

  28. [28]

    Vardi, and Lijun Zhang

    37 Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, and Lijun Zhang. Divide-and-conquer determinization of Büchi automata based on SCC decomposition. In Sharon Shoham and Yakir Vizel, editors,Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 ofLecture Notes in C...

    2022

  29. [29]

    In: Shoham, S., Vizel, Y

    URL: https://doi.org/10.1007/ 978-3-031-13188-2_8,doi:10.1007/978-3-031-13188-2_8. 38 Yong Li, Andrea Turrini, Lijun Zhang, and Sven Schewe. Learning to complement Büchi automata. In Isil Dillig and Jens Palsberg, editors,Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-...

    work page doi:10.1007/978-3-031-13188-2_8 2018

  30. [30]

    39 Yong Li, Moshe Y

    URL: https://doi.org/10.1007/978-3-319-73721-8_15,doi:10.1007/978-3-319-73721-8_15. 39 Yong Li, Moshe Y. Vardi, and Lijun Zhang. On the power of unambiguity in Büchi complement- ation. In Jean-François Raskin and Davide Bresolin, editors,Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, B...

    work page doi:10.1007/978-3-319-73721-8_15 2020

  31. [31]

    41 Juraj Major, František Blahoudek, Jan Strejček, Miriama Sasaráková, and Tatiana Zbončáková

    commit 02092adca492678407bd74b5d3bbe103d8c2b400. 41 Juraj Major, František Blahoudek, Jan Strejček, Miriama Sasaráková, and Tatiana Zbončáková. ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors,Automated Technology for Verification and Analysis - 17th International ...

    2019

  32. [32]

    42 Max Michel

    URL: https://doi.org/10.1007/978-3-030-31784-3_21,doi:10.1007/978-3-030-31784-3_21. 42 Max Michel. Complementation is more difficult with automata on infinite words.CNET, Paris, 15,

    work page doi:10.1007/978-3-030-31784-3_21

  33. [33]

    44 Reed Oei, Dun Ma, Christian Schulz, and Philipp Hieronymi

    URL:https://www.sciencedirect.com/science/ article/pii/0304397584900495,doi:10.1016/0304-3975(84)90049-5. 44 Reed Oei, Dun Ma, Christian Schulz, and Philipp Hieronymi. Pecan: An automated theorem prover for automatic sequences using Büchi automata.CoRR, abs/2102.01727,

    work page doi:10.1016/0304-3975(84)90049-5

  34. [34]

    45 Nir Piterman

    URL: https://arxiv.org/abs/2102.01727,arXiv:2102.01727. 45 Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata.Log. Methods Comput. Sci., 3(3), 2007.doi:10.2168/LMCS-3(3:5)2007. 46 Shmuel Safra. On the complexity ofω-automata. In29th Annual Symposium on Foundations of Computer Science, White Plains, New York, US...

    work page doi:10.2168/lmcs-3(3:5)2007 2007

  35. [35]

    48 Sven Schewe

    doi:10.1145/73007.73019. 48 Sven Schewe. Büchi complementation made tight. In Susanne Albers and Jean-Yves Marion, editors,26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 ofLIPIcs, pages 661–672. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany,

    work page doi:10.1145/73007.73019 2009

  36. [36]

    URL:https: //doi.org/10.4230/LIPIcs.STACS.2009.1854,doi:10.4230/LIPICS.STACS.2009.1854. 49 A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic.Theoretical Computer Science, 49(2-3):217–237,

    work page doi:10.4230/lipics.stacs.2009.1854 2009

  37. [37]

    50 Moshe Y. Vardi. The Büchi complementation saga. In Wolfgang Thomas and Pascal Weil, editors,STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, February 22-24, 2007, Proceedings, Lecture Notes in Computer Science, pages 12–22. Springer,

    2007

  38. [38]

    51 Moshe Y

    URL:https://doi.org/10.1007/978-3-540-70918-3_2, doi: 10.1007/978-3-540-70918-3_2. 51 Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). InProceedings of the Symposium on Logic in Computer Science (LICS ’86), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 332–344. IEEE Computer Society,

    work page doi:10.1007/978-3-540-70918-3_2 1986