episciences.org_737_20230327221811588
20230327221811588
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
18605974
08
21
2014
Volume 10, Issue 3
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
nonterminating execution exists, as the greatest fixpoint of the function that
maps a set of states into its preimage with respect to the transition
relation. This definition allows to compute the weakest nontermination
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.
08
21
2014
737
https://arxiv.org/licenses/nonexclusivedistrib/1.0
arXiv:1302.2762
10.48550/arXiv.1302.2762
10.1145/3121136
10.17863/cam.41431
1983/bfcd960bb1f8448494d9826cdf6635ba
10.2168/LMCS10(3:8)2014
https://lmcs.episciences.org/737

https://lmcs.episciences.org/737/pdf

https://lmcs.episciences.org/737/pdf