基于限界传递相似度图的FCA概念相似度计算方法

使用相似度图计算FCA概念相似度需要构造相似关系的传递闭包,对于复杂问题会导致相似度图规模过大,从而影响相似度评价的效率.为了降低相似度图规模,提出一种基于限界传递相似度图的FCA概念相似度计算方法.该方法首先通过限定传递相似关系的长度来避免构造相似关系的传递闭包,得到的限界传递相似度图中忽略了长度超过界限且对区分FCA概念无用的传递相似关系,能够有效压缩相似度图的规模;然后给出了动态传递相似度计算方法和由限界传递相似度图构建二部图的方法.实验结果表明,使用限界传递相似度图能够在不损失计算结果准确度的情况下有效提高FCA概念相似度计算的效率.     

无界Petri网的可达树的综述

Petri网自提出以来得到了学术界和工业界的广泛关注. Petri网系统的可达性是最基本性质之一.系统的其他相关性质都可以通过可达性进行分析.利用等价的有限可达树来研究无界Petri网可达性,依然是一个开放性问题.该研究可以追溯到40年前,但由于问题本身的复杂性和难度太大,直到最近20年,经过国内外诸多学者的不懈努力,才逐渐取得了一些阶段性的成果和部分突破.本文回顾了近40年来国内外学者为彻底解决该问题作出的贡献.重点对4种开创性的研究成果展开讨论,分别为有限可达树、扩展可达树、改进可达树及新型改进可达树.探讨了今后无界Petri网可达性问题的研究方向.     

不确定规划中可达关系的快速求解算法

在不确定规划领域中,通常需要在同一个不确定状态转移系统中解决多个规划问题,如果能得到不确定规划中状态之间的可达关系即可方便求解该规划问题,然而现有矩阵乘法求解可达关系时存在算法复杂度高的问题。为此,设计一种快速求解不确定规划中状态之间可达关系的算法,将确定动作和不确定动作区分处理,先求解所有确定动作的可达关系,再采用链表和队列求解不确定动作的可达关系。实验结果表明,与矩阵乘法相比,该算法能得到更全面的可达关系,且求解效率更高。     

A Reduced Reachability Tree for a Class of Unbounded Petri Nets

As a powerful analysis tool of Petri nets, reachability trees are fundamental for systematically investigating many characteristics such as boundedness, liveness and reversibility. This work proposes a method to generate a reachability tree, called ωRT for short, for a class of unbounded generalized nets called ω-independent nets based on new modified reachability trees (NMRTs). ωRT can effectively decrease the number of nodes by removing duplicate and ω-duplicate nodes in the tree, and verify properties such as reachability, liveness and deadlocks. Two examples are provided to show its superiority over NMRTs in terms of tree size.      

EPr／TN网可达性分析的冗余并发后继标识

文中针对ＥＰｒ／ＴＮ网在可达性分析时出现的冗余发后继现象，从产生原因入手，给出一种解决算法，并由此深入这种扩展Ｐｅｔｒｉ网固有不完备性，最后提出了改进方法。     

Efficient SAT-based bounded model checking for software verification

This paper discusses our methodology for formal analysis and automatic verification of software programs. It is applicable to a large subset of the C programming language that includes pointer arithmetic and bounded recursion. We consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. We perform this analysis via a translation to a Boolean circuit representation based on modeling basic blocks. The program is then analyzed by a back-end SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program.     

间歇式化工系统的Petri网优化调度与控制方法

为了解决复杂间歇式化工系统的优化调度和控制问题,提出了一种基于Petri网的优化调度与控制方法:首先,根据加工工艺,建立加工过程的赋时Petri网模型;其次,根据间歇式化工生产对象的拓扑结构,在该赋时Petri网模型中引入阀门系统的网结构,从而获得系统的受控Petri网模型;最后,利用可达图来计算加工时间最短的控制策略,借助网结构信息,得到了控制策略的阀门控制矩阵,并用一个示例演示验证了本文方法.     

概率布尔控制网络的弱能控性

本文研究了概率布尔控制网络的弱能控性,系统的弱能控性是概率布尔网络精确能控的一个推广.首先利用矩阵的半张量积和逻辑变量的向量表示,概率布尔控制网络被表示为离散时间动态系统.接着给出概率布尔控制网络弱能控的定义,从离散时间系统的结构矩阵出发,构造了最大概率转移矩阵,矩阵中的元素表示相应状态之间可能发生转移的最大概率,在此基础上研究了概率布尔控制网络的弱能控的条件,同时给出了两个状态弱能达时控制序列的设计算法.最后通过例子进一步解释了弱能控的概念和控制序列设计算法的有效性.     

标记迁移系统的组合可达性分析

标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描述和精确表达。本文对其基本原理进行了分析和概括,并作了形式化陈述,证明了相关结论。本文的工作有助于深入理解和澄清组合可达性分析的内部工作机制。     

极小极大加系统(F,G,H)的输出反馈镇定

研究了一般化非自治非线性极小极大加系统的输出反馈镇定问题.首先,提出了闭环系统单极大射影系统表达式.其次,研究指出闭环单极大射影子系统存在严格的颜色匹配关系.接着,针对颜色匹配的复杂情况,提出新的着色图构造.以往对闭环单极大射影子系统中出现的新增圈研究,仅涉及含有一条反馈弧的圈,本文指出新增圈中可能包含由多条反馈弧构成的圈.最后,根据新着色图和新增罔特点得到了系统输出反馈镇定的一个充分条件.