eng
episciences.org
Logical Methods in Computer Science
1860-5974
2014-08-21
Volume 10, Issue 3
10.2168/LMCS-10(3:8)2014
737
journal article
Deciding Conditional Termination
Radu Iosif
Filip Konecny
Marius Bozga
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
overapproximating 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.
https://lmcs.episciences.org/737/pdf
Computer Science - Logic in Computer Science
Computer Science - Formal Languages and Automata Theory