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.展开更多
In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs i...In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research. A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software. Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method＇s effectiveness. Linear temporal logic was used to model an interdomain routing system and its properties were analyzed. An example is included to demon- strate the method＇s reliability.展开更多
基金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.
基金Supported by the Basic Research Foundation of Tsinghua National Laboratory for Information and Technology (TNList)the JSPS Foundation
文摘In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research. A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software. Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method＇s effectiveness. Linear temporal logic was used to model an interdomain routing system and its properties were analyzed. An example is included to demon- strate the method＇s reliability.
