A Comparative Study of Algorithms for Büchi Complementation
Date Issued
2008
Date
2008
Author(s)
Luo, Chi-Jian
Abstract
Büchi Complementation is a fundamental problem in the automata-theoretic approacho model checking. The theoretically optimal upper bound is 2O(n log n) which is providedy M. Michel in 1988. The precise bound of Büchi complementation is (0.36n)n).hen the tighter bounds are (0.76n)n) which is provided by Qiqi Yan and O((0.97n)n)hich is provided by O. Kupferman et al. The first optimal complementation algorithmas proposed by Safra in 1989. Since then a large number of optimal algorithms haveeen proposed. These algorithms construct Büchi automata using different intermediateutomata and the constructed Büchi automata have different state spaces. Thus, there areome people proposed a few theoretical comparisons of Büchi complementation. Theseomparisons include explains of algorithms, but do not include the implementation ofeveral algorithms and the experimental results.he first purpose of this thesis is to provide a more complete comparison of Büchiomplementations. For comparative experiment, we implement these algorithms to comparehese complementations. In these experiments, some algorithms have worse timeomplexity, but the efficiency of Büchi complementation is better such as Safra’s construction. algorithm which is lower theoretical complexity does not guarantee that its more efficient algorithm. We also find some bugs in these complementation algorithmshen we implement them. It shows that the cross-checking between complementationethods is helpful to improve the accuracy of the implementations and check the correctnessf the methods. The second purpose is to understand these algorithms hownd why to do these Büchi complementations and explain these algorithms in detail.o describe them more clear, we use some examples and illustrations which show theselgorithms in detail. In these examples, some relationships between these algorithmsre also showed. These relationships help us to understand the Büchi complementationlgorithms. The platform of the implementations is GOAL. For this research, we extendOAL, a graphical tool for manipulating omega-automata and temporal formulae,ith six complementation algorithms. The capability of research and education are alsonhanced in GOAL.
Subjects
Model Checking
Complementation
Determinization
Büchi Automata
Omega-automata
Verfication
File(s)![Thumbnail Image]()
Loading...
Name
ntu-97-R95725029-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):a6caa7dcb4e21a72ec2019bf26415411