Foundation of Modular Verification via Stone-Like Dualities and theMicrocosm Principle

最初的目标是联合收割机的微观世界的原则（数学模型的模块化建设的计算机系统）和石头一样的对偶（数学模型的模态逻辑），并将其应用到系统验证。然而，在我们的研究过程中，在更广泛的意义上对数学（特别是范畴论）在系统验证中的应用感兴趣，我们获得了关于纤维化（一种逻辑的数学模型，用于范畴逻辑）中的不动点逻辑的形式化及其在模型检查中的应用的新见解。我们决定继续这个新的方向，并得到了关于共归纳谓词的范畴构造的结果。研究现在正在继续，以便框架也容纳归纳谓词。

The initial objective was to combine the microcosm principle (a mathematical model of modular construction of computer systems) and Stone-like dualities (a mathematical model of modal logic) and to apply it to system verification. However, in the course of our research with interests in the application of mathematics (category theory in particular) to system verification in a broader sense, we obtained new insights on the formalization of fixed-point logics in a fibration (a mathematical model of logics, used in categorical logic) and its application to model checking. We decided to pursue this new direction, and obtained results on the categorical construction of coinductive predicates. The research is being continued now so that the framework also accommodates inductive predicates.