本项目主要对近似等价、代数与模态逻辑两种形式化途径的融合等方面做了较系统的研究，取得的主要成果包括如下方面：.1）将Pola和Tabuada提出的刻画近似行为等价的概念“交替近似互模拟”推广到一般情形，研究了一般的交替转换系统中交替近似互模拟的基本性质，提出了一种近似互模拟模态特征表述方式，基于交替时序逻辑给出了交替近似互模拟的模态逻辑特征，从而建立了交替转换系统间行为近似等价性与其所满足的逻辑性质之间的内在联系。并将此概念用于刻画带扰动控制系统与其有限抽象之间的关系，提出了一个控制策略算法并证明了算法的正确性。.2）基于对偶理论给出了Rank-1模态逻辑都有余代数语义的一种新的证明方法，并且建立了通过对偶理论构造出来的函子和Schröder所构造的函子的等价性。提出了模态词带布尔结构的余代数模态逻辑系统，并基于公理的一步可靠与完备性研究了该类逻辑系统的可靠完备性。建立了具体范畴上的拟终结对象可以刻画的等价关系的特征，并给出拟终结对象形成的格结构的性质。.3）基于逻辑标记转换系统（LLTS)，较深入地研究了含逻辑连接词、模态词以及标准进程代数算子的代数演算系统，这方面的工作不但将Luttgen与Vogler的工作提升到纯粹的代数形式， 而且在如下方面深化和扩展了他们的工作：a）建立了刻画Luttgen与Vogler提出的模拟关系的可靠和基完备的公理系统；b）基于余代数终结语义的思想， 给出将模态词always与unless纳入进程代数的两种不同的途径，其中基于递归算子的途径较之Luttgen与Vogler的构造要简洁得多；c）建立了CLLT与ACTL(基于动作的计算树逻辑)之间的内在联系，包括CLLT进程项的ACTL逻辑特征公式表示、ACTL逻辑公式终结模型的CLLT特征项表示以及CLLT与ACTL之间的伽罗瓦连接；d）研究了LLTS上的递归构造，建立了同余性以及方程解的唯一性定理。这部分的工作为形式化规范提供了一种可以自由混合使用逻辑连接词（合取、析取）、模态词（always，unless）以及标准进程代数算子的代数演算系统，该系统支持模块化设计与推理，并可将表示安全性性质的ACTL逻辑公式以代数项的形式加以表示和推理。. 基于上述工作，我们已完成5篇学术论文，其中包括3篇60页左右的长文。