2020 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 |
時間論理などの数学的な言語でシステムの振る舞い（トレース）に関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，時間論理仕様の検証の効率化に向けて，仕様検証において基盤となるωオートマトンや無限ゲームの操作・判定における効率化手法の提案，及びそれを基盤とする効率的な仕様検証法の提案を行う．
2020年度は，2019年度に引き続き，ユニバーサルω木オートマトンの空判定手続きの部分シンボリック技法による効率的な実装手法の開発に取り組んだ．部分シンボリック技法は，オートマトンの操作・判定の手続きを効率的に実装する技法のひとつである．通常のシンボリック技法では，オートマトン全体をひとつのBinary Decision Diagram (BDD)で表現するのに対して，部分シンボリック技法では，BDDを部分的に利用する．通常のシンボリック技法には，次のような問題がある：(i)煩雑な手続きへの適用が難しい，(ii)他の効率化技法（特に，アルゴリズムレベル（上位レイヤ）での効率化）との併用が難しい．一方，部分シンボリック技法は，適用可能な範囲が広く，また他の効率化技法との併用が行いやすいという特徴を持つ．本年度は，昨年度に提案したユニバーサルω木オートマトン空判定の部分シンボリック技法による実装手法のパフォーマンスを実験により確認した．
|
| 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 |
部分シンボリック技法について，さらなる検討を行う予定である．部分シンボリック技法には，（BDDを利用してオートマトンのどの部分をどのように表現するかによって）いくつかのバリエーションがありえる．各バリエーションの特徴について考察していきたい．
|
| Causes of Carryover |
（理由）新型コロナウイルス感染症の影響で，国際会議に参加することができなかったため，次年度使用額が生じた．
（利用計画）より大規模な実験を行うため，計算サーバーの新調を検討している．
|
Research Products
(1 results)
