CILinear:一个线性不变式自动构造工具

构造不变式是程序验证的重要组成部分,而开源工具Interproc能对简单的程序设计语言构造线性不变式。基于Interproc和C程序编译工具CIL,针对简化的C程序设计并实现了自动构造数值型程序变量线性不变式的工具CILinear,并与Interproc进行了比较。实验表明CILinear能有效地构造线性不变式,并且比Interproc支持的语法更多。通过实例讨论了CILinear在程序验证中的实际应用。

扩展线性时段不变式的模型检验研究进展

扩展线性时段不变式是时段演算中的一类重要公式.时段演算是周巢尘院士于20世纪90年代提出的一种用于嵌入式实时软件设计的演算系统,它开创性地将积分概念引入计算机实时软件的分析中,从而能够描述处理连续时间区间性质,是国际上公认的描述和分析实时系统的主流方法之一.由于时段演算内容丰富并且相关的综述和专著已出版,文章旨在对扩展线性时段不变式这一时段演算子集的模型检验问题的研究情况进行论述:①介绍时段演算、线性不变式及其扩展;②分别论述线性时段不变式以及扩展线性时段不变式的模型检验研究情况,其中重点介绍扩展的线性时段不变式,在离散时间语义和连续时间语义下的近期验证成果.

概率线性时段不变式的统计模型检验

模型检验是软件工程形式化方法的一个重要组成部分,线性时段不变式是形式化方法中表述系统性质的一种重要表达式。对线性时段不变式的模型检验一直是形式化方法研究的一个重要内容。该文提出了一种针对带概率的线性时段不变式的模型检验方法,该方法针对不带有不确定性的概率模型,运用统计模型检验的方法,基于UPPAAL工具实现了概率线性时段不变式的统计模型检验。

一类线性时段不变式的验证优化与实现

线性时段不变式是一类重要的时段演算公式。文献[1]中提出一种验证算法,能够针对以时间自动机建模的系统,模型检验其是否满足一个扩展的线性时段不变式。在验证一类特定公式时,该算法需要引入O(b)个辅助变量,且需全程保留它们的值,会导致检验这类公式所需的变量数和复杂度急剧增长。该文提出一种基于系统反转的模型检验方法。

反向验证带切变的线性时段不变式

线性时段不变式是一类重要的时段演算公式,可以用来描述实时系统的时段性质,对其验证算法的研究具有相当高的理论意义和实际应用价值。文献[3]中提出的算法在验证某些公式时需要引入O(b)个辅助变量,庞大的变量数目会限制该算法在实际工业领域的应用。针对该问题,本文提出了一种新颖的解决思路——通过反转原系统得到其反向系统,然后在反向系统上验证对应的反向公式。它与在原系统上验证正向公式的结果等价,但只需引入O(1)个辅助变量,扩大了文献[3]所提算法在实际工业领域的适用范围。

New criterion for delay-dependent absolute stability of Lurie system with interval time-varying delay

The delay-dependent absolute stability for a class of Lurie systems with interval time-varying delay is studied. By employing an augmented Lyapunov functional and combining a free-weighting matrix approach and the reciprocal convex technique, an improved stability condition is derived in terms of linear matrix inequalities （LMIs）. By retaining some useful terms that are usually ignored in the derivative of the Lyapunov function, the proposed sufficient condition depends not only on the lower and upper bounds of both the delay and its derivative, but it also depends on their differences, which has wider application fields than those of present results. Moreover, a new type of equality expression is developed to handle the sector bounds of the nonlinear function, which achieves fewer LMIs in the derived condition, compared with those based on the convex representation. Therefore, the proposed method is less conservative than the existing ones. Simulation examples are given to demonstrate the validity of the approach.

基于实时自动机的连续时段演算的验证

时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑。扩展线性时段不变式是时段演算的重要子集。针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法。该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题,从而可以采用量词消去技术进行求解。首先,运用符号化的思想,在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;然后,将每条符号化路径片段转化为一个量词线性算术公式;最后,利用量词消去工具求解。与已有工作相比,基于实时自动机设计了验证算法。另外,降低了验证复杂度,并且加速了验证过程的实际速度。

Compliant landing of a trotting quadruped robot based on hybrid motion/force robust control

