基于偏序约简的智能电网大数据预处理方法

针对电力一次系统和电力信息系统的数据所具有的多维度、时空混杂等特征,建立了一种基于偏序约简的大数据属性约简预处理方法。该方法综合利用了MapReduce的可并行化优点,着眼于并发事件间的独立性,可以满足电力大数据属性维度与约简方面的覆盖要求。最后,分别以某光伏发电系统监测数据、变压器故障诊断数据和智能变电站通信系统实时性与可靠性预测数据为例,对属性约简进行模拟计算,并通过Hadoop平台进行测试,表明所提出的电力大数据属性约简方法性能优良。

不完备区间值信息系统中的粗集理论

针对不完备区间值信息系统,提出了一种用于分类的偏序关系,并给出了计算这种偏序关系约简的实际操作方法。在不完备区间值决策系统中,根据基于偏序关系的粗糙集模型,引入了上、下近似约简的概念。上、下近似约简是保持所有决策类的下、上近似都不发生变化的最小属性子集,借此获取简化的决策规则。

嵌入偏序约简的状态事件线性时序逻辑验证

模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.

基于偏序归约的状态空间约简算法

目前,针对安全协议分析的偏序归约算法较为复杂且不易实现,限制了其适用范围,未考虑约简诚实主体会话中的逆序结点。针对该问题,采用偏序归约的思想,提出一种诚实主体会话中逆序结点的约简算法以及一种迹等价迁移冗余后继结点的约简算法。两种算法思想简单,易于实现。实例表明,这两种算法有效地约简了安全协议的状态空间。

不协调格值目标信息系统的近似约简

针对不协调格值目标信息系统的属性约简问题,提出不协调格值目标信息系统上近似约简与下近似约简的概念,并得到2种约简的判定定理。给出求解上、下近似约简的辨识矩阵及约简方法。通过实例验证得出,该约简方法具有实效性,格值目标信息系统的值域最为广泛,适用于由属性值域构成格的信息系统。

模型检测新技术研究

Model checking is an algorithmic verification technique that checks automatically whether a given finite state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space explosion problem. In this paper, several important approaches have been proposed for dealing with the state explosion problem. Such approaches are symbolic, abstraction, partial-order reduction, compositional reasoning, etc. Then,a number of way are proposed for verifying real-time and hybrid systems using model checking. At last, several approaches combining model checking and other verification techniques or mathematical methods are consid- ered.

安全协议状态空间的束动作偏序约简算法

目前安全协议分析的偏序归约算法较为复杂、不易实现,限制了其适用范围,且以动作为基础,粒度较小,对减少状态空间的作用有限。针对该问题提出了一种束动作偏序约简算法,将同一会话中的动作序列看做一个束动作,根据攻击者截获的消息与攻击者知识集间的关系,判断迹等价的束动作迁移所到达的后继状态是否为冗余节点,以约简状态空间。该算法思想简单、易于实现;实例表明它有效地约简了安全协议的状态空间。

基于偏序约简程序可达图的并发程序切片方法

并发程序切片是一种重要的并发程序分析手段.基于程序可达图可构造以程序状态和语句二元组为节点的、依赖关系具有可传递性的并发程序依赖图,解决依赖关系的不可传递性问题,提高切片精度.程序可达图通过交织执行模拟并发活动,分析代价较高.偏序约简是一种十分有效的并发系统状态空间约简技术,约简的并发系统状态空间包含所有的并发程序执行代表.为提高效率,该文将偏序约简技术扩展到程序可达图的约简中,在偏序约简理论的基础上,证明了基于未约简和约简的并发程序可达图构造的并发程序依赖图在进行切片计算时是等价的.实验结果表明,采用偏序约简技术使基于程序可达图的并发程序切片方法在保证切片精度不受损失的前提下显著提高切片效率.与其它高精度切片方法相比,基于约简程序可达图的切片方法的精度更高,在大多数情况下,切片效率也有一定提高.

基于偏序关系的粗糙集规则提取方法

规则提取算法中通常先约简属性再约简属性值,但该算法当属性数量增多时,会增加约简的复杂性,从而影响规则提取的速度.针对此问题,本文提出了一种基于偏序关系的粗糙集规则提取方法.首先,在不同粒度的知识空间上建立偏序关系;然后,利用各知识空间中隐含的属性冗余度作为启发式信息,对冗余属性进行逐层约简;最后,在约简后的属性集上提取决策规则.实例表明,该方法降低了属性约简的复杂性,提高了规则提取的速度.

任意阶PDE降噪特性分析

通过对分数阶微积分原理的研究,提出了任意阶偏微分方程(partial differential equations,简称PDE)降噪的统一模型,实现了基于任意阶PDE降噪的数值化方法,并分析了任意阶PDE降噪特性。该数值化方法能够快速实现信号降噪,耗时少。通过仿真实验,分析了PDE降噪性能的影响因素,与其他去噪方法进行了对比分析,并对现场实测信号进行了降噪分析。结果表明,PDE数值求解降噪方法性能优良,算法简单。

基于覆盖约简的粒度空间及粗糙集模型研究

在覆盖粗糙集的并可约粒度空间模型研究中,针对从覆盖到基的约简规则,结合偏序关系的哈斯图,给出一种对覆盖约简的新方法.另外,在并可约粒度空间上讨论了粗糙集模型的相关性质.

模型检测中的偏序约简

