GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD

SHEN Liyong , WU Min , YANG Zhengfeng , ZENG Zhenbing

系统科学与复杂性(英文) ›› 2013, Vol. 26 ›› Issue (2) : 291-301.

PDF(189 KB)
PDF(189 KB)
系统科学与复杂性(英文) ›› 2013, Vol. 26 ›› Issue (2) : 291-301. DOI: 10.1007/s11424-013-1004-1

GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD

    SHEN Liyong1 , WU Min2 , YANG Zhengfeng2 , ZENG Zhenbing2
作者信息 +

GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD

    SHEN Liyong1 , WU Min2 , YANG Zhengfeng2 , ZENG Zhenbing2
Author information +
文章历史 +

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.

引用本文

导出引用
SHEN Liyong , WU Min , YANG Zhengfeng , ZENG Zhenbing. GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD. 系统科学与复杂性(英文), 2013, 26(2): 291-301 https://doi.org/10.1007/s11424-013-1004-1
SHEN Liyong , WU Min , YANG Zhengfeng , ZENG Zhenbing. GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD. Journal of Systems Science and Complexity, 2013, 26(2): 291-301 https://doi.org/10.1007/s11424-013-1004-1
PDF(189 KB)

157

Accesses

0

Citation

Detail

段落导航
相关文章

/