基于悖论分析和增量求解的快速反例压缩算法

使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL(brute force lifting)算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT(boolean satisfiablilty problem)的快速反例压缩算法.首先,根据反证法和排中律原理,该算法对每一个自由变量v,构造一个SAT问题,以测试v是否能够避免反例.而后对其中不可满足的SAT问题,进行悖论分析,抽取出导致悖论的变量集合.所有不属于该集合的变量,均可作为无关变量直接剔除.同时,该算法使用增量式SAT求解方法,以避免反复搜索冗余状态空间.理论分析和实验结果表明,与BFL算法相比,该算法能够在不损失压缩率的前提下获得1～2个数量级的加速.     

变量极小不可满足在模型检测中的应用

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.     

多类有重叠问题的扩张矩阵算法

示例学习是从某一概念的已给的正例集合和反例集合中归纳产生出描述所有正例并排除所有反例的该概念的一般规则,而扩张矩阵理论将寻找正例在反例背景下所满足的公式等价为在反例矩阵上找出一条生路.该文针对多类有重叠问题,改进了原有的扩张矩阵算法,引入了基于平均熵的最短公式近似解的启发式搜索,并利用势函数估计正、反例间重叠区域的概率密度函数,从而获得类间非线性判别界面.文章将此算法应用于手写汉字识别,通过分析比较,论述了改进算法的有效性.     

基于OBDD的SMC反例生成研究

针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量,使得反例难以理解。提出一种改进的反例生成算法,将反例中的状态扩展为一个状态集,使用零压缩二叉决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)来存储所求出的状态集。删除了系统中的无关变量,仅保留了相关的变量,实验表明该算法能有效地减少状态的变量数,减少存储反例所需的空间。     

基于多项式符号代数方法的高层次数据通路的等价验证

基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求.由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法.深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式.从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Gr(o)bner基计算的有效代数求解算法.针对不同基准数据通路的实验结果表明了该算法的有效性.     

基于符号模型检测的符号有向图故障诊断解形式化验证

由于定量信息和非线性因果关系的丢失,符号有向图(SDG)的故障诊断解需要进一步进行校核与验证.将SDG故障诊断解的验证置于符号模型检测框架中进行研究,提出了基于符号模型检测的SDG故障诊断解形式化验证方法.首先定义了SDG模型的有限状态变迁系统形式化描述,建立了符号模型检测(SMV)模型;其次引入故障传播时间定义了模型观测变量的动态验证信息,提出了基于步进式监控的动态推理验证策略;然后扩展了动态推理验证过程的SMV模型,提出了验证算法SSDGFD_SMC;最后,通过一个简单贮水罐系统的SDG模型实例验证了算法SSDGFD_SMC的有效性.     

基于符号运算的归纳变量识别与约化

针对归纳变量的识别及归约问题提出一种基于符号运算的新算法。通过初始变量替换赋值语句中的右值,用以表达变量间的迭代与依赖关系,由此建立有向依赖图用于识别归纳变量。为归纳变量构建递归方程组并利用符号运算进行求解,获得独立的仅依赖于迭代次数的数学形式。实验结果表明,该方法适用于各种复杂的归纳变量,能够解决现有算法无法处理的一些问题。     

面向实时传值系统的局部模型检测

为对实时传值系统进行模型检测，本文给出了时间符号迁移图作为系统的建模语言，以及实时谓词μ演算作为刻画性质的逻辑语言。本文给出了基于时间符号迁移图和实时谓词μ演算的一个模型检测算法，该算法动态生成和检测可达的状态空间，并且采用对数据变量on—the—fly实例化以及动态切分时间计值集合的方法，是一个局部算法。该算法不仅能处理基于有限域的变量，还可处理一类数据域无穷的变量(称“数据无关”变量)。     

反例引导的C代码空间流模型检测方法

软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度难以得到保证.为此,通过结合模型检测与稀疏值流分析方法,设计了一种空间流模型,实现了对C程序在符号变量层面和地址空间层面的状态行为的有效描述,并提出了一种反例引导的抽象细化和稀疏值流强更新算法(CEGAS),实现了C程序指向信息敏感的形式化验证.建立了包含多种指针操作的C代码基准库,并基于该基准库进行了对比实验.实验结果表明:所提出的模型检测算法CEGAS在分析含有多种C代码特性的任务中,与现有模型检测工具相比均能取得突出的结果,其检测准确度为92.9%,每行代码的平均检测时间为2.58 ms,优于现有检测工具.     

用改进的1-DNF算法获取最强反例集合的方法

利用正样例集合和未标识样例集合获取初始的最强反例集合是使用两步框架方法构造一个面向PU问题文本分类器的基础。该文指出了使用1-DNF算法抽取初始的最强反例集合的局限性，提出了对算法1-DNF的改进方法。实验结果表明，与原算法相比，它大大增加了获取的最强反例数目，加快了算法的收敛速度，提高了分类器的精度。     

Computer generation of symbolic kinematics for robot manipulators

