強連結成分の性質を用いたOWCTYモデル検査アルゴリズムの高速化
スポンサーリンク
概要
- 論文の詳細を見る
Model checking is an exhaustive search method of verification. Automata-based LTL model checking is one of the methods to solve accepting cycle search problems. Model checking is prone to state-space explosion, and we may expect that parallel processing would be a promising approach. However, the optimal sequential algorithm is based on post-order depth-first seach and is difficult to parallelize. Alternative parallel algorithms have been proposed, and OWCTY_reversed is one of them. OWCTY_reversed is known to be a stable and fast algorithm for models that accept some words, but it does not use the characteristics of the automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the SCCs (strongly connected components) of property automata. The algorithm removes states that are judged not to form accepting cycles faster than OWCTY_reversed. We experimented and compared the two algorithms using DiVinE, and confirmed improvements both in performance and scalability.
論文 | ランダム
- ウイグルで暴動 その理由とは
- ウイグルの母が語った「一万人が消された夜」
- 中国政府は彼らに何をしたのか 在日ウイグル人が語った暴動の深層
- AFTER TWENTY YEARS(5)建国六十年の中国が「ウイグルの緊張」に震える
- 被爆地からの提言 長崎原爆資料館にウイグルの被爆の実相を