A divide and conquer approach to parallelization of LTL model checking

2022 Fiscal Year Final Research Report

• Project/Area Number: 19H04082
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: OGATA Kazuhiro 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
• Project Period (FY): 2019-04-01 – 2023-03-31
• Keywords: モデル検査 / 分割統治 / 並列化 / leads-to性 / eventual性 / 条件付安定性 / until性 / until安定性

Outline of Final Research Achievements

By splitting an infinite state tree constructed from each initial state into multiple layers and tackling each sub-state space, the state space explosion in model checking can be alleviated. By handling multiple sub-state spaces simultaneously, the model checking running performance can be improved. Several important classes of linear temporal logic (LTL) properties, such as leads-to properties, can be dealt with. We built sequential and parallel versions of a support tool for each property class and conduct cases studies with such tools, demonstrating the usefulness of the techniques proposed and the support tools.

Free Research Field

計算機科学

Academic Significance and Societal Importance of the Research Achievements

ソフトウェアは我々の生活に深く入り込んでいる。大変便利であるが、複雑であればあるほど潜在的不具合が存在する可能性は大きい。顕在化すると、財政的損失ばかりでなく人命にも危険が及ぶ可能性すらある。このため、潜在的不具合は可能な限り取り除いたほうが良い。そのための有望な技術にモデル検査がある。しかし、ソフトウェア産業界において日常業務での使用に耐えうるようにするには解決すべき課題がある。状態空間爆発の緩和と実行速度の改善だ。状態空間を複数の空間に分割することで状態空間爆発を緩和し、複数の部分状態空間を並列にモデル検査することで実行速度を改善した。ソフトウェア産業界での実用化に向けて前進できた。