论文标题
降低（TO）等级：有效的基于等级的Büchi自动机互补（技术报告）
Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report)
论文作者
论文摘要
本文提供了一些基于等级的方法来补充Büchi自动机的方法。我们从Schewe的理论上最佳结构开始，并开发了一套用于修剪其状态空间的技术，这是实践中获得小型补充自动机的关键。特别是，降低（除了一个）具有其属性（至少一些）所谓的超紧密跑步的属性，这些跑步是其排名尽可能紧的运行。我们对大型基准的评估表明，优化确实有助于基于等级的方法，并且在大量情况下，获得的补体是大量Büchi互补工具所产生的补体。
This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe's theoretically optimal construction and develop a set of techniques for pruning its state space that are key to obtaining small complement automata in practice. In particular, the reductions (except one) have the property that they preserve (at least some) so-called super-tight runs, which are runs whose ranking is as tight as possible. Our evaluation on a large benchmark shows that the optimizations indeed significantly help the rank-based approach and that, in a large number of cases, the obtained complement is the smallest from those produced by a large number of state-of-the-art tools for Büchi complementation.
