2012 Fiscal Year Final Research Report
Foundation of Modular Verification via Stone-Like Dualities and theMicrocosm Principle
| Project/Area Number |
23654033
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
HASUO Ichiro 東京大学, 大学院・情報理工学系研究科, 講師 (60456762)
|
|---|
| Project Period (FY) |
2011 – 2012
|
| Keywords | システム検証 / ソフトウェア学 / 数学基礎論 / 数理論理学 / 応用数学 |
|---|
| Research Abstract |
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.
|