A compliant landing strategy for a trotting quadruped robot on unknown rough terrains based on contact force control is presented. Firstly, in order to lower the disturbance caused by the landing impact force, a landing phase is added between the swing phase and the stance phase, where the desired contact force is set as a small positive constant. Secondly, the joint torque optimization of the stance legs is formulated as a quadratic programming(QP) problem subject to equality and inequality/bound constraints. And a primal-dual dynamical system solver based on linear variational inequalities(LVI) is applied to solve this QP problem. Furthermore, based on the optimization results, a hybrid motion/force robust controller is designed to realize the tracking of the contact force, while the constraints of the stance feet landing angles are fulfilled simultaneously. Finally, the experiments are performed to validate the proposed methods.

Sign-invariant and Explicit Solutions of Nonlinear Reaction-Diffusion Systems

Using the sign-invariant theory, we study the nonlinear reaction-diffusion systems. We also obtain some new explicit solutions to the nonlinear resulting systems.

Proximal Point-Like Method for Updating Simultaneously Mass and Stiffness Matrices of Finite Element Model

The problem of correcting simultaneously mass and stiffness matrices of finite element model of undamped structural systems using vibration tests is considered in this paper.The desired matrix properties,including satisfaction of the characteristic equation,symmetry,positive semidefiniteness and sparsity,are imposed as side constraints to form the optimal matrix pencil approximation problem.Using partial Lagrangian multipliers,we transform the nonlinearly constrained optimization problem into an equivalent matrix linear variational inequality,develop a proximal point-like method for solving the matrix linear variational inequality,and analyze its global convergence.Numerical results are included to illustrate the performance and application of the proposed method.

A novel stabilization approach for small signal disturbance of power system with time-varying delay

Small signal instability may cause severe accidents for power system if it can not be dear correctly and timely. How to maintain power system stable under small signal disturbance is a big challenge for power system operators and dispatchers. Time delay existing in signal transmission process makes the problem more complex. Conventional eigenvalue analysis method neglects time delay influence and can not precisely describe power system dynamic behaviors. In this work, a modified small signal stability model considering time varying delay influence was constructed and a new time delay controller was proposed to stabilize power system under disturbance. By Lyapunov-Krasovskii function, the control law in the form of nonlinear matrix inequality （NLMI） was derived. Considering synthesis method limitation for time delay controller at present, both parameter adjustment method by using linear matrix inequality （LMI） solver and iteration searching method by solving nonlinear minimization problem were suggested to design the controller. Simulation tests were carried out on synchronous-machine infinite-bus power system. Satisfactory test results verify the correctness of the proposed model and the feasibility of the stabilization approach.

Robust synchronization of uncertain complex systems with time-varying delays

Synchronization analysis and design problems for uncertain time-delayed high-order complex systems with dynamic output feedback synchronization protocols are investigated. By stating projection on the synchronization subspace and the complement synchronization subspace, synchronization problems are transformed into simultaneous stabilization problems of multiple subsystems related to eigenvalues of the Laplacian matrix of the interaction topology of a complex system. In terms of linear matrix inequalities(LMIs), sufficient conditions for robust synchronization are presented, which include only five LMI constraints.By the changing variable method, sufficient conditions for robust synchronization in terms of LMIs and matrix equalities are given,which can be checked by the cone complementarily linearization approach. The effectiveness of theoretical results is shown by numerical examples.

The Generalized KKM Map and Its Applications to Variational Inequalities

In this paper,applying the concept of generalized KKM map,we study problems of variational inequalities.We weaken convexity(concavity)conditions for a functional of two variables ■(x,y)in the general variational inequalities.Last,we show a proof of non-topological degree meth- od of acute angle principle about monotone operator as an application of these results.

SUSY QCD Impact on Top-Pair Production Associated with a Z^0-Boson at a Photon-Photon Collider

The top-pair production in association with a Z^0-boson at a photon-photon collider is an important process in probing the coupling between top-quarks and vector boson and discovering the signature of possible new physics. We describe the impact of the complete supersymmetric QCD （SQCD） next-to-leading order （NLO） radiative corrections on this process at a polarized or unpolarized photon collider, and make a comparison between the effects of the SQCD and the standard model （SM） QCD. We investigate the dependence of the lowest-order （LO） and QCD NLO corrected cross sections in both the SM and minimal supersymmetric standard model （MSSM） on colliding energy √s in different polarized photon collision modes. The LO, SM NLO, and SQCD NLO corrected distributions of the invariant mass of tt^--pair and the transverse momenta of final Z^0-boson are presented. Our numerical results show that the pure SQCD effects in γγ →tt^- Z^0 process can be more significant in the ＋＋ polarized photon collision mode than in other collision modes, and the relative SQCD radiative correction in unpolarized photon collision mode varies from 32.09% to -1.89% when √s goes up from 500 GeV to 1.5 TeV.

