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...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2014-08-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/737/pdf |
_version_ | 1797268680927608832 |
---|---|
author | Radu Iosif Filip Konecny Marius Bozga |
author_facet | Radu Iosif Filip Konecny Marius Bozga |
author_sort | Radu Iosif |
collection | DOAJ |
description | 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. |
first_indexed | 2024-04-25T01:36:20Z |
format | Article |
id | doaj.art-26e58fb05f53467ab2996778debc30ee |
institution | Directory Open Access Journal |
issn | 1860-5974 |
language | English |
last_indexed | 2024-04-25T01:36:20Z |
publishDate | 2014-08-01 |
publisher | Logical Methods in Computer Science e.V. |
record_format | Article |
series | Logical Methods in Computer Science |
spelling | doaj.art-26e58fb05f53467ab2996778debc30ee2024-03-08T09:37:13ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742014-08-01Volume 10, Issue 310.2168/LMCS-10(3:8)2014737Deciding Conditional TerminationRadu IosifFilip KonecnyMarius BozgaWe 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/pdfcomputer science - logic in computer sciencecomputer science - formal languages and automata theory |
spellingShingle | Radu Iosif Filip Konecny Marius Bozga Deciding Conditional Termination Logical Methods in Computer Science computer science - logic in computer science computer science - formal languages and automata theory |
title | Deciding Conditional Termination |
title_full | Deciding Conditional Termination |
title_fullStr | Deciding Conditional Termination |
title_full_unstemmed | Deciding Conditional Termination |
title_short | Deciding Conditional Termination |
title_sort | deciding conditional termination |
topic | computer science - logic in computer science computer science - formal languages and automata theory |
url | https://lmcs.episciences.org/737/pdf |
work_keys_str_mv | AT raduiosif decidingconditionaltermination AT filipkonecny decidingconditionaltermination AT mariusbozga decidingconditionaltermination |