论文部分内容阅读
近年来,并发系统有着颇为广泛的应用。事件结构作为并发系统的语义模型之一,引起了理论与工程学界极大的关注和兴趣,并吸引了大量的学者进行研究。传统的事件结构建立在抽象动作符号集合之上,但抽象的动作不能细致地描述系统行为,也不能处理近似问题。然而,近似问题在工程应用中却是非常常见。例如,在实际测量和计算过程中,测量误差和截断误差经常是不可避免的,这意味着经常无法获得完全精确的解。实际上,工程问题的解并不总是精度越高越好,还需要平衡好精度与时间复杂度、空间复杂度的关系,换言之,完全精确的解有时也是不必要的。此外,近似还经常应用于以下两方面:一是简化系统,在预先给定的可以容忍的误差范围内,对原始系统进行近似化简,从而得到一个复杂度降低的简化系统;二是扩展系统之间的传统精确等价关系,通常把两个系统之间的近似程度解读为距离,从而可以将两个系统之间的传统精确等价关系扩展为具有鲁棒性的近似等价关系。因此,如果要将传统事件结构的应用扩展到更广的领域,有必要将事件结构扩展以处理近似问题。在并发系统模型理论中,系统的简化问题是核心问题之一。在进行系统简化时,语义等价是最常用的方法之一。目前已经有大量的学者对语义等价进行研究,并且形成了完整的理论体系。语义等价分为线性时间等价和分支时间等价两类。线性时间等价主要包括迹等价,分支时间等价主要包括(单元)失败等价和互模拟等价。但是目前迹等价、(单元)失败等价和互模拟等价主要应用于标签变迁系统的化简,极少应用于事件结构的化简。实际上,目前事件结构上(近似)语义等价理论尚不健全,如何将语义等价应用于事件结构的理论研究成为需要深入研究的重要问题。为了解决以上问题,本文在传统的事件结构中引入多项式代数,提出了多项式代数事件结构的概念。由多项式代数事件结构诱导出对应的多项式代数交织标签变迁系统和多项式代数步进标签变迁系统,从而使得线性时间-分支时间等价谱系理论可以应用于多项式代数事件结构,最终建立了多项式代数事件结构的近似和近似等价理论.具体地,本文的研究方法和主要成果如下:1)提出了多项式代数事件结构的概念,并使用两种不同的构造方法,将传统事件结构转化为多项式代数事件结构,验证了传统事件结构是多项式代数事件结构的特例。2)讨论了多项式代数事件结构的刻画能力,举例并分析了如何应用多项式代数事件结构刻画计算机程序。在分析过程中,本文发现在五种经典事件结构(基本事件结构、稳定事件结构、流事件结构、集束事件结构和扩展集束事件结构)中,流事件结构最适合作为程序的模型。3)重点研究了事件结构并行特性中的交织语义和步进语义。结合事件结构的格局结构定义,由多项式代数事件结构可以诱导出多项式代数交织标签变迁系统和多项式代数步进标签变迁系统,从而使得线性时间-分支时间等价谱系理论可以应用于多项式代数事件结构。4)在线性时间-分支时间等价谱系理论的研究中,本文分别讨论了可达性等价、迹等价、失败等价、单元失败等价和互模拟等价。其中,根据是否引入观测值,将所有语义等价分成基于迹和基于可见迹两个子类。值得一提的是,本文提出了最小单元失败集合的概念,并证明了最小单元失败集合方法在所有能判定单元失败等价的方法中是最优的。因此,运用最小单元失败集合方法可以极大地简化单元失败等价的验证计算。本文分别对一个规模较小的实例和一个规模较大的实例进行分析,结果显示使用最小单元失败集合方法比传统方法判定单元失败等价减少了较多的工作量。5)构建了多项式代数事件结构的近似理论。一方面,结合实例分别运用了泰勒展开、最佳一次逼近和分段线性插值等数值近似理论近似化简多项式代数事件结构,并在实例中探讨了误差传递问题。另一方面,给多项式代数事件结构诱导出的多项式代数标签变迁系统赋予Baire度量,并结合豪斯多夫距离,以及迹集合和互模拟关系的定义,给出迹距离函数和互模拟距离函数,从而量化了多项式代数事件结构之间的近似关系。6)构建了多项式代数事件结构的近似等价理论。本文创新性地引入弱化了的Baire度量,使得得到的度量具有传递性性质。然后结合豪斯多夫距离,定义了多项式代数事件结构的近似迹等价和近似单元失败等价。如果假设观测值空间为n维空间,类似地,就可以得到多项式代数事件结构的近似可达性等价和近似互模拟等价定义。这些近似等价都具有传递性,因此可以多次运用这些近似等价来化简模型,并且各个传统精确等价是对应的近似等价的特例。这些近似等价之间的粗糙关系与传统精确等价之间的粗糙关系保持一致。综上所述,多项式代数事件结构能够更细致地刻画系统行为,并且可以处理近似问题。虽然多项式代数事件结构较传统事件结构数学形式更复杂,但是多项式代数事件结构也因此可以运用数值近似理论进行化简。本文提出的多项式代数事件结构以及建立的多项式代数事件结构近似和近似等价理论,将为并发系统的研究提供有力支撑。