| 研究実績の概要 |
本研究の目標たる新パラダイム計算の研究において，２つの獲得目標（ハイブリッドシステムの自動検証，量子計算のための抽象機械）およびこれらに通底する理論的基盤について，想定以上の成果を得た．
ハイブリッドシステムの自動検証については，システム検証の自動化のための有力な手法である抽象解釈を超準解析によって拡張し，理論的枠組およびプロトタイプ実装を得た [Kido, Chaudhuri & Hasuo]．この理論的成果（応用可能性はロングレンジで追求する）に加え，産業界のニーズに直結した物理情報システムのモデルベース開発に対する論理学的サポートについても，多様なロバスト値を表現できる時相論理の理論体系を構築し，これをもとにした falsification ツールを実装した [Akazaki & Hasuo]．上記二つの成果については論文を準備中である．
量子計算のための抽象機械については，トップ国際会議 CSL-LICS にて発表された論文２報に加え，そのうちの一つに基づいたツールを実装した [Muroya, Kataoka, Hasuo & Hoshino]（論文投稿済）．このプロトタイプ実装は，量子プログラミングのみならず，データサイエンス等の応用が期待される確率的プログラミングに対しても有用なツールの基礎となることが期待される．
さらに，これら意味論的研究に通底する理論的基盤について，余代数的模倣関係を量的システムに適用し線形計画法によるアルゴリズムを得た論文 [Urabe & Hasuo, CONCUR'14] が，並列システム検証分野のトップ国際会議 CONCUR 2014 にて最優秀論文賞を受けた．また，プログラム論理のモナドによる一般的定式化について国際ワークショップ CMCS 2014 にて招待講演を行い，同内容のジャーナル論文が採択された [Hasuo, Theor. Comp. Sci., to appear]．
|
