TY - JOUR
T1 - Speedup of OWCTY model checking algorithm using strongly connected components
AU - Kawabata, Toshiki
AU - Kobayashi, Fumiyoshi
AU - Ueda, Kazunori
PY - 2011
Y1 - 2011
N2 - 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 algorithmfor 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 algorithmremoves 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.
AB - 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 algorithmfor 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 algorithmremoves 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.
KW - Accepting cycle search
KW - Model checking
KW - Parallelization
KW - Strongly connected components
UR - http://www.scopus.com/inward/record.url?scp=78650971028&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78650971028&partnerID=8YFLogxK
U2 - 10.1527/tjsai.26.341
DO - 10.1527/tjsai.26.341
M3 - Article
AN - SCOPUS:78650971028
VL - 26
SP - 341
EP - 346
JO - Transactions of the Japanese Society for Artificial Intelligence
JF - Transactions of the Japanese Society for Artificial Intelligence
SN - 1346-0714
IS - 2
ER -