データドリブン検証手法の圏論・不動点理論による抽象理論確立と新アルゴリズムの導出

利用范畴论和不动点理论建立数据驱动验证方法的抽象理论并推导新算法

• 批准号: 22KJ1437
• 负责人: 郡 茉友子
• 金额: $ 1.6万
• 依托单位: The Graduate University for Advanced Studies
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2023
• 资助国家: 日本
• 起止时间: 2023-03-08 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22KJ1437/
• 关键词: 形式検証; 不動点; 圏論

本研究ではデータドリブン検証手法群を圏論と不動点理論をもちいた抽象理論の樹立と、それを生かして新アルゴリズムを導出することを目指している。令和4年度はデータドリブン検証手法の一つであるIC3/PDRの抽象化を行った。束論とその不動点理論を用いて抽象化を行い、最小不動点がある値以下かどうかという非常に一般的な問題を解くアルゴリズムを擬似コードとして記述した。この抽象化されたアルゴリズムから、束などのパラメータを変えることで具体化を行うことができる。特に遷移システムに対して具体化するために、圏論の余代数とファイブレーションを用いたフレームワークを作った。これにより既存のIC3/PDR由来のアルゴリズムを統一的に扱うことができた。理論的な結果だけでなく、擬似コードをもとにHaskellで実装を行った。型クラスを用いて抽象度を保った実装を行い、ユーザーが様々な具体化を扱えるように実装した。以上の成果についての論文は査読付き国際会議CAV'22に採択され、口頭発表も行った。IC3/PDRに関しては抽象理論の樹立という本研究の目標を達成したといえる。また、ピサ大学のFilippo Bonchi氏のもとで研究活動を行い、CAV'22論文で樹立した抽象理論をもとにアルゴリズムの改善に取り組んだ。抽象化によって他の手法を適用しやすくなったことを利用し、改善を行った。特に、不動点を使った検証において効果的な手法である抽象解釈を参考にした。令和5年度は引き続き抽象化を生かしてアルゴリズムの改善を目指す予定である。

在本研究中，我们的目标是利用范畴论和不动点理论建立数据驱动验证方法的抽象理论，并利用该理论推导新的算法。 2020财年，我们抽象出了IC3/PDR，这是数据驱动的验证方法之一。我使用束理论及其不动点理论对其进行了抽象，并编写了一个伪代码算法来解决最小不动点是否小于或等于某个值的非常普遍的问题。从这个抽象算法中，可以通过更改捆绑等参数使其具体化。为了将其专门应用于过渡系统，我使用范畴论中的余代数和纤维化创建了一个框架。这使得以统一的方式处理现有的 IC3/PDR 派生算法成为可能。我们不仅基于理论结果，还基于伪代码在 Haskell 中实现了它。我们使用类型类来维护抽象级别并实现它，以便用户可以处理各种实例化。上述结果的论文被同行评审的国际会议CAV'22接受，并进行了口头报告。可以说，本研究建立IC3/PDR抽象理论的目的已经达到。他还在比萨大学 Filippo Bonchi 的指导下进行了研究活动，并致力于基于其 CAV'22 论文中建立的抽象理论改进算法。我们利用抽象使得应用其他方法变得更容易这一事实进行了改进。我们特别提到了抽象解释，这是使用不动点进行验证的有效方法。 2025 财年，我们计划继续利用抽象来改进算法。

项目成果

University of Pisa(イタリア)

比萨大学（意大利）

The Lattice-Theoretic Essence of Property Directed Reachability Analysis.

属性导向可达性分析的格理论本质。

• 发表时间: 2022
• 作者: Mayuko Kori