2018 Fiscal Year Annual Research Report
定性的検証手法の余代数による一般化と，定量的検証手法の導出
| Project/Area Number |
16J08157
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
卜部 夏木 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2016-04-22 – 2019-03-31
|
| Keywords | 形式検証 / 圏論 / 不動点 / 確率的システム / マルチンゲール / ランキング関数 / テイル確率 / スーパバイザリ制御 |
|---|
| Outline of Annual Research Achievements |
前々年度，申請者は「ランキング関数」という検証手法を圏論的に一般化・具体化する事で確率的遷移系に対し「γ縮尺劣マルチンゲール」と呼ばれる概念を得る事に成功した．これを用いると確率的遷移系の停止確率の下限を定量的に見積もることができる．今年度は京都大学の滝坂透氏，総合研究大学院大学の大藪雄一郎氏との共同研究の一環で，確率的プログラムの停止確率の下限をγ縮尺劣マルチンゲールを用い計算するアルゴリズムを提案し，それを実際に実装・実験を行ってその有用性を確かめた．申請者は具体的なアルゴリズムの導出および実装の一部を担当した．申請者の貢献度は20%程度である．結果をまとめた論文は国際会議ATVA 2018に採択された．
確率的システムに対し，その終了までにかかるステップ数がある値以上になる確率を「テイル確率」と呼ぶ．東京大学の内藏理史と共同で，マルチンゲールを用いて確率的システムのテイル確率の上限を与える研究も行った．申請者の貢献度は10%程度である．結果をまとめた論文は国際会議TACAS 2019に採択された．
また，大阪大学の榊原愛海氏および潮俊光教授と共同で離散事象システムのスーパバイザリ制御に関する研究も行った．本研究ではLTL[F]と呼ばれる線形時相論理（LTL）の定量的な拡張を考え，与えられたLTL[F]式の評価値がある閾値を超えるように離散事象システムを制御するスーパーバイザを構成する方法を与えた．申請者の貢献は50%程度である．結果をまとめた論文は今後査読付きの雑誌に投稿される予定である．
また，前年度国際ワークショップCMCS 2018に投稿され採択されていた論文の発表が本年度申請者によって行われた．それ以外にも，国際会議CPS Week 2018およびETAPS 2018に参加し，議論及び動向調査を行った．
また，前々年度，前年度，本年度の成果を博士論文として体系化した．
|
| Research Progress Status |
平成30年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
平成30年度が最終年度であるため、記入しない。
|
