Kofola 1.0: A Modular Approach to {\omega}-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

TL;DR
Kofola is an efficient, modular tool for automata complementation and inclusion checking, leveraging structural decomposition and on-the-fly algorithms to outperform existing solutions in verification tasks.
Contribution
It introduces a modular framework for B"uchi automata complementation and inclusion checking, with novel heuristics and an on-the-fly emptiness algorithm for improved performance.
Findings
Kofola outperforms state-of-the-art tools on practical benchmarks.
The modular approach improves robustness and efficiency.
On-the-fly emptiness checking accelerates verification processes.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
