不可满足公式的同态证明系统

合取范式(CNF)公式H到F的同态φ是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.     

k-LSAT (k≥3)是NP-完全的

合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF_≥k是子句长度大于或等于k的CNF公式子类,判定问题LSA(≥k)的NP-完全性与LCNF(≥k)中是否含有不可满足公式密切相关.即LSAT_≥k的NP-完全性取决于LCNF_≥k是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF_≥3和LCNF_≥4中的不可满足公式,并提出公开问题:对于k≥5,LCNF_≥k是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.     

命题线性时序逻辑的对偶模型问题的复杂性

定义了一个命题线性时序逻辑的对偶模型的概念.一个公式f的对偶模型是指f的满足以下条件的两个模型(即状态的w序列):在每个位置上这两个模型对原子命题的赋值都是对偶的.然后,对于确定一个公式f是否有对偶模型的判定问题(记为DM)和在一个Kripke-结构中确定是否存在从两个给定状态出发的对偶模型满足给定公式f的判定问题(记为KDM)的复杂性进行了研究.证明了以下结果:对于只含有F("Future")算子的命题线性时序逻辑,DM和KDM都是NP完全的;而对于以下命题线性时序逻辑,DM和KDM都是PSPACE完全的:含有F,X ("Next")算子的逻辑、含有U("Until")算子的逻辑、含有U,S,X算子的逻辑以及由Wolper给出的含有正规语言算子的逻辑(一般称为扩展时序逻辑,简称ETL).     

Trace 演算

文章定义了基于踪迹(trace)的逻辑语言L_Trace,它是一阶线性时序逻辑语言的扩充,同时也是“对象演算”研究工作的基础.Trace演算所述的“对象”用来刻画具有内部状态和外部行为的动态实体,语法上由对象标记表示.对象标记Ω=(S,F,A,E)包含4个部分:数据类型S、函数F、属性A和动作E.Σ=(S,F)构成通常代数规范意义下的标记,可将动作看成一广义数据类型,从而得到标记Σ的动作扩充ΣE.对象标记的语义解释结构由关于标记ΣE的代数、映射和动作与踪迹的关系定义.ΣE-代数给出关于数据参数的解释;映射给出属性在动作踪迹中所取的值;而动作与踪迹的关系则给出执行一有限踪迹以后该动作是否允许执行.在定义了Trace演算的语法和语义之后,文章给出了Trace演算的公理系统及其可靠性证明.     

相应于无冲突依赖的规范化对象模式森林

