基于双格的多值模型的精化关系与对称化简

多值模型是传统布尔模型的扩展。与布尔模型相比,多值模型更适合对包含不确定和不一致信息的软件系统进行建模。为了解决模型检测时的状态爆炸问题,研究了对基于双格的多值模型的对称化简方法。提出了一种新的多值模型的精化关系,证明其保持对[μ]演算公式的模型检测结果的正确性。定义多值模型的对称化简商结构,证明商结构与原模型之间存在互为精化的关系,因此对[μ]演算公式的模型检测在二者上可以得到相同的结果。     

多智能体系统可控性的图论刻画

研究领航者-跟随者结构多智能体系统的可控性问题.利用松弛的等价分化刻画了系统可控性与信息拓扑结构之间的关系,为系统可控性提供了基于图论的判别方法.基于置换群理论将对称的概念推广到多领航者系统,并证明了3种图论工具（对称性、等价分化和松弛的等价分化）之间的包含关系.仿真结果验证了所提出方法的有效性.     

对称轮轨系统的“合成分岔图”法

定义对称轮轨系统对称性分岔的概念,由数值积分得到系统的时间响应并建立对称轮轨系统的离散动态Poincare映射截面及其对称截面,提出"合成分岔图"的构造方法,应用该方法对一两轴转向架系统运行与理想平直轨道上的对称/不对称分岔行为和混沌运动进行分析.在研究速度范围内,发现系统存在大量的对称运动形式,也存在很多的不对称运动形式,系统的对称性刚开始是通过不可捉摸突变而破坏的.     

对称布尔函数的算术相关函数

算术相关函数是最近提出的一种研究布尔函数密码学性质的方法,该方法通过定义多元2-adic数上的加法和乘法运算,构建一种新的环结构,实现对经典相关函数的带进位计算的模拟。首先介绍了算术相关函数的定义,并针对具有良好密码学性质的对称布尔函数讨论了其算术相关函数的性质和取值,最后利用对称布尔函数的实值对称性证明了对称布尔函数的算术自相关函数也是一个与向量的重量有关的实值对称函数,至多是n+1值的。     

对称布尔函数的算术相关函数

算术相关函数是最近提出的一种研究布尔函数密码学性质的方法,该方法通过定义多元2-adic数上的加法和乘法运算,构建一种新的环结构,实现对经典相关函数的带进位计算的模拟。首先介绍了算术相关函数的定义,并针对具有良好密码学性质的对称布尔函数讨论了其算术相关函数的性质和取值,最后利用对称布尔函数的实值对称性证明了对称布尔函数的算术自相关函数也是一个与向量的重量有关的实值对称函数,至多是n+1值的。     

基于动态阈值对称差分和背景差法的运动对象检测算法

提出一种基于动态阈值对称差分和背景差法的运动对象检测算法.首先通过建立一个基于统计的可靠背景更新模型,由背景差法得到基本准确的前景图像;然后与用对称差分法得到的差分图像综合;最后得到完整可靠的运动目标图像.中间采用了一种动态的最优阈值获取方法,然后用形态学滤波和连通区域面积检测进行后处理,以消除噪声和背景扰动带来的影响,并用区域填充算法来填补目标区域的小孔,从而将视频序列中的运动目标比较可靠地检测出来.实验结果表明,该方法快速、准确,有一定的实际应用价值.     

基于决策图的复杂系统模型对称约减方法

针对复杂随机系统模型检测过程中的状态空间爆炸问题,提出一种用于支持迁移回报特征描述的概率模型对称约减方法.通过引入状态集等价关系唯一表示函数,约减了原模型中的状态集尺寸;通过加入回报特征描述,改进了传统的多终端二元决策图,用于表示概率回报模型中的迁移关系;基于迁移矩阵,提出了一种高效的对称约减算法,完成了迁移关系的约简.实验结果表明了该方法的可行性与有效性.     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

一种通用的局部内蕴对称检测算法

