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

通过类石对偶性和微观世界原理进行模块化验证的基础

• 批准号: 23654033
• 负责人: HASUO Ichiro
• 金额: $ 2.41万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Challenging Exploratory Research
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23654033/
• 关键词: システム検証; ソフトウェア学; 数学基礎論; 数理論理学; 応用数学; 余代数; 圏論的論理; 不動点論理; 圏論; 仕様記述; 国際研究者交流 オランダ; 国際研究者交流 イギリス; 国際研究者交流 ポーランド; 国際研究者交流 オーストリア

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.

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

项目成果

Hyperstream processing systems: nonstandard modeling of continuous-time signals

• DOI: 10.1145/2429069.2429120
• 发表时间: 2013-01
• 作者: Kohei Suenaga;Hiroyoshi Sekine;I. Hasuo

越境する数学

跨越国界的数学

• 发表时间: 2013
• 作者: M.Takeda;Y.Tawara;宮田大毅;西浦廉政
• 通讯作者: 西浦廉政

The Microcosm Principle and Compositionality of GSOS-Based Component Calculi. Proc

基于 GSOS 的分量演算的微观原理和组合性。

• DOI: 10.1007/978-3-642-22944-2_16
• 发表时间: 2011
• 期刊: Lecture Notes in Computer Science
• 作者: Yiling Lin;Miwako Mishima;Junya Satoh and Masakazu Jimbo;遠藤久顕;Ichiro Hasuo
• 通讯作者: Ichiro Hasuo

Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications

非标准静态分析：离散验证方法转移到混合应用

• 发表时间: 2012
• 作者: S. Mase;K. Takahashi;N. Mochida;Ichiro Hasuo
• 通讯作者: Ichiro Hasuo

Traces for Coalgebraic Components.

代数分量的迹线。

• DOI: 10.1017/s0960129510000551
• 发表时间: 2011
• 期刊: Mathematical Structures in Computer Science
• 影响因子: 0.5
• 作者: Ichiro Hasuo;Kenta Cho;Toshiki Kataoka;and Bart Jacobs;Ryoichi Kobayashi;Ichiro Hasuo and Bart Jacobs
• 通讯作者: Ichiro Hasuo and Bart Jacobs