University of Minnesota
Software Engineering Center

You are here

Algebraic Implementation of Model Checking

Date of Publication: 
March 1996
Associated Research Groups: 
Publication Files: 
We describe an algebraic methodology for implementing model checking algorithms. In this methodology temporal logic formulas are seen as phrases of a source language L_s and the sets of states of a the associated model are seen as elements of an algebra of sets called the target language, L_t. Thus, the model checker becomes an algebraic compiler C : L_s -> L_t which maps temporal logic formulas in L_s into the sets of states of the model in L_t which satisfy these formulas. Since algebraic compilers can be automatically generated from algebraic specifications of the source and target algebras this methodology enjoys the advantage of the automatic generation of model checking algorithms from the algebraic specification of the temporal logics and their associated models. Also, since algebraic compilers implement translation via a homomorphism between the source and target algebras, which is a naturally parallel computation, the model checkers thus implemented are naturally parallel algorithms.
In Proc. of the 3rd AMAST Workshop on Real-Time Systems held in Salt Lake City, Utah March 6-8 1996.
@inproceedings{Eric96, author = "Rus, Teodor and Van Wyk, Eric", title = "Algebraic Implementation of Model Checking Algorithms", booktitle = "Third AMAST Workshop on Real-Time Systems, Proceedings", year = 1996, month = "March 6", pages = "267--279" }