The maude LTL model checker

Steven Eker, José Meseguer, Ambarish Sridharanarayanan

Research output: Contribution to journalConference articlepeer-review


The Maude LTL model checker supports on-the-fly explicit-state model checking of concurrent systems expressed as rewrite theories with performance comparable to that of current tools of that kind, such as SPIN. This greatly expands the range of applications amenable to model checking analysis. Besides traditional areas well supported by current tools, such as hardware and communication protocols, many new applications in areas such as rewriting logic models of cell biology, or next-generation reflective distributed systems can be easily specified and model checked with our tool.

Original languageEnglish (US)
Pages (from-to)162-187
Number of pages26
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Apr 2004
EventWRLA 2002, Rewriting Logic and it's Applications - Pisa, Italy
Duration: Sep 19 2002Sep 21 2002


  • Concurrent systems
  • Maude
  • Model checking

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'The maude LTL model checker'. Together they form a unique fingerprint.

Cite this