2021 Fiscal Year Research-status Report
効率的なωオートマトン操作法と非制限的仕様検証への応用
| Project/Area Number |
18K18028
|
|---|
| Research Institution | Takushoku University |
|---|
Principal Investigator |
島川 昌也 拓殖大学, 工学部, 助教 (00749161)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | ωオートマトン / 仕様検証 |
|---|
| Outline of Annual Research Achievements |
時間論理などの数学的な言語でシステムの振る舞い(トレース)についての仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，時間論理仕様の検証の効率化に向けて，仕様検証において基礎となるωオートマトンや無限ゲームの操作・判定の効率化手法の提案，及びそれを利用した効率的な仕様検証器の実装を行う.
2021年度は，これまでに引き続き，部分シンボリック技法による効率的な実装手法の開発に取り組んだ．通常のシンボリック技法では，オートマトン全体をひとつのBinary Decision Diagram (BDD)で表現するのに対して，部分シンボリック技法ではBDDを部分的に利用する．通常のシンボリック技法には，煩雑な手続きへの適用が難しいという問題がある一方，部分シンボリック技法は，適用可能な範囲が広いという特徴を持つ．本年度は，部分シンボリック技法には複数のバリエーションがあるため，それらについて検討を行った．具体的には，次の2種類の部分シンボリックについて検討した：(i) 各遷移にラベルされる遷移条件をひとつのBDDで表現するアプローチ，(ii) 各状態からの複数の遷移をひとつのBDDで表現するアプローチ（BDDの変種であるMtBDDを利用）．また，この2種類の部分シンボリック技法のユニバーサルω木オートマトンの空判定への適用についても検討し，実際にそのパフォーマンスを実験により確認した．
|
| 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 |
(理由) 新型コロナウイルス感染症の影響で，国際会議に参加することができなかったため，次年度使用額が生じた．
(利用計画) 実験のための計算機の新調を検討している．
|
