A Comparative Study of Algorithms for Büchi Complementation

• Main Authors: Chi-Jian Luo, 羅啟建
• Other Authors: Yih-Kuen Tsay
• Format: Others
• Language: en_US
• Published: 2008
• Online Access: http://ndltd.ncl.edu.tw/handle/42181931272759046300

碩士 === 國立臺灣大學 === 資訊管理學研究所 === 96 === 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.