装配几何可行性判别的符号OBDD技术研究

采用了有序二叉决策图(OBDD)描述装配几何可行性,给出了装配操作及其几何可行性的符号表示,设计了装配操作几何可行性的符号OBDD判别算法,给出了装配几何可行性的研究实例,开发了装配的原型系统以支持装配规划,原型系统运行结果表明符号OBDD技术用于装配几何可行性判别的有效性。     

一种基于熵的OBDD变量排序算法

有序二叉决策图（OBDD）是一种有效表示布尔函数的数据结构，其大小依赖于所采用的变量序。熵是定量描述布尔函数中变量重要性的一种方法。基于变量的熵值分析了高质量变量序的特征，给出了一种基于熵的OBDD变量排序算法。实验结果表明：该算法与模拟退火算法和遗传算法结果相当。时间仅为相应算法的80．84％和29．79％。     

概率非否认协议的模型检测分析

基于概率模型检测技术，建立了需要保证ε-公平性的非否认协议的概率模型，根据不同行为将主体建立有限状态机模型。使用概率模型检测器PRISM，验证了概率非否认协议的有效性、公平性和时限性。在恶意实体能力和网络环境等不同情况下，分析了破坏协议公平性的概率。     

Petri网的符号ZBDD可达树分析技术

Petri网是一种适合于并发系统建模、分析和控制的图形工具.可达树是Petri网分析的典型技术之一,它通过标识向量集合表征系统的状态空间,组合复杂性严重制约了该分析技术可处理系统问题的规模.零压缩决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)是一种新型的数据结构,是表示和处理稀疏向量集合的一种有效技术.文章基于Petri网町达标识向量的稀疏特征,给出了Petri网分析的符号ZBDD技术,该技术通过对标识向量(状态)的布尔向量表示、可达标识向最(状态)的符号ZBDD生成,实现Petri网可达状态空间的高效符号操作和紧凑符号表示.实验表明,基于ZBDD的符号可达性分析算法能够有效处理较大规模Petri网问题.     

基于时态认知逻辑的Web服务模型检测

传统模型检测技术主要采用时态逻辑描述被验证的规范,人们较少注意多智能体认知逻辑的模型检测问题.而在分布式系统领域,系统和协议的规范很适合用认知逻辑来描述.Web服务是一个典型的分布式系统.把Web服务组合建模为多智能体系统,并成功采用我们实现的时态认知逻辑符号模型检测工具MCTK验证了SAS股票分析服务实例.同时采用WSAT,WS-Engineer和SPIN 3个模型检测工具在相同实验环境下验证了该实例,实验结果表明我们的Web服务模型检测方法不仅比这3个模型检测工具更高效,而且支持认知逻辑规范的验证,这是这3个模型检测工具所不具备的.     

控制系统软件的方法论设计

现代计算机技术、ＶＬＳＩ技术的发展为复杂,高级 控制系统的实现提供了良好的机遇,而这一机遇却被该类系统设计过程中所遇到的困难所平衡,控制系统软件的设计与开发则是所要克服的主要困难之一,从软件工程角度提出了控制系统软件的方法论设计思想,并对有关问题进行了讨论。     

基于分支程序逆向评估的安全多方计算

针对传统决策函数表示计算复杂度高、编码规模大、参与者局限于2方问题,提出一个基于边值二叉决策图和分支程序逆向评估的解决方案。引入边值二叉决策图(EVBDD)技术,给出一种基于 EVBDD的安全2方计算协议;引入分支程序逆向评估方法,将安全计算参与者由传统的2方扩展到多方;借助基于边值二叉决策图的安全计算协议为基础协议,设计一个基于分支程序逆向评估安全多方计算协议;对协议的正确性、安全性和效率进行分析。与现有解决方案相比,新协议提高了效率,弥补了因隐私泄漏出现的安全问题。     

基于社会新闻数据集的伦理行为判别方法

人工智能(artificial intelligence,AI)应用的伦理风险和挑战引起了人们的普遍关注,如何从技术实现角度开发出遵守人类价值观和伦理规范的AI系统,即,符合伦理的AI设计,是亟需解决的重要问题之一.基于机器学习的伦理与道德判别是此方面的有益探索.社会新闻数据具有丰富的伦理和道德的内容及知识,为机器学习的训练数据开发提供了可能.鉴于此,本文构建了具有人类行为伦理和道德属性的社会新闻数据集,附之以法律与行为规范数据集,用以机器学习的训练和测试;建立了基于使用信息实体的增强语言表示(enhanced language representation of information entities,ERNIE)和卷积神经网络(convolutional neural network,CNN)的伦理行为判别模型ERNIE-CNN,通过词的向量表示计算语义相似度来提取关于行为的伦理判断.实验结果表明,提出的模型具有比基准模型更好的性能,验证了方法和模型的有效性.     

基于OBDD的多方信息安全比较相等协议

针对现有解决方案计算复杂度高、编码规模大以及因明文数量限制而导致的密文碰撞的安全问题,利用基于OBDD的安全函数评估协议和加法同态加密机制,提出一个新的多方信息安全比较相等协议,并分析了该协议的安全性、正确性和效率。该协议对参与者的私有信息采用常规的二进制编码,利用基于OBDD的安全函数评估协议对参与者的私有信息进行评估,并利用加法同态加密机制计算具有相等私有信息的参与者数目。与已有解决方案相比,该协议不仅降低了计算复杂度,而且弥补了已有解决方案存在的安全问题,并具有良好的可扩展性。     

一类约束语言的上限能控子语言进一步讨论

事件与状态为离散事件动态系统的二特征量，状态的逻辑演化关系可用有限自动机模型来描述，系统的逻辑运行特性则为事件集上的事件串（序列）。受禁状态集或（和）受禁事件串集为离散事件动态系统的一类重要性能指标。Ｌｉｎ等对其首先进行了讨论，给出了受禁状态集或（和）受禁事件串集约束语言指标的上限能控子语言及其该指标下离散事件动态系统监控器综合的计算方法。在对该类约束语言的上限能控子语言展开了进一步的讨论同时，修