摘要:命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

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

摘要:在基于语言考虑代码安全性的工作中,往往需要将高级语言程序翻译成类型化低级语言的程序进行类型检查.许多高级语言具有类型调度结构,在向低级语言的编译过程中需要用标签机制来实现.针对具有多继承接口的Java程序包含的一种特殊的类型调度结构,提出了一种新的标签类型.包含这种标签类型的低级语言能够有效地实现Java程序中的接口调用.这种对接口调用的编译方法被用在一个以类型化低级语言为验证语言的Java字节码即时编译器中.

摘要:反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.

摘要:均值漂移是一种有效的统计迭代算法,已广泛应用于聚类分析、跟踪、图像分割、图像平滑、滤波、图像边缘提取和信息融合等方面.但是,其收敛性仍没有得到严格的证明,而收敛性是任何迭代算法的必要前提.推广并严格证明了该算法的收敛性.首先将均值漂移算法做了以下推广:反映不同样本点处局部空间结构的差异及其各向异性.然后,在推广的条件下从数学上严格证明了均值漂移算法的收敛性.最后,探讨了均值漂移算法中参数的自适应选择方法.从而为该算法的应用奠定了理论基础.

摘要:输入队列因具有良好的可扩展性而广泛应用于高速交换机和路由器中,但输入队列需要精心设计调度算法以获取较好的性能.Round-Robin算法因其简单性和并行性而得到广泛的研究,但现有的Round-Robin算法在突发流量和非均匀流量下的负荷-延迟性能较差.提出了调度决策在时隙间进行迭代的思想,并利用队列长度具有随机性的特点设计了能近似最大匹配的Round-Robin算法--iSLOT.仿真结果表明,iSLOT不仅在均匀流量下是稳定的,在非均匀流量和突发流量下的吞吐率及延迟性能均远好于现有的Round-Robin算法.

摘要:吴方法是由我国科学家吴文俊院士开创的一个新兴研究领域.考虑到吴方法"分而治之"的思想非常适合分布式计算,将分布式计算技术引入到该方法的计算过程中,给出一种既可以在集群环境下,也可以在网格环境下实现的分布式吴方法计算框架.首先分析了吴方法分布式计算需求,并以特征列计算为例来说明吴方法分布式计算算法,然后讨论了符号计算基本数据类型:大整数和多项式的消息传递方法,最后简单给出了在网格环境下基于符号计算软件系统ELIMINO和网格中件间Globus Toolkits 3的分布式吴方法计算环境的设计、实现与实验结果.

摘要:k-Median问题的近似算法研究一直是计算机科学工作者关注的焦点,现有研究结果大多是关于欧式空间和Metric空间的,一般距离空间k-Median的结果多年来一直未见.考虑一般距离空间k-Median问题,设d_max/d_min表示k-Median实例中与客户点邻接的最长边长比最短边长的最大者.首先证明d_max/d_min≤ω+ε的k-Median问题不存在近似度小于1+ω-1/e的多项式时间近似算法,除非,由此推出Metric k-Median问题不可近似到1+2/e,除非NP(∈)DTME(N^{O(log logn)}).然后给出k-Median问题的一个局部搜索算法,分析表明,若有d_max/d_min≤ω,则算法的近似度为1+ω-1/2.该结果亦适用于Metric k-Median,ω≤5时,局部搜索算法求解Metric k-Median的近似度为3,好于现有结果3+2/P.通过计算机实验,进一步研究了k-Median局部搜索求解算法的实际计算效果和该算法的改进方法.

摘要:支持多实例的工作流管理系统为工作流过程处理带来极大的灵活性,活动多实例要解决的主要问题之一是多实例的调度控制.在分析了多实例的分配和汇聚等问题之后,针对过程中活动间不同活动语义的上下文,对活动多实例的活动属性进行了统一的形式描述,提出了活动多实例控制体Shell,用于控制活动多实例的分配和提交.Shell可以根据不同的活动语义,处理多实例的同步并控制整个过程的运行.Shell的提出解决了工作流执行中一个活动多个执行实例的同步执行问题.

摘要:提出了一种支持软件过程控制与改进的主动度量模型AMM(active measurement model)和度量方法.模型形式化描述了软件过程的目标、特征和度量指标等关键元素以及相互间的关系,给出了确定软件过程度量的原则、方法和步骤.基于该度量模型,软件组织一方面可以依据确定的过程目标,主动导出合适的度量过程;另一方面还可以依据度量的结果,识别过程改进的机会,并主动导出过程改进的方向.为正确的决策和成功的结果提供有效的支持.

