Algebraic implementation of model checking algorithms

Theodor Rus, Erick Van Wyk

Research output: Chapter in Book/Report/Conference proceedingChapter


The following sections are included: Introduction, Algebraic Specification of CTL, Algebraic Implementation of a Model Checker, Structure of an Algebraic Compiler, The Macro Processor Generating Satisfiability Sets, Generating a Model Checker Program, Implementing the Macro Processor formula, Conclusions.

Original languageEnglish (US)
Title of host publicationReal-time Systems
Subtitle of host publicationModeling, Design And Applications
PublisherWorld Scientific Publishing Co.
Number of pages19
ISBN (Electronic)9789812708472
StatePublished - Jan 1 2007
Externally publishedYes

Bibliographical note

Publisher Copyright:
© 2007 by World Scientific Publishing Co. Pte. Ltd.


Dive into the research topics of 'Algebraic implementation of model checking algorithms'. Together they form a unique fingerprint.

Cite this