Groebner bases computation in Boolean rings for symbolic model checking
Quôc-Nam Trân, Moshe Y. Vardi · international conference on Modelling and simulation · 2007
Model checking is an algorithmic approach for automatically verifying whether a hardware or software system functions correctly. Typically, computation is carried over Boolean algebras using binary decision diagrams (BDDs) or satisfiability (SAT) solvers. In this paper we show that computation for model checking can also be carried over the dual Boolean rings of the Boolean algebras by means of efficient polynomial and Groebner basis (GB) computation. We also show how all operations required for model checking can be implemented by means of Groebner bases.