Reduction of the number of states and the acceleration of LMNtal parallel model checking

Ryo Yasuda, Taketo Yoshida, Kazunori Ueda

Research output: Contribution to journalArticlepeer-review


SLIM is an LMNtal runtime. LMNtal is a programming and modeling language based on hierarchical graph rewriting. SLIM features automata-based LTL model checking that is one of the methods to solve accepting cycle search problems. Parallel search algorithms OWCTY and MAP used by SLIM generate a large number of states for problems having and accepting cycles. Moreover, they have a problem that performance seriously falls for particular problems. We propose a new algorithm that combines MAP and Nested DFS to remove states for problems including accepting cycles. We experimented the algorithm and confirmed improvements both in performance and scalability.

Original languageEnglish
Pages (from-to)182-187
Number of pages6
JournalTransactions of the Japanese Society for Artificial Intelligence
Issue number1
Publication statusPublished - 2014


  • Accepting cycle search
  • Model checking
  • Nested depth first search
  • Parallelization

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence


Dive into the research topics of 'Reduction of the number of states and the acceleration of LMNtal parallel model checking'. Together they form a unique fingerprint.

Cite this