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