时间自动机与自动验证

给出时间自动机的基本概念,描述了区域自动机的构造方法,并且实现了区域自动机的构造算法.简述了通过时间自动机进行自动验证的过程,最后分析了区域自动机构造算法的时间复杂度.     

多速率混合系统的符号化可达性分析

针对目前还没有专门的数据结构处理多速率混合系统的符号化可达性问题，定义了多速率区域来表示和处理多速率自动机的无穷状态空间，从而把多速率混合系统的符号化可达性分析等价地转化成多速率区域上的3种操作，即并操作、变量重赋值操作和控制状态上的时间流逝操作．从理论上证明了多速率区域在这3种操作上的封闭性，同时定义了矩阵数据结构不同上限矩阵（DCM），并用其存储多速率区域，这样就得到了一种专门处理多速率混合系统符号化可达性分析的数据结构．理论上证得，DCM可以大大降低可达性分析算法的复杂度．     

一种时间自动机时钟离散化算法

稠密时间自动机被广泛应用于实时系统自动验证.然而其在补操作下不封闭,因而导致多种线性实时性质不可验证.离散时间自动机虽不存在此问题,但该模型表达能力偏弱.因此,提出了一种时间自动机时钟离散化算法,结合时钟物理约束因素,证明了新方法可有效解决上述问题.     

一种时间自动机可达性检测方法

本文首先给出对时间自动机时钟约束作等价处理的方法,然后以一个例子详细说明如何构造时钟区域自动机以及对它作相应的可达性关系的分析。     

时间自动机与自动验证

给出时间自动机的基本概念，描述了区域自动机的构造方法，并且实现了区域自动机的构造算法，简述了通过时间自动机进行自动验证的过程，最后分析了区域自动机构算法的时间复杂度。     

确定的与非确定的公式时钟自动机的等价性

本文分析了传统的时间自动机在实时系统进行形式化验证方面所存在的问题,提出了一种新的形式化验证工具——公式时钟自动机,给出了公式时钟自动机的形式化定义。在公式时钟自动机中,每一个事件对应一个命题、并且针对给定命题集上的每个时态公式,我们定义两个时钟:公式记录时钟与公式预测时钟。前者记录公式最近一次被满足时距目前的时间,后者预测下一次公式将被满足时距目前的时间。最后讨论了公式时钟自动机的确定性和非确定性,并证明了确定的公式时钟自动机和非确定的公式时钟自动机的等价性。     

汉字有穷自动机的优化及相关算法研究

在研究了汉字有穷自动机可以表示的语言基础上,引进了最小状态汉字有穷自动机和可区分状态的概念,并利用汉字有穷自动机间的等价性和可区分状态的性质,给出了一种最小化算法,实验证明,此算法优于最小化汉字有穷自动机算法.     

一种基于流的XML查询算法设计与实现

针对密集型数据查询要消耗大量内存的缺陷,设计了一种基于流的XM L文档查询算法.该算法在对XM L流的一次单向读取过程中处理XPath,接收查询表达式,将表达式转换为树形自动机,自动机以流的方式接收并处理XM L文档,同时输出当前处理结果.在查询树状态转换过程中附加了缓存操作,用于保存XM L流中暂时无法判断的文档片段.算法测试表明其占用内存空间基本恒定,不会随被查询文档的增大而增加.     

基于元胞自动机的单源点最短路求解算法

针对图的单源点最短路问题,提出一种改进的基于元胞自动机模型的求解算法并分析了其算法复杂度.该算法定义了一个元胞自动机模型,通过元胞空间上元胞状态的变化,能够获得某设定结点到其他结点的最短路.在实验阶段,分别用经典Dijkstra算法和提出的算法对随机生成的不完全无向图进行分析.结果表明,相比于经典的Dijkstra算法,该算法不但能够获得与之相同的仿真结果,并且具有规则简单、易于实现、效率高等特点,具有明显的优越性.     

典型"稳定婚姻问题"的简明矩阵算法实现

对于典型“稳定婚姻问题”，借助矩阵（二维数组）给出了一种简明的实现方法．在本算法中，所采用的存储结构和实现方法灵活巧妙，通俗易懂，方便实现；而且用于存储所要处理数据的内存空间相对于其它一些算法节省了一半，空间复杂度为O（1）；由于存储结构的巧妙性，算法的时间复杂度在最好的情况下为线性时间N，在最坏的情况下为O（N^2）．     

时间自动机与信号自动机的互模拟算法

基于时间自动机的验证工具已被广泛应用于实时系统模型验证。信号自动机为一类实时系统建立了比时间自动机更适合的模型,但是它还不能用于实际的实时系统模型验证,因为没有验证算法可用。把信号自动机验证问题归约到了时间自动机验证问题：证明了两种自动机具有相同的识别语言能力,证明了二者具有双向模拟关系,并在此基础上提出了线性的互模拟算法。把互模拟算法和已有的时间自动机验证算法结合起来,就得到了信号自动机的验证算法,从而解决了对信号自动机模型的验证问题。     

时钟同步、钟速同步的再讨论