Computer generation of symbolic solutions for the direct and inverse robot kinematics is a desired capability not previously available to robotics engineers. In this article, we present a methodology for the design of a software system capable of solving the direct and inverse kinematics for n degree of freedom (dof) manipulators in symbolic form. The inputs to the system are the Denavit-Hartenberg parameters of the manipulator. The outputs of the system are the direct and inverse kinematics solutions in symbolic form. The system consists of a symbolic processor to perform matrix and algebraic manipulations and an expert system to solve the class of nonlinear equations involved in the solution of the inverse kinematics problem. The system can be used to study robot kinematics configurations whose inverse kinematics solutions are not known to exist a priori. Two examples are included to illustrate its capabilities. The first example provides explicit analytical solutions, previously believed nonexistent, for a 3 dof manipulator. A second example is included for a robot whose inverse kinematics solution requires intensive algebraic manipulations.     

The Study of Motion for a Gyroscope with Gimbal Suspension: Obtaining the Highest Approximations for a Drift of Magnus

Here we give a solution to the classic problem of the applied mechanics of the gyroscope. The problem is reduced to using the computer algebra system REDUCE. We show that symbolic computation is very convenient for applied mechanics.     

Performance Prediction in Symbolic Scheduling of Partitioned Programs with Weight Variation

In this paper we consider the symbolic scheduling of partitioned loop programs which are modeled as iterative task graphs (ITGs). Each task in such a graph is coarse grained and contains a large chunk of computations. The weights of computation and communication vary from one iteration to another depending on the index value of the loop. The goal of scheduling such graphs is to incorporate the symbolic variables in weight functions and loop bounds and provide an asymptotically optimal schedule and predict its performance accurately. We provide a lower bound for optimal scheduling when weights of iterative task graphs change monotonically in the course of iterations and there is a sufficient number of processors. We present a technique that devises a valid symbolic schedule without searching all task instances and examine the asymptotic performance of this schedule compared to an optimal solution. Finally, we present case studies and experimental results on nCUBE-2 to verify our solutions.     

基于混合输入的环境交互问题研究

针对软件安全测试中静态符号执行技术难以处理环境交互的问题, 提出了一种基于混合输入的符号执行方法。首先, 定义了程序执行的一致性模型, 系统化地分析了符号执行与实际执行的逼近问题; 接着, 提出了符号执行与具体执行的转换方法及维护一致性的启发式策略; 最后, 通过区分可求解约束和复杂约束条件, 提出了具体值和符号值混合代入法化简复杂约束的路径求解算法。实验结果表明该方法在处理环境交互问题上的可行性和有效性, 扩展了静态符号执行的能力。     

The solution of a nonclassic problem for one-dimensional hyperbolic equation using the decomposition procedure

In this article, we propose a new approach for solving an initial–boundary value problem with a non-classic condition for the one-dimensional wave equation. Our approach depends mainly on Adomian's technique. We will deal here with new type of nonlocal boundary value problems that are the solution of hyperbolic partial differential equations with a non-standard boundary specification. The decomposition method of G. Adomian can be an effective scheme to obtain the analytical and approximate solutions. This new approach provides immediate and visible symbolic terms of analytic solution as well as numerical approximate solution to both linear and nonlinear problems without linearization. The Adomian's method establishes symbolic and approximate solutions by using the decomposition procedure. This technique is useful for obtaining both analytical and numerical approximations of linear and nonlinear differential equations and it is also quite straightforward to write computer code. In comparison to traditional procedures, the series-based technique of the Adomian decomposition technique is shown to evaluate solutions accurately and efficiently. The method is very reliable and effective that provides the solution in terms of rapid convergent series. Several examples are tested to support our study.     

A symbolic interpretation for back-propagation networks

Two main problems for the neural network (NN) paradigm are discussed: the output value interpretation and the symbolic content of the connection matrix. In this article, we construct a solution for a very common architecture of pattern associators: the backpropagation networks. First, we show how Zadeh's possibility theory brings a formal structure to the output interpretation. Properties and practical applications of this theory are developed. Second, a symbolic interpretation for the connection matrix is proposed by designing of an algorithm. By accepting the NN training examples as input this algorithm produces a set of implication rules. These rules accurately model the NN behavior. Moreover, they allow to understand it, especially in the cases of generalization or interference.     

Some new solitonary solutions of the modified Benjamin-Bona-Mahony equation

In this paper, we use the exp-function method to construct some new soliton solutions of the Benjamin-Bona-Mahony and modified Benjamin-Bona-Mahony equations. These equations have important and fundamental applications in mathematical physics and engineering sciences. The exp-function method is used to find the soliton solution of a wide class of nonlinear evolution equations with symbolic computation. This method provides the concise and straightforward solution in a very easier way. The results obtained in this paper can be viewed as a refinement and improvement of the previously known results.     

Using symmetries in the eigenvalue method for polynomial systems

One way of solving polynomial systems of equations is by computing a Gröbner basis, setting up an eigenvalue problem and then computing the eigenvalues numerically. This so-called eigenvalue method is an excellent bridge between symbolic and numeric computation, enabling the solution of larger systems than with purely symbolic methods. We investigate the case that the system of polynomial equations has symmetries. For systems with symmetry, some matrices in the eigenvalue method turn out to have special structure. The exploitation of this special structure is the aim of this paper. For theoretical development we make use of SAGBI bases of invariant rings. Examples from applications illustrate our new approach.