形式化方法经过几十年的研究发展，为并发系统的建模与验证做出了巨大的贡献。事件结构是一种主流高效的形式化方法，由基于抽象动作的事件以及事件之间的因果、矛盾、并发三种逻辑关系组成，通过抽象、离散化的刻画方法不仅可以为并发系统的行为及结构进行直观且有逻辑的表达，而且可以为并发系统进行基于状态遍历或事件遍历的各种计算和推理。　　在计算机科学和控制理论、控制工程领域，并发系统的组成和结构越来越复杂，并且对支撑建模与验证的形式化工具的要求水准也越来越高。比如，对同时存在离散行为和连续行为的混杂并发系统，如果使用传统的离散事件结构来建模，则难点主要是对“数据流交换过程”的处理上和对“连续的状态变化”的处理上。原因在于，传统的事件结构建立在“动作集合”之上，动作集合中的元素是抽象的，不能刻画数据流，集合本身只有交并补等简单操作，不合有其他数据间的运算操作，因而无法对数据流交换过程进行表示和处理，而数据流交换过程恰恰是并发系统最重要的行为特征之一;传统的事件结构中状态是离散的，不能刻画连续的状态变化，而数据流的连续演化也是并发系统最重要的行为特征之一。对于混杂并发系统，如果一定要使用传统的事件结构来建模的话，那么只有先将一系列连续行为抽象为一个离散行为之后再使用事件结构建立被压缩了的模型;作为形式化方法的另一主流技术模型检测方法对于“连续的状态变化”的处理上也无能为力，由于模型检测方法同样也只能用于有限状态空间的离散系统。　　因此对并发系统的设计和验证需要一套新的形式化理论与方法。本文围绕建立具有刻画数据流交换过程和数据流连续演变过程功能的新型事件结构理论这一主旨开展研究，主要贡献包括:　　(1)针对并发系统建模的第一个难点在于对“数据流交换过程”的表示和处理上，研究能够描述数据流交换过程的多项式代数事件结构，并且将事件结构中的事件对应着并发系统中的一段数据流交换过程。研究如何将代数符号计算方法运用到多项式代数事件的计算和推理之中。理想和代数簇反映了多项式代数系统解的结构和性质，研究如何充分利用吴特征集方法和Gr(o)bner基方法等计算多项式理想及代数簇的经典符号计算方法来获取事件的代数结构及性质，由事件的代数结构及性质来获得事件之间的应有的逻辑关系，然后将事件根据逻辑关系分解或合并，使建模的事件结构得到进一步优化。　　(2)针对复杂并发系统建模的第二个难点在于同时对“数据流交换过程和数据流连续演化过程”的表示和处理上，研究能够既描述数据流交换过程又描述数据流连续演化过程的微分多项式代数事件结构，并且将微分多项式代数事件结构中的事件对应着复杂并发系统中的一段数据流交换及连续演化过程。研究如何将微分代数符号计算方法运用到微分代数事件的计算和推理之中。　　(3)针对复杂的并发系统内部往往会出现一些功能行为相同的重复数据流交换过程和数据流连续演变过程，以及大量由并发执行导致的不确定性的数据流交换过程和数据流连续演变过程，给系统的建模和验证增加了不少困难，并且有时还会出现“状态爆炸”导致验证瘫痪的情况，研究找到一种合适的等价判定方法来判定这些数据流交换过程和数据流连续演变过程的等价，约简冗余的数据流交换过程和数据流连续演变过程以化简系统的整体结构和行为。在Glabbeek等价谱系中，轨迹等价与互模拟等价是两种广受欢迎的等价方法，因此研究建立在多项式代数事件结构及微分多项式代数事件结构之上的轨迹等价与互模拟等价的判定方法，研究两个多项式代数事件相互等价的标准及其Gr(o)bner基方法和吴特征列方法在两个多项式代数事件相互等价上的判定方法，研究给出两个微分代数事件相互等价的标准以及使用吴微分特征集方法来判定两个微分代数事件相互等价的计算方法。　　(4)针对微分多项式代数事件结构能够刻画数据流交换过程和数据流连续演变过程的特点，研究微分多项式代数事件结构的层次化方法及变元细化的实现机理。研究微分多项式代数事件结构的交织轨迹等价与交织互模拟等价的判定方法，并且研究两种交织等价在微分多项式代数事件结构层次化下的保持问题。由于使用步进事件变迁可以解决标记变迁系统使用单个事件变迁而不能表示真并发的情况，因此进一步研究微分多项式代数事件结构的步进轨迹等价与步进互模拟等价的判定方法，并且研究两种步进等价在微分多项式代数事件结构层次化下的保持问题。针对一类具有束事件变迁性质的微分多项式代数事件结构，研究交织等价、步进等价在代数束事件结构层次化下的保持问题。　　(5)在Pratt的动态逻辑和Platzer的微分动态逻辑的基础上，研究寻找适合在多项式代数事件结构和微分多项式代数事件结构上使用的动态逻辑刻画系统，将形式化方法结构层次上的事件结构模型与形式化方法逻辑层次上的这一事件动态逻辑系统相结合，为并发系统的设计与验证分析提供更强大的支撑框架。设计改造若干适用于多项式代数事件结构及微分多项式代数事件结构的推理法则，并且研究通过可靠性定理和完备性定理把语法范畴的形式可推演性与语义范畴的逻辑推论之间建立等价关联。研究如何在安全苛求的列车控制系统CBTC之中应用事件动态逻辑推演系统，来保证列车高速度、高密度和高安全性的运营。　　(6)基于并发系统性质验证的角度开展研究。一是研究在微分多项式代数事件结构中引入事件不变式的思想，事件不变式是动态事件结构理论框架的重要组成部分，用于表示对系统可达状态的上界逼近，可以通过它来分析和验证系统的性质;研究在复杂的微分多项式代数事件结构中如何使用基于参数化模板和约束求解的技术、基于抽象解释与Widening算子的技术来生成有效的多项式事件不变式。二是针对能够表示数据流交换过程和数据流连续演变过程的微分多项式代数事件结构，研究可达性、活性及公平性等动态性质;借助于作为状态转移图的标记变迁系统，用图论的方法来研究和分析可达性、活性及公平性的内在表现规律;研究动态性质在以变元细化为核心的微分多项式代数事件结构层次化下的可保持性问题。　　综上所述，本文以复杂并发系统的建模与验证为目标，通过多项式代数、微分代数等工具手段，研究建立一套具有刻画数据流交换过程和数据流连续演变过程功能的新一代事件结构及其细化理论和方法。