摘要:提出了一种将布尔公式划分为子句组来进行布尔可满足性判定的方法.CNF(conjunctive normal form)公式是可满足的当且仅当划分产生的每个子句组都是可满足的,因此,通过判定子句组的可满足性来判定原公式的可满足性,相当于用分治法将复杂问题分解为多个子问题来求解.这种分治判定方法一方面降低了原公式的可满足性判定复杂度;另一方面,由于子句组的判定可以并行,因而判定速度能够得到进一步的提高.对于不能直接产生布尔子句组划分的情形,提出了一种利用聚类技术将CNF公式聚类成多个簇,然后消去簇间的公共变量来产生子句组划分的方法.

摘要:人工蜂群算法是近年来提出的较为新颖的全局优化算法,已成功地应用于解决不同类型的实际优化问题.然而在该算法及相关的改进算法中,侦察蜂通常采用随机初始化的方法来生成新食物源.虽然这种方法较为简单,但易造成侦察蜂搜索经验的丢失.从算法搜索过程的内在机制出发,提出采用正交实验设计的方式来生成新的食物源,使得侦察蜂能够同时保存被放弃的食物源和全局最优解在不同维度上的有益信息,提高算法的搜索效率.在16个典型的测试函数上进行了一系列实验验证,实验结果表明:1) 该方法能够在基本不增加算法运行时间的情况下,显著地提高人工蜂群算法的求解精度和收敛速度;2) 与3种典型的变异方法相比,有更好的整体性能;3) 可作为提高其他改进人工蜂群算法性能的通用框架,具备有良好的普适性.

摘要:开放移动平台的涌现,加速了服务组合技术在移动应用开发过程中的应用和发展.当前的移动应用开发大多采用静态的服务分类聚集的组合方式,很容易引起功能过载和服务访问链过长的问题,严重影响了移动应用的易用性.针对这一问题,结合移动应用领域的特点,提出一种探索式服务组合方法.该方法通过感知上下文变化为用户构造当前环境下可用的服务集合,并通过交互将用户选择的服务即时地组合到应用中.基于上下文构造可组合的候选服务集合是其中一个核心技术,采用历史挖掘的算法,利用用户在不同上下文环境下选择服务的历史记录,挖掘出上下文与服务间的关联关系,以此作为匹配候选服务的依据.在关联规则挖掘方面,对传统的FP-tree算法进行了扩展,使其支持移动应用领域中二维数据项的挖掘.实验结果表明,扩展后的算法比传统算法在服务匹配方面具有更高的准确率和命中率.

摘要:针对一类中断驱动系统提出了一种建模和模型检验的方法.该系统通常由中断处理程序和操作系统调度的任务组成,前者由中断源触发后处理中断事件,后者则负责处理系统的日常任务以及某些中断处理事件的后续处理.因为这类系统是实时控制系统,对中断事件的处理需要在规定时间内响应并完成,否则可能造成严重的系统失效.为了帮助系统设计人员在系统设计过程中应用模型检验技术来提高系统的正确性,首先确定了此类系统中与时序性质相关的系统要素(包括系统调度任务、中断源、中断处理程序)和相关参数,并要求设计人员在设计阶段明确指出这些要素的参数.然后,提出了将这些要素和参数自动转化为形式化模型的方法:使用时间自动机对中断事件进行建模,使用中断向量表和CPU处理栈对中断处理过程进行建模.对于得到的形式化模型,给出了针对中断处理超时错误的检测方法,并在此基础上给出了针对共享资源的完整性、子程序原子性的检验方法.

摘要:通过定义不可满足概念间的覆盖关系,发现MUPS和MIPS之间的内在关联,从而引出不可满足概念的R-MUPS;给出并证明不一致本体术语集中至少存在一个不可满足概念的R-MUPS就是该术语集的MIPS;利用这一结论,提出基于有序标签演算的R-MUPS算法,采用深度优先遍历原则合并分支计算R-MUPS,同时缓存覆盖概念集合,加快MIPS的求解,实现本体调试.通过概念扩展树与概念R-MUPS算法的等价性,证明算法的正确性并分析其复杂度.最后,利用自动生成本体、现实本体及其扩建本体的数据进行全面测试.实验结果表明:基于R-MUPS的MIPS求解方法能够高效、准确地完成本体调试任务.

