Generating model checkers from algebraic specifications

Teodor Rus, Eric Van Wyk, Tom Halverson

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


There is a great deal of research aimed toward the development of temporal logics and model checking algorithms which can be used to verify properties of systems. In this paper, we present a methodology and supporting tools which allow researchers and practitioners to automatically generate model checking algorithms for temporal logics from algebraic specifications. These tools are extensions of algebraic compiler generation tools and are used to specify model checkers as mappings of the form MC: Ls → Lt, where Ls is a temporal logic source language and Lt is a target language representing sets of states of a model M, such that MC(f ∈ Ls) = {s ∈ M

Original languageEnglish (US)
Pages (from-to)249-284
Number of pages36
JournalFormal Methods in System Design
Issue number3
StatePublished - May 1 2002


  • Algebraic specification
  • Compiler
  • Language
  • Macro-operation
  • Macro-processor
  • Model checking
  • Temporal logic

Fingerprint Dive into the research topics of 'Generating model checkers from algebraic specifications'. Together they form a unique fingerprint.

Cite this