Generating exact nonlinear ranking functions by symbolic-numeric hybrid method |
| |
Authors: | Liyong Shen Min Wu Zhengfeng Yang Zhenbing Zeng |
| |
Institution: | 11004. School of Mathematical Sciences, Graduate University of Chinese Academy of Sciences, Beijing, 100049, China 21004. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China
|
| |
Abstract: | This paper presents a hybrid symbolic-numeric algorithm to compute ranking functions for establishing the termination of loop programs with polynomial guards and polynomial assignments. The authors first transform the problem into a parameterized polynomial optimization problem, and obtain a numerical ranking function using polynomial sum-of-squares relaxation via semidefinite programming (SDP). A rational vector recovery algorithm is deployed to recover a rational polynomial from the numerical ranking function, and some symbolic computation techniques are used to certify that this polynomial is an exact ranking function of the loop programs. At last, the authors demonstrate on some polynomial loop programs from the literature that our algorithm successfully yields nonlinear ranking functions with rational coefficients. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|