群机器人区域覆盖算法高阶逻辑建模与验证

区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群...     

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.     

融合语义主题的图像自动标注

由于语义鸿沟的存在,图像自动标注已成为一个重要课题.在概率潜语义分析的基础上,提出了一种融合语义主题的方法以进行图像的标注和检索.首先,为了更准确地建模训练数据,将每幅图像的视觉特征表示为一个视觉"词袋";然后设计一个概率模型分别从视觉模态和文本模态中捕获潜在语义主题,并提出一种自适应的不对称学习方法融合两种语义主题.对于每个图像文档,它在各个模态上的主题分布通过加权进行融合,而权值由该文档的视觉词分布的熵值来确定.于是,融合之后的概率模型适当地关联了视觉模态和文本模态的信息,因此能够很好地预测未知图像的语义标注.在一个通用的Corel图像数据集上,将提出的方法与几种前沿的图像标注方法进行了比较.实验结果表明,该方法具有更好的标注和检索性能.     

穿刺机器人运动安全性的形式化分析与建模

混成系统是实时嵌入式系统的重要子类,其行为中存在连续变化和离散跳转混杂的情况,使得混成系统行为复杂,安全性难以掌握。近年来,混成系统在医疗环境中得到越来越广泛的应用。其中,医疗机器人的穿刺运动控制系统呈现高度复杂的混成性,如果机器人在穿刺过程中失控将导致不可挽回的严重后果。因此穿刺机器人运动行为的安全性设计成为了亟需解决的问题。首先根据穿刺机器人的运动学设计,将机器人的复杂运动分解。然后基于微分动态逻辑理论从混成系统的角度出发对穿刺机器人的运动控制系统进行了形式化建模与分析,并使用证明工具KeYmaera归纳出微分不变式,获得了控制模型的参数约束。最后提出了针对机器人运动到某一靶目标区域这类运动学问题的一般性验证模型。     

一种CBR与RBR相结合的快速预案生成系统

将范例推理(case based reasoning,CBR)与规则推理(rule based reasoning, RBR)两种人工智能技术相结合,实现一种快速预案生成系统.它有效地解决了单纯RBR系统在预案生成过程中的时间延迟缺陷和知识库难以获取的瓶颈.通过CBR工具,能够把以前发生的紧急事件和解决方案生成预案.一旦新的事件发生,首先从预案库中进行案例的相似性检索,如果没有检索到预案或者检索到的预案匹配度很低,再采用RBR系统对紧急事件进行规则推理,然后把推理结果重新存入预案库.实验数据表明,这种方法对单纯RBR系统在时间响应上进行了有效的优化.另外,因为案例的获取比专家系统推理规则的获取容易得多,它同时解决了RBR系统推理规则难以获取的瓶颈.根据这种思想,实现了CBR与RBR结合的快速预案生成系统.目前,它已经应用到抗洪抢险的预案生成和城市应急联动的决策支持上,效果表明它在预案生成速度以及实际可操作性上都具有明显优势.     

最大目标频繁模式挖掘算法研究

传统的频繁模式挖掘算法往往会得到成百上千的结果模式,面对繁多的频繁模式用户通常要经过“二次挖掘”才能得到有用的目标模式。怎样根据用户需求直接挖掘用户感兴趣的目标模式是该文的研究目标。文章在FP-树的基础上设计了紧缩的、非冗余的TFP-树,它能有效过滤与目标模式无关的项和事务,而仅保留与目标模式相关的信息,缩小TFP-树的大小规模。同时根据TFP-树的规律和特点,笔者设计了最大目标频繁模式挖掘算法,算法的结果模式具有以下两个特点:(1)满足用户需求的目标模式;(2)最大模式。该实验结果验证了TFP-树算法是有效的,而且显著改善了FP-树算法的性能。     

一种快速有效的图像纹理谱描述子

提出了一种基于纹理基元等价类的纹理谱描述子来描述图像的纹理特征．该纹理谱刻画邻域内像素灰度变化模式,以纹理谱直方图方式表示图像内容．与Gabor纹理特征的对比实验表明,文中的纹理谱描述子特征提取速度快、检索准确率高．最后给出了实验结果和性能评价．     

连续傅里叶变换基础理论的高阶逻辑形式化

连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相关系统奠定了基础.最后利用定理证明的方法对电阻电感电容(RLC)串联谐振电路的频率响应特性进行了验证,说明了CFT形式化的初步应用.     

混合生成式和判别式模型的图像自动标注

目的 由于图像检索中存在着低层特征和高层语义之间的“语义鸿沟”,图像自动标注成为当前的关键性问题.为缩减语义鸿沟,提出了一种混合生成式和判别式模型的图像自动标注方法.方法 在生成式学习阶段,采用连续的概率潜在语义分析模型对图像进行建模,可得到相应的模型参数和每幅图像的主题分布.将这个主题分布作为每幅图像的中间表示向量,那么图像自动标注的问题就转化为一个基于多标记学习的分类问题.在判别式学习阶段,使用构造集群分类器链的方法对图像的中间表示向量进行学习,在建立分类器链的同时也集成了标注关键词之间的上下文信息,因而能够取得更高的标注精度和更好的检索效果.结果 在两个基准数据集上进行的实验表明,本文方法在Corel5k数据集上的平均精度、平均召回率分别达到0.28和0.32,在IAPR-TC12数据集上则达到0.29和0.18,其性能优于大多数当前先进的图像自动标注方法.此外,从精度—召回率曲线上看,本文方法也优于几种典型的具有代表性的标注方法.结论 提出了一种基于混合学习策略的图像自动标注方法,集成了生成式模型和判别式模型各自的优点,并在图像语义检索的任务中表现出良好的有效性和鲁棒性.本文方法和技术不仅能应用于图像检索和识别的领域,经过适当的改进之后也能在跨媒体检索和数据挖掘领域发挥重要作用.     

Gauge积分在HOL4中的形式化

积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭 区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4 (Higher-Order Logic 4)中形式化,包括积分的线 性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯 西可积准则,并根据相关性质对反相积分器进行了验证。