【摘 要】
：
分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提
【基金项目】
：
本文受国家自然科学基金(11271237,11301321),中央高校基本科研业务费专项资金(GK201603086)资助
论文部分内容阅读
分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成
其他文献
多云(Multicloud)无需改变提供商的技术方案及运营方式,以独立于提供商的方式自由组合云资源,是一种认可度较高、具有重要推广价值的互联云模型。云经纪人支持向云提供商和云
介绍了一种电磁悬浮微驱动器的工作原理；针对磁悬浮微驱动器的运动特点，提出了一种基于最大值原理的模糊PID微驱动控制方法，对每种控制单元的输入输出信号与控制参数作了详细分
分析了烘道烘干温度及时间对涂漆零部件漆膜质量的影响，为保证烘道内工件处于最佳的烘干条件，提出了一种在虚拟仪器平台下的烘道高精度多路温度自动测试系统；根据铂电阻传感器的
模拟人的思维特点,分析混凝土搅拌站动态配料系统的控制过程,在系统动态称重配料过程中引入迭代自学习控制策略和预测模型算法控制（MAC）,并对该系统的非线性误差的控制过程进行
为了解决状态监测与故障诊断的统一建模问题，提出一种新型Petri网模型——监测诊断Petri网；首先对状态监测中的特征参量进行了分析，给出了一种实用的模糊隶属度函数形式，接着在基
随着大规模社会网络的发展,链接预测成为了一个重要的研究课题。研究了在社会网络中融合节点属性信息进行链接预测,在传统的社会-属性网络图模型的基础上,将节点属性的类别这
如何更大程度地延长网络的生命周期是设计无线传感器网络路由协议时需要考虑的重要因素。针对此问题,提出一种新型的基于改进粒子群优化的分簇算法。该算法调整了传统粒子群
系外行星的宜居性是近年来探索宇宙的一个热点研究课题,机器学习为系外行星宜居性分类提供了一种可行的手段。然而,现有的宜居性分类效果面临严重不足与局限。为此,给出一种
针对短文本特征词稀疏、表示能力不足等问题,提出了一种基于贝叶斯网的短文本特征扩展方法。该方法根据短文本中特征词之间的依赖关系构建语义贝叶斯网,定义特征词与短文本之
特征选择通过移除不相关和冗余的特征来提高学习算法的性能。基于进化算法在求解优化问题时表现出的优越性能,提出FSSAC特征选择方法。新的初始化策略和评估函数使得SAC能将