データドリブン検証手法の圏論・不動点理論による抽象理論確立と新アルゴリズムの導出
| Project/Area Number |
22KJ1437
|
|---|
| Project/Area Number (Other) |
22J21742 (2022)
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Multi-year Fund (2023)
Single-year Grants (2022) |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
郡 茉友子 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2023-03-08 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2024: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2023: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2022: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | 形式検証 / 不動点 / 圏論 |
|---|
| Outline of Research at the Start |
データドリブン検証手法群を圏論と不動点理論をもちいて抽象化し統一的理論をつくるとともに、それを生かして新アルゴリズムの導出を目指す。検証問題は不動点理論と深いつながりがあり、また圏論による検証手法の抽象化はよりよい手法の考案につながる。また、データドリブン検証手法は高い実効性により近年注目を集めているが、基礎理論が不在でヒューリスティクス的な立ち位置に置かれがちだった。これらを踏まえ、本研究では応用上重要なデータドリブン検証手法を対象として、基礎理論を構築しよりよい手法を考案する。
|
| 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以外のデータドリブン検証手法に焦点を当て、抽象理論の樹立を目指す。
|
Report
(2 results)
Research Products
(9 results)
