GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD

查看全文 作　　者：SHEN [1]Liyong;WU [2]Min;YANG [2]Zhengfeng;ZENG [2]Zhenbing

机构地区：[1]School of Mathematical Sciences,Graduate University of Chinese Academy of Sciences;[2]Shanghai Key Laboratory of Trustworthy Computing,East China Normal University

出　　处：《Journal of Systems Science & Complexity》索引2013年第26卷第2期,共11页

基　　金：supported in part by the National Natural Science Foundation of China under Grant Nos.10901055,61021004,91118007;by NKBRPC 2011CB302802,2011CB70690;by the Fundamental Research Funds for the Central Universities under Grant No.78210043 摘　　要：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. 关键词：非线性混合法参数多项式函数混合算法循环程序计算技术优化问题

相关文献

参考文献（21）
引证文献（8）
耦合文献（0）

参考文献(21)

引证文献(8)

互联网出版许可证新出网证(渝)字10号全国400电话 - 免长途话费

GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD

参考文献(21)

引证文献(8)

用户提示