2014 Fiscal Year Annual Research Report
新パラダイム計算をねじふせる―多様な意味論的手法の合同・発展・応用
| Project/Area Number |
24680001
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 情報理工学(系)研究科, 講師 (60456762)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | プログラム理論 / 形式検証 / 量子計算 / ハイブリッドシステム / 応用数学 / 国際研究者交流（フランス） / 国際研究者交流（イタリア） |
|---|
| Outline of Annual Research Achievements |
本研究の目標たる新パラダイム計算の研究において，２つの獲得目標（ハイブリッドシステムの自動検証，量子計算のための抽象機械）およびこれらに通底する理論的基盤について，想定以上の成果を得た．
ハイブリッドシステムの自動検証については，システム検証の自動化のための有力な手法である抽象解釈を超準解析によって拡張し，理論的枠組およびプロトタイプ実装を得た [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]．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
ハイブリッドシステム研究においては，当初想定しなかった抽象解釈への超準解析の応用や，より実践に近いモデルベース開発への論理学的手法の応用など，計画を超えたブレイクスルーが得られている．また，量子プログラミング言語の研究は，本研究のアプローチの汎用性を活かして新たな応用可能性（確率的プログラミング言語からデータサイエンスへ）につながっている．さらに余代数や圏論的論理においても着々と研究成果が得られつつある．
|
| Strategy for Future Research Activity |
研究トピックが当初計画をはるかに超えて多様化・深化しており，これらを引き続き追求しつつ，多様なトピックを俯瞰することで新たな統一的視座を得ることを目指したい．さらに，共同研究の範囲を広げ，当該コミュニティの協力を得てさらに強力に研究を推進する．
|
-
-
-
-
-
-
[Journal Article] The Geometry of Synchronization2014
Author(s)
Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo and Akira Yoshimizu
-
Journal Title
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Volume: なし
Pages: Article No. 35
DOI
Peer Reviewed / Acknowledgement Compliant
-
-
-
-
-
-
