kμ-Tree:一种空间有效的嵌入式闪存数据库索引

μ-Tree是直接建立在闪存之上的索引,它克服了传统B+树应用于闪存时引起的"游走树"现象,避免更新一页累及多页的现象.但μ-Tree也存在缺点:占用空间比传统B+树多.为克服μ-Tree存在的缺点,本文提出一套机制改进μ-Tree:k分法模型.在此模型中,我们分析了在给定扇出度F时,k值与总记录数n的关系,以及给定记录数n时,不同大小的索引记录项对k的影响;给出了确定k值的基本方法.实验结果表明,k比例划分可以有效地节省索引所占空间,空间节省最大达50%左右,平均可达39%.所提方法在空间资源受限的环境下具有良好的空间特性.

描述逻辑μALCIO的语义及推理

循环术语集是描述逻辑长期以来的研究难点,它的最基本的问题即语义及推理问题没有得到合理的解决.分析了描述逻辑循环术语集的研究现状和存在的问题,基于混合μ-演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCIO中,提出了一种允许包含循环术语集的描述逻辑μALCIO.给出了μALCIO的语法和语义,证明了μALCIO的可满足性推理等价于混合μ-演算的可满足性推理,并利用树自动机理论给出了μALCIO的可满足性推理算法以及给出了推理算法正确性证明和复杂性定理.

基于嵌套树的对等博弈应用研究

进行了软件系统性质验证研究。首先提出了用嵌套树表示软件程序的方法,以解决软件系统的抽象表示问题,该方法能在表示程序顺序结构的同时,更好地表示调用返回关系。然后定义了嵌套树上的μ-演算,以便将要验证的需求性质用公式表示,并把公式转化成非确定对等嵌套树自动机。最后将自动机与嵌套树结合,转化形成博弈图,并用对等博弈条件来判断博弈的输赢,这等同于检验验证公式是否在嵌套树上成立。相比直接验证,这种判定方法表达更为直观,且更有利于整个过程的自动化。研究表明,将嵌套树中的调用关系展开可形成概要标签树,嵌套树的对等博弈理论也可以应用到概要标签树中。

基于嵌套树模型检测的研究

文章针对软件验证过程中的结构抽象表示问题,考虑到结构程序的顺序结构、调用返回关系,给出了嵌套树以及嵌套状态机的定义。在该数据结构及μ演算的基础上,定义了嵌套树的μ演算(NT-μ)。NT-μ的公式语法是基于概要的,在嵌套状态机上提出基于概要类的模型检测。嵌套状态机的结点是有限的,且嵌套状态机有限的概要类对应于嵌套树中的无限的概要,因此该方法能提高检测的效率。

并发加权μ-演算的一致性内插

并发加权μ-演算(concurrent weightedμ-calculus,CWC)是对Kim. G. Larsen所提出的并发加权逻辑的强有力的扩充,通过加入不动点算子,增强表达能力,实现对复杂模块化系统的有效建模。对CWC进行了研究,给出了CWC的语法并阐述了CWC的标记加权转移语义。μ-演算与自动机理论密不可分,引入了轮替树自动机用于处理CWC,阐述了轮替树自动机与CWC之间的联系,构建了一种特定的用于CWC的轮替树自动机模型。一致性内插定理是Craig内插定理的加强和扩展,为了探究CWC上的一致性内插定理,根据Andrew M. Pitts提出的方法,利用互模拟量词寻找一致性插值。给出了互模拟量词在标记加权转移系统上的语义,并研究了互模拟量词和CWC上一致性内插定理之间的关系。在此过程中利用ω展开(unravelling),由ω展开树的一系列特性,结合轮替树自动机,证明了一致性内插定理在CWC上成立。

并发加权μ-演算的若干性质

最近,针对为组合性标记加权转移系统建模的需要,Larsen等人提出了并发加权逻辑。该逻辑是多模态的,包含了反映给定状态的资源总量和限制转换过程的模态词,以及能够应对组合性系统的二元模态词,可以有效地表达系统的质化、量化和模块化的性质。为了增强并发加权逻辑的表达能力,对带不动点算子的并发加权逻辑——并发加权μ-演算进行了研究,给出了并发加权μ-演算的语法和标记加权转移语义,在表达能力与复杂性之间建立了良好的平衡。研究了并发加权μ-演算与轮替树自动机之间的联系,构建了一种特定的用于并发加权μ-演算的轮替树自动机模型。该自动机模型在表达能力上与并发加权μ-演算互模拟等价。在此基础上,进一步证明了并发加权μ-演算的可判定性及小模型性。