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...

Full description

Bibliographic Details
Main Authors: Radu Iosif, Filip Konecny, Marius Bozga
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