有界闭域上的线性赋值循环终止性分析

对有界闭域上的线性赋值循环程序终止性问题进行研究.利用Jordan 标准型技术将原循环程序的终止性问题约减为终止性等价的具有简单结构的循环程序的终止性问题.证明了当线性迭代映射满足一定条件时,该类循环程序不可终止的充分必要条件是：迭代映射在有界闭域上有不动点或周期轨.     

单分支线性约束循环程序的终止性分析

秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.     

非线性循环的终止性分析

单重线性循环程序的终止性问题已被广泛研究,而有关非线性循环终止性判定的结果甚少.利用不动点理论研究了n维单重非线性循环的终止性问题,并建立了相应的符号判定算法,同时,对几类特殊循环的终止性进行了分析,得出了相应的结论.     

一类线性循环程序的终止性判定

提出一种判定这类线性循环程序是否终止的新方法,该方法通过分析循环变量每次迭代后的状态.最后得到循环条件的满足与否只是与变量的初始值和迭代的次数有关.从而判断该循环程序是否终止.根据该方法,不但能判断这一类程序是否终止.对于不是对所有输入都终止的程序,还能够给出程序终止的输入条件.     

有界闭连通域上的非线性循环终止性分析

运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法. 该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.     

有界闭区间并上的非线性循环程序的终止性验证

利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法.利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性.最后,给出计算实例演示该算法的算法步骤.     

循环条件的形式化推导在程序验证中的应用

提出了一种求解命令式程序中循环执行和终止条件的方法.该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导.现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序.提出的形式化方法可以在一个原型工具中实现,通过该工具来推导循环执行和终止条件,辅助程序验证和程序缺陷修正.     

基于SVM的多项式循环程序秩函数生成

程序终止性问题是自动程序验证领域中的一个研究热点.秩函数探测是进行终止性分析的主要方法.针对单重无条件分支的多项式循环程序,将其秩函数计算问题归结为二分类问题,从而可利用支持向量机（SVM）算法来计算程序的秩函数.与基于量词消去技术的秩函数计算方法不同,该方法能在可接受的时间范围内探测到更为复杂的秩函数.     

非线性循环的终止性分析?

单重线性循环程序的终止性问题已被广泛研究,而有关非线性循环终止性判定的结果甚少。利用不动点理论研究了n维单重非线性循环的终止性问题,并建立了相应的符号判定算法。同时,对几类特殊循环的终止性进行了分析,得出了相应的结论。     

多项式循环程序的秩函数探测

秩函数法是循环程序终止性分析的主流方法.针对一类多分支多项式循环程序,这类程序的秩函数计算问题被证明可归结为单形上正定多项式的探测问题,从而便于利用线性规划工具Simplex去计算这类程序的秩函数.不同于现有基于柱形代数分解的量词消去算法,该方法能够在可接受的时间内计算更为复杂的多项式秩函数.     

Influence of noise on wave boundary recognition by ECG measurement programs. Recommendations for preprocessing

In the international cooperative project entitled "Common Standards for Quantitative Electrocardiography" (CSE) systematic noise tests have been performed in order to compare measurement results of electrocardiographic computer programs under degraded operational conditions and to develop recommendations for preprocessing and measurement strategies. The influence of seven different high- and low-frequency noise types on the recognition of P, QRS, and T wave onsets and offsets was investigated. The analysis was performed on 160 electrocardiograms derived from two sets of 10 cases each, by eight electrocardiographic and six vectorcardiographic computer programs. The stability and precision of these programs were tested with respect to the results obtained (1) in the noise-free recordings and (2) by a group of five cardiologists who have analyzed the recordings previously in a Delphi reviewing process. Increasing levels of high-frequency noise shifted the onsets and offsets of most programs outward. Programs analyzing an averaged beat showed significantly less variability than programs which measure every complex or a selected beat. On the basis of the findings of the present study, a measurement strategy based on selective averaging is recommended for diagnostic ECG computer programs. However, averaging should be performed only if proper alignment and precise waveform comparison have been performed beforehand in order to exclude dissimilar complexes.     

Null-controllability of non-linear infinite delay systems with restrained controls

Sufficient conditions are developed for the null-controllability of non-linear infinite delay systems with restrained controls. If the uncontrolled system is uniformly asymptotically stable and if the linear control system is proper, then the non-linear infinite delay system is null-controllable under certain conditions.     

一般广义对象的严格真H∞控制器设计

考虑一般广义对象的严格真H∞控制器设计问题.基于线性矩阵不等式(LMI)方法, 指出严格真H∞控制器存在当且仅当H∞控制问题可解,并满足一个静态条件,最后提出了一 个基于LMI的严格真H∞控制器的设计方法.     

