University of Minnesota
Software Engineering Center

You are here

Teodor Rus

Recent Publications

Algebraic Implementation of Model Checking

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.