KMS Chongqing Institute of Green and Intelligent Technology, CAS
| Synthesis of ranking functions via DNN | |
Tan, Wang1,2; Li, Yi1 
| |
| 2021-02-26 | |
| 摘要 | We propose a new approach to synthesis of non-polynomial ranking functions for loops via deep neural network(DNN). Firstly, we construct a ranking function template by DNN structure. And then the coefficients of the template can be learned by the train-set we construct to get a candidate ranking function, which is transcendental and non-polynomial because of the existence of sigmoid activation function in the neural network. Finally, the candidate ranking function will be verified to show if it is a real ranking function. Most of the existing methods focus on linear or polynomial ranking functions, and are limited to verification tools, while in this paper we make progress regarding the synthesis of non-polynomial ranking functions and new verification method for candidate ranking functions. The experimental results show us that for some of loops from other work, we can find their ranking functions efficiently. Moreover, for some loops having multi-phase ranking functions obtained by existing methods, our method can directly detect their global ranking functions. Especially, our method can also detect the global ranking functions for some loops with transcendental terms, which cannot be dealt with by existing methods. |
| 关键词 | Ranking function DNN Termination Loop programs |
| DOI | 10.1007/s00521-021-05763-8 |
| 发表期刊 | NEURAL COMPUTING & APPLICATIONS
 |
| ISSN | 0941-0643 |
| 页码 | 21 |
| 通讯作者 | Li, Yi(liyi@cigit.ac.cn) |
| 收录类别 | SCI |
| WOS记录号 | WOS:000622272200002 |
| 语种 | 英语 |
