以DNA为载体的线性时序逻辑模型检测

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)为载体对线性时序逻辑(Linear Temporal Logic,LTL)实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.     

PSL的有界模型检验

 基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.     

模糊线性时序逻辑的可实现性

模糊线性时序逻辑（fuzzy linear temporal logic）被应用于刻画模糊系统的规范语言,其可实现性（realizability）用于判断满足该时序逻辑公式的开放系统模型是否存在.模糊线性时序逻辑可实现性和系统合成（synthesis）的基本思想是：给定模糊线性时序逻辑公式,判断是否存在满足该公式的系统.如果存在,则构造满足该公式的最优系统.为了检验模糊线性时序逻辑的可实现性,首先引入模糊Büchi博弈的定义,作为检验模糊线性时序逻辑公式是否可实现的模型.其次通过归约的方法,研究模糊Büchi博弈的性质（最优无记忆策略存在性.最后验证模糊线性时序逻辑的可实现性并且给出其系统合成的过程,并说明它们的时间复杂度.     

线性逆问题求解的多尺度降阶模型

基于相对误差协方差矩阵信息,该文给出线性逆问题求解的多尺度降阶模型,把高阶模型的求解问题转化为一个近似的低阶模型再进行求解．利用该降阶模型可以得到与完全模型相当的估计效果,同时又能大大降低逆算法的计算量,从而有效地解决逆问题求解中计算复杂度过高的难题,增强逆问题求解算法的可实施性,采用降阶模型进行求解还可以增加那些提供显著信息的点的估计精度。     

广义可能性计算树逻辑的模型检测问题

本文首先分别给出了"约束可达","总是可达"这两个公式在广义可能性计算树逻辑（GPoCTL）中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPoCTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPoCTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPoCTL模型检测问题的计算复杂度,得到了与上面相似的结论.     

区域指导的彩色图像插值

本文提出了一种针对彩色图像的区域指导的插值算法.该方法首先从低分辨率图像中计算象素沿梯度方向的1、2阶方向导数,然后把彩色图像划分为常数、线性和非线性区域,并对不同的区域施用不同复杂度的滤波器.实验结果表明,与传统的双线性插值相比,该方法可以明显改进插值图像的质量;重建所需的时间也比单纯使用复杂滤波器的时间减少很多,并且可以实现彩色图像的任意放大.     

p元扩域上的快速乘法

基于剩余算术理论构造了一类F_p[x]上的项式PAPB,给出了该型不可约多项式的存在数量估计;然后,利用剩余算术和中国剩余定理,提出了一种模PAPB乘法的快速实现算法;最后给出结果分析.理论和实验结果表明,在一定条件下,给出算法的计算复杂度仅有O(k~(1.5)),优于常用模二项式乘法O(k~2)的计算复杂度.因此,该类多项式在最优扩域和椭圆曲线算法中有较好的应用前景.     

基于频域插值的信道化原型滤波器设计

针对信道化原型滤波器设计复杂度较高的问题,提出一种满足线性相位要求的原型滤波器频域插值设计算法。该算法采用无约束迭代优化办法获得了阻带衰减较高的低阶滤波器模型,然后根据所推导的频域插值模型构建满足线性相位特性的原型滤波器频谱,最后通过快速傅里叶逆变换获得了满足信道化滤波器组完全重构特性要求的原型滤波器。所提设计算法将频域插值与迭代优化相结合,有效地解决了设计高阻带衰减的原型滤波器时待优化参数数目较大的问题,并且不会产生镜像频谱,省去了镜像抑制滤波器的设计。仿真结果表明,所提算法相比传统的时域插值设计算法具有显著的性能改善,并且降低了设计复杂度。     

基于FRFT的多LFM信号的分离及参数估计

线性调频（LFM）信号在某个阶次的FRFT域中具有能量聚集性,根据这一特性采用分数阶傅里叶变换（FRFT,Fractional Fourier Transform）来分离多个未知任何先验参数的LFM信号,通过在FRFT域搜索峰值点来检测并分离出LFM信号,并用相关系数对分离效果进行了评价。针对二维搜索峰值点的计算复杂性,提出了曲线拟合优化技术来进行FRFT模值检测,把二维搜索转化为一维曲线拟合问题,并介绍了高斯混合模型近似FRFT模值分布。计算机仿真表明,这一方法极大地降低了计算复杂度,对多分量LFM信号进行了有效的分离及参数估计。     

基于自动机的围线树生成与Euler数的计算

利用边界自动机跟踪图像所有区域边界,在自动机跟踪所有边界的同时生成围线的树结构,并基于围线的树结构给出了Euler数的计算方法.跟踪算法复杂度是线性的,能跟踪任意复杂图像区域.计算Euler数的算法不仅适用于整幅图像,而且适用于局部图像.     

具有模糊时态的广义可能性线性时序逻辑的模型检测