摘要:基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.IER(improved extension rule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需重新调用ER(extension rule)算法,降低了算法的求解效率.通过对子句集的极大项空间的研究,给出了子句集的极大项空间分解后子空间的求解方法.通过对扩展规则的研究,给出了极大项部分空间可满足性判定方法PSER(partial semi-extension rule).在IER算法判定子空间不可满足时,可以调用PSER算法判定子空间对应的补空间的可满足性,从而得到子句集的可满足性,避免了不能判定极大项子空间可满足性时需重新调用ER算法的缺点,使得IER算法更完备.在此基础上,还提出DPSER(degree partial semi-extension rule)定理证明方法.实验结果表明:所提出的DPSER和IPSER的执行效率较基于归结的有向归结算法DR、IER及NER算法有明显的提高.

摘要:研究一类特殊的矩阵分解问题:对由多个对象在一组连续时间点上产生的数据构成的矩阵R,寻求把它近似地分解为两个低秩矩阵U和V的乘积,即R≈U^T×V.有为数众多的时间序列分析问题都可归结为所研究问题的求解,如金融数据矩阵的因子分析、缺失交通流数据的估计等.提出了该问题的概率图模型,进而由此导出了其约束优化模型,最终给出了模型的求解算法.在不同的数据集上进行实验验证了该模型的有效性.

摘要:Extended IF 逻辑是一阶逻辑的扩张,其主要特点是可表达量词间的相互依赖和独立关系,但其命题部分至今没有得到公理化.基于Cirquent 演算方法,给出了一个关于Cirquent 语义(命题水平)可靠完备的形式系统.该系统能够很好地解释和表达命题联结词间的相互依赖和独立关系,从而使Extended IF 逻辑在命题水平得到了真正意义上的公理化.

摘要:提出具有模态词□φ=□₁V□₂φ的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□₁与□₂是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=□₁V□₂φ;框架定义为三元组W,R₁,R₂,模型定义为四元组W,R₁,R₂,I;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果□₁的可达关系R₁等于□₂的可达关系R₂,那么该逻辑的公理化系统变成S5.

摘要:不同于传统的k-Skyband 查询方法,提出一种相互k-Skyband 查询(MkSB),它从对称角度执行Skyline查询,找出所有既在q的动态k-Skyband(DkSB)中又在q的反向k-Skyband(RkSB)中的数据对象.进一步地,为了更好地支持用户决策和数据分析,排序操作被引入到MkSB算法中.因为MkSB 需要执行q的DkSB 和反向RkSB,故它需要遍历索引多次,从而导致了大量冗余的I/O 开销.利用信息重用技术和若干有效的修剪方法,MkSB 将多次的索引搜索合并成单次,极大地降低了I/O访问次数.同时,证明了基于窗口查询的MkSB(WMkSB)算法具有最低的I/O 代价.在真实与合成数据集上的实验结果表明,所提出的算法是有效的且明显胜过基于BBS 的算法,尤其WMkSB 算法具有极少的I/O 开销,通常能够减少95%以上的冗余I/O.

摘要:时间序列shapelets是时间序列中能够最大限度地表示一个类别的子序列.解决时间序列分类问题的有效途径之一是通过shapelets转换技术,将shapelets的发现与分类器的构建相分离,其主要优点是优化了shapelets的选择过程,并能够灵活应用不同的分类策略.但该方法也存在不足:一是在shapelets转换时,用于产生最好分类结果的shapelets数量是很难确定的;二是被选择的shapelets之间往往存在着较大的相似性.针对这两个问题,首先提出了一种简单有效的shapelet剪枝技术,用于过滤掉相似的shapelets;其次,提出了一种基于shapelets覆盖的方法来确定用于数据转换的shapelets的数量.通过在多个数据集上的测试实验,表明了所提出的算法具有更高的分类准确率.

摘要:标签云是社交网站提供在线资源说明与导航功能的一种流行机制.标签选择即从大量标签中选出有代表性的有限标签,是创建标签云的核心任务.标签选择结果的多样性,是影响用户满意度的一个重要因素.信息覆盖度与标签非相似性是在标签选择中引入多样性的两个主要角度.为了进一步提高标签选择结果的信息覆盖度与标签非相似性,提出了3种标签选择方法.在每种方法中,定义了目标函数以同时量化标签集合的信息覆盖度与标签非相似性,并设计了近似算法以求解相应的最大化问题;同时,还分析了近似算法的近似比.利用CiteULike网站与Last.fm网站的标注数据集,将所提出的方法与已有方法进行了比较.实验结果表明,所提出的方法在信息覆盖度与标签非相似性方面都具有较好的效果.

摘要:网络演化分析与事件检测,是当前社会网络研究的热点和难点.现有的研究工作主要是针对网络提出不同的模型,并用网络特征指标对仿真结果进行评价.这些方法存在如下问题:(1) 每种方法仅针对特定网络,通用性不高;(2) 特征指标多种多样,不同模型的表现情况缺乏统一的评价标准;(3) 未考虑网络演化的时间特性,难以描述网络演化的波动性,无法检测事件.针对上述问题,提出一种基于链路预测的社会网络事件检测方法LinkEvent(由相似性计算算法SimC和事件检测算法EventD组成),它可以对不同网络的波动性进行统一评价,并依此建立事件检测模型.主要工作包括:(1) 证明了链路预测可以反映网络演化机制,相同机制下的模型演化法和链路预测在分析网络演化上具有内在的一致性;(2) 基于链路预测,提出一种网络相似性计算算法SimC(similar computing),并在考虑微观因素的基础上进行改进;(3) 利用相似性计算结果,提出一种事件检测算法EventD(event detecting)检测出新事件.在不同特征的网络上进行实验,结果表明:所提出的LinkEvent方法能够较好地解决网络演化波动性问题,实现事件检测;同时也证明了利用链路预测技术进行网络演化分析的可行性以及相似性计算和事件检测算法的有效性.

摘要:网络层析成像能够在网络内部节点不提供测量协作的情况下,根据端到端的测量结果,间接地估计网络内部链路性能参数,是一种重要的网络测量手段,能直接指导网络管理和网络优化,目前受到国内外学术界和工业界广泛的关注.在广泛收集国内外资料的基础上,首先总结了目前网络层析成像使用的主要端到端测量方法和技术;再根据不同参数对链路性能刻画程度的不同,将链路性能参数的网络层析成像方法分为两类:定量参数推断方法和定性参数推断方法;然后,针对不同类型参数的估计问题,概括分析了现有算法的特点;最后指出该类方法未来的研究方向与潜在的应用前景.

摘要:由于位置感知移动电子设备的繁荣,位置服务(LBS)几乎在所有的社会和商业领域广泛流行.虽然LBS给个人和社会带来了巨大利益,但也给用户的隐私造成了严重威胁.因为用户享受LBS的同时需要向不可信的LBS提供商泄露其位置和查询属性,而附加在这些信息上的上下文揭露了用户的兴趣爱好、生活习惯、健康状况等.如何保护用户的隐私免受恶意提供商的侵犯,对LBS生态系统的健康发展至关重要,因而引起了研究者的广泛关注.对LBS隐私保护的研究现状与进展进行综述.首先介绍LBS隐私的概念和威胁模型;然后,从系统结构、度量指标、保护技术等方面对现有的研究工作进行细致的分类归纳和阐述,重点阐述当前LBS隐私保护研究的主流技术:基于扭曲法的隐私保护技术;通过对各类技术性能和优缺点的分析比较,指出了LBS隐私保护研究存在的问题及可能的解决方法;最后,对未来研究方向进行了展望.

摘要:为增强TCM芯片间密钥的互操作性,TCM提供了密钥迁移相关命令接口,允许用户设计密钥迁移协议以实现芯片间密钥的共享.通常,TCM密钥迁移协议以目标TCM上的新父密钥作为迁移保护密钥.研究发现,该协议存在两个问题:对称密钥不能作为被迁移密钥的新父密钥,违背了TCM的初始设计思想;缺少交互双方TCM的相互认证,导致源TCM的被迁移密钥可以被外部敌手获得,并且敌手可以将其控制的密钥迁移到目标TCM中.针对上述问题,提出两个新的密钥迁移协议:协议1遵循TCM目前的接口规范,以目标TCM的PEK(platform encryption key)作为迁移保护密钥,能够认证目标TCM,并允许对称密钥作为新父密钥;协议2简单改动了TCM接口,以源TCM和目标TCM进行SM2密钥协商,得到的会话密钥作为迁移保护密钥,解决了上述两个问题,并且获得了前向安全属性.最后,使用形式化分析方法对上述协议进行安全性分析,分析结果显示,协议满足正确性和预期的安全属性.

摘要:非结构P2P 网络中,已有的搜索协议对流行资源的搜索是有效的,但对于稀有资源的搜索是低效的.提高稀有资源的副本率,是解决其搜索低效性的根本方法.由于稀有资源在网络中的副本较少,其查询的点击率较低,因此,已存在的基于成功查询的被动副本复制策略不适合稀有资源副本流行度的提高.针对该问题,提出了一种稀有资源的主动复制与搜索策略,由拥有稀有资源的节点主动发起对稀有资源需求信息与需求节点的搜索,在搜索过程中,有效获取局部需求信息,将稀有资源主动复制到有需求的区域内及节点上,从而实现稀有资源的按需复制,有效提高其流行度和点击率.基于局部需求信息,提供3 种不同的按需复制策略,并给出了一种稀有资源搜索算法.实验结果表明:这种稀有资源的主动搜索复制策略能够以较低的复制消耗和网络开销,有效地提高稀有资源的副本率,进而提高稀有资源的点击率.

摘要:无线网络下传统匿名漫游协议中远程域认证服务器无法直接完成对移动节点的身份合法性验证,必须在家乡域认证服务器的协助下才能完成,导致漫游通信时延较大,无法满足物联网感知子网的快速漫游需求.针对上述不足,提出可证安全的物联网移动节点直接匿名漫游认证协议,远程域认证服务器通过与移动节点间的1轮消息交互,可直接完成对移动节点的身份合法性验证.该协议在实现移动节点身份合法性验证的同时,具有更小的通信时延、良好的抗攻击能力和较高的执行效率.相较于传统匿名漫游协议而言,该协议快速漫游的特点更适用于物联网环境.安全性证明表明,该协议在CK安全模型下是可证安全的.