A Computational Method for Temporal Logic Reasoning and Model Checking

Temporal logic is widely used to specify hardware and software systems. Reasoning in temporal logic has been used as an algorithmic approach for model checking for automatically verifying whether a hardware or software system functions correctly. In this paper, we present a computational method for direct computation of Groebner bases (GB) in Boolean rings for temporal logic reasoning and model checking. In contrast to other known algebraic approaches, the degree of intermediate polynomials during the calculation of Groebner bases using our method will never grow resulted in a significant improvement in running time and memory space consumption. We also show how calculation in temporal logic for model checking can be done by means of our direct and efficient Groebner basis computation in Boolean rings. We compare our novel method with previous known methods and report our experimental results.