Büchi自動機補集演算法之比較研究

Abstract

為Büchi自動機取補集在模型驗證中是一塊重要的領域。M. Michel在1988年就以提出此操作的理論最佳的上界為2O(n log n)，更精確的說是介於Ω((0.36n)n)。後人又得出更精確的理論界線介於Ω((0.76n)n)和O((0.97n)n)之間。從此便不斷有學者提出各種最佳化的補集演算法。這些演算法使用不同的技巧、自動機，並且產生出不一樣大小的補集自動機。因此到底哪一種演算法較好、較實用便成了許多學者探討的方向。但是盜墓錢為止都沒有一篇論文能夠較全面的比較每種演算法的實際運作，或者實際將各種演算法實做，並提供各種演算法的比較數據。 因此論文的第一個目的就是比較每種演算法的運作，為詳細的比較各個演算法，我們同時實做大部分的補集演算法，並用這些實做成果來跑比較實驗。在這些實驗中我們發現，一些演算法雖然沒有比較好的理論上界，但是在真實情況下通常比較有效率，像是Safra’s construction。同時在實做的過程中，我們也發現一些演算的的錯誤，並將其修正。我們發現各種補集演算法的交互檢查，給我們許多幫助和線索，這種檢查有助於提高實做的正確性以及檢查演算法自身的正確性。此外這篇論文的第二個目的則是讓人容易理解各種演算法的運作以及彼此之間的關聯性。因此我們將會詳細的介紹各種演算法，同時使用圖解的方式讓人們更容易理解演算法的運作。並使用演算法的關聯性，讓人們更容易融會貫通各種演算法。在實做方面，我們選擇GOAL作我們開發以及實驗的平台，GOAL是一套操作Omega自動機和時態邏輯的圖形工具，我們擴充六個補集演算法進這個工具。相信會改善這個工具的教育以及研究用途。

Büchi Complementation is a fundamental problem in the automata-theoretic approach to model checking. The theoretically optimal upper bound is 2O(n log n) which is provided by M. Michel in 1988. The precise bound of Büchi complementation is ((0.36n)n). Then the tighter bounds are ((0.76n)n) which is provided by Qiqi Yan and O((0.97n)n) which is provided by O. Kupferman et al. The first optimal complementation algorithm was proposed by Safra in 1989. Since then a large number of optimal algorithms have been proposed. These algorithms construct Büchi automata using different intermediate automata and the constructed Büchi automata have different state spaces. Thus, there are some people proposed a few theoretical comparisons of Büchi complementation. These comparisons include explains of algorithms, but do not include the implementation of several algorithms and the experimental results. The first purpose of this thesis is to provide a more complete comparison of Büchi complementations. For comparative experiment, we implement these algorithms to compare these complementations. In these experiments, some algorithms have worse time complexity, but the efficiency of Büchi complementation is better such as Safra’s construction. A algorithm which is lower theoretical complexity does not guarantee that it is more efficient algorithm. We also find some bugs in these complementation algorithms when we implement them. It shows that the cross-checking between complementation methods is helpful to improve the accuracy of the implementations and check the correctness of the methods. The second purpose is to understand these algorithms how and why to do these Büchi complementations and explain these algorithms in detail. To describe them more clear, we use some examples and illustrations which show these algorithms in detail. In these examples, some relationships between these algorithms are also showed. These relationships help us to understand the Büchi complementation algorithms. The platform of the implementations is GOAL. For this research, we extend GOAL, a graphical tool for manipulating omega-automata and temporal formulae, with six complementation algorithms. The capability of research and education are also enhanced in GOAL.