Stable inference as intuitionistic validity

The paper characterises the nonmonotonic inference relation associated with the stable model semantics for logic programs as follows: a formula is entailed by a program in the stable model semantics if and only if it belongs to every intuitionistically complete and consistent extension of the program formed by adding only negated atoms. In place of intuitionistic logic, any proper intermediate logic can be used.     

Strong equivalence of logic programs under the infinite-valued semantics

We consider the notion of strong equivalence [V. Lifschitz, D. Pearce, A. Valverde, Strongly equivalent logic programs, ACM Transactions on Computational Logic 2 (4) (2001) 526-541] of normal propositional logic programs under the infinite-valued semantics [P. Rondogiannis, W.W. Wadge, Minimum model semantics for logic programs with negation-as-failure, ACM Transactions on Computational Logic 6 (2) (2005) 441-467] (which is a purely model-theoretic semantics that is compatible with the well-founded one). We demonstrate that two such programs are strongly equivalent under the infinite-valued semantics if and only if they are logically equivalent in the corresponding infinite-valued logic. In particular, we show that strong equivalence of normal propositional logic programs is decidable, and more specifically coNP-complete. Our results have a direct implication for the well-founded semantics since, as we demonstrate, if two programs are strongly equivalent under the infinite-valued semantics, then they are also strongly equivalent under the well-founded semantics.     

A minimal property for characterizing deadlock-free programs

A fundamental issue in the development of concurrent programs is the resource allocation problem. Roughly speaking, it consists of providing some mechanism to avoid race conditions in the access of shared resources by two or more concurrent processes. For such a task, maybe the most widely mechanism consists of using critical sections.Unfortunately, it is also widely-known that programs which use several critical sections may suffer from deadlocks. In this paper, we identify a program property, namely, being stopper-free, which can be used to know if programs are deadlock-free. Indeed, since we have proved that programs are deadlock-free if and only if they do not have any stopper, thus looking for a stopper is equivalent to identifying a situation where a program may suffer a deadlock.     

基于Snake模型的快速目标检测算法的研究与仿真

该文提出了一种基于Snake模型的快速目标检测算法，可以实现图象全空域有效搜索。为了能够在实时图象处理系统中获得应用，该算法主要针对简单离散Snake模型进行改进。利用图象区域分割，并设置适当的目标判别方法，经有限次迭代之后能够有效地收敛到目标，并且对处于相邻图象块中的同一目标能进行自动合并。仿真结果表明：该算法即使在目标与背景的对比度很低的情况下也能有效地检测到目标。     

Passive and Conservative Continuous-Time Impedance and Scattering Systems. Part I: Well-Posed Systems

 Let U be a Hilbert space. By an ℒ (U)-valued positive analytic function on the open right half-plane we mean an analytic function which satisfies the condition . This function need not be proper, i.e., it need not be bounded on any right half-plane. We study the question under what conditions such a function can be realized as the transfer function of an impedance passive system. By this we mean a continuous-time state space system whose control and observation operators are not more unbounded than the (main) semigroup generator of the system, and, in addition, there is a certain energy inequality relating the absorbed energy and the internal energy. The system is (impedance) energy preserving if this energy inequality is an equality, and it is conservative if both the system and its dual are energy preserving. A typical example of an impedance conservative system is a system of hyperbolic type with collocated sensors and actuators. We give several equivalent sets of conditions which characterize when a system is impedance passive, energy preserving, or conservative. We prove that a impedance passive system is well-posed if and only if it is proper. We furthermore show that the so-called diagonal transform (which may be regarded as a slightly modified feedback transform) maps a proper impedance passive (or energy preserving or conservative) system into a (well-posed) scattering passive (or energy preserving or conservative) system. This implies that, just as in the finite-dimensional case, if we apply negative output feedback to a proper impedance passive system, then the resulting system is (energy) stable. Finally, we show that every proper positive analytic function on the right half-plane has a (essentially unique) well-posed impedance conservative realization, and it also has a minimal impedance passive realization. Date received: October 22, 2001. Date revised: May 13, 2002.     

Some symmetry results for optimal solutions in structural optimization

In the present paper, some symmetry results for optimal solutions in structural optimization have been proposed and proven. It is found that under some invariant assumptions, for many structural optimization problems that can be formulated as convex programs, there exists at least one symmetric global optimal solution if the prescribed loading and support conditions are symmetric. Furthermore, for some specific non-convex cases, a weaker result is also presented.