摘要:研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.

摘要:面向语义Web的需求,提出了一种新的描述逻辑与逻辑程序结合的杂合系统DLclog,它从语法和语义两方面扩展了Rosati提出的DL+log系统.在DLclog中,负DL原子可以出现在逻辑程序规则体中,并且使用McCarthy的并行限制(parallel circumscription)对其进行非经典解释,即出现在规则体中的DL谓词在其他DL谓词的解释任意发生变化的情况下,其外延在DL本体的模型中被解释为最小.使用这种方法,DL+log的非单调语义(NM-semantics,简称NM语义)被扩展成了DLclog的非单调限制语义(nonmonotonic circumscriptive semantics,简称NMC语义),从而成为目前表达能力和推理能力最强的杂合系统.此外,在DL本体使用ALCIO和ALCQO书写,且不允许属性(role)出现在规则中的失败否定(NAF)之后时,还给出了可靠完全的推理算法和NMC语义下可满足性的判定复杂度.

摘要:定义了一种称作混合区域的形式化结构表示矩形混合系统的状态集,它实际上是由一组特殊形式的线性不等式联立表示的多面体空间.证明了混合区域对于矩形混合系统的可达性操作的封闭性.此外,用矩形混合系统近似模拟非线性混合系统,相应地解决了非线性混合系统的可达性问题.使用混合区域,可以直接计算由某个正则的混合区域开始的可达集,这样,混合系统的可达性问题主要是求解混合区域的正则型问题,而这问题是一种线性规划问题,可以使用经典的线性规划算法加以解决.

摘要:线性mu-演算(μTL)是线性时序逻辑(LTL)的不动点扩展.LTL是一个便于规范和论证反应式系统的方法.μTL作为比LTL表达能力更强的逻辑,用LTL表示的性质度可由μTL表示.类似于LTL的直觉线性时序逻辑(LTL),提出一种基于直觉解释的μTL,称为直觉μTL(IμTL).确立了IμTL和ILTL的关系,比较了它们之间的表达能力.讨论了使用IμTL与安全性质和活性描述的关系以及描述“假设-保证”规范的问题.

摘要:将指纹识别中分类和匹配过程相结合,提出了一种包含奇异点周边的方向场和细节点等特征的奇异点邻近结构.该结构利用奇异点周边识别信息集中的特点,大大减少了匹配的计算量,并能够同时作为指纹分类和比对的特征,直接应用于指纹的连续分类和快速匹配过程,实现对大容量指纹数据库的快速识别.在NIST和FVC2004数据库上的测试结果显示,该算法在保证自动指纹识别系统(automatic fingerprint identification system,简称AFIS)的识别准确性的同时,还使得指纹在线识别系统的1:N辨识速度有显著的提高.

摘要:各个点在数据内部的组织结构中自然地扮演着3种不同的结构性角色,分别是毂、质心和野值.在基于邻域的聚类算法中,邻域密度因子能够识别分离数据集中的毂、质心和野值.但是,邻域密度因子对有噪声和重叠的数据往往失效.为了解决该问题,引入了基于多项式核的邻域密度因子,并在有向树框架下,提出了一种结构化的数据聚类算法,其计算复杂度线性于输入数据的大小.对带有噪声和重叠的数据集,该算法能够找到所有显著的、任意形状的不均衡聚类.在人工和真实数据集上的实验结果都证实了该算法的有效性和快速性.

摘要:Li等人提出的距离保持水平集方法有传统变分水平集方法不具备的许多优点,然而,它有初始曲线必须包围目标物体或完全置于目标物体内部或外部的缺点.提出一种自适应距离保持水平集方法,它无须初始曲线包围目标物体或完全置于目标物体内部或外部,即初始曲线可以置于图像的任何地方.它能够解决原方法所不能解决的一些图像分割问题,例如,能够从任意选取的一条初始曲线出发自动检测目标物体的内外轮廓,检测多目标物体以及深度凹陷区域的边缘,并能较好地提取目标物体的弱边界.对几幅具有不同目标边界形态的合成图像和自然图像进行了实验,结果都取得了预期的分割效果.

