Publication

Deciding Conditional Termination

2014
Article
Résumé

We address the problem of conditional termination, which is that of defining the set of initial configurations from which a given program always terminates. First we define the dual set, of initial configurations from which a non-terminating execution exists, as the greatest fixpoint of the function that maps a set of states into its pre-image with respect to the transition relation. This definition allows to compute the weakest non-termination precondition if at least one of the following holds: (i) the transition relation is deterministic, (ii) the descending Kleene sequence over-approximating the greatest fixpoint converges in finitely many steps, or (iii) the transition relation is well founded. We show that this is the case for two classes of relations, namely octagonal and finite monoid affine relations. Moreover, since the closed forms of these relations can be defined in Presburger arithmetic, we obtain the decidability of the termination problem for such loops. We show that the weakest non-termination precondition for octagonal relations can be computed in time polynomial in the size of the binary representation of the relation. Furthermore, for every well-founded octagonal relation, we prove the existence of an effectively computable well-founded witness relation for which a linear ranking function exists. For the class of linear affine relations we show that the weakest non-termination precondition can be defined in Presburger arithmetic if the relation has the finite monoid property. Otherwise, for a more general subclass, called polynomially bounded affine relations, we give a method of under-approximating the termination preconditions. Finally, we apply the method of computing weakest non-termination preconditions for conjunctive relations (octagonal or affine) to computing termination preconditions for programs with complex transition relations. We provide algorithms for computing transition invariants and termination preconditions, and define a class of programs, whose control structure has no nested loops, for which these algorithms provide precise results. Moreover, it is shown that, for programs with no nested control loops, and whose loops are labeled with octagonal constraints, the dual problem i. e. the existence of infinite runs, is NP-complete.

À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.