10.2168/LMCS-10(3:8)2014
https://lmcs.episciences.org/737
Iosif, Radu
Radu
Iosif
Konecny, Filip
Filip
Konecny
Bozga, Marius
Marius
Bozga
Deciding Conditional Termination
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.
Comment: 61 pages, 6 figures, 2 tables
episciences.org
Computer Science - Logic in Computer Science
Computer Science - Formal Languages and Automata Theory
arXiv.org - Non-exclusive license to distribute
2015-06-25
2014-08-21
2014-08-21
eng
journal article
arXiv:1302.2762
10.48550/arXiv.1302.2762
1860-5974
10.1145/3121136
10.17863/cam.41431
1983/bfcd960b-b1f8-4484-94d9-826cdf6635ba
https://lmcs.episciences.org/737/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 10, Issue 3
Researchers
Students