2020 Fiscal Year Annual Research Report
A divide and conquer approach to parallelization of LTL model checking
| Project/Area Number |
19H04082
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | モデル検査 / 状態爆発 / Leads-to性質 / 分割統治 / 並列化 |
|---|
| Outline of Annual Research Achievements |
（１）当該年度に予定していた研究実施計画に則り研究を実施し、以下の実績を達成した：
理論研究：pとqを状態命題としたとき、状態空間に対するp |-> q（Leads-to性質）のモデル検査と等価となる、状態空間を２以上（L+1、ここでLは正整数）のレイヤーに分割し得られる複数の小さな状態空間に対するモデル検査を行う方法を考案すると共に等価性の証明を行った。アルゴリズムの考案：理論研究で得られる「状態空間をL+1レイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法」に基づきアルゴリズムを設計した。支援ツールの開発：そのアルゴリズムを実現する支援ツールの逐次版と並列版のプロトタイプをMaudeを実装言語として用いて作成した。事例研究：既存のLTLモデル検査器では状態爆発のためモデル検査不能になる事例を支援ツールの逐次版を用いることでモデル検査可能になること、支援ツールの並列版を用いることでモデル検査の実行速度が改善できることを確認した。研究成果発表：理論研究の成果を国際学術誌The Computer Journal（CORE Rank B、IF 1.077、SJR Q2）に論文として発表すると共に支援ツールの逐次版と並列版に関する論文を国際会議に投稿した。
（２）当該年度には予定していなかった研究成果を達成した：
Leads-to性質に加え、Eventual性質（<> p, ここでpは状態命題）のモデル検査にも提案方法を拡張できることを示すと共に理論研究の成果を国際学術誌Mathematics（IF 1.747, SJR Q3）に論文として発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
当該年度に予定していた研究成果を達成すると共に当該年度には予定していなかった研究成果を達成したためである。当該年度には予定していなかった研究成果とは、Leads-to性質に加え、Eventual性質（<> p, ここでpは状態命題）のモデル検査にも提案手法を拡張できることを示すと共に理論研究の成果を国際学術誌Mathematics（IF 1.747, SJR Q3）に論文として発表したことである。
|
| Strategy for Future Research Activity |
2021年度の研究実施計画に則り本研究課題を推進する。
理論研究：状態空間を２以上（L+1、ここでLは正整数）のレイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法をLeads-to性質（p |-> q、ここでpとqは状態命題）とEventual性質（<> p、ここでpは状態命題）以外のLTL性質に拡張する。
アルゴリズムの考案：理論研究で得られる成果に基づきアルゴリズムを考案する。
支援ツールの開発：Leads-to性質用の支援ツールを完成させると共にEventual性質用の支援ツールのプロトタイプを作成する。
事例研究：相互排除プロトコル（たとえば、Dijkstraのバイナリセマフォの抽象化版であるQlock）を例に用い事例研究を行い、提案方法の有効性を確認する。
研究成果発表：国際会議（たとえば、Asia-Pacific Software Engineering Conference；2021年12月頃；CORE Rank B）や国際学術誌（たとえば、International Journal of Software Engineering and Knowledge Engineering；IF 0.4；CORE Rank B）に論文を投稿する。
|
