统一Büchi补语结构
Unifying Büchi Complementation Constructions
摘要：
Büchi自动机的补集是检验自动机包容性的必要条件，在形式化验证中具有重要的理论和实际意义。我们考虑两个最近的互补方法。第一种是Kupferman和Vardi的基于秩的方法，它在包含自动机所有运行的DAG上运行。这种方法是基于这样的观察，即该DAG的顶点可以以某种方式排名，称为奇数排名，当所有运行都被拒绝时。第二种是Kähler和Wilke的基于切片的方法。这种方法跟踪“分裂树”的级别-运行树，其中仅维护关于每个运行的历史的基本信息。虽然基于切片的构造在概念上很简单，但它生成的互补自动机比最近基于秩的Schewe构造的自动机要大得多，并且它很难对分裂树的级别进行符号编码。在这项工作中，我们重新制定了基于切片的方法在运行DAG和preorders状态。在这样做的时候，我们开始在基于秩的方法和基于切片的方法之间进行比较。通过对基于切片的方法的深入分析，我们强烈限制了它产生的不确定性。然后，我们能够采用基于切片的方法来提供一个新的奇数排名，称为回顾性排名，这是从Kupferman和Vardi提供的不同。这种新的排名使我们能够构建一个确定性的极限排名为基础的自动机具有高度限制的过渡功能。此外，通过将基于切片的方法用秩来表达，我们的方法提供了一个简单的符号编码，并实现了Schewe构造的紧界
英文摘要：
Complementation of Büchi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of Kähler and Wilke. This approach tracks levels of "split trees" - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees. In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly restricted transition function. Further, by phrasing the slice-based approach in terms of ranks, our approach affords a simple symbolic encoding and achieves the tight bound of Schewe's construction
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