首先概括对象依赖、无冲突对象依赖集合、规范化对象模式森林和复杂对象模式规范化设计算法的基本概念和性质;然后给出并证明相应于无冲突对象依赖集合M的规范化对象模式森林F的性质:P(F)是惟一的、不可分解的规范化对象模式森林的路径集合;M<=>OD(F)<=>P(F);P(F)是无(环的.这对于面向对象信息系统的开发有一定的意义.     

基于大间隔方法的汉语组块分析

汉语组块分析是中文信息处理领域中一项重要的子任务.在一种新的结构化SVMs(support vectormachines)模型的基础上,提出一种基于大间隔方法的汉语组块分析方法.首先,针对汉语组块分析问题设计了序列化标注模型;然后根据大间隔思想给出判别式的序列化标注函数的优化目标,并应用割平面算法实现对特征参数的近似优化训练.针对组块识别问题设计了一种改进的F1 损失函数,使得F1损失值能够依据每个句子的实际长度进行相应的调整,从而能够引入更有效的约束不等式.通过在滨州中文树库CTB4 数据集上的实验数据显示,基于改进的F1 损失函数所产生的识别结果优于Hamming 损失函数,各种类型组块识别的总的F1 值为91.61%,优于CRFs(conditional random fields)和SVMs 方法.     

带局部形状参数的λ-B曲线设计

目的 目前有很多研究B样条曲线的含参数扩展,给出的曲线都具备B样条曲线的局部形状控制性以及独立于控制顶点的形状可调性,但有些文献给出的参数是全局的,导致曲线不具备局部形状调整性,有些文献给出的调配函数不具有全正性,导致曲线不具备变差缩减性、保凸性。本文的出发点是构造同时具备保凸性、局部形状调整性、局部形状控制性的曲线。方法 首先运用拟扩展函数空间的理论框架证明了已有的3次Bézier曲线的扩展基,简称λμ-Bernstein基,恰好为所在空间中的规范B基。然后运用λμ-Bernstein基的线性组合来构造3次均匀B样条曲线的扩展基,根据预设的曲线性质反推出扩展基的性质,进而求出线性组合的系数,得出扩展基的表达式。扩展基可以表示成λμ-Bernstein基与一个转换矩阵的乘积,证明了转换矩阵的全正性,由扩展基定义了一种结构与3次B样条曲线相同的含一个局部形状参数的分段曲线。结果 转换矩阵的全正性决定了扩展基的全正性,扩展基的全正性决定了扩展曲线的变差缩减性、保凸性,形状参数的局部性决定了曲线的局部形状调整性,曲线的分段结构决定了曲线的局部形状控制性。结论 本文给出的构造具有全正性的B样条扩展基的方法具有一般性,与现有众多扩展曲线相比,本文方法构造的曲线因为具有变差缩减性和保凸性,从而为保形设计提供了一种有效方法。     

基于XYZ/E描述和验证容错系统

研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序P_F;基于P,F和恢复算法R,通过容错转换给出容错程序P_F-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质.     

基于CycleGAN的语音可懂度关键技术

语音可懂度增强是一种在嘈杂环境中再现清晰语音的感知增强技术. 许多研究通过说话风格转换(SSC)来增强语音可懂度, 这种方法仅依靠伦巴第效应, 因此在强噪声干扰下效果不佳. SSC还利用简单的线性变换对基频(F0)的转换进行建模, 并且只映射很少维的梅尔倒谱系数(MCEPs). 因为F0和MCEPs是语音的两个重要特征, 对这些特征进行充分的建模是非常必要的. 因此本文进行了一个创新性研究即通过连续小波变换(CWT)将F0分解为10维来描述不同时间尺度的语音, 以实现F0的有效转换, 而且使用20维表示MCEPs实现MCEPs的转换. 除此之外, 还利用iMetricGAN网络来优化强噪声中的语音可懂度指标. 实验结果表明, 提出的基于CycleGAN使用CWT和iMetricGAN的非平行语音风格转换方法(NS-CiC)在客观和主观评价上均显著提高了强噪声环境下的语音可懂度.     

单向Hash函数的一种构造方法*

单向Hash函数已成为密码学的一个重要组成部分．给定任一定长单向Hash函数f：∑^m→∑^t,m>t，本文给出了利用f构造一单向Hash函数F的一种新方法，该方法易于并行化．     

PARAMETRIC SOLUTIONS TO THE GENERALIZED SYLVESTER MATRIX EQUATION AX ‐ XF = BY AND THE REGULATOR EQUATION AX ‐ XF = BY + R

In this paper, explicit parametric solutions to the generalized Sylvester matrix equation AX ‐ XF = BY and the regulator matrix equation AX ‐ XF = BY + R are proposed without any transformation and factorization. The proposed solutions are presented in terms of the Krylov matrix of matrix pair (A, B), a symmetric operator and the generalized observability matrix of matrix pair (Z, F) where Z is an arbitrary matrix and is used to denote the degree of freedom in the solution. Due to its elegant form and convenient computation, these proposed solutions will play an important role in solving and analyzing these types of equations in control systems theory.     

A new solution to the generalized Sylvester matrix equation

This note deals with the problem of solving the generalized Sylvester matrix equation AV-EVF=BW, with F being an arbitrary matrix, and provides complete general parametric expressions for the matrices V and W satisfying this equation. The primary feature of this solution is that the matrix F does not need to be in any canonical form, and may be even unknown a priori. The results provide great convenience to the computation and analysis of the solutions to this class of equations, and can perform important functions in many analysis and design problems in control systems theory.     

H−/L∞ fault detection observer for linear parameter‐varying systems with parametric uncertainty

This paper considers H_?/L_∞ fault detection for discrete‐time linear parameter‐varying (LPV) systems with parametric uncertainty. In H_?/L_∞ fault detection scheme, residual generation and threshold computation are simultaneously designed. With consideration of H_?/L_∞ performance indices, the generated residual is sensitive to faults while robust against unknown disturbances. Furthermore, the L_∞ performance provides a time‐varying threshold for residual evaluation. This paper proposes a novel H_?/L_∞ fault detection observer design method to handle actuator fault detection for LPV systems with parametric uncertainty. Sufficient conditions of the fault detection observer design in the finite‐frequency domain are derived as linear matrix inequalities. Numerical simulations are used to illustrate the effectiveness and superiority of the proposed fault detection observer design approach.     

Parametric compensator design in the frequency domain

The parametric approach to the design of observer based compensators has hitherto only been formulated in the time domain. It yields an explicit parametric expression for the state feedback matrix (observer gain) given the closed loop eigenvalues and the corresponding sets of invariant parameter vectors. Using the polynomial approach to the design of observer based compensators this contribution presents an equivalent parameterization in the frequency domain. By introducing the closed loop poles and the set of so-called pole directions as new design parameters, one obtains expressions in parametric form for the polynomial matrix D(s) (D(s)), parameterizing the state feedback (state observer) in the frequency domain. It is shown how the pole directions are related to the invariant parameter vectors used in the time domain approach. Another new result is the parametric design of reduced order observers both in the frequency domain, and derived from those results, in the time domain. The proposed design procedure is also used to provide a parametric solution for the optimal LQG control problem in the presence of partially perfect measurements. Simple examples demonstrate the design procedure.     

矩阵方程AX-EXF=BY的通解及其应用

给出矩阵方程AX—EXY=BY的一个完全解析的、具有显式表达式和完全自由度的参数解(X,Y)．这里假设矩阵束(E,A B)为R-能控的,F为任意的方阵．相比于现有结论,求解算法不要求矩阵A和F具有特殊的形式,且对它们的特征值没有任何的限制,此外,本文给出的通解还具有结构简洁的特点,作为一个应用,给出了广义系统正常Luenberger函数观测器的一种参数化的设计方法,算例证明了方法的有效性．     

Solutions to the matrix equation

An explicit solution to the generalized Sylvester matrix equation AX−EXF=BY, with the matrix F being a companion matrix, is given. This solution is represented in terms of the R-controllability matrix of (E,A,B), generalized symmetric operator and a Hankel matrix. Moreover, several equivalent forms of this solution are presented. The obtained results may provide great convenience for many analysis and design problems. A numerical example is used to illustrate the effectiveness of the proposed approach.     

Resilient H∞ Control Design for Discrete‐Time Uncertain Linear Systems: An Auxiliary System Transformation Approach

This paper studies the resilient (non‐fragile) H∞ output‐feedback control design for discrete‐time uncertain linear systems with controller uncertainty. The design considers parametric norm‐bounded uncertainty in all state‐space matrices of the system, output and controller equations. The paper shows that the resilient H∞ output‐feedback control problem is equivalent to a scaled H∞ output‐feedback control problem of an auxiliary system without any system or controller uncertainty. Using the existing optimal H∞ design to solve the auxiliary system, the design guarantees that the resultant closed‐loop systems are quadratically stable with disturbance attenuation γ for all admissible system and controller uncertainties. A numerical example is given to illustrate the design method and its benefits.     

Periodically Time‐Varying Memory State‐Feedback for Robust H2 Control of Uncertain Discrete‐Time Linear Systems

This study is concerned with the synthesis of periodically time‐varying memory state‐feedback controllers (PTVMSFCs) for discrete‐time linear systems. In our preceding studies, we have already established a solid theoretical basis for linear matrix inequality (LMI)‐based (robust) H _∞‐PTVMSFCs synthesis, and the goal of this paper is to extend those results to the H ₂ performance criterion. In the H ₂ case, the main difficulty stems from the fact that we have to ensure the existence of common auxiliary variables for multiple LMI conditions that are related to the Lyapunov inequality and the inequalities for bounding traces that characterize the H ₂ norm. We can overcome this difficulty and derive a necessary and sufficient LMI condition for the optimal H ₂‐PTVMSFC synthesis. On the basis of this result, we also consider robust H ₂‐PTVMSFC synthesis for LTI systems with parametric uncertainties.