Journal articleKONEČNÝ Filip, IOSIF Radu and BOZGA Marius. Deciding Conditional Termination. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7214, pp. 252266. ISSN 03029743.  Publication language:  english 

Original title:  Deciding Conditional Termination 

Title (cs):  Rozhodování podmíněné konečnosti 

Pages:  252266 

Place:  DE 

Year:  2012 

Journal:  Lecture Notes in Computer Science, Vol. 2012, No. 7214, DE 

ISSN:  03029743 

Keywords 

termination problem, conditional termination problem, difference bounds relations, octagonal relations, finite monoid affine relations 
Annotation 

This paper addresses the problem of conditional termination, which is that of defining the set of initial configurations from which a given program terminates. First we define the dual set, of initial configurations, from which a nonterminating execution exists, as the greatest fixpoint of the preimage of the transition relation. This definition enables the representation of this set, whenever the closed form of the relation of the loop is definable in a logic that has quantifier elimination. This entails the decidability of the termination problem for such loops. Second, we present effective ways to compute the weakest precondition for nontermination for difference bounds and octagonal (nondeterministic) relations, by avoiding complex quantifier eliminations. We also investigate the existence of linear ranking functions for such loops. Finally, we study the class of linear affine relations and give a method of underapproximating the termination precondition for a nontrivial subclass of affine relations.We have performed preliminary experiments on transition systems modeling reallife systems, and have obtained encouraging results. 
BibTeX: 

@ARTICLE{
author = {Filip Konečný and Radu Iosif and Marius Bozga},
title = {Deciding Conditional Termination},
pages = {252266},
journal = {Lecture Notes in Computer Science},
volume = {2012},
number = {7214},
year = {2012},
ISSN = {03029743},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en?id=9986}
} 