局部内蕴对称在三维几何体中更具一般性,其检测对形状分析具有重要意义,但由于其求解的复杂性,使得局部内蕴对称的检测非常困难.文中面向三维网格模型,提出一种包括反射和平移等变换的通用局部内蕴对称检测算法.该算法使用选举和谱分析方法以及迭代精化对称对应矩阵,求解出更加精确、通用的局部内蕴对称性;进一步,根据对称检测结果对模型进行分割,得到有意义的分割结果.实验结果表明,采用文中算法可以正确地求解出通用的局部内蕴对称性,并能在通用对称属性引导下生成有意义的模型分割结果.     

动态商拓扑模型及其在路径查找中的应用

为解决动态环境下的问题求解,针对拓扑结构随时间变化的情况,文中借鉴社会学中的信任模型扩展传统的商空间理论,利用贝叶斯方法评估节点的可信度,提出一种基于信任机制的动态商拓扑模型.将该模型应用于最佳路径查找.仿真结果证实,该模型能以较小的时间花费为代价,有效提高路径可靠性,实现动态问题求解.     

Vector Symmetry Reduction

Symmetry reduction is an effective state-space reduction technique for model checking, and works by restricting search to equivalence class representatives with respect to a group of symmetries for a model. A major problem with symmetry reduction techniques is the time taken to compute the representative of a state, which can be prohibitive. In efficient implementations of symmetry reduction, a symmetry is applied to a state as a sequence of operations which swap component identities. We show that vector processing technology, common to modern computers, can be used to implement a vectorised swap operation, which can be incorporated into the representative computation algorithm to accelerate symmetry reduction. Via a worked example, we present details of this vector symmetry reduction method. We have implemented our techniques in the TopSpin symmetry reduction package for the Spin model checker, and present experimental results showing the speedups obtained via vectorisation for two case-studies running on a PowerPC vector processor.     

中介命题逻辑的一种无穷值语义模型及其意义

中介逻辑(medium logic, ML)自建立了它的三值语义模型后,ML就被许多学者认定为三值逻辑.对于中介逻辑核心理论的中介命题逻辑系统,给出一种真值域为[0,1]的无穷值语义模型,研究了它的性质,并证明了中介命题逻辑在此模型下具有可靠性与完备性.此模型的存在表明,认定中介逻辑是一种三值逻辑的理由是不充分的.该模型更适合反映中介逻辑的基本思想,而且为中介逻辑在其他领域的应用提供了一个基础.     

Exploiting symmetry in temporal logic model checking

In practice, finite state concurrent systems often exhibit considerable symmetry. We investigate techniques for reducing the complexity of temporal logic model checking in the presence of symmetry. In particular, we show that symmetry can frequently be used to reduce the size of the state space that must be explored during model checking. In the past, symmetry has been exploited in computing the set of reachable states of a system when the transition relation is represented explicitly [14, 11, 19]. However, this research did not consider arbitrary temporal properties or the complications that arise when BDDs are used in such procedures.We have formalized what it means for a finite state system to be symmetric and described techniques for reducing such systems when the transition relation is given explicitly in terms of states or symbolically as a BDD. Moreover, we have identified an important class of temporal logic formulas that are preserved under this reduction. Our paper also investigates the complexity of various critical steps, like the computation of the orbit relation, which arise when symmetry is used in this type of verification. Finally, we have tested our ideas on a simple cache-coherency protocol based on the IEEE Futurebus + standard.This research was sponsored in part by the Avionics Laboratory, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, Ohio 45433-6543 under Contract F33615-90-C-1465, ARPA Order No. 7597 and in part by the National Science Foundation under Grant No. CCR-8722633 and in part by the Semiconductor Research Corporation under Contract 92-DJ-294.The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. government.     

Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking

