| 研究概要 |
本研究の目標たる新パラダイム計算の研究のうち,特に獲得目標として挙げたハイブリッドシステムと量子プログラミングの研究について,ほぼ想定通りの成果を得た.
まずハイブリッドシステムに関しては,目標としていたプロトタイプ自動検証器の実装に至り,その成果をシステム検証分野のトップ会議CAV2012で発表した.この成果は超準解析を用いたハイブリッドシステム検証ツールとして世界に先駆けるものであり,その後も更なる実効性向上のため多様なプログラム検証手法の導入に向けて研究を行なっている.(超準解析を用いているため,既存の離散的手法がそのまま移転できる)
さらに,同じ方法論を用いてシグナル処理系のブロック線図(ハイブリッドシステム設計の現場で支配的)を検証する手法を提案し,プログラミング言語研究分野のトップ会議POPL2013で発表した.
また,より産業界の興味に近いハイブリッドシステムのテストケース生成問題についても,(超準解析を用いないが)プログラム論理を利用して検索空間を大きく削減する手法を学生・いくつかの企業と共に研究し,いくつかの予備的な結果を得た.今後これらの結果の諭文発表を目指す.
次に量子プログラミングについては,線形論理に基づいたproof netによる量子計算の表現について,学生・海外研究者と共に研究を行った.この研究は,来るべき量子抽象機械の設計に向けて多様な視点から検討を加えるために不可欠なものであり,現在成果の出版に向けて継続中である.さらに,より広い文脈の状態遷移システムについて,その仕様(特に安全性)を帰納的に記述するcoinductive predicateについて,圏諭的な一般化された枠組における定式化とその性質の研究を行った.得られた主結果はcoinductive predicateの意味のstepwiseな構成に関するものであり,理諭的興味とともに今後各種検証アルゴリズムの停止性証明への応用が期待される.この結果については現在諭文を投稿中である.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
ハイブリッド・システムについては検証器の実装を早々に完了し,その後の研究に着手することができた.量子計算についても,理論研究の展開が当初予想した以上の広範囲にわたっており,今後の具体的成果に結実することが期待される.さらに,coinductive predicateに関する研究はこれらのトピックの基礎となる結果であり,当初予想しなかった研究の方向性が生まれている.
|
