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

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 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.