Abstract | ||
---|---|---|
Multiphase ranking functions (M$Phi$RFs) are tuples $langle f_1,ldots,f_d rangle$ of linear functions that are often used to prove termination of loops in which the computation progresses through a number of phases. Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (Single-Path Constraint loops). The decision problem existence of a M$Phi$RF asks to determine whether a given SLC loop admits a M$Phi$RF, and the corresponding bounded decision problem restricts the search to M$Phi$RFs of depth $d$, where the parameter $d$ is part of the input. The algorithmic and complexity aspects of the bounded problem have been completely settled in a recent work. In this paper we make progress regarding the existence problem, without a given depth bound. In particular, we present an approach that reveals some important insights into the structure of these functions. Interestingly, it relates the problem of seeking M$Phi$RFs to that of seeking recurrent sets (used to prove non-termination). It also helps in identifying classes of loops for which M$Phi$RFs are sufficient. Our research has led to a new representation for single-path loops, the difference polyhedron replacing the customary transition polyhedron. This representation yields new insights on M$Phi$RFs and SLC loops in general. For example, a result on bounded SLC loops becomes straightforward. |
Year | DOI | Venue |
---|---|---|
2018 | 10.1007/978-3-030-32304-2_22 | static analysis symposium |
Field | DocType | Volume |
Discrete mathematics,Decision problem,Ranking,Computer science,Tuple,Polyhedron,Theoretical computer science,Linear function,Computation,Bounded function | Journal | abs/1811.07340 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Amir M Ben-Amram | 1 | 327 | 30.52 |
Amir M Ben-Amram | 2 | 327 | 30.52 |
Jesús J. Doménech | 3 | 0 | 0.34 |
S. Genaim | 4 | 112 | 4.94 |