pith. sign in

arxiv: 2605.15390 · v1 · pith:3NGDADBHnew · submitted 2026-05-14 · 💻 cs.LO · cs.FL

Kofola 1.0: A Modular Approach to {ω}-Regular Complementation and Inclusion Checking (Technical Report)

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

Pith reviewed 2026-05-19 15:14 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords Büchi automatacomplementationinclusion checkingstrongly connected componentsmodular frameworkemptiness checkingomega-regular languagesmodel checking
0
0 comments X

The pith

Kofola decomposes Büchi automata into strongly connected components and applies tailored complementation to each.

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

The paper presents Kofola as a tool for complementing Büchi automata and checking inclusion between them, operations central to verifying systems that run indefinitely. It breaks the input automaton into its strongly connected components and selects a complementation procedure matched to the structure of each component rather than applying one uniform method. A new on-the-fly emptiness checker for the generalized Rabin pair condition lets the process stop once enough states have been explored. If the approach holds, verification tasks in model checking and monitoring can scale to larger automata without exhausting time or memory.

Core claim

Kofola implements a modular complementation framework that decomposes the input automaton into strongly connected components and applies to each component a complementation algorithm tailored to its structural properties. Building on this modular construction, Kofola also provides modular inclusion checking with new heuristics. A key ingredient is a new on-the-fly emptiness-checking algorithm for the simple generalized Rabin pair condition produced by our complementation, allowing the search to terminate as soon as the explored state space suffices.

What carries the argument

The modular complementation framework that decomposes the automaton into strongly connected components and applies structure-specific algorithms, supported by an on-the-fly emptiness checker for the resulting generalized Rabin pair condition.

If this is right

  • Complementation of automata from real verification problems becomes feasible at larger sizes.
  • Inclusion checks between automata run faster through reuse of the same modular structure and added heuristics.
  • Verification tools can explore more complex omega-regular properties without early termination.
  • The produced generalized Rabin conditions can be handled directly in downstream emptiness checks without full expansion.

Where Pith is reading between the lines

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

  • The same SCC decomposition could be reused to speed up other automata operations such as equivalence checking or minimization.
  • Adding new component-specific algorithms would require only local changes to the framework rather than a full redesign.
  • The observed robustness suggests that structure-aware methods may generalize to nondeterministic automata beyond the Büchi case.

Load-bearing premise

The decomposition into strongly connected components combined with per-component tailored algorithms and the on-the-fly emptiness checker preserves correctness while delivering efficiency gains.

What would settle it

A Büchi automaton for which Kofola produces a complement that accepts a word the original rejects, or a benchmark suite from practical applications where Kofola times out or uses more memory than non-modular tools.

Figures

Figures reproduced from arXiv: 2605.15390 by Luk\'a\v{s} Hol\'ik, Nicolas Mazzocchi, Ondrej Alexaj, Ond\v{r}ej Leng\'al, Vojt\v{e}ch Havlena, Yong Li.

