Computer Science and Information Engineering, World Congress on (2009)
Los Angeles, California USA
Mar. 31, 2009 to Apr. 2, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSIE.2009.932
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.
Computational Method, Temporal Logic Reasoning, Groebner Basis, Model Checking
Q. Tran, "A Computational Method for Temporal Logic Reasoning and Model Checking," 2009 WRI World Congress on Computer Science and Information Engineering, CSIE(CSIE), Los Angeles, CA, 2009, pp. 55-59.