ON SUFFICIENT AND NECESSARY OF EXISTENCE FOR A CLASS OF SINGULAR OPTIMAL STOCHASTIC CONTROL

We study a class of discounted models of singular stochastic control. In thiskind of models, not only the structure of cost function has been extended to some general type, butalso the state can be represented as the solution of a class of stochastic differential equationswith nonlinear drift and diffusion term. By the various methods of stochastic analysis, we derivethe sufficient and necessary conditions of the existence of optimal control.

Stability control of steer by wire system based on μ synthesis robust control

The uncertainty influences may result in performance deterioration and instability to the steer by wire(SBW) system. Thus, it must make the control system keep robust stability from uncertainty, and have good robustness. In order to effectively restrain the interference and improve steering stability, this paper presents a μ synthesis robust controller based on SBW system, which considers the effect of model uncertainty and external disturbance on the system dynamics. Taking the ideal yaw rate tracking, interference suppression and excellent robustness as the control objectives, the μ synthesis robust controller is designed using linear fractional transformation theory to deal with the uncertainty. Then, it is testified through time domain and robustness simulation analysis. Simulation results show that the proposed controller can not only ensure robustness and robust stability of the system quite well, but improve handling stability of the vehicle effectively. The results of this study provide certain theoretical basis for the research and application of SBW system.

Gain-scheduling model predictive control for unmanned airship with LPV system description

This paper presents a gain-scheduling model predictive control(MPC) for linear parameter varying(LPV) systems subject to actuator saturation. The proposed gain-scheduling MPC algorithm is then applied to the lateral control of unmanned airship.The unmanned airship is modeled by an LPV-type system and transformed into a polytopic uncertain description with actuator saturation. By introducing a parameter-dependent state feedback law, the set invariance condition of the polytopic uncertain system is identified. Based on the invariant set, the gain-scheduling MPC controller is presented by solving a linear matrix inequality(LMI) optimization problem. The proposed gain-scheduling MPC algorithm is demonstrated by simulating on the unmanned airship system.

AN INTEGRO-DIFFERENTIAL PARABOLIC VARIATIONAL INEQUALITY ARISING FROM THE VALUATION OF DOUBLE BARRIER AMERICAN OPTION

This paper studies the nonlinear variational inequality with integro-differential term arising from valuation of American style double barrier option. First, the authors use the penalty method to transform the variational inequality into a nonlinear parabolic initial boundary problem(i.e., penalty problem). Second, the existence and uniqueness of solution to the penalty problem are proved by using the Scheafer fixed point theory. Third, the authors prove the existence of variational inequality' solution by showing the fact that the penalized PDE converges to the variational inequality. The uniqueness of solution to the variational inequality is also proved by contradiction.

Rosenthal's inequalities for independent and negatively dependent random variables under sub-linear expectations with applications

Classical Kolmogorov's and Rosenthal's inequalities for the maximum partial sums of random variables are basic tools for studying the strong laws of large numbers.In this paper,motived by the notion of independent and identically distributed random variables under the sub-linear expectation initiated by Peng(2008),we introduce the concept of negative dependence of random variables and establish Kolmogorov's and Rosenthal's inequalities for the maximum partial sums of negatively dependent random variables under the sub-linear expectations.As an application,we show that Kolmogorov's strong law of larger numbers holds for independent and identically distributed random variables under a continuous sub-linear expectation if and only if the corresponding Choquet integral is finite.

New Stability Criteria for High-Order Neural Networks with Proportional Delays

This paper is concerned with high-order neural networks with proportional delays. The proportional delay is a time-varying unbounded delay which is different from the constant delay, bounded time-varying delay and distributed delay. By the nonlinear transformation yi(t) = ui( et)(i = 1, 2,..., n), we transform a class of high-order neural networks with proportional delays into a class of high-order neural networks with constant delays and timevarying coefficients. With the aid of Brouwer fixed point theorem and constructing the delay differential inequality, we obtain some delay-independent and delay-dependent sufficient conditions to ensure the existence, uniqueness and global exponential stability of equilibrium of the network. Two examples with their simulations are given to illustrate the theoretical findings. Our results are new and complement previously known results.