2022 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性 / eventual性 / 条件付安定性 / until性 / until安定性 |
|---|
| Outline of Annual Research Achievements |
線形時相論理（LTL）で表現可能な代表的な性質のクラス（lead-to性、eventual性、条件付安定性、until性、until安定性）に対し、各初期状態から構築される無限木を複数の層に分割し、複数の部分空間ごとに独立にモデル検査することでもとの状態空間に対するモデル検査と同等のモデル検査結果を得ることのできる技術を考案すると共に正当性を証明した。部分空間ごとに独立に行えるモデル検査を同時に行うことで並列モデル検査を可能とする。モデル検査におけるもっともやっかいな状態空間爆発を緩和可能であると共にモデル検査にとって重要な実行速度の改善に貢献することができる。until性とuntil安定性を除き、逐次版と並列版の支援ツールを作成した。支援ツールの作成にはMaudeを用いた。支援ツールの実装において、部分空間のモデル検査においてすべての反例をひとつずつ探すことが実行面におけるボトルネックになっていたため、Tarjanの提案した、強連結要素を探すアルゴリズム用いて一度にすべての反例を探すことの出来るモデル検査器を、MaudeのLTLモデル検査器で使われているソフトウェアコンポネントを再利用するとで作成し、支援ツールで利用することにした。これによりそのボトルネックを解消することができた。提案方法では、上述した無限木をどのような層に分割するのか（レイヤーコンフィグレーション）がモデル検査の性能に大きく影響する。そこで、より良いレイヤーコンフィグレーションを探すことを支援するツールを作成した。事例実験により効果を確認することができた。提案方法は、LTLモデル検査の並列化のみならず、セキュリティプロトコル専用の解析ツールであるMaude-NPAやJavaのモデル検査器であるJava Pathfinder（JPF）の並列化にも有効であることを示した。
|
| Research Progress Status |
令和4年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和4年度が最終年度であるため、記入しない。
|