检查并发系统的性质变得日益困难。随着验证方法的发展,一些复杂系统并发性越来越高,越来越难以理解。偏序约简方法被提出以减少自动验证并发系统所需要的时间和内存。文中介绍了偏序约简技术的主要概念和基本算法,介绍了其在LTL中的应用,提出了改进方法。

基于CEGAR偏序化简的并行程序死锁检测

针对并发程序的模型检测存在大量的冗余交互和严重的状态空间爆炸问题,提出以迁移标记系统为建模语言计算Persistent Set并完成偏序化简的算法。将算法和CEGAR算法结合起来,实现对并发C程序的并行死锁检测。结果证明该算法在减缓状态空间爆炸和模型验证的效率方面较以往的算法有所提高。

基于偏序简化的并发系统验证

构件交互风格和交互协议的描述与验证是基于构件的分布式系统开发的基础和关键,而构件交互协议是一种典型的分布式并发系统。传统的方法难以解决系统建模和验证中的所谓的状态爆炸问题。偏序简化是应用迹的概念,对模型进行化简并且对模型进行死锁验证。但这样的验证重点放在了Petri网模型上,而没有涉及进程代数模型,所验证的只是模型是否有死锁状态。而以通信系统演算CCS为代表的进程代数,因其概念简洁,可用的数学工具丰富,在分布式并发系统的规范、分析、设计和验证方面获得了广泛应用。对此,提出将偏序规约应用于进程代数模型,给出基于进程代数模型的偏序简化算法,并提出利用进程代数模型偏序简化算法来验证安全性的方法。

基于粗糙集理论偏序决策表知识获取方法研究

介绍了基于偏序关系的偏序决策表,研究了偏序决策表各条件分类和决策分类集合之间的关系,提出了从各分类中计算偏序决策表核及属性约简方法,通过实例,验证了这些方法的有效性。

收缩候选回溯集的有状态动态偏序归约方法

在验证多线程并发程序时,将基于无状态或有状态搜索的软件模型检测与动态偏序归约方法相结合,能大幅缩减待验证程序的状态空间,而动态偏序归约需不断利用当前候选回溯集更新相应回溯集,导致更新回溯集的计算成本过高。为此,形式化定义收缩候选回溯集,消除原候选回溯集中满足同一回溯条件的冗余迁移。针对各交织的回溯点,使用当前收缩候选回溯集更新相应回溯集,实现基于有状态动态偏序归约方法的并发多线程程序验证。实验结果表明,与现有动态偏序归约方法相比,该方法能减少遍历迁移数,加速回溯集更新,提高动态软件模型检测效率。

区间值模糊决策序信息系统的部分一致约简

实际问题中,事物的一些属性值介于某个范围之间,常被用来刻画信息系统中的不确定信息。为了表达这种情况,属性值通常用模糊区间来表示,这种信息系统就是区间值模糊信息系统。本文通过在带有决策的区间值模糊信息系统中引入优势关系,建立区间值模糊决策序信息系统。在此基础上构造部分一致函数来简化知识的表达,并获得部分一致约简的判定定理,通过可辨识属性集和可辨识矩阵提供不协调的区间值模糊序信息系统的部分一致约简的具体方法,并结合投资风险这一具体案例的求解分析,进一步阐述了对部分一致约简研究的意义,丰富了区间值模糊序决策信息系统中的粗糙集方法。

模糊语言属性偏序结构图的逐层属性约简算法

在形式概念分析中,属性偏序结构图作为一种数据可视化工具,可有效解决用户认知过载的问题.在现实生活中,人们往往通过模糊语言值表达偏好信息,会产生大量的模糊语言值数据.为了解决在模糊语言环境下的属性约简问题,文中提出模糊语言属性偏序结构图的逐层属性约简算法.首先,基于模糊语言值形式背景构建模糊语言属性偏序结构图,将模糊语言值数据嵌入属性偏序结构图中.通过语言真值格蕴涵代数作为模糊语言值表示模型,表达模糊语言值间的序关系和不可比关系.然后,为了获取保持模糊语言值形式背景区分能力不变的最小属性子集,结合模糊语言值属性偏序结构图,搜索未与底层节点建立边的节点.在保证模糊语言值属性偏序结构图类等价的前提下,计算该节点及其子节点间的差别属性,并构造相应的逐层属性约简模型.最后,通过实例与对比实验验证文中算法的有效性和实用性.

基于偏序规约技术的网络程序JPF验证

为了减少网络程序模型检测过程中产生的系统状态数目,提出了一种架构感知偏序规约方案。针对目前模型检测器JPF内置的偏序规约机制不能够识别出线程启动时产生的冗余状态问题,设计了一种可应用于JPF的网络程序模型检测的解决方案。该方案通过消除线程启动时产生的冗余路径,有效减少了检测过程中产生的状态空间。实验结果表明,该方案能够有效消除对冗余状态的检测,减少了JPF对网络程序进行模型检测时产生的状态数。

并发错误动态检测方法

针对并发程序路径分支多、状态空间大导致并发错误检测时间长且效率低下的问题,在动态偏序化简算法的理论基础上,提出一种分布式的并发错误动态检测方法。该方法包括一个负载均衡节点和若干个计算节点,分别运行负载均衡算法和分布式动态偏序化简算法,依靠分布式系统强大的计算能力,提高并发错误检测的效率。实验结果表明,相对于动态偏序化简算法,该方法极大地缩短了并发错误的检测时间。