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

Ryo Yasuda, Taketo Yoshida, Kazunori Ueda

    Research output: Contribution to journalArticle


    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

    • Artificial Intelligence
    • Software

    Fingerprint 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