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

最初的目标是将微观原理（计算机系统模块化构造的数学模型）和Stone-like对偶性（模态逻辑的数学模型）结合起来，并将其应用于系统验证。然而，在我们对数学（特别是范畴论）应用于更广泛意义上的系统验证感兴趣的研究过程中，我们对fibration（逻辑的数学模型，用于范畴逻辑）中的不动点逻辑的形式化及其在模型检查中的应用获得了新的见解。我们决定继续这个新的方向，并在共归纳谓词的范畴建构上取得了一些成果。该研究目前仍在继续，因此该框架也适用于归纳谓词。

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.