共代数逻辑及其应用的初步研究

摘要

共代数是代数的对偶概念，基于观察的角度考察集合及其上操作。计算机科学中很多系统都可以归结为共代数，如自动机、抽象数据类型、面向对象设计语言等。目前，共代数方法已经被证明是研究状态系统的行为性质的可行途径。 模态逻辑是经典逻辑的扩充。由于添加了模态词，使得模态逻辑适合于描述动态系统的行为。模态逻辑的一些分支，如时态逻辑、认知逻辑等，已经广泛应用于模型检测、人工智能等计算机科学领域。 共代数逻辑是适合于描述共代数系统的逻辑。把模态逻辑作为共代数逻辑是共代数研究领域中一个新的研究方向。模态逻辑与共代数都与状态系统紧密相连，可以利用共代数对动态系统建立模型，然后利用模态逻辑描述共代数模型的行为性质，因此将共代数和模态逻辑融合在一起是自然的。而如何从共代数生成合适的模态逻辑则是共代数逻辑研究的重点。L．Moss，B．Jacobs,A．Kurz等人都在这方面作出了很大的贡献。 本文首先探讨了共代数与系统的关系，以及共代数与模态逻辑的内在联系，分析了几种共代数逻辑的特点，在此基础上研究了有限Kripke多项式函子上的模态逻辑，并证明该模态逻辑保持共代数的互模拟特性，具有充分性和可表达性。文章最后利用共代数逻辑方面的研究，给出内存管理系统的一个共代数规范，说明如何将共代数逻辑应用于计算机领域。

目录

文摘

英文文摘

第一章前言

1.1研究背景

1.2本文的主要研究内容

1.3研究意义

1.4论文的总体结构

第二章范畴理论

2.1对象与射

2.2函子

2.3自然变换

第三章共代数

3.1系统与共代数

3.2行为等价与互模拟

3.3终结共代数与共归纳

3.4标号变迁系统

第四章模态逻辑

4.1背景

4.2模态逻辑系统

4.3可能世界语义

4.4多模态逻辑

4.5模态逻辑与共代数

第五章共代数逻辑

5.1基本概念

5.2 L.Moss的共代数逻辑

5.3多项式函子共代数的逻辑

5.4 D.Pattinson的共代数逻辑

5.5有限Kripke多项式函子共代数的逻辑

第六章共代数逻辑的实例研究

6.1 FIASCO的内存管理

6.2共代数建模

6.3模态逻辑规范

6.4共代数逻辑与CCSL

第七章总结与展望

7.1本文的研究工作总结

7.2进一步研究工作

参考文献

致谢

原创性声明