On invariant checking

Checking whether a given formula is an invariant at a given program location (especially, inside a loop) can be quite nontrivial even for simple loop programs, given that it is in general an undecidable property. This is especially the case if the given formula is not an inductive loop invariant, as most automated techniques can only check or generate inductive loop invariants. In this paper, conditions are identified on simple loops and formulas when this check can be performed automatically. A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a loop. As a byproduct of this analysis, a new kind of loop invariant inside the loop body, called inside-loop invariant, is proposed. Such an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program verification. The use of such invariants for program debugging is explored; it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow, accessing array/collection data structures outside the range, divide by zero, etc.     

Comprehensive G?bner Basis Theory for a Parametric Polynomial Ideal and the Associated Completion Algorithm

Gr?bner basis theory for parametric polynomial ideals is explored with the main objective of mimicking the Gr?bner basis theory for ideals. Given a parametric polynomial ideal, its basis is a comprehensive Gr?bner basis if and only if for every specialization of its parameters in a given field, the specialization of the basis is a Gr?bner basis of the associated specialized polynomial ideal.For various specializations of parameters, structure of specialized ideals becomes qualitatively different even though there are significant relationships as well because of finiteness properties. Key concepts foundational to Gr?bner basis theory are reexamined and/or further developed for the parametric case:(i) Definition of a comprehensive Gr?bner basis,(ii) test for a comprehensive Gr?bner basis,(iii) parameterized rewriting,(iv) S-polynomials among parametric polynomials,(v) completion algorithm for directly computing a comprehensive Gr?bner basis from a given basis of a parametric ideal. Elegant properties of Gr?bner bases in the classical ideal theory, such as for a fixed admissible term ordering,a unique Gr?bner basis can be associated with every polynomial ideal as well as that such a basis can be computed from any Gr?bner basis of an ideal, turn out to be a major challenge to generalize for parametric ideals; issues related to these investigations are explored. A prototype implementation of the algorithm has been successfully tried on many examples from the literature.     

切向加速度与弦误差约束的CNC系统时间最优轨迹规划

针对计算机数控(CNC)系统给定参数化路径, 给出了一种求解时间最优轨迹规划问题的凸优化方法. 轨迹规划问题考虑切向加速度约束与弦误差约束. 通过建立两种约束下的状态容许空间, 分析约束对时间最优轨迹的影响. 通过非线性变量代换, 时间最优轨迹规划问题被表述为一个与时间无关的凸最优控制问题. 基于控制向量参数化(CVP)方法, 问题被进一步转化为易于求解的凸优化问题. 以路径参数对时间的二阶导数(参数加速度)为优化变量, 序列二次规划(SQP)方法获得问题数值解. 文末通过求解两个测试路径的时间最优轨迹规划问题, 验证方法的有效性.     

线性系统有限时间函数观测器设计的参数化方法

研究了线性系统有限时间函数观测器的参数化设计问题,其目的是通过设计参数化形式的函数观测器,使其在给定有限时间内能够直接估计关于线性系统状态的线性函数。基于一类Sylvester矩阵方程的参数化解,给出了该有限时间函数观测器所有增益矩阵的参数化表达式,其所含的自由参数为控制系统设计提供了全部的自由度,可通过适当选择这些自由参数使其满足某些系统性能指标。最后,数值例子及其仿真结果验证了所提线性系统有限时间函数观测器参数化设计方法的简单性和有效性。     

Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm

Gröbner basis theory for parametric polynomial ideals is explored with the main objective of mimicking the Gröbner basis theory for ideals. Given a parametric polynomial ideal, its basis is a comprehensive Gröbner basis if and only if for every specialization of its parameters in a given field, the specialization of the basis is a Gröbner basis of the associated specialized polynomial ideal. For various specializations of parameters, structure of specialized ideals becomes qualitatively different even though there are significant relationships as well because of finiteness properties. Key concepts foundational to Gröbner basis theory are reexamined and/or further developed for the parametric case: (i) Definition of a comprehensive Gröbner basis, (ii) test for a comprehensive Gröbner basis, (iii) parameterized rewriting, (iv) S-polynomials among parametric polynomials, (v) completion algorithm for directly computing a comprehensive Gröbner basis from a given basis of a parametric ideal. Elegant properties of Gröbner bases in the classical ideal theory, such as for a fixed admissible term ordering, a unique Gröbner basis can be associated with every polynomial ideal as well as that such a basis can be computed from any Gröbner basis of an ideal, turn out to be a major challenge to generalize for parametric ideals; issues related to these investigations are explored. A prototype implementation of the algorithm has been successfully tried on many examples from the literature.     

固体火箭主动段终端多约束能量管理制导方法

