The method of Groebner bases has become one of the most important techniques in providing an exact solution of nonlinear problems in multivariate polynomial ideal theory, computational algebra and elimination theory, in solving systems of algebraic equations, and in many other related areas. It is also being fruitfully used in a variety of seemingly unrelated research areas such as geometric theorem proving, integer programming, solid modeling, and engineering.
This project will develop the theories and algorithms for an efficient framework of PSPACE Groebner basis computation in Boolean rings and then apply this framework to temporal logic reasoning and model checking. The theoretical and algorithmic results of this research should have a broader impact on symbolic computation, temporal logic reasoning and related areas such as automated verification of hardware and software in model checking. Symbolic computation is an active and rich area with enormous activity and progress in the last twenty years. A new approach to temporal logic reasoning and model checking making use of results from symbolic computation seems to have considerable promise, both as a supplement to existing methods and as a way to bring a large body of powerful mathematical machinery to bear on the model checking problem.
