To combat the well-known state-space explosion problem in Prop ositional Linear T emp o- ral Logic （PLTL） model checking, a novel algo- rithm capable of translating PLTL formulas into Nondeterministic Automata （NA...To combat the well-known state-space explosion problem in Prop ositional Linear T emp o- ral Logic （PLTL） model checking, a novel algo- rithm capable of translating PLTL formulas into Nondeterministic Automata （NA） in an efficient way is proposed. The algorithm firstly transforms PLTL formulas into their non-free forms, then it further translates the non-free formulas into their Normal Forms （NFs）, next constructs Normal Form Graphs （NFGs） for NF formulas, and it fi- nally transforms NFGs into the NA which ac- cepts both finite words and int-mite words. The experimental data show that the new algorithm re- duces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature, respectively. These results indi- cate that the PLTL model checking technique em- ploying the new algorithm generates a smaller state space in verification of concurrent systems.展开更多
Chaos theory is used to prove that erratic and chaotic fluctuations can indeed arise in completely deterministic models. Chaos theory reveals structure in aperiodic, dynamic systems. A number of non-linear business cy...Chaos theory is used to prove that erratic and chaotic fluctuations can indeed arise in completely deterministic models. Chaos theory reveals structure in aperiodic, dynamic systems. A number of non-linear business cycle models use chaos theory to explain complex motion of the economy. Chaotic systems exhibit a sensitive dependence on initial conditions： Seemingly insignificant changes in the initial conditions produce large differences in outcomes. The basic aim of this analysis is to provide a relatively simple chaotic real-exchange-rate growth model that is capable of generating stable equilibria, cycles, or chaos.展开更多
Model uncertainty directly affects the accuracy of robust flutter and limit-cycle-oscillation (LCO) analysis. Using a data-based method, the bounds of an uncertain block-oriented aeroelastic system with nonlinearity a...Model uncertainty directly affects the accuracy of robust flutter and limit-cycle-oscillation (LCO) analysis. Using a data-based method, the bounds of an uncertain block-oriented aeroelastic system with nonlinearity are obtained in the time domain. Then robust LCO analysis of the identified model set is performed. First, the proper orthonormal basis is constructed based on the on-line dynamic poles of the aeroelastic system. Accordingly, the identification problem of uncertain model is converted to a nonlinear optimization of the upper and lower bounds for uncertain parameters estimation. By replacing the identified memoryless nonlinear operators by its related sinusoidal-input describing function, the Linear Fractional Transformation (LFT) technique is applied to the modeling process. Finally, the structured singular value(μ) method is applied to robust LCO analysis. An example of a two-degree wing section is carded out to validate the framework above. Results indicate that the dynamic characteristics and model uncertainties of the aeroelastic system can be depicted by the identified uncertain model set. The robust LCO magnitude of pitch angle for the identified uncertain model is lower than that of the nominal model at the same velocity. This method can be applied to robust flutter and LCO prediction.展开更多
The non-probabilistic approach to fatigue life analysis was studied using the convex models-interval, ellipsoidal and multiconvex models. The lower and upper bounds of the fatigue life were obtained by using the secon...The non-probabilistic approach to fatigue life analysis was studied using the convex models-interval, ellipsoidal and multiconvex models. The lower and upper bounds of the fatigue life were obtained by using the second-order Taylor series and Lagrange multiplier method. The solving process for derivatives of the implicit life function was presented. Moreover, a median ellipsoidal model was proposed which can take into account the sample blind zone and almost impossibility of concurrence of some small probability events. The Monte Carlo method for multi-convex model was presented, an important alternative when the analytical method does not work. A project example was given. The feasibility and rationality of the presented approach were verified. It is also revealed that the proposed method is conservative compared to the traditional probabilistic method, but it is a useful complement when it is difficult to obtain the accurate probability densities of parameters.展开更多
基金The first author of this paper would like to thank the follow- ing scholars, Prof. Joseph Sifakis, 2007 Turing Award Winner, for his invaluable help with my research and Dr. Kevin Lu at Brunel University, UK for his excellent suggestions on this paper. This work was supported by the National Natural Sci- ence Foundation of China under Grant No.61003079 the Chi- na Postdoctoral Science Foundation under Grant No. 2012M511588.
文摘To combat the well-known state-space explosion problem in Prop ositional Linear T emp o- ral Logic （PLTL） model checking, a novel algo- rithm capable of translating PLTL formulas into Nondeterministic Automata （NA） in an efficient way is proposed. The algorithm firstly transforms PLTL formulas into their non-free forms, then it further translates the non-free formulas into their Normal Forms （NFs）, next constructs Normal Form Graphs （NFGs） for NF formulas, and it fi- nally transforms NFGs into the NA which ac- cepts both finite words and int-mite words. The experimental data show that the new algorithm re- duces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature, respectively. These results indi- cate that the PLTL model checking technique em- ploying the new algorithm generates a smaller state space in verification of concurrent systems.
文摘Chaos theory is used to prove that erratic and chaotic fluctuations can indeed arise in completely deterministic models. Chaos theory reveals structure in aperiodic, dynamic systems. A number of non-linear business cycle models use chaos theory to explain complex motion of the economy. Chaotic systems exhibit a sensitive dependence on initial conditions： Seemingly insignificant changes in the initial conditions produce large differences in outcomes. The basic aim of this analysis is to provide a relatively simple chaotic real-exchange-rate growth model that is capable of generating stable equilibria, cycles, or chaos.
基金supported by the National Natural Science Foundation of China (Grant Nos. 90716006 and 10902006)Specialized Research Fund for the Doctoral Program of Higher Education (Grant No. 20091102110015)the Innovation Foundation of BUAA for PhD Graduates
文摘Model uncertainty directly affects the accuracy of robust flutter and limit-cycle-oscillation (LCO) analysis. Using a data-based method, the bounds of an uncertain block-oriented aeroelastic system with nonlinearity are obtained in the time domain. Then robust LCO analysis of the identified model set is performed. First, the proper orthonormal basis is constructed based on the on-line dynamic poles of the aeroelastic system. Accordingly, the identification problem of uncertain model is converted to a nonlinear optimization of the upper and lower bounds for uncertain parameters estimation. By replacing the identified memoryless nonlinear operators by its related sinusoidal-input describing function, the Linear Fractional Transformation (LFT) technique is applied to the modeling process. Finally, the structured singular value(μ) method is applied to robust LCO analysis. An example of a two-degree wing section is carded out to validate the framework above. Results indicate that the dynamic characteristics and model uncertainties of the aeroelastic system can be depicted by the identified uncertain model set. The robust LCO magnitude of pitch angle for the identified uncertain model is lower than that of the nominal model at the same velocity. This method can be applied to robust flutter and LCO prediction.
基金supported by the Program for New Century Excellent Talents in University of Chinathe Advanced Research Foundation of China (Grant No. 9140A27050109JB1112)
文摘The non-probabilistic approach to fatigue life analysis was studied using the convex models-interval, ellipsoidal and multiconvex models. The lower and upper bounds of the fatigue life were obtained by using the second-order Taylor series and Lagrange multiplier method. The solving process for derivatives of the implicit life function was presented. Moreover, a median ellipsoidal model was proposed which can take into account the sample blind zone and almost impossibility of concurrence of some small probability events. The Monte Carlo method for multi-convex model was presented, an important alternative when the analytical method does not work. A project example was given. The feasibility and rationality of the presented approach were verified. It is also revealed that the proposed method is conservative compared to the traditional probabilistic method, but it is a useful complement when it is difficult to obtain the accurate probability densities of parameters.
