东篱科研大数据发现系统（DRDS）

位置：成果数据库 > 期刊 > 期刊详情页

DISCOVERING NON-TERMINATING INPUTS FOR MULTI-PATH POLYNOMIAL PROGRAMS

ISSN号：1009-6124
期刊名称：《系统科学与复杂性学报：英文版》
时间：0
分类：O15-4[理学—数学;理学—基础数学] TP393[自动化与计算机技术—计算机应用技术;自动化与计算机技术—计算机科学与技术]
作者机构：[1]Chongqing Key Laboratory of Automated Reasoning and Cognition, CIGIT, Chinese Academy of Sciences, Chongqing 400714, China, [2]Department of Computer Science and Technology, East China Normal University, Shanghai 200241, China., [3]State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China, [4]Chongqing Key Laboratory of Automated Reasoning and Cognition, CIGIT, Chinese Academy of Sci- ences, Chongqing 400714, China.
相关基金：This research was supported by the National Basic Research Program of China under Grant No. 2014CB340700, the National Science and Technology Major Project of China under Grant No. 2012ZX01039-004, the National Natural Science Foundation of China under Grant Nos. 91118007, 11071273, 61202131, 11401218, cstc2012ggB40004, cstc2013jjys40001, SRFDP under Grant No. 20130076120010, the Open Project of Shanghai Key Laboratory of Trustworthy Computing under Grant No. 07dz22304201307, and West Light Foundation of Chinese Academy of Sciences.

作者： LIU Jiang[1], XU Ming l[2], ZHAN Naijun[3], ZHAO Hengjun[3,4]

关键词：多项式理论, 多路径, 输入, 多项式理想, 充分条件, MPP, 方程式, 作者, Polynomial ideals, polynomial programs, termination analysis.

中文摘要：

这份报纸与方程式的环警卫一起调查多路径多项式节目(MPP ) 的结束问题。同时为结束和 nontermination 建立足够的条件，作者建议强壮 / 弱的非结束的观点它 under/over-approximates 非结束。基于多项式理想理论，作者证明所有强壮的非终止的输入(SNTI ) 的集合和弱非终止的输入(WNTI ) 两个都对应于某些多项式理想的真实变化。而且，作者证明 SNTI 的变化是可计算出来的，并且在一些足够的条件下面， WNTI 的变化也是可计算出来的。然后由在平行检查计算 SNTI 和 WNTI 变化，考虑 MPP 的结束性质能被维护。作为后果，作者为 MPP 的结束分析建立一个新框架。

英文摘要：

This paper investigates the termination problems of multi-path polynomial programs （MPPs） with equational loop guards. To establish sufficient conditions for termination and nontermination simultaneously, the authors propose the notion of strong/weak non-termination which under/over- approximates non-termination. Based on polynomial ideal theory, the authors show that the set of all strong non-terminating inputs （SNTI） and weak non-terminating inputs （WNTI） both correspond to tile real varieties of certain polynomial ideals. Furthermore, the authors prove that the variety of SNTI is computable, and under some sufficient conditions the variety of WNTI is also computable. Then by checking the computed SNTI and WNTI varieties in parallel, termination properties of a consid- ered MPP can be asserted. As a consequence, the authors establish a new framework for termination analysis of MPPs.

同期刊论文项目