Non-Termination Sets of Simple Linear Loops
Logic in Computer Science
2015-03-20 v1
Abstract
A simple linear loop is a simple while loop with linear assignments and linear loop guards. If a simple linear loop has only two program variables, we give a complete algorithm for computing the set of all the inputs on which the loop does not terminate. For the case of more program variables, we show that the non-termination set cannot be described by Tarski formulae in general
Cite
@article{arxiv.1206.0232,
title = {Non-Termination Sets of Simple Linear Loops},
author = {Liyun Dai and Bican Xia},
journal= {arXiv preprint arXiv:1206.0232},
year = {2015}
}
Comments
15 pages, 3 figures