Termination of 2 variable constraint loops decided in polynomial time
On Deciding the Constraint Loop Problem in Dimension Two
Logic in Computer Science
Summary
The problem of checking whether certain loops in computer programs will stop or keep running forever has been an open question for a while. Previously, it was proven that for loops with two real-number variables, you can decide if they terminate. The authors improved this by showing the decision can be done much faster—in polynomial time instead of requiring much more resources. They also built a practical tool using existing software to efficiently check these loops.
What this means in practice
- •For software verification engineers: Efficiently determine if loops with two real-valued variables terminate to improve program correctness checks.
- •For embedded systems developers: Use fast termination checks for small-variable loops to ensure reliability and prevent infinite loops in device software.
Authors
Daria Goliasova, Toghrul Karimov
Abstract
Recently, Guilmant, Lefaucheux, Ouaknine, and Worrell [2] proved decidability of the termination problem for linear constraint loops over two real-valued variables, thus settling a wellknown open problem. Their algorithm is based on a theoretical result that such a loop does not terminate if and only if it has a witness of an infinite run of a specific shape. By analysing the structure of the witness carefully, we show that termination such loops can be decided in polynomial time, improving on the polynomial space bound argued by Guilmant et al. We also present an efficient implementation of the polynomial-time algorithm based on the satisfiability modulo theories (SMT) solver Z3.