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