Computer Science ›› 2017, Vol. 44 ›› Issue (1): 194-198, 213.doi: 10.11896/j.issn.1002-137X.2017.01.037

Previous Articles     Next Articles

New Method for Computing Eventual Linear Ranking Functions

ZHU Guang, LI Yi and WU Wen-yuan   

  • Online:2018-11-13 Published:2018-11-13

Abstract: Termination of linear loop programs has received extensive attention in these years.In this paper,we focused on the termination of linear constraint loops which has no traditional linear ranking functions.A method of detecting eventual linear ranking functions by Bagnara were introduced for termination analysis first.Such an eventual linear ranking function implies the loop terminates.We presented a new method for computing eventual linear ranking functions.Semi-algebraic systems,equivalent to linear increasing functions and eventual linear ranking functions,were established.Several methods for synthesizing eventual linear ranking functions were compared.And experimental results show that the semi-algebraic system for synthesis of eventual linear ranking functions established by our method is simpler.

Key words: Linear loop programs,Termination analysis,Eventual linear ranking functions,Mathematica

[1] BAGNARA R,MESNARD F.Eventual linear ranking functions[C]∥Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming.Madrid,Spain,ACM,2013: 229-238 .
[2] BAGNARA R,MESNARD F,PESCETTI A, et al.A new look at the automatic synthesis of linear ranking functions[J].Information and Computation,2012,215(3):47-67.
[3] BEN-AMRAM A M,GENAIM S,MASUD A.On the Termination of Integer Loops[M].Verification,Model Checking,and Abstract Interpretation.V.Kuncak and A.Rybalchenko,SpringerBerlin Heidelberg,2012,7148:72-87.
[4] BEN-AMRAM A M,GENAIM S.On the linear ranking problem for integer linear-constraint loops[C]∥Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL’13).Rome,Italy,ACM.2013:51-62.
[5] BEN-AMRAM A M,GENAIM S.Ranking Functions for Linear-Constraint Loops[J].Journal of the ACM,2014,61(4):1-55.
[6] BRADLEY A,MANNA Z,SIPMA H.Linear Ranking with Rea-chability.Computer Aided Verification[M].Etessami K,Rajamani S.Springer Berlin Heidelberg,2005,3576:491-504.
[7] BRADLEY A,MANNA Z,SIPMA H.The Polyranking Principle.Automata,Languages and Programming[M].Caires L,Ita-liano G,Monteiro L,et al.eds.,Springer Berlin Heidelberg,2005,3580:1349-1361.
[9] CHEN H Y,FLUR S,MUKHOPADHYAY S.TerminationProofs for Linear Simple Loops[M]∥Static Analysis.A.Miné and D.Schmidt,Springer Berlin Heidelberg,2012,0:422-438.
[10] CHEN Y H,XIA B C,YANG L,et al.Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems[M]∥Theoretical Aspects of Computing(ICTAC 2007).Springer Berlin Heidelberg,2007:34-49.
[11] CHEN Y H,XIA B X,YANG L,et al.Generating Polynomial Invariants with DISCOVERER and QEPCAD[M].Formal Methods and Hybrid Real-Time Systems.CliffB Jones,Zhiming Liu and Jim Woodcock,Springer Berlin Heidelberg,2007,4700:67-82.
[12] COLN M,SIPMA H.Synthesis of Linear Ranking Functions.Tools and Algorithms for the Construction and Analysis of Systems[M].T.Margaria and W.Yi,Springer Berlin Heidelberg,2001,2031:67-81.
[13] COOK B,GULWANI S,LEV-AMI T,et al.Proving Conditional Termination.Computer Aided Verification[M].A.Gupta and S.Malik,Springer Berlin Heidelberg,2008,5123:328-340.
[14] GANTY P,GENAIM S.Proving Termination Starting from the End.Computer Aided Verification[M].Sharygina N,Veith H.Springer Berlin Heidelberg,2013,8044:397-412.
[15] HEIZMANN M,HOENICKE J,LEIKE J,et al.Linear Ranking for Linear Lasso Programs[M].Automated Technology for Verification and Analysis.Van Hung D,Ogawa M.Springer International Publishing,2013,8172:365-380.
[16] PODELSKI A,RYBALCHENKO A.A Complete Method forthe Synthesis of Linear Ranking Functions[M].Verification,Model Checking,and Abstract Interpretation.Steffen B,Levi G.Springer Berlin Heidelberg,2004,2937:239-251.
[17] TIWARI A.Termination of Linear Programs.Computer Aided Verification[M].R.Alur and D.Peled,Springer Berlin Heidelberg,2004,3114:70-82.
[18] LI K,SHAN Z G,WANG J,et al.Overview on Major Research Plan of Trustworthy Software[J].Bulletin of National Natural Science Foundation of China,2008,2(3):145-151.(in Chinese) 李克,单志广,王戟,等.可信软件基础研究重大研究计划综述[J].中国科学基金,2008,22(3):145-151.
[19] YANG L,ZHANG J Z,HOU X R.Nonlinear Systems of Algebraic Equations and Automated Theorem Proving[M].Beijing:Shanghai Scientific and Technological Education Publishing House,1996.(in Chinese) 杨路,张景中,侯晓荣.非线性代数方程组与定理机器证明[M].北京:上海科技教育出版社,1996.
[20] YANG L,XIA B C.Inequality Machine Proving and Automated Discovery[M].Beijing:Science Press,2008.(in Chinese) 杨路,夏壁灿.不等式机器证明与自动发现[M].北京:科学出版社,2008.

No related articles found!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .