2012 Fiscal Year Annual Research Report
新パラダイム計算をねじふせる―多様な意味論的手法の合同・発展・応用
| Project/Area Number |
24680001
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (A)
|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 大学院・情報理工学系研究科, 講師 (60456762)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | プログラム理論 / 形式検証 / 量子計算 / ハイブリッドシステム / 応用数学 |
|---|
| Research Abstract |
本研究の目標たる新パラダイム計算の研究のうち,特に獲得目標として挙げたハイブリッドシステムと量子プログラミングの研究について,ほぼ想定通りの成果を得た.
まずハイブリッドシステムに関しては,目標としていたプロトタイプ自動検証器の実装に至り,その成果をシステム検証分野のトップ会議CAV2012で発表した.この成果は超準解析を用いたハイブリッドシステム検証ツールとして世界に先駆けるものであり,その後も更なる実効性向上のため多様なプログラム検証手法の導入に向けて研究を行なっている.(超準解析を用いているため,既存の離散的手法がそのまま移転できる)
さらに,同じ方法論を用いてシグナル処理系のブロック線図(ハイブリッドシステム設計の現場で支配的)を検証する手法を提案し,プログラミング言語研究分野のトップ会議POPL2013で発表した.
また,より産業界の興味に近いハイブリッドシステムのテストケース生成問題についても,(超準解析を用いないが)プログラム論理を利用して検索空間を大きく削減する手法を学生・いくつかの企業と共に研究し,いくつかの予備的な結果を得た.今後これらの結果の諭文発表を目指す.
次に量子プログラミングについては,線形論理に基づいたproof netによる量子計算の表現について,学生・海外研究者と共に研究を行った.この研究は,来るべき量子抽象機械の設計に向けて多様な視点から検討を加えるために不可欠なものであり,現在成果の出版に向けて継続中である.さらに,より広い文脈の状態遷移システムについて,その仕様(特に安全性)を帰納的に記述するcoinductive predicateについて,圏諭的な一般化された枠組における定式化とその性質の研究を行った.得られた主結果はcoinductive predicateの意味のstepwiseな構成に関するものであり,理諭的興味とともに今後各種検証アルゴリズムの停止性証明への応用が期待される.この結果については現在諭文を投稿中である.
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
ハイブリッド・システムについては検証器の実装を早々に完了し,その後の研究に着手することができた.量子計算についても,理論研究の展開が当初予想した以上の広範囲にわたっており,今後の具体的成果に結実することが期待される.さらに,coinductive predicateに関する研究はこれらのトピックの基礎となる結果であり,当初予想しなかった研究の方向性が生まれている.
|
| Strategy for Future Research Activity |
平成24年度の研究において有望な理論的萌芽が多数得られたので,これらについて学生・国内外の協力研究者と共に発展させ,論文等具体的成果に結実させる.
|
| Expenditure Plans for the Next FY Research Funding |
研究の一端を担う学生たちがいまだ修士1年であったので,基礎的な学習を重視した結果,成果発表等に伴う旅費が少なくなった.これらの学生たちはすでに研究成果をあげつつあり,次年度以降の成果発表のための旅費の一部として使用する.
|
