交替布奇自動機與反交替布林布奇自動機之語言操作

Abstract

ω-自動機於20世紀60年代首次引入，並成為非終止程序的規範與驗證的有用工具。不同類型的自動機有不同的表現力和複雜性, 交替布林自動機 (ABA) 允許存在性和普遍性的轉移，這使得它比原本的布林自動機更簡潔。然而，據我們所知，在初始狀態唯一的限制下，目前還沒有明確的構建出ABA的交集。 先前的工作表明，使用更加緊湊的自動機進行合成可能會帶來顯著的加速，這表明 ABA 對於在有限時間內解決複雜合成問題具有巨大潛力。此外，維持 ABA 具有單一初始狀態也相當重要，這可以避免驗證複雜度增長過快。上述兩個原因促使我們尋找 ABA 對於常見的語言操作之明確構造，並提出比 ABA 更緊湊的新自動機。 在這項工作中，我們給出了一個ABA交集的簡潔構建。我們還提出一個基於ABA的新ω-自動機，稱為反向交替布林自動機 (rABBA)，並提供rABBA基本語言操作的構建，包括交集、並集和互補。

ω-automaton is first introduce in 1960s, and become a useful tool for specification and verification of non-terminating programs. Different type of automata have different expressive power and complexity. Alternating Büchi automaton (ABA) allows both existential and universal transition, which makes it more succinct than origin Büchi automaton. However, to the best of our knowledge, there is still no explicit construction for intersection of ABA with single initial state. Previous work shows that using a compact automaton to perform synthesis may lead to a significant acceleration, which suggests that ABA has a great potential for solving complex synthesis problem in limited time. Additionally, it’s important that ABA has a single initial state to avoid rapid growth of complexity during verification. The two reasons above motivate us to find an explicit construction of common language operations for ABA, and propose an new automaton which is more compact than ABA. In this work, we give a compact construction for intersection of ABA. We also propose a new ω-automaton based on ABA, called reversed alternating Booloean Büchi automaton, and provide the construction of basic language operation of rABBA, including intersection, union, and complementation.