摘要:G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值.

摘要:为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验.

摘要:讨论了以基于前缀封闭集合的Heyting代数的直觉解释的线性μ-演算(IμTL)作为描述“假设-保证”的逻辑基础的问题,提出了一个基于IμTL的“假设-保证”规则.该规则比往常应用线性时序逻辑(LTL)作为规范语言的那些规则具有更好的表达能力,扩展了对形如“always ?”等安全性质的“假设-保证”的范围,具备更一般的“假设-保证”推理能力及对循环推理的支持.

摘要:提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL 的工具中得以实现.APL 自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.

摘要:介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.

摘要:服务消费者在选择服务之前,通常需要基于其他消费者的经验对未使用过的服务的质量进行预测.考虑到不同服务消费者对同一服务的服务质量的感受之间可能存在较大的差别,提出了一种QoS(quality of service)预测方法.该方法以消费者的历史经验为基础,计算消费者之间以及服务之间的相似程度,并以此相似度为基础对消费者并未使用过的服务的QoS进行预测.实验结果表明,这种方法可以显著提高Web服务质量预测的准确性.

摘要:基于时序逻辑CTL(computation tree logic)的一种扩展CTL-FV对优化编译中的语句交换和变量替换这两种常见变换的保义性条件给出了形式刻画,采用含条件重写规则定义了保义语句交换T_exch和保义变量替换T_sub,并基于一种归纳证明框架对它们的保义性进行了证明.此外,基于变换Texch对程序基本块内保依赖语句重排的保义性也给出了一种构造性的证明.

摘要:提出了一种基于图转换的模型重构描述语言.针对模型重构的特征,设计了模型重构描述语言的基本元素,并给出了如何通过这些基本元素描述模型重构及重构规则的方法.在此基础上,给出了根据形式化重构规则执行模型重构的具体步骤和策略,并提供了较为完整的模型重构CASE支撑工具.通过实例讨论了该模型重构描述语言的描述能力.结果表明,该语言具有较强的描述能力,能够比较简洁地描述复杂的模型重构规则.

摘要:随着Web Service组合变得越来越复杂,通过测试来保证服务质量和可靠性也变得越来越重要.将传统数据流分析方法扩展用于Web Service组合测试,提出了一种基于BPEL的Web Service组合的数据流分析测试方法.该方法基于一个测试模型:Web Service组合测试模型WSCTM,该测试模型可以捕获Web Service组合的数据流接口.采用基于服务的模型WSCTM,数据流可以从3个视点来分析:服务间、服务内和服务实现构件间.从而,Web Service组合的数据流测试可以在三层上得到实现.基于以上方法,可得到Web Service组合的定义-使用链,最终可产生满足既定测试标准以获得需求Web服务组合质量要求的测试路径.

摘要:在对类型范畴理论进行扩展的基础上,将其与进程代数相结合,为软件体系结构模型及其间的转换关系提供了一种统一的语义描述框架.模型的结构语义由类型范畴图表来指代,其行为语义则由范畴附带的进程行为迹来表示,模型间的映射关系用范畴理论中的态射和函子来形式化描述.该描述框架可用于模型转换中特性保持问题的描述、分析和判定,从而为模型驱动的软件开发提供有力的支持.

摘要:对自然语言处理研究中的复述的研究现状与进展进行了总结,分别介绍了复述的应用、复述资源的获取、复述句的生成、复述的评测以及与复述紧密联系的相关研究等.重在对复述研究的主流方法和前沿进展进行概括、比较和分析,以期对后续研究有所助益.

摘要:研究的目的是对现有的无监督词义消歧技术进行总结,以期为进一步的研究指明方向.首先,介绍了无监督词义消歧研究的意义.然后,重点总结分析了国内外各类无监督词义消歧研究中的各项关键技术,包括使用的数据源、采用的消歧方法、评价体系以及达到的消歧效果等方面.最后,对14个较有特色的无监督词义消歧方法进行了总结,并指出无监督词义消歧的现有研究成果和可能的发展方向.

