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.

翻译：我们提出Kofola——一种用于Büchi自动机补集与包含检测的高效工具，这两者是自动机理论验证中的核心任务，广泛应用于模型检验、运行时监控和定理证明。Kofola实现了前沿的模块化补集框架，将输入自动机分解为强连通分量，并针对每个分量应用与其结构特性相匹配的补集算法。基于这一模块化构造，Kofola还提供了集成新启发式策略的模块化包含检测功能。其关键组件是一种针对补集操作产生的简单广义Rabin对条件的新型即时空满检测算法，该算法能在已探索状态空间足够时立即终止搜索。实验评估表明，Kofola与当前最先进的补集和包含检测工具相比具有高度竞争力：在评估中它是最鲁棒的工具，且在来自实际应用的基准测试中，其性能常比竞品高出数个数量级。