|
時間論理などの数学的な言語でシステムの振る舞い(トレース)についての仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，時間論理仕様の検証の効率化に向けて，仕様検証において基礎となるωオートマトンや無限ゲームの操作・判定の効率化手法の提案，及びそれを利用した効率的な仕様検証器の実装を行う．
これまでに本研究では，ωオートマトン操作・判定の効率的な実装手法「部分シンボリック技法」を2種提案し，それらをユニバーサルω木オートマトンの空判定へ適用した際のパフォーマンスを実験により確認している（通常のシンボリック技法ではオートマトン全体をひとつのBDDで表現するのに対して，部分シンボリック技法ではBDDを部分的に利用する．通常のシンボリック技法には煩雑な手続きへの適用が難しいという問題がある一方，部分シンボリック技法は適用可能な範囲が広いという特徴を持つ．）2022年度は，ユニバーサルωオートマトン／非決定性ωオートマトンの積合成演算／和集合演算／補集合演算へ，2種類の部分シンボリック技法を適用する方法を検討し，実際にそのパフォーマンスを実験により確認した．2種の部分シンボリック技法のうちの片方（2021年度に提案したBDDの変種であるMtBDDを利用する技法）は，対象のオートマトンに非決定的な分岐が少ないときに特に有効であることがわかった．
また，これまでに提案してきたωオートマトン操作・判定の実装手法を基盤として，仕様検証器の実装を行った．積合成演算／和集合演算の実装法は部分仕様の統合において活用し，補集合演算や空判定の実装法は，仕様の実現可能性や強充足可能性と呼ばれる性質の判定において活用した．
|
