Speedup of OWCTY model checking algorithm using strongly connected components

Toshiki Kawabata, Fumiyoshi Kobayashi, Kazunori Ueda

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)341-346
Number of pages6
JournalTransactions of the Japanese Society for Artificial Intelligence
Volume26
Issue number2
DOIs
Publication statusPublished - 2011 Jan 12

Keywords

  • Accepting cycle search
  • Model checking
  • Parallelization
  • Strongly connected components

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Speedup of OWCTY model checking algorithm using strongly connected components'. Together they form a unique fingerprint.

  • Cite this