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
|
| Project Status |
Completed (Fiscal Year 2012)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2012: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2011: ¥2,340,000 (Direct Cost: ¥1,800,000、Indirect Cost: ¥540,000)
|
|---|
| 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.
|
Report
(3 results)
Research Products
(24 results)
