Witness to non-termination of linear programs

doi:10.1016/j.tcs.2017.03.036

CORC > 重庆绿色智能技术研究院 > 中国科学院重庆绿色智能技术研究院 > 自动推理与认知研究中心

	Witness to non-termination of linear programs
	Li, Yi
刊名	THEORETICAL COMPUTER SCIENCE
	2017-06-12
卷号	681 页码:75-100
关键词	Linear loops Program termination Semi-algebraic sets Witness to non-termination
ISSN号	0304-3975
DOI	10.1016/j.tcs.2017.03.036
通讯作者	Li, Y (reprint author), Chinese Acad Sci, Chongqing Inst Green & Intelligent Technol, Chongqing Key Lab Automated Reasoning & Cognit, Beijing, Peoples R China.
英文摘要	In his CAV 2004 paper, Tiwari has proved that, for a class of linear programs over the reals, termination is decidable. And Tiwari has shown that the termination of a linear program P-1 whose assignment matrix (A) over tilde is not in the Jordan canonical form is equivalent to that of a linear program J(1) whose assignment matrix A is in the Jordan Canonical Form. In most cases, the method of Tiwari provides only a so-called N-nonterminating point. In this paper, we propose two new methods to decide whether Program P-1 terminates or not over the reals. Our methods are based on the construction of a subset of the set NT of non-terminating points of Program J(1.) Any point in such a subset is a witness to non termination of Program J(1). Furthermore, it is shown that Program J(1) is non-terminating if and only if such a subset is nonempty. In terms of the property, the first method is given to check whether Program J(1) terminates or not. Different from the existing methods, the point obtained by our first method is a non-terminating point, rather than a N-nonterminating point. More importantly, such a subset is also proven to be A((B) over cap)-invariant for some positive integer (B) over cap. This enables us to check directly the termination of Program J(1) by verifying the satisfiability of finitely many quantified formulas over the reals. This suggests our second method for checking the termination of Program J(1). (C) 2017 Elsevier B.V. All rights reserved.
语种	英语
出版者	ELSEVIER SCIENCE BV
WOS记录号	WOS:000404502300006
内容类型	期刊论文
源URL	[http://172.16.51.4:88/handle/2HOD01W0/209]
专题	自动推理与认知研究中心
通讯作者	Li, Yi
作者单位	Chinese Acad Sci, Chongqing Inst Green & Intelligent Technol, Chongqing Key Lab Automated Reasoning & Cognit, Beijing, Peoples R China
推荐引用方式 GB/T 7714	Li, Yi. Witness to non-termination of linear programs[J]. THEORETICAL COMPUTER SCIENCE,2017,681:75-100.
APA	Li, Yi.(2017).Witness to non-termination of linear programs.THEORETICAL COMPUTER SCIENCE,681,75-100.
MLA	Li, Yi."Witness to non-termination of linear programs".THEORETICAL COMPUTER SCIENCE 681(2017):75-100.