针对不同高度的单箭多轨道运载任务,提出了一种多级固体火箭上升段分步满足终端多约束的能量管理制导方法。火箭前期飞行通过程序指令控制基准弹道,以满足期望的高度与当地弹道倾角约束为目的将弹道优化转参数优化问题处理,减少了约束条件；后期飞行通过姿态交变机动的闭路能量管理制导方法,耗散多余能量控制飞行速度,达到了满足终端速度、高度、倾角等多约束条件的火箭不同高度入轨。仿真结果表明,该能量管理制导方法有效可行且在不同轨道运载任务中具有较好的适用性。     

一类非线性参数化系统的自适应学习控制

针对控制增益是未知时变的并含有混合未知参数的非线性参数化系统,利用将整个区间分段与反馈线性化相结合,提出了一种新的自适应学习控制方法。该方法可以处理参数在一个未知紧集内周期性快时变的非线性系统。通过引进新颖的微分-差分混合型参数自适应律,使广义跟踪误差在误差平方范数意义下渐近收敛于零。通过构造Lyapunov泛函,给出了广义跟踪误差收敛的充分条件。实例仿真结果说明了该方法的可行性和有效性。     

植物果实的几何造型及可视化研究

提出了一种基于曲面参数方程的植物果实的造型方法。该方法使用凹凸纹理处理方式对椭球面参数方程进行变形,模拟各种不同形状植物果实形状;利用正弦函数的变化规律对植物表面颜色纹理进行模拟。给出了仿真水果模型的实例,模型的可控参数较少,变换灵活,形象直观,易于构建虚拟植物果实的生长模型。     

Profile Statistical Inference for Partially Linear Additive Models with a Diverging Number of Parameters

This paper considers partially linear additive models with the number of parameters diverging when some linear constraints on the parametric part are available. This paper proposes a constrained profile least-squares estimation for the parametric components with the nonparametric functions being estimated by basis function approximations. The consistency and asymptotic normality of the restricted estimator are given under some certain conditions. The authors construct a profile likelihood ratio test statistic to test the validity of the linear constraints on the parametric components,and demonstrate that it follows asymptotically chi-squared distribution under the null and alternative hypotheses. The finite sample performance of the proposed method is illustrated by simulation studies and a data analysis.     

基于扩展时间影响网络的作战任务效能计算方法

由于战场环境的复杂性,作战任务与作战目标间通常存在动态不确定的因果影响关系。目前,传统的解析模型及作战模拟方法在计算作战任务效能时,存在因果建模能力不足,运行效率低下的问题。通过引入时间影响网络,并利用循环弧和强度参数扩展其时间约束,进一步表达了作战行动间异步和同步关系,提出了一种基于扩展时间影响网络的作战任务效能计算方法。在一定作战想定背景下,结合登岛作战任务示例验证了该方法的可行性和有效性。     

Synchronized path following control of multiple homogenous underactuated AUVs

This paper addresses the problem of synchronized path following of multiple homogenous underactuated autonomous underwater vehicles(AUVs).The dedicated control laws are categorized into two envelopes:One is steering individual underwater vehicle to track along predefined path,and the other is ensuring tracked paths of multiple vehicles to be synchronized,by means of decentralized speed adaption under the constraints of multi-vehicle communication topology.With these two tasks formulation,geometric path following is built on Lyapunov theory and backstepping techniques,while injecting helmsman behavior into classic individual path following control.Synchronization of path parameters are reached by using a mixture of tools from linear algebra,graph theory and nonlinear control theory.A simple but effective control design on direct inter-vehicle speed adaption with min- imized communication variables,enables the multi-AUV systems to be synchronized and stabilized into an invariant manifold,and all speeds converge to desired assignments as a byproduct.Simulation results illustrate the performance of the synchronized path following control laws proposed.     

基于物理的植物器官实时变形模拟

近年来,各种方法被用来模拟可变形物体的实时变形。提出了一种基于质点-弹簧系统的植物器官变形模拟方法,并根据交互式设计的要求开发了参数化的植物器官几何造型和弹簧模型生成方法,简化了质点-弹簧模型的构造。实验结果表明,该方法能够获得具有较高真实感的变形效果,能够适用于多种植物器官一般情况下的变形模拟;同时,参数化的几何曲面和物理模型生成能够满足于交互式实时模拟的需要。     

Design of Luenberger function observer with disturbance decoupling for matrix second-order linear systems-a parametric approach

1.INTRODUCTIONThere have been many approaches to disturbance de-couplinginlinear multivariable control systemdesign.Linnemann[1]proposed a numerically stable algorithmfor disturbance decoupling by measurement feedback.Van Der Woude[2]considered the combined problemof disturbance decoupling and stabilization by mea-surement feedback.Syrmos[3]proposed a numericallyefficient algorithm based on Sylvester equations forthe problemof disturbance decoupling with arbitrarypole placement usingstat…     

一种脉冲多普勒雷达解速度模糊新方法

