Detail publikace

Deciding Conditional Termination

Originální název

Deciding Conditional Termination

Anglický název

Deciding Conditional Termination

Jazyk

en

Originální abstrakt

This paper addresses the problem of conditional termination, which is that of defining the set of initial configurations from which a given program terminates. First we define the dual set, of initial configurations, from which a non-terminating execution exists, as the greatest fixpoint of the pre-image of the transition relation. This definition enables the representation of this set, whenever the closed form of the relation of the loop is definable in a logic that has quantifier elimination. This entails the decidability of the termination problem for such loops. Second, we present effective ways to compute the weakest precondition for non-termination for difference bounds and octagonal (non-deterministic) relations, by avoiding complex quantifier eliminations. We also investigate the existence of linear ranking functions for such loops. Finally, we study the class of linear affine relations and give a method of under-approximating the termination precondition for a non-trivial subclass of affine relations.We have performed preliminary experiments on transition systems modeling real-life systems, and have obtained encouraging results.

Anglický abstrakt

This paper addresses the problem of conditional termination, which is that of defining the set of initial configurations from which a given program terminates. First we define the dual set, of initial configurations, from which a non-terminating execution exists, as the greatest fixpoint of the pre-image of the transition relation. This definition enables the representation of this set, whenever the closed form of the relation of the loop is definable in a logic that has quantifier elimination. This entails the decidability of the termination problem for such loops. Second, we present effective ways to compute the weakest precondition for non-termination for difference bounds and octagonal (non-deterministic) relations, by avoiding complex quantifier eliminations. We also investigate the existence of linear ranking functions for such loops. Finally, we study the class of linear affine relations and give a method of under-approximating the termination precondition for a non-trivial subclass of affine relations.We have performed preliminary experiments on transition systems modeling real-life systems, and have obtained encouraging results.

BibTex


@article{BUT91442,
  author="Filip {Konečný} and Iosif {Radu} and Marius {Bozga}",
  title="Deciding Conditional Termination",
  annote="This paper addresses the problem of conditional termination, which is that of
defining the set of initial configurations from which a given program terminates.
First we define the dual set, of initial configurations, from which
a non-terminating execution exists, as the greatest fixpoint of the pre-image of
the transition relation. This definition enables the representation of this set,
whenever the closed form of the relation of the loop is definable in a logic that
has quantifier elimination. This entails the decidability of the termination
problem for such loops. Second, we present effective ways to compute the weakest
precondition for non-termination for difference bounds and octagonal
(non-deterministic) relations, by avoiding complex quantifier eliminations. We
also investigate the existence of linear ranking functions for such loops.
Finally, we study the class of linear affine relations and give a method of
under-approximating the termination precondition for a non-trivial subclass of
affine relations.We have performed preliminary experiments on transition systems
modeling real-life systems, and have obtained encouraging results.",
  address="NEUVEDEN",
  chapter="91442",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="7214",
  volume="2012",
  year="2012",
  month="april",
  pages="252--266",
  publisher="NEUVEDEN",
  type="journal article - other"
}