時序邏輯至自動機轉換演算法之深入比較研究

Abstract

Translation of a temporal formula into an automaton is a central issue in the automatabased approach to model checking. In the approach, model checking of a system M against a temporal specification f proceeds in three steps: (1) generate an automaton A¬f for the negation of f, (2) construct a product automaton A that is the intersection of M and A¬f , and (3) check the emptiness of the product automaton A. The time needed to complete the model checking task is proportional to the size of A, which is the product of the sizes of M and A¬f . For a given system, the size of A¬f determines the size of A. Therefore, the smaller A¬f is, the faster the model checking task may be carried out. In this thesis, we investigate an extensive collection of translation algorithms, including all of the well-known ones. We compare the state and the transition sizes of the automata generated from these algorithms. An algorithm that generates smaller automata should be more helpful when it is applied in model checking. The reason is that when one needs to certify that a system satisfies the desired property, the complete product automaton must be constructed. To perform the comparison, we implement not only the translation algorithms but also possible improvements in the GOAL tool. From the experimental results, we observe that none of the algorithms can always generate the smallest automaton for each of the temporal formulae considered. We therefore propose a portfolio for choosing suitable algorithms for different kinds of temporal formulae. We also design and implement an open repository called B‥uchi Store where one can look up the B‥uchi automaton for a given temporal formula.