Algebraic Implementation of Model Checking

Abstract

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.