A rewriting-based model checker for the linear temporal logic of rewriting

Kyungmin Bae, José Meseguer

Research output: Contribution to journalArticlepeer-review


This paper presents a model checker for LTLR, a subset of the temporal logic of rewriting TLR* extending linear temporal logic with spatial action patterns. Both LTLR and TLR* are very expressive logics generalizing well-known state-based and action-based logics. Furthermore, the semantics of TLR* is given in terms of rewrite theories, so that the concurrent systems on which the LTLR properties are model checked can be specified at a very high level with rewrite rules. This paper answers a nontrivial challenge, namely, to be able to build a model checker to model check LTLR formulas on rewrite theories with relatively little effort by reusing Maude's LTL model checker for rewrite theories. For this, the reflective features of both rewriting logic and its Maude implementation have proved extremely useful.

Original languageEnglish (US)
Pages (from-to)19-36
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Dec 20 2012


  • model checking
  • reflective transformation
  • rewriting logic
  • temporal logic of rewriting

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'A rewriting-based model checker for the linear temporal logic of rewriting'. Together they form a unique fingerprint.

Cite this