中国科学院重庆绿色智能技术研究院机构知识库

QQ客服 官方微博 反馈留言

	Witness to non-termination of linear programs
	Li, Yi
	2017-06-12
摘要	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.
关键词	Linear loops Program termination Semi-algebraic sets Witness to non-termination
DOI	10.1016/j.tcs.2017.03.036
发表期刊	THEORETICAL COMPUTER SCIENCE
ISSN	0304-3975
卷号	681页码:75-100
通讯作者	Li, Y (reprint author), Chinese Acad Sci, Chongqing Inst Green & Intelligent Technol, Chongqing Key Lab Automated Reasoning & Cognit, Beijing, Peoples R China.
收录类别	SCI
WOS记录号	WOS:000404502300006
语种	英语