摘要:提出一种大规模数据集求解核主成分的计算方法.首先使用Gram矩阵生成一个Gram-power矩阵,根据线性代数的理论可知,新形成的矩阵和原先的Gram矩阵具有相同的特征向量.因此,可以把Gram矩阵的每一列看成核空间迭代算法的输入样本,这样,无须使用特征分解即可迭代地计算出核主成分.该算法的空间复杂度只有O(m);在大规模数据集的情况下,时间复杂度也降低为O(pkm).实验结果表明了所提出算法的有效性.更为重要的是,在大规模数据集的情况下,当传统的特征分解技术无法使用时,该方法仍然可以提取非线性特征.

摘要:所提出的模型利用协商历史中隐含的信息自动对数据进行标注以形成训练样本,用最小二乘支持向量回归机学习此样本得到对手效用函数的估计,然后结合自己和对手的效用函数构成一个约束优化问题,用遗传算法求解此优化问题,得到的最优解就是己方的反建议.实验结果表明,在信息保密和没有先验知识的条件下,此模型仍然表现出较高的效率和效用.

摘要:结合步行机器人行走的动力学特性,通过对机器人的加速度传感器信息进行离散傅立叶变换,建立了行走相关特征值的概率模型.通过使用马氏距离作为判定标准,对步行机器人的行走稳定性给出定量描述.四足步行机器人平台上的实验结果表明,该模型能够实时反映机器人的行走特性,帮助机器人在行走状态受环境影响发生改变时,根据行走特征及时调整运动,保证其稳定性.

摘要:提出了一种研讨模型.该模型用简化的Toulmin模型表示争议内部结构,用Dung的抽象辩论框架的方法定义争议之间的关系,给出了争议可防卫性和陈述可接受性算法.用该模型对已有文献中的实例重新建模,结果表明,该模型能够准确计算陈述可接受性并得出研讨结果.该模型研究出发点是对实际群体研讨建模,但也可以用于非经典逻辑形式系统建模.

摘要:在图嵌入(graph embedding)的框架下提出一种根据表情相似度构建邻接权重图的方法来学习人脸表情子空间.数据集中人脸图像的表情以半监督-学习的方式来估计,人脸图像之间的表情相似性由表情模糊隶属度矢量之间的内积来度量,与个体、光照、姿态等人脸差异无关.在得到的子空间内,相似表情的人脸图像位于流形上的邻近位置,表情数据在子空间内按语义的分布很好地揭示了表情模糊、演变的特性.在Cohn-Kanade人脸表情数据库和实验室自行采集的人脸表情数据集上的实验结果说明了该方法的有效性.因此,该方法可以很好地应用于各种基于人脸表情识别的人机交互中.

摘要:对现有的应用于移动互联网的P2P技术方面的研究进行了分析.首先介绍了P2P技术和移动互联网的概念,并提出将P2P技术应用在移动互联网所面临的挑战和应用模式.其次,分别针对集中式架构、超级节点体系架构和ad hoc架构对应用于互联网的P2P网络体系架构进行了阐述.再其次,针对移动终端的两种接入模式,分别在资源定位算法和跨层优化两个方面进行了介绍.对各关键技术的特点进行了详细的分析,指出其存在的不足.最后,对未来的工作进行了展望.

摘要:提出一种基于确定的有穷状态自动机(deterministic finite automaton,简称DFA)的正则表达式压缩算法.首先,定义了膨胀率DR(distending rate)来描述正则表达式的膨胀特性.然后基于DR提出一种分片的算法RECCADR (regular expressions cut and combine algorithm based on DR),有效地选择出导致DFA状态膨胀的片段并隔离,降低了单个正则表达式存储需求.同时,基于正则表达式的组合关系提出一种选择性分群算法REGADR(regular expressions group algorithm based on DR),在可以接受的存储需求总量下,通过选择性分群大幅度减少了状态机的个数,有效地降低了匹配算法的复杂性.