摘要:针对基于Petri网离散事件系统关于标识向量和Parikh向量的不等式约束反馈控制器设计问题,提出一种新的控制器设计方法.该方法首先利用Petri网的状态方程把关于标识向量和Parikh向量的不等式约束转变成关于Parikh向量的不等式约束,然后基于Petri网库所是关于Parikh向量的不等式约束的观点构造控制器.最后将该方法与Iordache和Moody提出的方法作比较,实验结果显示该方法更简单、有效.

摘要:在用数量化理论3类(quantification theory of type 3,简称QT3)定量地分析软件需求的基础上,以质量功能展开(quality function deployment,简称QFD)中的质量屋(house of quality,简称HOQ)系列矩阵为纲领,基于由模糊技术改进后的模糊层次分析法(fuzzy analytic hierarchy process,简称FAHP),提出了一种软件需求定量分析及其向设计实现过程模糊映射的方法.将该方法具体应用于CD-R/RW光盘刻录机软件的开发过程,其有效性得到了验证.

摘要:传统TCP(transmission control protocol)本是为有线网络设计,它假设包丢失全是由网络拥塞引起,这个假设不能适应于MANET (mobile ad hoc network),因为MANET中除了拥塞丢包以外,还存在由于较高比特误码率、路由故障等因素引起的丢包现象.当出现非拥塞因素丢包时,传统TCP将错误地触发拥塞控制,从而引起TCP性能低下.任何改进机制都可以分为发现问题和解决问题两个阶段.首先概括了MANET中影响TCP性能的若干问题;然后针对发现问题和解决问题两个阶段,详细地对每一阶段中存在的各种可行方法进行了分类、分析和比较;最后指出了MANET中TCP性能优化的研究方向.

摘要:在分析Ad Hoc网的单播QoS路由问题的基础上,提出了一种新的Ad Hoc网的分布式QoS路由算法--EBLLD(entropy-based long-life distributed QoS routing)算法.其核心思想是提出了衡量路径稳定性的新尺度--熵,并利用熵来选择长寿的路径,减少了重建路由(或路由修复)的次数,从而在Ad Hoc网的网络拓扑频繁变化的环境中尽可能地提供QoS保证.同时该算法还利用本地组播机制和启发函数排序过滤和熵尺度排序过滤减小了其路由消息开销.仿真结果表明,EBLLD算法能够以较小的路由消息开销获得较高的路由成功率.此外,EBLLD算法具有可扩展性,可以应用于较大规模的Ad Hoc网中.

摘要:首先将基于门限结构的彼得森可验证秘密共享方案(Pedersen-VSS)转换成可以抵抗一般结构敌手攻击的方案(Pedersen-VSS-General).指出R. Canetti等人在设计分布式密钥生成方案(DL-Key-Gen)时,关于零知识证明使用的一个错误,并给出一种改进方案.基于以上设计,提出一个可以抵御一般结构敌手攻击的自适应安全的分布式密钥生成方案,该方案的安全性不依赖于"擦除"假设.对于这个方案给出详细的基于黑盒模拟的安全性证明.

摘要:Linux是目前广泛用于路由设备中的操作系统,而流量管理是这种网络操作系统的一个重要功能.研究了Linux系统的流量管理机制,发现当前Linux系统所采用的在网络接口的出口实现的基于网络包调度的流量管理机制缺乏对于网络带宽在系统范围的全局性的管理,也缺乏对于输入流的网络处理的有效管理和调度,从而造成不必要的CPU资源的浪费.为解决这一问题,提出了一种新颖的网络带宽管理机制,它通过调度网络协议处理所占用的CPU时间来实现带宽管理.这种新的机制将网络带宽的管理和调度从网络接口的出口点转移到处理接收到的网络包的系统软件中断处理程序中,从而克服了原来的流量管理机制的缺点.通过系统实现和对比实验,发现该机制本身给系统带来的负载小于Linux原来的流量管理机制,同时可以提供更好的流量隔离,并且能够有效地节省用于网络处理的CPU资源.

摘要:分析了王尚平等人提出的群签名成员删除方案,给出在群管理员更换群密钥后,已被删除成员更新其特性密钥、证明其成员资格和产生有效签名的方法,说明该方案是不安全的,不能真正删除群成员.

摘要:针对移动Agent数据保护这一特定的安全问题,提出了关联密钥链加密IKCE(interrelated keys chains encryption)机制,并对该机制进行了安全性分析和性能分析.IKCE机制的核心思想是在移动Agent数据加密的密钥之间建立一种关联关系,从而达到Agent数据保护的目的.研究表明,IKCE机制对于移动Agent数据保护是可行的.