2011 Fiscal Year Research-status Report
ストーン双対性と小宇宙原理による，モジュラーなシステム検証の一般理論
| Project/Area Number |
23654033
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 情報理工学(系)研究科, 講師 (60456762)
|
|---|
| Project Period (FY) |
2011-04-28 – 2013-03-31
|
| Keywords | 国際研究者交流 オランダ / 国際研究者交流 イギリス / 国際研究者交流 ポーランド / 国際研究者交流 オーストリア |
|---|
| Research Abstract |
本研究課題の第一の背景は，研究代表者による，モジュラーなシステム設計の数学的モデリング(圏論的な「小宇宙原理」による)である．平成23年度においてはまず，この論文を国際会議CALCOの予稿集の中で出版し，会議中に発表を行った．この際，理論・応用両面にわたって，多くの有意義なフィードバックを得た．また，本研究課題のもう一つの背景たる双対性について，指導学生とともにサーベイと研究を行った．本研究課題では，仕様記述のための様相論理の基礎として双対性を用いるが，双対性の応用範囲はこれにとどまらず，計算機科学・論理学・数学のあらゆる側面にわたっている．平成23年度においては，これらさまざまな双対性，特に量子力学の基礎における双対性について，理解の深化を図った．これは，研究課題進展のための数学的基礎整備となるものである．さらに，応用面での可能性として，Oxford 大の M. Kwiatkowska 教授との議論から，一階モデリング言語 Promela が応用上のターゲットとして有望であるという知見を得た．Promela は，(おそらく最も普及した)モデル検査ツール SPIN においてシステム記述に用いられるモデリング言語であり，応用がうまくいったあかつきには大きなインパクトが期待できる．平成23年度には，産業界の研究者との研究協力も開始した．議論を通じて明らかになったのは，システムコンポーネントの組み合わせと，そのモジュラーな品質保証が，産業界のシステム設計の現場でも大きな問題であることである．今後この協力関係を継続し，本研究課題で得られた理論的成果の応用を図っていきたい．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
挑戦的な本研究課題にあって，目的とする理論的枠組が既に得られたわけではないが，理論面・応用面から，その基盤整備を着実に積み重ねている実感がある．平成24年度においては，ぜひこれを実際の理論的枠組に結実させたい．
|
| Strategy for Future Research Activity |
平成23年度に行ったサーベイ・理論的基盤整備・応用的基盤整備をもとに，理論的なブレイクスルーを図る．理論的な成果が得られるかどうかは，対時間・対費用で計算できるものでは決してないが，外部（とくに国外）の研究者との戦略的な協働によって，成功率をできるだけ上げることを試みたい．
|
| Expenditure Plans for the Next FY Research Funding |
主に議論のための研究者往来（旅費）に用いる．
|
