移动环境公平支付协议的设计与分析研究

结合固定网络中的支付协议并充分考虑移动装置和无线网络的特点,提出了一种移动环境公平支付协议。利用模型检验工具对协议进行分析并将该协议与其他支付协议进行比较,分析和比较结果表明,该协议具有公平、保密、高效等特点,适用于移动环境。     

基于模糊逻辑的CCPN瞬时引发速率求解方法

瞬时引发速率是连续Petri网模型分析的基础和关键。引入模糊理论提出了一种基于模糊决策的迁移优先权的模糊综合评价模型，实现了迁移优先权的动态计算。提出了基于线性规划方法的瞬时引发速率的求解算法，解决了有效冲突情形下瞬时引发速率的求解问题。实例表明了所提出方法的有效性。     

基于有序二叉决策图的装配序列符号表示方法

通过建立装配状态的二进制编码和装配操作的布尔特征函数,给出了装配序列描述的有序二叉决策图(OBDD)方法;建立了从装配序列的与或图模型到OBDD模型的转换规则;并对装配序列表示的与或图模型和OBDD模型进行了存储效率比较.实验结果表明:OBDD方法具有较好的存储性能,可以改善复杂装配体的装配序列表示的存储效率,适合于复杂装配体的可行装配序列的描述.     

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能.     

基于相似性负采样的知识图谱嵌入

针对现有知识图谱嵌入模型通过从实体集中随机抽取一个实体来生成负例三元组,导致负例三元组质量较低,影响了实体与关系的特征学习能力。研究了影响负例三元组质量的相关因素,提出了基于实体相似性负采样的方法来生成高质量的负例三元组。在相似性负采样方法中,首先使用K-Means聚类算法将所有实体划分为多个组,然后从正例三元组中头实体所在的簇中选择一个实体替换头实体,并以类似的方法替换尾实体。通过将相似性负采样方法与TransE相结合得到TransE-SNS。研究结果表明:TransE-SNS在链路预测和三元组分类任务上取得了显著的进步。     

基于ALC的事例库结构及检索研究

为了提高基于ALC的事例检索的效率,通过概念距离及LCS推理给出了索引节点密度大且带权重的事例库层次结构,实现了事例更细致的分类及统一概念距离的语义。根据该结构的组织方式、LCS概念及概念距离给出了事例筛选及相似性度量算法,证明了通过事例筛选得到的候选事例集明显减小,采用相似性度量算法能得到合理的候选事例序列,从而提高了基于ALC的事例检索的效率。     

图编辑距离概述

图编辑距离是图模式匹配技术中常用的方法之一。基于图编辑距离的匹配方法能够处理多种类型的图数据,因而受到了学术界的广泛关注。首先介绍了图编辑距离的相关概念;然后简述了基于启发式搜索技术的精确图编辑距离算法,重点分析了基于二分图匹配的近似图编辑距离算法;最后对现存的一些图编辑问题进行了总结,并对未来的发展趋势进行了展望。     

基于OBDD的描述逻辑εL循环术语集推理

循环术语集推理是描述逻辑研究中面临的难点问题,尚未得到很好的解决.有序二叉决策图（ordered binary decision diagram,简称OBDD）是一种对布尔函数进行紧凑表示和高效操作的数据结构,适用于表示和处理大规模问题.将OBDD应用于描述逻辑循环术语集的推理.首先,针对描述逻辑εL中的循环术语集,给出了描述图上关于最大模拟关系的重要性质,并借助集合表示和集合运算对该性质进行了表述和证明.在此基础上,应用布尔函数对描述图进行编码,给出了基于OBDD求解最大模拟关系的方法,进而给出了最大不动点语义下基于OBDD对概念包含关系进行判定的算法;接下来,基于OBDD给出了求解描述图中可以到达循环路径的所有结点的方法,进而给出了最小不动点语义下基于OBDD对概念包含关系进行判定的算法;最后,对算法的正确性、复杂度等进行了分析和证明,并对算法进行了编程实现,给出了关于计算性能的实验结果.该工作为循环术语集的推理提供了一条有效途径,也为OBDD在逻辑推理中的应用提供了新的案例.     

Statecharts语义问题的若干探讨

Statecharts是一种用以规约复杂反应式系统行为的可视化语言。由于该类系统的行为复杂性 ,定义其精确的语义是困难的。许多人在这方向上对其进行了研究 ,但是仍有些模棱两可的地方。在本文将对 Statecharts语言中什么是一步、迁移的多个条件和动作、不确定性这些语义问题进行探讨。