多速率混合系统的符号化可达性分析

针对目前还没有专门的数据结构处理多速率混合系统的符号化可达性问题，定义了多速率区域来表示和处理多速率自动机的无穷状态空间，从而把多速率混合系统的符号化可达性分析等价地转化成多速率区域上的3种操作，即并操作、变量重赋值操作和控制状态上的时间流逝操作．从理论上证明了多速率区域在这3种操作上的封闭性，同时定义了矩阵数据结构不同上限矩阵（DCM），并用其存储多速率区域，这样就得到了一种专门处理多速率混合系统符号化可达性分析的数据结构．理论上证得，DCM可以大大降低可达性分析算法的复杂度．     

临界状态下中立型时滞差分方程解的振动性

考虑中立型时滞差分方程　　△ (xn-pnxn-k) qnxn-l =0 ,n =0 ,1,2 ,… ( )其中pn,qn(n =0 ,1,2 ,… )是实数且pn≥ 0 ,qn≥ 0 ,k和l是非负整数 ,获得了临界状态下方程 ( )所有解振动的一个充分条件 .     

具有可和系数中立型时滞差分方程的振动性与正解的存在性（英）

考虑如下形式的线性中立型时滞差分方程△(Xn-PnXn-k)+qnXn-l=0,n=0,1,2,……其中{Pn}、{qn}均为实数列且Qn≥0,k,l为非负整数.在允许Pn-1振动情况下,本文建立了该方程所有解振动性和正解存在性的几个新的充分条件,其中不需要文献中通常用到的发散条件 qn=∞,作为应用,证明了方程△[xn-esin xn-4k]+ceβn-1=0,c＞0所有解振动的充要条件为β≤ .     

分数阶金融模型的混沌控制

本文运用时滞反馈控制策略研究了一类分数阶金融模型的混沌控制问题,通过分析受控系统的特征方程,建立了系统稳定和Hopf分支存在的充分准则.设计的反馈控制器能有效地抑制系统的混沌行为.数值模拟证实了理论分析的有效性.     

利用投影时序逻辑的多内核进程调度建模与验证

针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公式P,在PTL公理系统的基础上,通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验,结果表明所提方法可验证多内核处理器进程调度的系统性质,保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点,因此该方法也适用于一般的并发系统验证.     

面向命题投影时序逻辑的安全协议模型检测

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.     

具有无界时滞的泛函微分方程解的振动性

运且一种有效的方法研究一类形式广泛的泛函微分方程解的振动性，得到了Ｈｕｎｔ－Ｙｏｒｋ型定理的一般形式，推广了一系列已有的结论。     

广义随机Petri网下的组合Web服务建模与评价

为了保证用语义Web服务标记语言(OWL-S)描述的组合Web服务的可靠性,确保组合服务具有较高的系统性能,提出了一种用广义随机Petri网(GSPN)对OWL-S过程模型进行建模、分析、验证以及评估的方法.首先给出从OWL-S过程模型到GSPN的映射规则和转换方法,然后针对得到的GSPN模型,采用S-不变量、T-不变量,通过可达性等分析方法验证OWL-S过程模型的正确性,最后构造与GSPN同构的马尔可夫链,并根据其稳定状态概率进行系统性能评价.经数学工具验证结果表明,所建模型是正确、可靠的,并发现了组合服务中的瓶颈.所提方法可支持组合Web服务的重建、优化和决策.     

正整数分拆数的一个递推公式

本文给出了计算正整数分拆数的一个递推公式: a_n~h=sum from i=h to [n/2] a_(mj)~i+1 (1≤h≤[n/2]) a_n~h=1 ([n/2]相似文献   

临界状态下中立型时滞微分方程解的振动性

讨论了一类中立型时滞微分方程所有解的振动性,获得了临界状态下该方程所有解振动的一个充分条件。