权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

AF: Small: Collaborative Research: Efficient Groebner Basis Computation in Boolean Rings for Temporal Logic Reasoning and Model Checking

AF：小：协作研究：用于时态逻辑推理和模型检查的布尔环中的高效 Groebner 基计算

基本信息

批准号：
1355991
负责人：
Quoc-Nam Tran
金额：
$ 6.04万
依托单位：
University of Texas at Tyler
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2013
资助国家：
美国
起止时间：
2013-08-19 至 2014-10-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1355991&HistoricalAwards=false
关键词：
AF Small Collaborative Research Efficient

项目摘要

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.

Groebner基的方法已经成为在多元多项式理想理论、计算代数和消去理论、求解代数方程组和许多其他相关领域中提供非线性问题精确解的最重要的技术之一。它也被卓有成效地应用于各种看似不相关的研究领域，如几何定理证明、整数规划、实体建模和工程。本项目将发展一个有效的布尔环PSPACE Groebner基计算框架的理论和算法，并将该框架应用于时间逻辑推理和模型检验。本研究的理论和算法成果将对符号计算、时间逻辑推理以及模型检查中软硬件的自动验证等相关领域产生更广泛的影响。符号计算是近二十年来蓬勃发展的一个活跃而丰富的领域。一种利用符号计算结果进行时间逻辑推理和模型检验的新方法似乎有相当大的前景，既可以作为现有方法的补充，也可以作为一种将大量强大的数学机器引入模型检验问题的方法。