Algebraic Implementation of Model Checking Algorithms
Theodor Rus, Eric R. Van Wyk · Amast series in computing · 2007
We describe an algebraic methodology for implementing model checking algo-rithms. In this methodology temporal logic formulas are seen as phrases of a source language Ls and the sets of states of a as elements of an algebra of sets called the target language, Lt. Thus, the model checker becomes an algebraic compiler C: Ls! Lt which maps temporal logic formulas in Ls into the sets of states of the model in Lt which satisfy these formulas. Since algebraic compilers can be automatically generated from algebraic speci¯cations of the source and tar-get algebras this methodology enjoys the advantage of the automatic generation of model checking algorithms from the algebraic speci¯cation 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. 1