On ranking functions for single-path linear-constraint loops

Program termination is a fundamental research topic in program analysis. In this paper, we present a new complete polynomial-time method for the existence problem of linear ranking functions for single-path loops described by a conjunction of linear constraints, when variables range over the reals (...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2020-12, Vol.22 (6), p.655-666
Main Authors: Li, Yi, Wu, Wenyuan, Feng, Yong
Format: Article
Language:English
Subjects:
Computer Science
Integers
Mathematical analysis
Polynomials
Ranking
Software Engineering
Software Engineering/Programming and Operating Systems
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Program termination is a fundamental research topic in program analysis. In this paper, we present a new complete polynomial-time method for the existence problem of linear ranking functions for single-path loops described by a conjunction of linear constraints, when variables range over the reals (or rationals). Unlike existing methods, our method does not depend on Farkas’ Lemma and provides us with counterexamples to existence of linear ranking functions, when no linear ranking function exists. In addition, we extend our results established over the rationals to the setting of the integers. This deduces an alternative approach to deciding whether or not a given SLC loop has a linear ranking function over the integers. Finally, we prove that the termination of bounded single-path linear-constraint loops is decidable over the reals (or rationals).
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-019-00549-9