摘要:提出了一种基于选择复制的动态数据传输策略SRAD(selective replication-based adaptive data delivery scheme),基本思想是把消息(message)动态的复制给更有可能与汇聚点(sink node)通信的传感器节点.SRAD由数据传输和队列管理两个主要部分组成:前者根据Random Waypoint随机运动模型下不同时刻各传感器节点传输概率的大小进行数据消息的传输;后者通过消息的生存时间ST(survival time)值决定队列中消息传递的优先顺序和丢弃原则,以进一步降低网络传输能耗.模拟实验结果表明,与现有的几种DTMSN(delay tolerant mobile sensor networks)数据传输算法相比,SRAD的网络寿命相对较长,且它能以较低的数据传输能耗和传输延迟获得较高的数据传输成功率.

摘要:从数据场思想出发,提出了一种基于拓扑势的社区发现算法.该方法引入拓扑势描述网络节点间的相互作用,将每个社区视为拓扑势场的局部高势区,通过寻找被低势区域所分割的连通高势区域实现网络的社区划分.理论分析与实验结果表明,该方法无须用户指定社区个数等算法参数,能够揭示网络内在的社区结构及社区间具有不确定性的重叠节点现象.算法的时间复杂度为O(m+n^3/γ)～O(n²),n为网络节点数,m为边数,2<γ<3为一个常数.

摘要:建立并行下载模型,并基于这一模型,从下载节点效益的角度出发,分析并提出最优机制.这种最优机制包括最优的选择源节点集合和文件分块方案.理论分析表明,这种机制能够使下载节点代价函数最小.仿真结果说明了这种机制的有效性.

摘要:在前人优化研究方法的基础上,结合网络编码优化问题自身的特点提出了新的解决方案.首先是算法的预处理部分:1) 给出了统一的方法由不同的资源描述函数生成遗传算法所必须的适应值函数,使得各种不同的网络编码资源优化问题都能利用同样的遗传算法模型;2) 通过检验有多条输入链路的输出链路进一步缩小优化算法的搜索范围.其次,针对网络编码资源优化问题随机解几乎不能让所有接收者都达到组播速率的特点,在一般的遗传算法中加入以下新的处理:1) 在初始化阶段使用更为精细的算法产生更高质量的初始成员.2) 在遗传算法每次循环开始时额外调用初始成员生成算法,加入一定数量的新成员,从而避免了局部性问题.3) 对于不能达到最大组播速率的网络编码方案,基于各个接收者各自的接收速率确定更为合适的适应值而不是统一设为?1,从而使这些方案也能参与算法的进一步处理而不是完全被淘汰.模拟实验结果显示,新的优化算法不仅运行得更快,而且输出的网络编码方案所消耗的资源也更少.

摘要:为了提高大规模网络中别名解析的效率,在用traceroute测量得到的IP级网络拓扑的基础上,提出别名过滤的概念.首先从理论上研究别名关系具有的性质,由此提出处理traceroute数据的3个属性;然后提出并设计了别名过滤算法AF(alias filtering)和别名验证算法VAR(validation of alias relationship).最后,利用CAIDA(Cooperative Association for Internet Data Analysis)的Skitter项目得到的中国、日本、韩国这3个国家因特网的traceroute数据集对上述算法进行了验证分析.结果表明,别名过滤的概念非常重要并且文中提出的算法效率比较高.

摘要:提出一种交错编码的多重门限调度算法(interleaving coded multi-threshold scheduling,简称ICMTS).该算法将前、后级队列门限标记交错编码作为权值表征输入调度过程前、后两级队列的整体调度需求,根据交错编码的权值对前级虚拟输出队列进行优化调度判决,并通过多重门限机制降低算法的硬件资源开销.采用流模型证明当加速因子为2时,ICMTS算法可获得100%的吞吐量,并给出ICMTS算法的工程简化设计方案,复杂度为O(logN).仿真仿真结果表明,采用ICMTS算法的工程简化方案即可获得比现有算法更优的调度性能.

摘要:给出了描述行为驱动的信任管理语言RT_B.将变量引入到角色中可以记录用户的累积行为状态;行为驱动的信任规则根据用户已发生的行为调整其在本信任域中被分配的角色;组合规则提高了信任判定的效率;信任策略更新规则允许信任域在系统状态发生变化时自动调整信任策略.描述了行为驱动的信任管理的实现框架,并讨论了优化实现的几种机制.