AF: Small: Comprehensive Groebner, Parametric GCD Computations and Real Geometric Reasoning

University Of New Mexico, Albuquerque NM

Investigators

Abstract

Mathematical modeling of physical phenomena and cyber-physical systems and prediction from their behavior are hallmarks of scientific investigation. Checking validity of the modeling process is a critical component of this analytical approach. Polynomials are often one of the simplest tools employed in this endeavor. In order to model variations in the size of components and exogenous changes, variables in polynomials are typically classified into parameters and non-parameters. A prime and simple example is that of a quadratic equation a* square(x) + b * x + c, which behaves very differently for different values of its parameters a, b and c. It has equal solutions under certain parameter values, real solutions under other values and complex solutions or no solution at all under different parameter values. Structural properties of models are expressed using parameters since for different parameters, model can behave significantly different. It becomes critical to develop algorithms that can identify different classes of parameter values for which a model behaves significantly different. Such analysis will benefit many diverse applications including robotics, kinematics, modeling, computer vision, drug design based on molecular modeling and chemical relations, genetic pathways, and numerous cyber physical systems integrating control, hardware and software. The project has all of the theoretical, implementation and application components. The fundamental nature of problems investigated in this project and their application in many domain are likely to appeal to a broad set of students with diverse backgrounds especially from under-represented groups, both graduate and undergraduate. The material generated from this project will be integrated into courses on automated reasoning, mathematical modeling and cyber-physical systems that the researchers at the University of New Mexico (UNM) are teaching. The challenges offered and numerous benefits seen for the national laboratories in New Mexico and society at large by engaging in these investigations will attract participation and offer different career opportunities to the UNM students. This project is jointly funded by Algorithmic Foundations in Computing and Communications Foundations and the Established Program to Stimulate Competitive Research (EPSCoR). The project will involve algorithmic development research in solving parametric multivariate polynomial systems symbolically and real geometry reasoning. The main tool used is that of comprehensive Groebner basis computations and their use in many basic primitive used in other symbolic computation algorithms including parametric greatest common division of polynomials. These algorithms will serve as a basis for the development of a pragmatic, incomplete, approximate quantifier elimination approach over the complex numbers and the reals with the goal of producing meaningful and useful output for applications. Unlike Tarski's method and related algorithms based on Collins' Cylindrical Algebraic Decomposition (CAD), comprehensive Groebner basis computations will be used for polynomial equalities. Results about Positivstellensatz for inequalities using the sum of squares approach and real root counting based on quadratic forms will be explored. Techniques for Groebner basis computations will be adapted for polynomial inequalities to develop heuristics to decide non-negativity of polynomials. Since these problems are of very high computational complexity, their relevance in practical applications calls for developing special heuristics specific to application problems. The research team's experience in theorem proving and its application will be exploited to develop a software tool. Heuristics will be explored to make these implementations efficient. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.