2018 Fiscal Year Research-status Report
効率的なωオートマトン操作法と非制限的仕様検証への応用
| Project/Area Number |
18K18028
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
島川 昌也 東京工業大学, 情報理工学院, 助教 (00749161)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | ωオートマトン / 仕様検証 |
|---|
| Outline of Annual Research Achievements |
時間論理などの数学的な言語でシステムの振る舞い（トレース）に関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，時間論理仕様の検証の効率化に向けて，仕様検証において基礎となるωオートマトンや無限ゲームの操作・判定の効率化手法の提案，及びそれを利用した効率的な仕様検証器の実装を行う．
本年度は，無限ゲームの単純化手法の開発に取り組んだ．一部の仕様検証においては，仕様から無限ゲームを構成してそれを解析する．一般にその無限ゲームのサイズは大きく，検証のコストは高い．その問題を低減するため，以下に取り組んだ．(A)無限ゲーム上の模倣関係を導入した．この模倣関係は，非決定性グラフの模倣関係の一般化となっている（非決定性グラフは選言的な分岐のみを持つのに対して，無限ゲームは連言的な分岐も持つ）．(B) Aの模倣関係をベースに，勝利戦略が存在するかを判定する上で不必要なエッジを無限ゲームから取り除く手法を提案した．(C) Bの単純化を仕様から無限ゲームを構成する途中に（on-the-flyに）適用する手法を提案した（無限ゲームを構成される際に各ノードにラベルされる情報から模倣関係を算出できることを利用する）．上記の単純化は，無限ゲームのサイズを小さくするだけでなく，無限ゲームを構成するコストを下げることもできる．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
無限ゲームの単純化手法の開発に取り組み，一定の成果が得られた．それゆえ，現在までの進捗状況はおおむね順調であると判断した．
|
| Strategy for Future Research Activity |
今年度提案した無限ゲーム単純化手法の実装方法について検討する．また，提案した単純化手法をより多くの例題を用いて実験により評価する．
|
| Causes of Carryover |
（理由）国際会議の参加費や英文校正費用にあてる予定であった分が学内予算でまかなえたため，次年度使用額が生じた．
（利用計画）実験の補助を学生に依頼するため，ノートPCを数台購入する予定である．残りは当初の計画通り，国際会議の参加費・旅費，及び英文校正費用にあてる予定である．
|
Research Products
(1 results)
