Structures for Abstract Rewriting

When rewriting is used to generate convergent and complete rewrite systems in order to answer the validity problem for some theories, all the rewriting theories rely on a same set of notions, properties, and methods. Rewriting techniques have been used mainly to answer the validity problem of equational theories, that is, to compute congruences. Recently, however, they have been extended in order to be applied to other algebraic structures such as preorders and orders. In this paper, we investigate an abstract form of rewriting, by following the paradigm of logical-system independency. To achieve this purpose, we provide a few simple conditions (or axioms) under which rewriting (and then the set of classical properties and methods) can be modeled, understood, studied, proven, and generalized. This enables us to extend rewriting techniques to other algebraic structures than congruences and preorders such as congruences closed under monotonicity and modus ponens. We introduce convergent rewrite systems that enable one to describe deduction procedures for their corresponding theory, and we propose a Knuth-Bendix–style completion procedure in this abstract framework.     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

FFT处理机的形式化模型及正确性验证

快速傅立叶变换的应用领域非常广泛,其硬件实现方法多种多样,验证这些电路的正确性具有很强的实用价值。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是随着参与运算的点数的增加,穷尽模拟全部输入情况所耗费的时间越来越长,甚至难以实现。而形式化方法使用纯数学手段证明电路的正确性,克服了传统方法的缺点。首先用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,然后给出它的正确性验证,探索了验证处理复数的复杂电路正确性的方法。     

一种改进的基于约束关系的XML查询重写算法研究

查询重写是解决数据集成、查询优化和物理层数据独立性等问题的关键技术.以往工作主要集中在关系数据模型方面.最近Michigan大学Timber研究小组提出一种全新的基于约束的XML查询重写算法.然而,该算法未考虑存在内定谓词情况下的重写问题,应用范围受到一定限制.在原算法的重写思想基础上,提出了一种基于约束的XML查询重写的改进算法.通过引入映射规则中的约束条件,消除阻碍重写的Skolem函数,从而解决内定谓词问题,增大原算法的应用范围.证明了改进算法的正确性.性能分析和测试结果表明,改进算法并不增加实质性的性能代价.     

一种基于H.264/AVC码流的镜头边界检测方法

H.264/AVC作为新一代的视频标准正得到不断的推广,也将被越来越多的用于视频压缩和传输等方面.由于H.264/AVC标准中引入了许多新的特性,因此,传统的基于MPEG-1/2码流的压缩域镜头边界检测算法不再适用.本文根据宏块运动矢量信息、参考帧信息和4×4DC图,提出了一种在H.264/AVC码流上检测镜头边界的算法.实验结果表明,提出的镜头检测算法,不仅能很好地检测切变还能有效地检测渐变,达到了很好的检测效果.     

H.264/AVC快速帧间模式选择研究

在帧间预测编码过程中,常采用多种模式和多参考帧进行精确的运动估计,使用穷举搜索模式选择算法获取最佳模式,提高H.264/AVC的率失真性能,但穷举搜索的计算量非常大.该文研究了快速模式选择算法,改进了H.264时间效率、提高了实时性,提出了模式选择优化算法的基本思路,讨论了几种有代表性的快速帧间模式选择算法,分析了各种快速算法的优化依据和性能,探讨了快速帧间模式选择算法的研究方向.     

H.264 CABAC加速器的设计

H.264主要档次采用的CABAC熵编码技术在提高视频压缩比率的同时,严重增加了编/解码的计算复杂度,嵌入式系统由于其低成本低功耗的要求,需要专用硬件加速器来进行CABAC编/解码。设计了一个高性能H.264 CABAC硬件加速器,该加速器可配置为编码或解码模式,高效地实现CABAC编/解码操作。通过性能评估实验,在220 MHz时钟频率下,该加速器能够实现平均147 Mbps(1.5 cycle/bit)的编码速度和220 Mbps(1 cycle/bit)的解码速度。与软件实现相比,加速器获得50倍以上的性能提升。     

一种针对H.264/AVC中4×4块的快速帧内预测模式选择算法

帧内预测模式计算量很大,确定一个MB的预测模式需要耗费上百种组合模式的RD代价,因此有必要研究RDO模式下的快速帧内预测模式选择快速算法.本文提出了针对4×4块的帧内预测快速三步算法,利用不同预测方向间RD值的紧密联系可以有效找到最小值周围的预测方向,从而跳过其他不可能的预测模式.此算法仅仅需要检测6种模式,而全搜索算法为9种模式.仿真结果显示,该算法能够获得和全搜索相似的PSNR质量,仅增加约1%比特率.     

H．264／AVC中的CABAC编码技术

CABAC是新一代视频压缩算法标准H.264/AVC中采用的新熵编码技术,使用它可以有效提高编码效率,节约码流。这里介绍了CABAC编码中算术编码理论的原理和内容模型的基本类型,并以运动矢量差值MVD的编码方法为例详细分析了CABAC的编码过程。     

H.264帧间模式选择优化算法

提出一种新的H.264快速模式选择算法：根据块的细节程度和纹理方向选择不同模式集，这些模式集比整个模式集模式数量大大减小，从而提高了模式搜索速度。信噪比的降低与比特率的增加都在可接受范围内，仿真结果证明了算法的有效性。