Kofola 1.0: A Modular Approach to ω-Regular Complementation and Inclusion Checking (Technical Report)
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914567983988736 |
|---|---|
| author | Alexaj, Ondrej Havlena, Vojtěch Holík, Lukáš Lengál, Ondřej Li, Yong Mazzocchi, Nicolas |
| author_facet | Alexaj, Ondrej Havlena, Vojtěch Holík, Lukáš Lengál, Ondřej Li, Yong Mazzocchi, Nicolas |
| contents | We present Kofola, an efficient tool for complementation and inclusion checking of Büchi 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_15390 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Kofola 1.0: A Modular Approach to ω-Regular Complementation and Inclusion Checking (Technical Report) Alexaj, Ondrej Havlena, Vojtěch Holík, Lukáš Lengál, Ondřej Li, Yong Mazzocchi, Nicolas Logic in Computer Science Formal Languages and Automata Theory We present Kofola, an efficient tool for complementation and inclusion checking of Büchi 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. |
| title | Kofola 1.0: A Modular Approach to ω-Regular Complementation and Inclusion Checking (Technical Report) |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2605.15390 |