2023 Fiscal Year Research-status Report
データドリブン検証手法の圏論・不動点理論による抽象理論確立と新アルゴリズムの導出
| Project/Area Number |
22KJ1437
|
|---|
| Allocation Type | Multi-year Fund |
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
郡 茉友子 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2023-03-08 – 2025-03-31
|
| Keywords | 形式検証 / 不動点 / 圏論 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、圏論と不動点理論を用いてデータドリブン検証手法の抽象理論を構築し、新たなアルゴリズムを導出することにある。
前年度では、データドリブン検証手法の一つであるIC3/PDRの抽象理論を構築していた。この抽象理論では、既存のアルゴリズムを数学的に自然な形で再構成し、様々なシステムに適用できるよう抽象化していたが、ヒューリスティクスに関する具体的な議論は不在で、システムごとに異なる非自明なヒューリスティクスを使っていた。
そのため、令和5年度ではこの点の改善を目指し、ヒューリスティクスを数学的に自然な形で得るための新たな理論の構築をし、新アルゴリズムを導出した。もとの抽象化では、一般的なシステムを対象とするために少ない構造を使っていたが、今回はまず構造を持たせた特定のシステムで抽象化した上で、抽象解釈を活用して汎用性のある新アルゴリズムを構築した。前回の試みよりも、システムのどの構造がアルゴリズムに必要なのかを明確にできたといえる。今回の抽象化では、不動点理論の双対的な二つの探索方法を組み合わせており、もとの抽象化よりIC3/PDRに本質的に近いものとなっている。また、新アルゴリズムは自動的に非自明なヒューリスティクスを備えており、特に確率的システムで有効であることを実験で確認した。
以上の成果についての論文は査読付き国際会議CAV'23に採択され、口頭発表も行った。また、Distinguished paper awardを受賞した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の研究計画は以下の通りである。
(1)データドリブン検証手法の一つであるCEGISの抽象理論樹立(採用前~2年目)、(2) データドリブン検証手法の一つであるIC3/PDRの抽象理論樹立(採用前~2年
目)、(3) 新アルゴリズムの開発と実装(2年目~3年目)。
(2), (3)に関しては目標を達成し、CAV'22, CAV'23論文として成果を発表した。しかし、(1)に関しては未着手である。
|
| Strategy for Future Research Activity |
令和5年度で、IC3/PDRに関して樹立した抽象理論をもとにした新アルゴリズムの導出という本研究の目標を達成したといえる。さらに、これまでの結果で作った複数のアルゴリズムを統合する理論を構築する予定である。
また、IC3/PDR以外のデータドリブン検証手法に焦点を当て、抽象理論の樹立を目指す。
|
