发表咨询:400-808-1731
订阅咨询:400-808-1751
省级期刊
影响因子 0.3
人气 17056
部级期刊
影响因子 0.38
人气 12698
统计源期刊
影响因子 1.71
人气 12518
CSSCI南大期刊
影响因子 5.52
人气 11807
北大期刊
影响因子 3.18
人气 11592
北大期刊
影响因子 0.62
人气 10628
省级期刊
影响因子 0.42
人气 10372
统计源期刊
影响因子 1.29
人气 9877
省级期刊
影响因子 0.67
人气 9281
CSSCI南大期刊
影响因子 1.11
人气 8356
摘要:G(p)和Gp→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中求解这些模态算子的现有的两种重要方法从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对优化编译中的语句交换和变量替换这两种常见变换的保义性条件给出了形式刻画,采用含条件重写规则定义了保义语句交换 Texch和保义变量替换 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的抽象辩论框架的方法定义争议之间的关系,给出了争议可防卫性和陈述可接受性算法.用该模型对已有文献中的实例重新建模,结果表明,该模型能够准确计算陈述可接受性并得出研讨结果.该模型研究出发点是对实际群体研讨建模,但也可以用于非经典逻辑形式系统建模.
摘要:在图嵌入(graphembedding)的框架下提出一种根据表情相似度构建邻接权重图的方法来学习人脸表情子空间.数据集中人脸图像的表情以半监督.学习的方式来估计,人脸图像之间的表情相似性由表情模糊隶属度矢量之间的内积来度量,与个体、光照、姿态等人脸差异无关.在得到的子空间内,相似表情的人脸图像位于流形上的邻近位置,表情数据在子空间内按语义的分布很好地揭示了表情模糊、演变的特性在Cohn-Kanade人脸表情数据库和实验室自行采集的人脸表情数据集上的实验结果说明了该方法的有效性.因此,该方法可以很好地应用于各种基于人脸表情识别的人机交互中.
摘要:对现有的应用于移动互联网的P2P技术方面的研究进行了分析.首先介绍了P2P技术和移动互联网的概念,并提出将P2P技术应用在移动互联网所面临的挑战和应用模式.其次,分别针对集中式架构、超级节点体系架构和ad hoc架构对应用于互联网的P2P网络体系架构进行了阐述.再其次,针对移动终端的两种接入模式,分别在资源定位算法和跨层优化两个方面进行了介绍.对各关键技术的特点进行了详细的分析,指出其存在的不足.最后,对未来的工作进行了展望.