| 研究実績の概要 |
具体的研究項目(A1-B2)に加え，それらに通底する理論的基盤について研究を進め，（いくつかのトップ国際会議論文を含む）複数の論文として成果を発表した．
[中川・蓮尾，TGC'16]においては，「できるだけ早く何かを実現したい」等の仕様を表現できる線形時相論理の割引付き解釈に対して，近最適スケジューラを求める方法を与えた．これは研究項目(A1,A2)に寄与する成果である．
プログラミング言語分野のトップ国際会議での論文[蓮尾・清水・Cirstea, POPL'16]においては，不動点論理，特に最小不動点（活性）と最大不動点（安全性）が交替で現れる仕様の数学的基礎の研究に取り組んだ．このような交替性不動点論理式は，モデル検査においてはもちろん，近年では制御理論など，より広いヘテロジニアス・システムの品質保証の文脈で重要視されており，この成果は研究項目(A1,A2,B2)に寄与する重要な成果である．今後この成果の応用を追求する予定であるが，特に(A1)に関して，Buechi 受理条件付き確率的システムの間の模倣関係について成果を得て，論文を投稿した[卜部・清水・蓮尾, 投稿中]．
システム検証分野のトップ国際会議での論文[赤崎・蓮尾, CAV'15]においては，モデルベース開発の現場における反例生成の重要性に鑑み，仕様記述言語（時相論理）に《平均化様相演算子》を導入して，確率的最適化による反例生成を効率化する研究を行った．これは特に優れた論文として学術誌特集号への招待を受けた（現在査読中）．この成果は産業界の現場において形式論理の果たしうる役割を示唆するものとして，本研究において重要なものと考える．
論文[木戸・蓮尾・Chaudhuri, VMCAI'16]においては，超準アプローチ（研究項目(B2)の基盤）におけるスケーラビリティの課題を抽象解釈によって乗り越える試みを行った．ここでは抽象領域として凸多面体を用いたが，楕円等を用いる拡張について現在研究を推進している．
|
