The construction of Büchi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first construction algorithm to obtain simple Büchi 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 Büchi automata, without transformation into transition-based automata. A form-filling algorithm for the Büchi automata, which is based on the form-filling algorithm for deterministic automata, was developed by redefining parts of the configuration of the Büchi 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.

An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period. This reduces the cost during the abstraction period relative to models requiring many useless states. A dining-philosophers example comparing this abstraction method with conventional methods indicates that a large proportion of the state space has been reduced by this abstraction method. Finally, the abstract method is shown to be correct and an analysis is given to show how such a large proportion of states can be reduced.

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 demonstrate the method’s reliability.

The least-squares (LS) algorithm has been used for system modeling for a long time. Without any excitation conditions, only the convergence rate of the common LS algorithm can be obtained. This paper analyzed the weighted least-squares (WLS) algorithm and described the good properties of the WLS algorithm. The WLS algorithm was then used for adaptive control of linear stochastic systems to show that the linear closed-loop system was globally stable and that the system identification was consistent. Compared to the past optimal adaptive controller, this controller does not impose restricted conditions on the coefficients of the system, such as knowing the first coefficient before the controller. Without any persistent excitation conditions, the analysis shows that, with the regulation of the adaptive control, the closed-loop system was globally stable and the adaptive controller converged to the one-step-ahead optimal controller in some sense.