2012 Fiscal Year Annual Research Report
ストーン双対性と小宇宙原理による，モジュラーなシステム検証の一般理論
| Project/Area Number |
23654033
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 情報理工学(系)研究科, 講師 (60456762)
|
|---|
| Keywords | システム検証 / 余代数 / 圏論的論理 / 不動点論理 / 圏論 / 仕様記述 / 国際研究者交流 オランダ |
|---|
| Research Abstract |
本研究の最終目的たる計算機システムの正しさの数学的保証に向けて，当初計画のアプローチを変更したものの，基礎的な結果を得た．
具体的には以下のとおりである．当初計画では，システムの要素還元的（「モジュラーな」）設計手法を数学的に余代数と小宇宙原理によって表現し，これを様相論理の数学的表現であるストーン双対性と組み合わせることによって，計算機システムのモジュラーな仕様記述・検証の手法を目指した．しかし研究を進めるうちに，次のような関連した話題に関して新しい知見が得られた．すなわち，システム検証という応用面における，リアクティブ・システムの仕様記述と検証のための不動点論理（LTL やμ計算など）の重要性であり，また，その数学面では，論理の圏論的モデルとしてストーン双対性の代替となるファイブレーションの概念である．特にファイブレーションは Lawvere 以来圏論的論理の基本的構造として用いられ，ストーン双対性よりもさらに一般的な状況に適用できる．
これらの概念に対する新しい知見を発展させ，ファイブレーションの表す論理の上で余帰納的述語（主に安全性仕様の記述に用いられる）を定式化し，さらにその余帰納的述語の具体的な再帰的構成法（ωチェインによる）と，この再帰が飽和するための一般的な十分条件を圏論の言葉で与えた．この十分条件はファイブレーションと locally presentable category という，これまであまり交わりのなかった圏論の2つのトピックの融合によってもたらされたものである．
以上のように研究実績は当初計画とは方向の違うものになったが，計算機システムの品質保証という最終目的に対しては，かえって重要性の高いものであると考える．当初計画の中にあって今回の成果の中で考察されなかったモジュラー性については，今回の成果に立脚したさらなる研究が期待される．
|
