Generating model checkers from algebraic specifications

Teodor Rus, Eric Van Wyk, Tom Halverson

Research output: Contribution to journalArticlepeer-review

6 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 | s |= f}. The algebraic specifications for a model checker define the logic source language, the target language representing sets of states in a model, and the embedding of the source language into the target language. Since users can modify and extend existing specifications or write original specifications, new model checking algorithms for new temporal logics can be easily and quickly developed; this allows the user more time to experiment with the logic and its model checking algorithm instead of developing its implementation. Here we show how this algebraic framework can be used to specify model checking algorithms for CTL, a real-time CTL, CTL*, and a custom extension called CTLe that makes use of propositions labeling the edges as well as the nodes of a model. We also show how the target language can be changed to a language of binary decision diagrams to generate symbolic model checkers from algebraic specifications.

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

Bibliographical note

Copyright 2008 Elsevier B.V., All rights reserved.


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


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

Cite this