A Second-Order Formulation of Non-Termination
Logic in Computer Science
2014-12-11 v1
Abstract
We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is generally undecidable. However, by restricting the language to known decidable cases, we exhibit new classes of loops, the non-termination of which is decidable. We present a bunch of examples.
Cite
@article{arxiv.1412.3271,
title = {A Second-Order Formulation of Non-Termination},
author = {Fred Mesnard and Etienne Payet},
journal= {arXiv preprint arXiv:1412.3271},
year = {2014}
}
Comments
8 pages