2016 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 | 形式検証 / 圏論 / 余代数 / 定量的システム / 確率的オートマトン / 模倣 / ranking function |
|---|
| Outline of Annual Research Achievements |
今後重要になると予想されるサイバーフィジカルシステム等の検証では，システムの定性的な仕様だけでなく，定量的な仕様の検証も重要となる．本研究では既存の定性的検証手法を圏論を用い一般化し，別の定量的なシステムに対し具体化する事で新しい定量的検証手法を導出する事を目指す．前年度は「模倣」と「ranking function」という２種の検証手法を圏論的に一般化・具体化する事を目指し，一定の成果を得た．
「模倣」については，Buechiオートマトンという定性的システムに対する既存の模倣の概念を，圏論的に一般化する事を目指した．その前段階としてまずBuechiオートマトンの「ふるまい」を圏論的に捉える事を目指し，成功した．この成果をまとめた論文を国際会議CONCUR2016に投稿し採択され，口頭発表を行った．そしてこの結果を用いBuechiオートマトンに対する既存の模倣の概念を圏論的に一般化し，確率的Buechiオートマトンと呼ばれる定量的システムへ新しい模倣の概念を定義する事に成功した．この結果は学術雑誌に投稿中である．
「ranking function」についても同様に，非決定性オートマトンという定性的システムに対するranking functionの概念の圏論的な一般化に成功し，これを具体化する事で確率的オートマトンという定量的システムに対しranking functionの概念を得る事に成功した．確率的オートマトンに対しては既にranking functionと同様の概念が既に知られていたが，我々が得た概念はこの既存の概念とは異なる新しい物である事がわかった．この成果をまとめた論文を国際会議LICS2017に投稿し採択された．
これらは申請者が主導し研究を行った．
又，LICS2016，CAV2016，POPL2017などの国際会議に参加し，議論及び動向調査を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
当初の計画に関連する理論的な研究において，予想もしなかった大きな進展が得られた．
まず，研究計画の通りBuechi オートマトンと呼ばれる定性的システムのふるまいの圏論的な特徴付け，及びそれを用いたBuechi オートマトンに対する模倣と呼ばれる検証手法の圏論的な一般化と具体化を行い，新しい模倣の概念を確率的 Buechi オートマトンと呼ばれる定量的変種に定義する事に成功した．これら成果をそれぞれ論文としてまとめ，国際会議及び学術雑誌に投稿し，前者は国際会議 CONCUR 2016 に採択され申請者が発表を行った．
当初の研究計画ではこの後，Buechi オートマトンの一般化である parity オートマトンへの拡張，及び応用を目指し得られた模倣の概念を用いた検証ツールの実装・評価を行うとしていたが，前年度の研究では代わりに模倣とは別の ranking function と呼ばれる検証手法について模倣と同様に圏論的な一般化と定量的システムへの具体化を行った．この成果も論文としてまとめ，国際会議 LICS 2017に採択された．
前者の「模倣」はシステムの安全性（safety）の検証に通常用いられるのに対し，後者の「ranking function」はシステムの活性（liveness）の検証に用いられる．したがって模倣だけでなく ranking function の概念を圏論的に一般化した事で将来の応用の範囲を広げることができたと考える．また，上述の通り国際会議論文２本が採択され，学術誌論文１本が投稿中である．
|
| Strategy for Future Research Activity |
前年度は「模倣（simulation）」と「ranking function」という定性的な検証手法を圏論的に一般化，具体化することで，定量的システムに対する新しい検証手法を定義する事に成功した．本年度はこの新しい検証手法を用いたツールの実装，及び実行時のリソース消費量の評価を行う事を主眼において研究を進める．特に最初は得られた検証手法のうち確率的オートマトンに対する ranking function についてこれを行うことを目指す．
|