运用Stokes定理,给出了坐标钟同步及钟速同步的充要条件,分别讨论了在有奇点和有奇环的情况下条件成立的时空区域,指出只要本文校钟方案可以实现,任意含有有限个奇点和不的时空都可以调整坐标及钟速同步,并以Vaidya时空为例,指出其中既可以调整坐标钟同步,又可以调整钟速同步。     

时间ω-树自动机识别语言的一个条件

时间自动机被广泛用于实时系统验证和模型检验.为适应不同类型的系统验证需要,不少时间自动机的相关模型被提出.时间树自动机是这样的新模型之一.目前主要是针对时间树自动机识别的语言类及相关性质的研究.本文提出了时间树自动机识别语言的一个条件,并证明了结论的正确性.如果一个语言不能满足该条件,它一定不能被时间树自动机识别.这为证明一个具体语言不能被时间树自动机识别提供了思路.     

PET系统时钟的设计方案探究

文章通过对目前系统时钟的几种设计方案的比较，认为有锁相环（PLL）的专用时钟系统芯片，能产生多类时钟标准、多种时钟频率和多路时钟驱动，且具有稳定的性能，成为高性能时钟系统的解决方案。     

基于安全充分捕获技术的多时钟数字系统测试矢量生成

针对多时钟数字系统提出了一种新颖的产生测试矢量的方法——安全充分捕获技术(Safe and Complete Capture Technology,S&CCT).该方法对电路系统中的时钟按照一定的标准分为等效时钟和串行时钟,然后确定正确的时钟捕获顺序.使用并发故障模拟器从逻辑上和时序上对生成的测试矢量进行仿真,测试矢量生成器使用该仿真信息,以避免生成失效测试矢量.实验证明,S&CCT与传统方法相比,测试矢量数目减少50％左右,不仅大大减少了测试矢量的数目,对电路的硬件开销也几乎没有影响.     

基于新的波形读写技术的虚拟信号发生器的研究与设计

软件合成是现代虚拟信号发生器波形产生的主要方法。为了解决在硬件内存有限的情况下,无法满足大数据量波形存储的问题,基于任意波形发生器PXIe—5442硬件平台,引出了一种新的波形读写技术——波形数据流盘技术;该技术采用边读边写的方式,能够在小的内存空间中连续的产生波形,并在此基础上完成了虚拟信号发生器的设计与编程。结果表明了该方法大大提高了板载内存的利用率以及在LabVIEW环境下编程的高效性与良好的可读性。     

星载原子钟磁致频移影响在轨评估

星载原子钟作为磁敏感设备,外界磁场变化会导致星载原子钟输出频率发生变化.本文采用星载主备原子钟比相法评估了10颗配置星载氢原子钟的MEO导航卫星原子钟频率稳定度,短期稳定度平均值优于1×10^?12τ^?1/2,天稳均优于7×10^?15.基于该稳定度水平,本文针对导航卫星原子钟磁致频移进行了初步评估,得到磁力矩器工作情况下原子钟磁致频移达到1×10^?13量级,磁力矩器持续工作1 h将引起钟差预报误差0.4 ns.本文将在轨磁力矩器工作状态等效为磁致频移噪声,仿真分析了其对星载原子钟稳定度的影响,仿真结果表明,该磁致频移噪声将恶化星载原子钟长期稳定度,尤其对稳定度更高的原子钟恶化更明显.本文最后就如何降低磁致频移对星载原子钟的影响进行了讨论.     

基于可逆记忆CA融合时间延迟的图像加密算法研究

针对当前的元胞自动机加密系统不具备记忆功能,使其安全性\加密速度不理想;且目前的图像加密算法都忽略考虑时间延迟现象,无法体现加密的真实过程。对此,提出一种可逆线性记忆元胞自动机(cellular automata-CA)与时间延迟函数,采用二者相融合的加密算法来克服上述问题;并将非线性耦合置乱方法引入算法中。首先迭代一维线性分段映射所得到的一维数组,该数组通过非线性耦合置乱方法后得到一个置乱数组,并利用该数组对初始图像进行置乱处理,改变像素位置;然后将时间延迟引入到Logistic映射中,利用可逆线性记忆元胞自动机的演变规则对二者相融合所生成的时间延迟伪随机数组进行迭代,得到迭代数组。利用该迭代数组根据像素扩散机制对置乱图像进行扩散加密处理,改变其像素值。借助MATLAB仿真软件来验证算法。结果表明:提出的图像加密新算法具有优异的加密性能,加密机制高度安全,其密钥空间巨大,抗攻击能力大幅度提升。     

Frequency Calibration and Stabilization of the Cooling Laser of Ytterbium Lattice Clock with Molecular Iodine Spectroscopy

In order to apply the frequency comparison among the different optical clocks, transportable optical clocks(TOCs) is suggested as a valuable tool. For transportable clocks, the key technique is how to lock the lasers involved in the whole system. In this paper, we carry out a new way to calibrate and lock the second stage cooling laser of the ytterbium lattice clock with molecular iodine spectroscopy. The locking spectral width of 556 nm laser can be narrowed to 195 kHz, which can be used for frequency control and the stabilization of the second stage cooling. So the new method will make the transportable optical clocks more compact and robust in the future.