This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 WRI World Congress on Computer Science and Information Engineering
A Computational Method for Temporal Logic Reasoning and Model Checking
Los Angeles, California USA
March 31-April 02
ISBN: 978-0-7695-3507-4
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.
Index Terms:
Computational Method, Temporal Logic Reasoning, Groebner Basis, Model Checking
Citation:
Quocnam Tran, "A Computational Method for Temporal Logic Reasoning and Model Checking," csie, vol. 3, pp.55-59, 2009 WRI World Congress on Computer Science and Information Engineering, 2009
Usage of this product signifies your acceptance of the Terms of Use.