Radu Iosif ; Filip Konecny ; Marius Bozga - Deciding Conditional Termination

lmcs:737 - Logical Methods in Computer Science, August 21, 2014, Volume 10, Issue 3 - https://doi.org/10.2168/LMCS-10(3:8)2014
Deciding Conditional Termination

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

    Volume: Volume 10, Issue 3
    Published on: August 21, 2014
    Accepted on: June 25, 2015
    Submitted on: September 30, 2012
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1145/3121136
    Source : ScholeXplorer IsReferencedBy DOI 10.17863/cam.41431
    Source : ScholeXplorer IsReferencedBy HANDLE 1983/bfcd960b-b1f8-4484-94d9-826cdf6635ba
    • 10.1145/3121136
    • 10.1145/3121136
    • 10.1145/3121136
    • 1983/bfcd960b-b1f8-4484-94d9-826cdf6635ba
    • 10.17863/cam.41431
    Bit-Precise Procedure-Modular Termination Analysis
    Chen, Hong-Yi ; David, Cristina ; Kroening, Daniel ; Schrammel, Peter ; Wachter, Björn ;

    6 Documents citing this article


    Consultation statistics

    This page has been seen 535 times.
    This article's PDF has been downloaded 3538 times.