2017 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 | 形式検証 / 圏論 / 不動点 / Buechiオートマトン / parityオートマトン / supermartingale / 確率的オートマトン / ranking function |
|---|
| Outline of Annual Research Achievements |
サイバーフィジカルシステムなどの検証においては，システムの定性的な仕様だけでなく，定量的な仕様（「システムが正常に停止する確率は○○%以上」など）の検証も重要となる．本研究では既存の定性的なシステムの検証手法を圏論という数学の理論を用い一般化し，別の定量的なシステムに対し具体化する事で新しい定量的な検証手法を導出する事を目指す．
今年度は「Buechi／parityオートマトン」と呼ばれるシステムに対する検証手法の圏論的な一般化を目指し，その前段階としてそれらの「ふるまい」を圏論的に捉える研究を主に行った．申請者は同様の研究を前年度に行い一定の成果を得ているが，本年度の研究ではそれとは異なる新しい「ふるまい」の捉え方を行った．これにより前年度の枠組みでは扱えなかった検証手法を扱う事が可能になる事が期待される．この結果を論文としてまとめ、国際ワークショップCMCS2018に採択された．
更に，京大の滝坂氏，総研大の大藪氏と共同で確率的システムが停止する確率を「supermartingale」という概念を用い定量的に見積もる研究を行った．この研究では実際に実装・実験を行い，提案するアルゴリズムの有用性を確かめた．これは滝坂氏が主導して行った研究であり，申請者は具体的なアルゴリズムの導出等を行った．申請者の貢献度は25%程度である．この結果は今後論文としてまとめられ査読付きの国際会議に投稿される予定である．
又，前年度申請者は「ranking function」という検証手法を圏論的に一般化し，これを具体化する事で定量的システムに対し同種の概念を得る事に成功していた．この成果をまとめた論文は前年度国際会議LICS2017に投稿され採択されていたが，その発表が本年度申請者によって行われた．それ以外にも，ETAPS2017，POPL2018などの国際会議に参加し，議論及び動向調査を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画に関連する理論的な研究において，進展が得られた. まず，当初の研究計画にあった「申請者が前年度に得た確率的オートマトンに対するranking function」を用いた検証ツールの実装・評価については，本年度中に論文等の形で成果を発表するには至らなかったが，具体的なアルゴリズムを考案し，現在実装・評価を行おうとしている所である．考案したアルゴリズムは上述の滝坂氏，大藪氏と行った研究において実装したアルゴリズムと共通する部分があり，その実装においては本年度の経験が役に立つと考えている．また,前述の通り，本年度可能にしたBuechiオートマトン及びparityオートマトンに対し新しい「ふるまい」の捉え方により，これまでは扱えなかった検証手法の新たな圏論的な一般化が期待されるが，これは当初の研究計画にある「モデル検査の手法の圏論的な一般化，定量的な具体化」につながるものである.
|
| Strategy for Future Research Activity |
今年度は Buechiオートマトン及びparityオートマトンに対し，新しいふるまいの捉え方を可能にした．今後はこの枠組みを用いた既存の定性的検証手法の圏論的な一般化及びそれによる定量的検証手法の導出を目指す．具体的には，現在この結果を用いて「delayed simulation」という，Buechiオートマトンの状態数削減に有用である事が知られている検証手法を圏論的に一般化する研究をThorsten Wissmann氏と共に行っている．
また，今年度滝坂氏，大藪氏と行った研究も参考に，前年度得られた「確率的遷移系に対するranking function」を用いたツールの実装，及び実行時のリソース消費量の評価を行う事も目指す．この実装においては半正定値計画問題ソルバ（SDPソルバ）の利用が有効であると考えている．
更に，前年度，本年度，次年度の成果を博士論文として体系化する．
|
