The construction of B0chi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first constr,uction algorithm to obtain simple B0chi automata from linear-time tempora...The construction of B0chi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first constr,uction algorithm to obtain simple B0chi automata from linear-time temporal logic which significantly reduces the sizes of the state spaces. A form-filling algorithm was used to reduce the size of the generated automata and the algorithms were applied directly to state-based Buchi automata, without transformation into transition-based automata. A form-filling algorithm for the Buchi automata, which is based on the form-filling algorithm for deterministic automata, was developed by redefining parts of the configuration of the Buchi automata as well as the transition function. The correctness of this form-filling algorithm was proven. Tests show that this approach is competitive, especially on LTL formulae in the form of G, F, and U.展开更多
基金Supported by the National Natural Science Foundation of China(No. 60635020)the Basic Research Foundation of Tsinghua National Laboratory for Information Science and Technology(TNList)the Foundation of Japan Society for the Promotion of Science
文摘The construction of B0chi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first constr,uction algorithm to obtain simple B0chi automata from linear-time temporal logic which significantly reduces the sizes of the state spaces. A form-filling algorithm was used to reduce the size of the generated automata and the algorithms were applied directly to state-based Buchi automata, without transformation into transition-based automata. A form-filling algorithm for the Buchi automata, which is based on the form-filling algorithm for deterministic automata, was developed by redefining parts of the configuration of the Buchi automata as well as the transition function. The correctness of this form-filling algorithm was proven. Tests show that this approach is competitive, especially on LTL formulae in the form of G, F, and U.