摘要:研究基于可信度的模糊一阶模态逻辑,给出了基于常域的模糊一阶模态逻辑语义以及推理形式系统描述.为有效进行模糊断言间的推理,考虑了模糊约束的概念.模糊约束是一个表达式,其中既有语法成分又包含意义信息.模糊推理形式系统中的基本对象是模糊约束,针对模糊约束引进可满足性概念,研究模糊约束可满足性相关性质.利用模糊约束的概念,模糊断言间的推理可以直接在语义环境下加以考虑,因此,以模糊约束为基本元素的模糊推理形式系统随之建立.主要分析新产生断言有效性与模糊约束集可满足性之间的关系,并在此基础上给出了模糊推理形式系统的推理规则.进一步的工作可探讨模糊推理形式系统的可靠性与完全性,建立推理过程的能行机制.研究结果可在人工智能和计算机科学等领域得以应用.

摘要:对网络体系结构的研究现状进行了介绍.基于MCES(micro-communication element structure)架构设计了一种基于服务的网络体系结构原型.在原型系统中,实现了服务元的合理组合和调度,并从体系结构上更好地支持QoS和网络安全.同时,通过改进的套接字机制实现了向后兼容现有TCP/IP网络应用程序,满足了用户不断增长的网络服务要求.基于Linux的实验结果显示,该体系结构组成的系统是合理的、可行的,并具有很好的传输效率和可扩展性.

摘要:首先定义和分析了IEEE 802.16e无线城域网中的一个新问题,即如何在保证移动终端服务质量的前提下,通过合理地调度终端的单播业务和多播业务来降低终端能耗.针对该问题,提出一种基于调度集合的联合调度算法(scheduling set based integrated scheduling,简称SSBIS).SSBIS算法将所有移动终端划分到多播调度集合或单播调度集合中,并利用多播数据的传输特点,在多播数据传输的相邻时隙内发送多播调度集合中所有终端的单播数据,而对于单播调度集合中的终端,则通过凸优化方法求得使终端休眠时间最长的单播业务调度方案,以达到降低终端能耗的目的.仿真实验显示,SSBIS算法在满足移动终端的最小数据速率要求的同时,可以明显地降低终端能耗.

摘要:提出一种按序排队(in-order queuing,简称IOQ)PPS体系结构,通过在分流控制器引入固定尺寸的缓冲区,实现负载在每个交换平面的均匀分配;中间层组合输入输出排队(combined input-and-output queuing,简称CIOQ)交换平面受控于中央调度器,在每个时间槽(time slot),中央调度器将同一种匹配实施到每一个交换平面,称之为同步调度策略.可以证明,在该体系结构下,轮询(round robin)分派算法配合同步调度策略可以保证同一条流的信元按序从交换平面读出.进一步提出了严格最长队列优先同步调度算法,极大地减少了中央调度器需要维护的状态信息和信元重定序开销.与目前主流的PPS设计相比,IOQ PPS(in-order queuing parallel packet switch)实现机制简单,易于硬件实现.模拟结果表明,IOQ PPS具有最优的延迟性能.

摘要:提出了一种TBPR(time-based broadcasting for power-aware routing)协议.TBPR采用路由请求报文延迟发送机制,并通过比较路径中的累计功率消耗,选择能量消耗较低的路由,以降低网络的能量消耗,延长网络的生存周期.计算机仿真实验表明,TBPR能够取得较好的节能效果,并降低无线Ad Hoc网络中的能量消耗.

摘要:根据给定的处于关键时刻的人体关键姿态,运用优化方法生成满足牛顿力学的人体运动是人体运动仿真研究的重要问题.由于牛顿力学的强非线性和数值优化方法只能找到局部最优解,将牛顿力学约束直接作为约束条件的优化模型在实践中的收敛性不好.通过将牛顿力学约束转化为目标函数,同时增加对关键时刻的优化,提高了模型的收敛性,使其不依赖于被仿真运动的类型、人体质量参数和关键时刻准确程度等因素.仿真出来的人体运动尽可能地满足了牛顿力学.通过仿真7类复杂的蹦床运动验证了新模型的有效性,同时还将该模型用于人体受力分析和体育运动的新动作设计.

摘要:设计并实现了一套针对海量数据的处理和分析算法框架,并将其融入实验室早先开发完成的医学影像算法研发平台MITK(medical imaging toolkit)中,真正建立起一个海量医学影像数据的处理平台,并在此基础上研究了针对海量数据的基于光线投射和三维纹理的快速体绘制算法,提出了一种半自适应分块的方法对原始数据进行分块,在不对分块速度产生太大影响的基础上得到了更好的分块结果,同时使用图形硬件来进一步加速整个算法的绘制流程.实验结果表明了该平台和算法对于海量医学数据处理和可视化的有效性.