2019 Fiscal Year Research-status Report
効率的なωオートマトン操作法と非制限的仕様検証への応用
| Project/Area Number |
18K18028
|
|---|
| Research Institution | Takushoku University |
|---|
Principal Investigator |
島川 昌也 拓殖大学, 工学部, 助教 (00749161)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | ωオートマトン / 仕様検証 |
|---|
| Outline of Annual Research Achievements |
時間論理などの数学的な言語でシステムの振る舞い（トレース）に関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，時間論理仕様の検証の効率化に向けて，仕様検証において基盤となるωオートマトンや無限ゲームの操作・判定における効率化手法の提案，及びそれを基盤とする効率的な仕様検証法の提案を行う．令和元年度は，以下について取り組んだ．
＜無限ゲームの単純化手法について＞ ：昨年度提案した無限ゲームの単純化手法を実験により評価し，多くの例題でこの手法が有効であることを確認した．
＜ωオートマトン操作・判定の効率的な実装方法について＞：部分シンボリック技法というオートマトン操作・判定の実装技法をユニバーサル木オートマトンの空判定に適用する方法を提案した．部分シンボリック技法とは，我々が過去に与えたオートマトン操作・判定の実装技法である．通常のシンボリック技法では，オートマトン全体を一つのBDD (Binary Decision Diagram)で表現するのに対して，この部分シンボリック技法では，各状態からのエッジをBDDで表現する（この技法は多様なオートマトン操作・判定に適用できるという長所を持つ．通常のシンボリック技法は一部のオートマトン操作への適用が難しい．）．この技法により，一部のユニバーサル木オートマトンの空判定をより効率的に行える．
|
| 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 |
（理由）国際会議の参加費や英文校正費にあてる予定であった分が学内予算でまかなえたため，次年度使用額が生じた．
（利用計画）計算機環境の充実，国際会議への参加，及び英文校正にあてる予定である．
|
