Eventual Linear Ranking Functions for Multi-path Linear Loops

摘要：

　　Termination of linear loop programs has received extensive attention in these years.In this paper,we focus on the termination of multi-path linear constraint loops.For a multi-path linear constraint loop which has no global linear ranking functions or lexicographic linear ranking functions,we present two complete methods to synthesize global eventual linear ranking functions and lexicographic eventual linear ranking functions of such loops,respectively.

关键词： Termination Analysis Eventual Linear Ranking Functions Multi-path Linear Constraint Loop Programs Regular Chains

作者: Guang Zhu Yi Li Wenyuan Wu

作者单位: College of Computer Science and Technology Chongqing University of Posts and Telecommunications Chon Key Laboratory of Automated Reasoning and Cognition CIGIT,CAS,Chongqing,China 400714

会议类型: 国际会议

会议名称: 2016IEEE第二届信息技术、网络、电子及自动化控制会议

会议地点: 重庆

会议语种:英文

页码: 331-337

在线出版日期: 2016-03-20（万方平台首次上网日期，不代表论文的发表时间）