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