本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL（Generalized Possibilistic Fuzzy Linear Tempora Logic）的语构以及基于路径和基于语言的两种语义解释,证明了GPoFLTL在模糊时态方面对GPoLTL（Generalized Possibilistic Linear Tempora Logic）进行了扩张,并通过实例说明了GPoFLTL比GPoLTL具有更强的表达能力;其次在广义可能性测度下通过模糊矩阵运算讨论了"不久","几乎总是"等几类模糊时态性质的模型检测问题;最后研究了模糊时态性质的必要性阈值模型检测问题,给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.     

Invisible formal methods for embedded control systems

Embedded control systems typically comprise continuous control laws combined with discrete mode logic. These systems are modeled using a hybrid automaton formalism, which is obtained by combining the discrete transition system formalism with continuous dynamical systems. This paper develops automated analysis techniques for asserting correctness of hybrid system designs. Our approach is based on symbolic representation of the state space of the system using mathematical formulas in an appropriate logic. Such formulas are manipulated using symbolic theorem proving techniques. It is important that formal analysis should be unobtrusive and acceptable to engineering practice. We motivate a methodology called invisible formal methods that provides a graded sequence of formal analysis technologies ranging from extended typechecking, through approximation and abstraction, to model checking and theorem proving. As an instance of invisible formal methods, we describe techniques to check inductive invariants, or extended types, for hybrid systems and compute discrete finite state abstractions automatically to perform reachability set computation. The abstract system is sound with respect to the formal semantics of hybrid automata. We also discuss techniques for performing analysis on nonstandard semantics of hybrid automata. We also briefly discuss the problem of translating models in Simulink/Stateflow language, which is widely used in practice, into the modeling formalisms, like hybrid automata, for which analysis tools are being developed.     

精确学习模型下确定的有穷自动机的学习

利用多态自动机和有穷自动机的关系，根据多态自动机的学习算法，给出了EXACT学习模型下，确定的有穷自动机的学习算法，并对算法复杂度做了分析，说明确定的有穷自动机在EXACT模型下可以在多项式时间内进行学习。这样就可以用软件来模拟确定的有穷自动机的学习。     

基于启发式SCCs的广义Büchi 自动机判空检测算法

 基于自动机理论模型检测的一个关键算法是判断有穷状态系统是否满足属性的判空检测.对标准Büchi自动机作判空检测,容易引起状态爆炸.本文以TGBA为研究对象,提出基于启发式SCCs的广义Büchi自动机判空检测算法.该算法在on-the-fly算法的基础上结合启发式深度优先搜索和SCCs检测算法,能较快地判断TGBA的非空性.通过正确性证明、复杂性分析和实验验证了该算法的正确可行性.在TGBA非空的情况下,该算法的时空性能比已有算法更优.     

相控阵天线的互耦和近场校准

本文在分析相控阵天线近场特性的基础上,根据信号子空间的基本理论,结合模拟退火算法,提出了一种利用近场辅助源估计相控阵天线互耦系数的方法.大量的计算机仿真结果表明,本方法使用校准源少,校准源到天线阵距离近,算法稳健,即使在雷达工作、并且存在其它未知信号时,也能准确估计出天线阵的互耦系数.     

用于电磁波多尺度问题求解的高效FDTD-PITD混合算法北大核心CSCD

针对电磁波多尺度问题的高效仿真需求,提出了基于亚网格技术的时域有限差分(FDTD)方法与时域精细积分(PITD)方法的混合数值算法。该混合算法的基本思想是采用局部亚网格技术分别对精细结构区域以及其他区域进行剖分,并应用FDTD方法和PITD方法分别对粗网格区域与细网格区域进行求解,同时构建信息交互策略交换细网格区域与粗网格区域的计算信息。一方面该方法减少了电磁波多尺度问题的网格剖分数目,显著降低了内存需求;另一方面由于应用于细网格区域的PITD方法不受Courant-Friedrich-Levy(CFL)数值稳定性条件的限制,该混合方法能够采用较大的时间步长进行仿真,减少了迭代步数以及CPU执行时间。数值计算结果验证了混合算法的稳定性、可行性以及高效性。     

New edge-directed interpolation

This paper proposes an edge-directed interpolation algorithm for natural images. The basic idea is to first estimate local covariance coefficients from a low-resolution image and then use these covariance estimates to adapt the interpolation at a higher resolution based on the geometric duality between the low-resolution covariance and the high-resolution covariance. The edge-directed property of covariance-based adaptation attributes to its capability of tuning the interpolation coefficients to match an arbitrarily oriented step edge. A hybrid approach of switching between bilinear interpolation and covariance-based adaptive interpolation is proposed to reduce the overall computational complexity. Two important applications of the new interpolation algorithm are studied: resolution enhancement of grayscale images and reconstruction of color images from CCD samples. Simulation results demonstrate that our new interpolation algorithm substantially improves the subjective quality of the interpolated images over conventional linear interpolation.     

A fast algorithm for optimal linear interpolation

A fast algorithm for computing the optimal linear interpolation filter is developed. The algorithm is based on the Sherman-Morrison inversion formula for symmetric matrices. The relationship between the derived algorithm and the Levinson algorithm is illustrated. It is shown that the new algorithm, in comparison with the well-known algorithms, requires fewer multiplications and hence is of lower complexity