速度模糊是脉冲多普勒雷达中的一个重要问题。在没有别的信息源情况下,需要用雷达测得的距离信息来解速度模糊,因为距离回路输出与速度回路输出代表同一个目标的距离和径向速度,它们之间存在确定关系。推导最小二乘法解速度模糊的方法,提出一种新的不变量嵌入法解速度模糊的方法。通过理论分析和仿真证明不变量嵌入法可以有效地解速度模糊,并且实质上就是最小二乘法,其在提高距离精度上等效于测距、测速回路构成的复合控制系统。     

QoS multicast routing algorithm based on GA

1 .INTRODUCTIONTheprovisionofquality of service (QoS) guaranteesisofutmostimportanceforthedevelopmentofthemulticastservices .Multicastroutinghascontinuedtobeaveryimportantresearchissueintheareasofnet worksanddistributedsystems.Ithasattractedtheinterestsof…     

参数效应的仿真与反馈环及延迟三组合分析法——以场供给侧改革为例

规划落实、政策执行、措施实施皆是通过参数调控系统相关发展速度实现,为此进行参数调控流率效应方法研究.调控流率效应研究必须建立参数调控的可靠性高的模型,必须进行仿真、反馈环、延迟3组合分析,才可能具体清楚回答运行中的问题,实际应用需要,查文献还未见此种三组合分析法,为此,进行"参数调控流率入树建模和仿真、反馈环、延迟三组合分析法"研究.顶天立地,通过南昌大学系统工程科研教学基地明鑫农场供给侧改革,生产雷竹笋、有机鱼、有机生猪特色农产品系统实例,阐述此"三组合分析法".首先基于逐树设撤关联数结构行为检验法,建立场的8参数调控的8棵流率基本入树可靠性高的模型.接着,依据实际分析与场规划,分别确定8参数的调控区间,设参数的调控区间最小值组合为最不满意方案,区间最大值组合为最满意方案,对两方案进行参数调控效应仿真分析.随后,建立8阶参数枝向量行列式计算反馈环,获12条参数调控反馈环.接着,分别围绕雷竹笋产业、有机鱼产业和开发青饲料发展有机猪促进圈养猪转型3个子系统的6条反馈环分别进行反馈环结构图、反馈环正负极性、延迟阶数确定研究后,进行仿真、反馈环、延迟3结合具体分析结果,然后,依据3结合的具体分析和反馈环、延迟原理,提出了供给侧改革的操作性强的管理思路与技术.通过研究,建立了实际背景强的"参数调控入树流率建模和仿真、反馈环、延迟三组合分析"新方法.     

基于抖动的CAN型网络带宽优化调度

合理调配有限的带宽资源，尽可能地降低网络对系统性能的影响，以满足控制系统动态性能和实时性的要求是网络化控制领域亟须解决的关键问题。结合CAN网的运行特性，提出基于抖动的带宽优化调度算法。在满足控制系统动态性能和网络可调度性条件下，确定网络化控制系统中各控制闭环的最优采样周期和初相，在兼顾周期抖动对控制闭环动态性能影响的同时合理地调配带宽资源，使系统具有较高的带宽资源利用率。     

Elevation estimation for low-angle target based on reflection paths suppression

In the signal processing for metrewave radar, the reflection paths of target echoes can cause severe error in the elevation estimation for the low-angle target tracking. The exact angles of the reflection paths are unknown beforehand, and therefore, the reflection paths can not be suppressed easily. Therefore, in this article, an improved reflection paths suppression approach is presented. A block matrix aggregate is constructed based on the possible angles of the reflection paths. Combined with the beamforming-like processing, a generalized maximum likelihood estimation is derived to optimize the estimation. Moreover, the noise reduction method based on the Toeplitz covariance matrix is used for better performance. This approach is applied to the real data collected by the low-angle tracking radar with 8-channel vertical array. The experiment results show that the reflection effects are reduced and the accuracy of the elevation estimate is improved.     

通用系统仿真工具GSST

本文描述了通用系统仿真工具ＧＳＳＴ的原理和组织结构。ＧＳＳＴ可从结构、行为、功能三方面描述仿真对象，系统建模及仿真过程同时考虑对象中的定性约束和定量关系。对仿真得到的观测数据可进一步进行定性解释和归纳解释处理，以得到直观、便于理解的结果。     

Finding Efficient Solutions for Multiobjective Decision Making

ＦｉｎｄｉｎｇＥｆｆｉｃｉｅｎｔＳｏｌｕｔｉｏｎｓｆｏｒＭｕｌｔｉｏｂｊｅｃｔｉｖｅＤｅｃｉｓｉｏｎＭａｋｉｎｇ￥ＬＩＢｏ（ＳｅｃｔｉｏｎｏｆＭａｔｈｅｍａｔｉｃｓＳｈａｎｄｏｎｇＩｎｓｔ．ｏｆＢｌｄｇ．ＭａｔｅｒｉａｌｓＪｉｎａｎ，２５００２２）Ａ...