Figure 1
Figure 1. Figure 1: Architecture of Kofola Kofola is implemented in C++ and avail￾able at [2] under the GNU GPL 3.0 license. Its architecture is shown in Section 2. The Frontend uses Spot [21] to read input au￾tomata A1.hoa and, for inclusion checking only, A2.hoa, both in the HOA [7] format. Next, the automata enter Preprocessing and setup, where (i) Spot reduces them using ei￾ther Low or High reduction level, depending on t… view at source ↗
Figure 2
Figure 2. Figure 2: Visualization of macrostate’s succes￾sor computation over symbol a. The input of the top-level algorithm are, except the automaton itself, also partitions P1, . . . , Pk of the input au￾tomaton and the partial algorithms AlgP1 , . . . , AlgPk . The macrostates of the top-level algoritm are then of the form (S, M1, . . . , Mk), where S is the set of reachable states and M1, . . . , Mk are macrostates of the… view at source ↗
Figure 3
Figure 3. Figure 3: Comparison of state counts of complement automata generated by [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Comparison of runtime of inclusion checking for [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
read the original abstract

We present Kofola, an efficient tool for complementation and inclusion checking of B\"uchi automata, two central tasks in automata-theoretic verification with applications in model checking, monitoring, and theorem proving. Kofola implements a state-of-the-art modular complementation framework that decomposes the input automaton into strongly connected components and applies to each component a complementation algorithm tailored to its structural properties. Building on this modular construction, Kofola also provides modular inclusion checking with new heuristics. A key ingredient is a new on-the-fly emptiness-checking algorithm for the simple generalized Rabin pair condition produced by our complementation, allowing the search to terminate as soon as the explored state space suffices. Empirical evaluation shows that Kofola is highly competitive with state-of-the-art complementation and inclusion-checking tools: it is the most robust tool in our evaluation and often outperforms competitors by several orders of magnitude on benchmarks from practical applications.

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

1 major / 2 minor

Summary. The paper presents Kofola 1.0, a tool for complementation and inclusion checking of Büchi automata. It implements a modular framework that decomposes the input automaton into strongly connected components (SCCs) and applies a complementation algorithm tailored to the structural properties of each component. The approach is extended to modular inclusion checking with new heuristics. A central technical contribution is a new on-the-fly emptiness-checking algorithm for the simple generalized Rabin pair condition generated by the per-SCC complementation, which permits early termination once the explored state space is sufficient. Empirical evaluation on benchmarks from practical applications indicates that Kofola is the most robust tool in the comparison and frequently outperforms existing state-of-the-art tools by several orders of magnitude.

Significance. If the modular decomposition preserves correctness and the on-the-fly emptiness checker is shown to be sound for the Rabin-pair conditions arising from SCC-specific complementation, the work would provide a practically significant advance in automata-theoretic verification. The combination of structural decomposition with a specialized emptiness procedure directly targets the performance bottlenecks in complementation and inclusion, which are core operations in model checking, monitoring, and theorem proving. Reproducible tool implementation and evaluation on application-derived benchmarks would further strengthen the contribution.

major comments (1)
  1. [emptiness-checking algorithm section] The section describing the on-the-fly emptiness checker for generalized Rabin pairs must supply a complete argument that the early-termination criterion remains sound when the acceptance condition is produced by per-SCC complementation. In particular, it is necessary to show that no accepting run can exist outside the current exploration frontier even if the Rabin pairs introduced by individual SCC complements depend on paths that cross original component boundaries. Without this argument, both the claimed correctness and the reported speed-ups rest on an unverified assumption.
minor comments (2)
  1. [abstract and introduction] The abstract and introduction should include a brief pointer to the specific theorem or lemma that establishes correctness of the modular construction.
  2. [empirical evaluation] Benchmark tables would benefit from explicit reporting of the number of timeouts and memory-outs for each tool to substantiate the robustness claim.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed and constructive review. The positive assessment of the practical significance of Kofola 1.0 is appreciated. We address the single major comment below and will revise the manuscript to strengthen the presentation.

read point-by-point responses

  1. Referee: [emptiness-checking algorithm section] The section describing the on-the-fly emptiness checker for generalized Rabin pairs must supply a complete argument that the early-termination criterion remains sound when the acceptance condition is produced by per-SCC complementation. In particular, it is necessary to show that no accepting run can exist outside the current exploration frontier even if the Rabin pairs introduced by individual SCC complements depend on paths that cross original component boundaries. Without this argument, both the claimed correctness and the reported speed-ups rest on an unverified assumption.

    Authors: We agree that an explicit, self-contained soundness argument for the early-termination criterion is required when the generalized Rabin pairs originate from the modular per-SCC complementation. Although the overall construction composes the per-SCC complements in a manner that keeps the acceptance condition local to the explored states (because each SCC complement is self-contained and the on-the-fly search respects the original transition structure), the manuscript currently presents the emptiness procedure at a high level without spelling out the cross-boundary case. In the revised version we will add a dedicated lemma (or subsection) that proves: (i) any accepting run of the complemented automaton must eventually enter and remain in one of the complemented SCCs, and (ii) the Rabin-pair condition for that SCC can be satisfied only by states reachable within the current exploration frontier, independent of unvisited paths that cross original component boundaries. This addition will also clarify why the reported speed-ups are sound. We therefore mark this revision as necessary. revision: yes

Circularity Check

0 steps flagged

No circularity: algorithmic framework and empirical results are self-contained

full rationale

The paper describes a modular complementation construction for Büchi automata that decomposes into SCCs and applies per-component algorithms, plus an on-the-fly emptiness checker for the resulting generalized Rabin conditions. These steps are standard automata-theoretic constructions and implementation choices whose correctness rests on established theory rather than any equation that reduces by definition to a fitted parameter, self-citation chain, or renamed input. Performance claims are supported by direct benchmarking against external tools on practical instances, with no load-bearing derivation that collapses to the paper's own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The contribution rests on standard automata-theoretic background rather than new free parameters, ad-hoc axioms, or invented entities.

axioms (1)
  • standard math Standard definitions and closure properties of Büchi automata and ω-regular languages hold.
    The modular complementation framework is built directly on these established properties.

pith-pipeline@v0.9.0 · 5725 in / 1312 out tokens · 45460 ms · 2026-05-19T15:14:45.565041+00:00 · methodology

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

56 extracted references · 56 canonical work pages

  1. [1]

    Automata-benchmarks.https://github.com/ondrik/automata-benchmarks/ tree/master/omega/(2025) 2.Kofola.https://github.com/VeriFIT/kofola(2025)

    work page 2025

  2. [2]

    In: Touili, T., Cook, B., Jackson, P.B

    Abdulla, P.A., Chen, Y., Clemente, L., Hol´ ık, L., Hong, C., Mayr, R., Vojnar, T.: Simulation subsumption in Ramsey-based B¨ uchi automata universality and inclusion testing. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15- 19, 2010. Proceedings. Lecture Notes in ...

    work page 2010

  3. [3]

    Springer (2010).https://doi.org/10.1007/978-3-642-14295-6_14,https: //doi.org/10.1007/978-3-642-14295-6_14

    work page doi:10.1007/978-3-642-14295-6_14 2010

  4. [4]

    In: Katoen, J., K¨ onig, B

    Abdulla, P.A., Chen, Y., Clemente, L., Hol´ ık, L., Hong, C., Mayr, R., Vojnar, T.: Advanced Ramsey-based B¨ uchi automata inclusion testing. In: Katoen, J., K¨ onig, B. (eds.) CONCUR 2011 - Concurrency Theory - 22nd International Con- ference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6901, pp...

    work page doi:10.1007/978-3-642-23217-6_13 2011

  5. [5]

    Alexaj, O., Havlena, V., Hol´ ık, L., Leng´ al, O., Li, Y., Mazzocchi, N.: Artifact: Kofola1.0: A modular approach toω-regular complementation and inclusion checking (october 2025).https://doi.org/10.5281/zenodo.17478623,https:// doi.org/10.5281/zenodo.17478623

    work page doi:10.5281/zenodo.17478623 2025

  6. [6]

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

    Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for B¨ uchi automata. In: Dawar, A., Gr¨ adel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Ox- ford, UK, July 09-12, 2018. pp. 46–55. ACM (2018).https://doi.org/10.1145/ 3209108.3209138,https://doi.org/10.1145/3209108.3209138

    work page doi:10.1145/3209108.3209138 2018

  7. [7]

    In: Kroening, D., Pasareanu, C.S

    Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., Kret´ ınsk´ y, J., M¨ uller, D., Parker, D., Strejcek, J.: The Hanoi omega-automata format. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Confer- ence, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science,...

    work page doi:10.1007/978-3-319-21690-4_31 2015

  8. [8]

    In: Chen, Y., Cheng, C., Esparza, J

    Baier, C., Blahoudek, F., Duret-Lutz, A., Klein, J., M¨ uller, D., Strejcek, J.: Generic emptiness check for fun and profit. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th Interna- tional Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11...

    work page doi:10.1007/978-3-030-31784-3_26 2019

  9. [9]

    In: Sankaranarayanan, S., Sharygina, N

    Beutner, R., Finkbeiner, B.: AutoHyper: Explicit-state model checking for Hy- perLTL. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and 13 Practice of Software, ETAPS 2022, Paris, France, ...

    work page doi:10.1007/978-3-031-30823-9_8 2023

  10. [10]

    In: Lahiri, S.K., Wang, C

    Blahoudek, F., Duret-Lutz, A., Strejˇ cek, J.: Seminator 2 can complement general- ized B¨ uchi automata via improved semi-determinization. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp....

    work page doi:10.1007/978-3-030-53291-8_2 2020

  11. [11]

    In: Birkedal, L

    Breuers, S., L¨ oding, C., Olschewski, J.: Improved Ramsey-based B¨ uchi complemen- tation. In: Birkedal, L. (ed.) Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2...

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

  12. [12]

    1960 internat

    B¨ uchi, J.R.: On a decision method in restricted second order arithmetic, logic, methodology and philosophy of science (proc. 1960 internat. congr.) (1962)

    work page 1960

  13. [13]

    In: McAllester, D.A

    Bustan, D., Grumberg, O.: Simulation based minimization. In: McAllester, D.A. (ed.) Automated Deduction - CADE-17, 17th International Conference on Au- tomated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings. Lec- ture Notes in Computer Science, vol. 1831, pp. 255–270. Springer (2000).https: //doi.org/10.1007/10721959_20,https://doi.org/10.1...

    work page doi:10.1007/10721959_20 2000

  14. [14]

    In: Lin, A.W

    Chen, Y., Havlena, V., Leng´ al, O.: Simulations in rank-based B¨ uchi automata complementation. In: Lin, A.W. (ed.) Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1- 4, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11893, pp. 447–

    work page 2019

  15. [15]

    Springer (2019).https://doi.org/10.1007/978-3-030-34175-6_23,https: //doi.org/10.1007/978-3-030-34175-6_23

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

  16. [16]

    In: Foster, J.S., Grossman, D

    Chen, Y., Heizmann, M., Leng´ al, O., Li, Y., Tsai, M., Turrini, A., Zhang, L.: Ad- vanced automata-based algorithms for program termination checking. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. pp. 135–150. ACM (...

    work page doi:10.1145/3192366.3192405 2018

  17. [17]

    Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Log. Methods Comput. Sci.15(1) (2019).https://doi.org/10.23638/LMCS-15(1:12)2019,https://doi.org/10. 23638/LMCS-15(1:12)2019

    work page doi:10.23638/lmcs-15(1:12)2019 2019

  18. [18]

    In: Wing, J.M., Woodcock, J., Davies, J

    Couvreur, J.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM’99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I. Lecture Notes in Computer Science, vol. 1708, pp. 253–271. Springer (1999).https://...

    work page doi:10.1007/3-540-48119-2_16 1999

  19. [19]

    In: Leucker, M., Rueda, C., Valencia, F.D

    Diekert, V., Muscholl, A., Walukiewicz, I.: A note on monitors and B¨ uchi au- tomata. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, Oc- tober 29-31, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9399, 14 pp. 39–57. Springer (2015).https://doi.or...

    work page doi:10.1007/978-3-319-25150-9_3 2015

  20. [20]

    In: Shoham, S., Vizel, Y

    Doveri, K., Ganty, P., Mazzocchi, N.: FORQ-based language inclusion formal test- ing. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th Inter- national Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 109–129. Springer (2022).https://doi.org/10.1007/978-3-031...

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

  21. [21]

    In: Haddad, S., Varacca, D

    Doveri, K., Ganty, P., Ranzato, F.: Inclusion testing of B¨ uchi automata based on well-quasiorders. In: Haddad, S., Varacca, D. (eds.) 32nd International Con- ference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol. 203, pp. 3:1–3:22. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2021).https://doi.org/10.423...

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

  22. [22]

    (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II

    Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber- Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From Spot 2.0 to Spot 2.10: What’s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lec...

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

  23. [23]

    Emerson, E.A., Lei, C.: Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program.8(3), 275–306 (1987).https://doi.org/10.1016/ 0167-6423(87)90036-0,https://doi.org/10.1016/0167-6423(87)90036-0

    work page doi:10.1016/0167-6423(87)90036-0 1987

  24. [24]

    MIT Press (2023)

    Esparza, J., Blondin, M.: Automata Theory: An Algorithmic Approach. MIT Press (2023)

    work page 2023

  25. [25]

    Friedgut, E., Kupferman, O., Vardi, M.Y.: B¨ uchi complementation made tighter. Int. J. Found. Comput. Sci.17(4), 851–868 (2006).https://doi.org/10.1142/ S0129054106004145,https://doi.org/10.1142/S0129054106004145

    work page doi:10.1142/s0129054106004145 2006

  26. [26]

    In: Sankaranarayanan, S., Sharygina, N

    Havlena, V., Leng´ al, O., Li, Y., ˇSmahl´ ıkov´ a, B., Turrini, A.: Modular mix-and- match complementation of B¨ uchi automata. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 249–270. Springer Nature Switzerland, Cham (2023),https://doi.org/10.1007/ 978-3-031-30823-9_13

    work page 2023

  27. [27]

    In: Echihabi, K., Meyer, R

    Havlena, V., Leng´ al, O., Smahl´ ıkov´ a, B.: Deciding S1S: down the rabbit hole and through the looking glass. In: Echihabi, K., Meyer, R. (eds.) Networked Systems - 9th International Conference, NETYS 2021, Virtual Event, May 19- 21, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12754, pp. 215–

    work page 2021

  28. [28]

    Springer (2021).https://doi.org/10.1007/978-3-030-91014-3_15,https: //doi.org/10.1007/978-3-030-91014-3_15

    work page doi:10.1007/978-3-030-91014-3_15 2021

  29. [29]

    In: Haddad, S., Varacca, D

    Havlena, V., Leng´ al, O.: Reducing (to) the ranks: Efficient rank-based B¨ uchi au- tomata complementation. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol. 203, pp. 2:1–2:19. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2021).https://doi.org/...

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

  30. [30]

    In: Shoham, S., Vizel, Y

    Havlena, V., Leng´ al, O., ˇSmahl´ ıkov´ a, B.: Complementing B¨ uchi automata with Ranker. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th Inter- national Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 188–201. Springer (2022). 15 https://doi.org/10.1007...

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

  31. [31]

    In: Fisman, D., Rosu, G

    Havlena, V., Leng´ al, O.,ˇSmahl´ ıkov´ a, B.: Sky is not the limit: Tighter rank bounds for elevator automata in B¨ uchi automata complementation. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Confer- ences on Theory and Pra...

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

  32. [32]

    Hieronymi, P., Ma, D., Oei, R., Schaeffer, L., Schulz, C., Shallit, J.O.: Decidability for Sturmian words. Log. Methods Comput. Sci.20(3) (2024).https://doi.org/ 10.46298/LMCS-20(3:12)2024,https://doi.org/10.46298/lmcs-20(3:12)2024

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

  33. [33]

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

    K¨ ahler, D., Wilke, T.: Complementation, disambiguation, and determinization of B¨ uchi automata unified. In: Aceto, L., Damg˚ ard, I., Goldberg, L.A., Halld´ orsson, M.M., Ing´ olfsd´ ottir, A., Walukiewicz, I. (eds.) Automata, Languages and Pro- gramming. pp. 724–735. Springer Berlin Heidelberg, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-...

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

  34. [34]

    In: Liu, Z., Ravn, A.P

    Karmarkar, H., Chakraborty, S.: On minimal odd rankings for B¨ uchi complemen- tation. In: Liu, Z., Ravn, A.P. (eds.) Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14- 16, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5799, pp. 228–

    work page 2009

  35. [35]

    Springer (2009).https://doi.org/10.1007/978-3-642-04761-9_18,https: //doi.org/10.1007/978-3-642-04761-9_18

    work page doi:10.1007/978-3-642-04761-9_18 2009

  36. [36]

    In: Lahiri, S.K., Wang, C

    Kret´ ınsk´ y, J., Meggendorfer, T., Sickert, S.: Owl: A library forω-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verifi- cation and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. pp. 543–550. Lecture Notes in Com- puter Science, Springer (2018).https://do...

    work page doi:10.1007/978-3-030-01090-4_ 2018

  37. [37]

    In: Alur, R., Henzinger, T.A

    Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification. pp. 372–382. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)

    work page 1996

  38. [38]

    ACM Trans

    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log.2(3), 408–429 (2001).https://doi.org/10.1145/377978. 377993,https://doi.org/10.1145/377978.377993

    work page doi:10.1145/377978 2001

  39. [39]

    In: Huisman, M., Pasareanu, C.S., Zhan, N

    Li, Y., Tsay, Y., Turrini, A., Vardi, M.Y., Zhang, L.: Congruence relations for B¨ uchi automata. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) Formal Meth- ods - 24th International Symposium, FM 2021, Virtual Event, November 20- 26, 2021, Proceedings. Lecture Notes in Computer Science, vol. 13047, pp. 465–

    work page 2021

  40. [40]

    Springer (2021).https://doi.org/10.1007/978-3-030-90870-6_25,https: //doi.org/10.1007/978-3-030-90870-6_25

    work page doi:10.1007/978-3-030-90870-6_25 2021

  41. [41]

    In: Shoham, S., Vizel, Y

    Li, Y., Turrini, A., Feng, W., Vardi, M.Y., Zhang, L.: Divide-and-conquer deter- minization of B¨ uchi automata based on SCC decomposition. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Com- puter Science, vol. 13372, pp. 152–...

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

  42. [42]

    In: Dillig, I., Palsberg, J

    Li, Y., Turrini, A., Zhang, L., Schewe, S.: Learning to complement B¨ uchi automata. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Inter- pretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10747, pp. 313–335. Springer (2018).h...

    work page doi:10.1007/978-3-319-73721-8_ 2018

  43. [43]

    In: Chen, Y., Cheng, C., Esparza, J

    L¨ oding, C., Pirogov, A.: New optimizations and heuristics for determinization of B¨ uchi automata. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technol- ogy for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 317–333. Spring...

    work page doi:10.1007/978-3-030-31784-3_18 2019

  44. [44]

    Miyano, S., Hayashi, T.: Alternating finite automata onω-words. Theo- retical Computer Science32(3), 321–330 (1984).https://doi.org/https: //doi.org/10.1016/0304-3975(84)90049-5,https://www.sciencedirect.com/ science/article/pii/0304397584900495

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

  45. [45]

    CoRRabs/2102.01727(2021), https://arxiv.org/abs/2102.01727

    Oei, R., Ma, D., Schulz, C., Hieronymi, P.: Pecan: An automated theorem prover for automatic sequences using B¨ uchi automata. CoRRabs/2102.01727(2021), https://arxiv.org/abs/2102.01727

    work page arXiv 2021

  46. [46]

    Piterman, N.: From nondeterministic B¨ uchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci.3(3) (2007).https://doi.org/10. 2168/LMCS-3(3:5)2007,https://doi.org/10.2168/LMCS-3(3:5)2007

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

  47. [47]

    Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundam. Informaticae119(3-4), 393–406 (2012).https://doi. org/10.3233/FI-2012-744,https://doi.org/10.3233/FI-2012-744

    work page doi:10.3233/fi-2012-744 2012

  48. [48]

    In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October

    Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October

    work page

  49. [49]

    pp. 319–327. IEEE Computer Society (1988).https://doi.org/10.1109/ SFCS.1988.21948,https://doi.org/10.1109/SFCS.1988.21948

    work page doi:10.1109/sfcs.1988.21948 1988

  50. [50]

    In: Albers, S., Marion, J

    Schewe, S.: B¨ uchi complementation made tight. In: Albers, S., Marion, J. (eds.) 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings. LIPIcs, vol. 3, pp. 661–672. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, Germany (2009).https://doi.org/10.4230/LIPIcs.STACS.20...

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

  51. [51]

    In: Chaudhuri, S., Farzan, A

    Sickert, S., Esparza, J., Jaax, S., Kˇ ret´ ınsk´ y, J.: Limit-deterministic B¨ uchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Ver- ification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9780, pp. 312–332. Spring...

    work page doi:10.1007/978-3-319-41540-6_ 2016

  52. [52]

    Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B¨ uchi automata with applications to temporal logic. Theor. Comput. Sci.49, 217– 237 (1987).https://doi.org/10.1016/0304-3975(87)90008-9,https://doi. org/10.1016/0304-3975(87)90008-9

    work page doi:10.1016/0304-3975(87)90008-9 1987

  53. [53]

    In: 12th Annual Sym- posium on Switching and Automata Theory (swat 1971)

    Tarjan, R.: Depth-first search and linear graph algorithms. In: 12th Annual Sym- posium on Switching and Automata Theory (swat 1971). pp. 114–121 (1971). https://doi.org/10.1109/SWAT.1971.10

    work page doi:10.1109/swat.1971.10 1971

  54. [54]

    Tsai, M., Fogarty, S., Vardi, M.Y., Tsay, Y.: State of B¨ uchi complementation. Log. Methods Comput. Sci.10(4) (2014).https://doi.org/10.2168/LMCS-10(4: 13)2014,https://doi.org/10.2168/LMCS-10(4:13)2014 17

    work page doi:10.2168/lmcs-10(4: 2014

  55. [55]

    In: Chockler, H., Hu, A.J

    Vardi, M.Y.: Automata-theoretic model checking revisited. In: Chockler, H., Hu, A.J. (eds.) Hardware and Software: Verification and Testing, 4th Interna- tional Haifa Verification Conference, HVC 2008, Haifa, Israel, October 27-30,

    work page 2008

  56. [56]

    Lecture Notes in Computer Science, vol

    Proceedings. Lecture Notes in Computer Science, vol. 5394, p. 2. Springer (2008).https://doi.org/10.1007/978-3-642-01702-5_2,https://doi.org/10. 1007/978-3-642-01702-5_2 18

    work page doi:10.1007/978-3-642-01702-5_2 2008