This work presents a collection of methods that integrate symmetry reduction and under-approximation with symbolic model checking in order to reduce space and time. The main objective of these methods is falsification. However, under certain conditions, they can provide verification as well.We first present algorithms that use symmetry reduction to perform on-the-fly model checking for temporal safety properties. These algorithms avoid building the orbit relation and choose representatives on-the-fly while computing the reachable states. We then extend these algorithms to check liveness properties as well. In addition, we introduce an iterative on-the-fly algorithm that builds subsets of the orbit relation rather than the full relation.Our methods are fully automatic once the user supplies some basic information about the symmetry in the verified system. Moreover, the methods are robust and work correctly even if the information supplied by the user is incorrect. Furthermore, the methods return correct results even when the computation of the symmetry reduction has not been completed due to memory or time explosion.We implemented our methods within the IBM model checker Rule-Base and compared their performance to that of RuleBase. In most cases, our algorithms outperformed RuleBase in both time and space.     

Fast global and partial reflective symmetry analyses using boundary surfaces of mechanical components

Axisymmetry and planar reflective symmetry properties of mechanical components can be used throughout a product development process to restructure the modeling process of a component, simplify the computation of tool path trajectories, assembly trajectories, etc. To this end, the restructured geometric model of such components must be at least as accurate as the manufacturing processes used to produce them, likewise their symmetry properties must be extracted with the same level of accuracy to preserve the accuracy of their geometric model. The proposed symmetry analysis is performed on a B-Rep CAD model through a divide-and-conquer approach over the boundary of a component with faces as atomic entities. As a result, it is possible to identify rapidly all global symmetry planes and axisymmetry as well as local symmetries. Also, the corresponding algorithm is fast enough to be inserted in CAD/CAM operators as part of interactive modeling processes, it performs at the same level of tolerance than geometric modelers and it is independent of the face and edge parameterizations.     

隐含多项式曲线对称性几何特征及其检测研究

隐舍多项式曲线在物体描述和识别中具有许多优点并得到实际应用,因而物体的对称性检测问题可以转换成对隐含多项式曲线的对称性检测来研究。对隐含多项式曲线对称几何结构性质进行了探讨,提出隐含多项式曲线如果是对称的,则其充分必要条件是首二次因子积组成的椭圆图形是对称的,同时指出椭圆图形对称轴就是隐含多项式曲线的对称轴。算法较为简单和直观．实验结果证明算法的有效性和可操作性。     

中介命题逻辑一种新的无穷值语义模型及意义

中介逻辑ML（Medium Logic）,自建立了它的三值语义模型后,ML就被许多学者认定为三值逻辑。对于中介逻辑核心理论的中介命题逻辑系统,潘给出了一种无穷值语义模型,并证明了中介命题逻辑在此模型下具有可靠性与完备性。在此基础上,给出一种真值域为[0,λ)∪(λ,1](λ∈(0.5,1))的无穷值语义模型,研究了它的性质,证明了中介命题逻辑在该模型下也具有可靠性与完备性。新模型的存在进一步表明,认定中介逻辑是一种三值逻辑的理由是不充分的。新模型不仅反映了中介逻辑的基本思想,而且为中介逻辑在其他领域的应用提供了基础。     

Symmetry and Network Structure

In this paper, the auto-association problem is discussed using group theoretical methods. Considering the symmetry group of a given set of test sequences, it is shown to be possible to construct a class of neural networks acting as auto-associators on this set. It turns out that the symmetry of the network structure is already determined by the symmetries of the set of test sequences, indicating that learning a set of elements applied is concerned with finding invariant relations inherent in this set. Moreover, the main result offers the possibility, to construct all optimal network structures and, hence, to decide whether a solution found by a particular learning algorithm is optimal or not.     

基于多子模式的NAM图像表示方法

基于多子模式的非对称逆布局模式表示可以作为一种无损图像表示方法,本文以包括点、直线、矩形和三角形的典型多子模式为研究对象,提出了一种基于多种子模式的NAM图像表示方法.其中,三角形典型子模式包括四种走向的非等腰直角三角形,因此在子模式抽取时需要对三角形进行不等腰处理.本文给出了MNAM的表示思想,对其在计算机内的存储结...