Büchi互补状态
State of Büchi Complementation
摘要：
自1960年提出Büchi自动机的形式化以来，Büchi自动机的补性研究已经有50多年的历史。已知的互补构建可以分为基于Ramsey的、基于确定的、基于秩的和基于切片的方法。关于这些方法的性能，已经有一些复杂性分析，但很少有实验结果。特别缺乏的是对所有四种方法的比较实验，以了解它们在实践中的表现。在本文中，我们回顾了这四种方法，提出了几种优化算法，并对四种被认为是每种方法中最有效的代表性结构进行了比较实验。实验结果表明：（1）基于确定性的Safra-Piterman构式在产生更小的补语和在分配的时间内完成更多的任务方面优于其他三种构式;（2）所提出的启发式显著改善了Safra-Piterman构式和基于切片的构式。
英文摘要：
Complementation of Büchi automata has been studied for over five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. Regarding the performance of these approaches, there have been several complexity analyses but very few experimental results. What especially lacks is a comparative experiment on all of the four approaches to see how they perform in practice. In this paper, we review the four approaches, propose several optimization heuristics, and perform comparative experimentation on four representative constructions that are considered the most efficient in each approach. The experimental results show that (1) the determinization-based Safra-Piterman construction outperforms the other three in producing smaller complements and finishing more tasks in the allocated time and (2) the proposed heuristics substantially improve the Safra-Piterman and the slice-based constructions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
