| 研究実績の概要 |
2017年度においては，獲得目標の一つである高階関数型確率的プログラムの静的解析アルゴリズムの開発に向けて，その基礎となる確率的状態機械および命令形プログラムの解析手法に特に注力して研究を継続した．国際会議予稿集論文として発表した論文 [Cirstea, Shimizu & Hasuo, CALCO’17], [Urabe, Hara & Hasuo, LICS’17] はこの方向の成果であり，圏論的定式化によって定性的なモデル検査アルゴリズムを定量的なアルゴリズムに拡張するものである．特に，理論計算機科学分野の旗艦国際会議で発表された後者の論文においては，圏論的一般論の具体化の一例として，確率的状態機械の可達性確率を定量的に下から近似する新奇な手法を与えた．近年確率的プログラミング言語の分野でマルチンゲールを基礎とした解析手法が盛んに研究されているが，前述の可達性確率近似手法はこれらと補完的関係にある手法である．これらのさまざまな解析手法について不動点理論の視点から理論的整理を行い，また自動解析アルゴリズムの理論整備と実装を行う論文を，現在準備中である [Takisaka, Oyabu, Urabe & Hasuo, in preparation]．
また，理論計算機科学分野の旗艦国際会議での予稿集論文 [Dal Lago, Tanaka, Yoshimizu, LICS’17] においては，並行計算を行う高階計算系を，複数トークンで拡張した GoI によって状態遷移系に翻訳する成果を得た．
|
