Efficient two-step digit-set-restricted modified signed-digit algorithm based on optoelectronic shared content-addressable memory

A two-step digit-set-restricted modified signed-digit (MSD) adder based on symbolic substitution is presented. In the proposed addition algorithm, carry propagation is avoided by using reference digits to restrict the intermediate MSD carry and sum digits into {(1) over bar ,0} and {0, 1}, respectively. The algorithm requires only 12 minterms to generate the final results, and no complementarity operations for nonzero outputs are involved, which simplifies the system complexity significantly. An optoelectronic shared content-addressable memory based on an incoherent correlator is used for experimental demonstration. (c) 2005 Society of Photo-Optical Instrumentation Engineers.

Efficient two-step digit-set-restricted modified signed-digit algorithm based on optoelectronic shared content-addressable memory

A two-step digit-set-restricted modified signed-digit (MSD) adder based on symbolic substitution is presented. In the proposed addition algorithm, carry propagation is avoided by using reference digits to restrict the intermediate MSD carry and sum digits into {(1) over bar ,0} and {0, 1}, respectively. The algorithm requires only 12 minterms to generate the final results, and no complementarity operations for nonzero outputs are involved, which simplifies the system complexity significantly. An optoelectronic shared content-addressable memory based on an incoherent correlator is used for experimental demonstration. (c) 2005 Society of Photo-Optical Instrumentation Engineers.

Mathematical symbols and computing methods in high dimensional biomimetic informatics and their applications

High dimensional biomimetic informatics (HDBI) is a novel theory of informatics developed in recent years. Its primary object of research is points in high dimensional Euclidean space, and its exploratory and resolving procedures are based on simple geometric computations. However, the mathematical descriptions and computing of geometric objects are inconvenient because of the characters of geometry. With the increase of the dimension and the multiformity of geometric objects, these descriptions are more complicated and prolix especially in high dimensional space. In this paper, we give some definitions and mathematical symbols, and discuss some symbolic computing methods in high dimensional space systematically from the viewpoint of HDBI. With these methods, some multi-variables problems in high dimensional space can be solved easily. Three detailed algorithms are presented as examples to show the efficiency of our symbolic computing methods: the algorithm for judging the center of a circle given three points on this circle, the algorithm for judging whether two points are on the same side of a hyperplane, and the algorithm for judging whether a point is in a simplex constructed by points in high dimensional space. Two experiments in blurred image restoration and uneven lighting image correction are presented for all these algorithms to show their good behaviors.

弱互模拟等价类算法改进

大量的硬件和软件系统广泛应用在一些重要的领域，在许多情况下错误和失效是不可接受的。需要提供方法来检验软硬件的正确性，增强我们对软硬件系统的信心。形式化验证提供了提高软硬件可靠性的方法。 互模拟等价类和弱互模拟等价类可以用来降低形式化验证中模型的规模。弱互模拟等价类有两种算法：一种是先计算迁移关系的自反传递闭包，然后调用互模拟等价类的算法。另一种是作为IGPTPartEF的一个特例，直接在原图上用划分精化的方法计算。针对这些计算弱互模拟等价类的算法，我们提出两种改进算法。 首先，我们观察到有些状态在划分精化的过程中不会被再次切分，可以事先将它们归类到一个组，在划分精化过程中以这些组为基本单位进行切分，可以在很大程度上减小算法花费的时间。我们用该思想给设计出了改进算法一。 然后，我们观察在Paige-Tarjan算法中引入了“处理比较小的一半”的思想来改进计算互模拟等价类的算法，它使得计算互模拟等价类的算法的时间复杂度从O(mn)（其中m是边数，n是顶点数）改进到O(mlgn)，而在前面所述的弱互模拟等价类算法中并没有引入“处理比较小的一半”。我们引入这一思想，设计出了改进算法二。 之后，我们设计实现了原型工具，并进行了数据实验来证实算法在时间上与原算法相比有明显改进。

π-演算互模拟判定算法的优化和实现

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

带赋值符号迁移图的局部优化算法

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

一种分布式吴方法计算模型

吴方法是由我国科学家吴文俊院士开创的一个新兴研究领域.考虑到吴方法"分而治之"的思想非常适合分布式计算,将分布式计算技术引入到该方法的计算过程中,给出一种既可以在集群环境下,也可以在网格环境下实现的分布式吴方法计算框架.首先分析了吴方法分布式计算需求,并以特征列计算为例来说明吴方法分布式计算算法,然后讨论了符号计算基本数据类型:大整数和多项式的消息传递方法,最后简单给出了在网格环境下基于符号计算软件系统ELIMINO和网格中件间Globus Toolkits 3的分布式吴方法计算环境的设计、实现与实验结果.

参数化系统安全性的启发式符号验证

参数化系统(paramterized system)是指包含特定有限状态进程多个实例的并发系统,其中的参数是指系统内进程实例的数目,即系统的规模.反向可达性分析(backward reachability analysis)已被广泛用于验证参数化系统是否满足以向上封闭(upward-closed)集合表示的安全性(safety property).与有限状态系统验证相类似,参数化系统的验证同样也面临着状态爆炸(state explosion)问题,并且模型检测算法的有效性依赖于如何采用有效的数据结构表示状态集合.针对表示无穷状态的向上封闭集合,研究人员提出了多种基于约束(constraint-based)的符号表示方法.但这些方法依然面临着符号状态爆炸(symbolic state explosion)问题或者其包含判定问题,即判断一个约束条件集合符号化表示的实际状态集合是否为另一约束条件集合所对应的状态集合的子集,是Co-NP完全问题.因此,虽然有限状态验证技术能够验证一些具有一定规模的问题,但现有针对参数化系统的验证方法所能解决的问题的规模较为有限,需要近一步提高模型检测算法的效率.针对参数化系统提出了加快反向可达性分析的多个启发式规则,实验结果表明,这些启发式规则可以使算法的效率提高几个数量级,从而有助于解决现有参数化系统验证方法所存在的问题.