从不确定Büchi和Streett自动机到确定奇偶自动机
From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata
摘要：
在本文中，我们重新Safra的确定性结构的自动机上无限的话。我们将展示如何构造具有较少状态的确定性自动机，最重要的是，奇偶校验接受条件。确定性在许多应用中被使用，例如树自动机的推理，CTL* 的可满足性，以及逻辑规范的可实现性和综合。所有这些应用的上界减少使用我们的建设产生的较小的确定性自动机。此外，奇偶校验接受条件允许使用更有效的算法（与处理Rabin或Streett接受条件相比）。
英文摘要：
In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
