Eventual linear ranking functions for multi-path linear loops
Guang Yu Zhu, Yi Li, Wenyuan Wu · 2016 IEEE Information Technology, Networking, Electronic and Automation Control Conference · 2016
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.