In this paper we introduce a class of constraint logic programs such that their termination can be proved by using affine level mappings. We show that membership to this class is decidable in polynomial time.
Recently, decidability of classes of imperative programs has been studied in @cite_19 @cite_10 @cite_1 . Tiwari considers real-valued programs with no nested loops and no branching inside a loop @cite_1 . Such programs correspond to one-binary-rule CLP( @math ). The author provides decidability results for subclasses of these programs. Our approach does not restrict nesting of loops and it allows internal branching . While in general termination of such programs is undecidable @cite_1 , we identified a subclass of programs with decidable termination property. Termination of the following CLP( @math ) program and its imperative equivalent can be shown by our method but not by the one proposed in @cite_1 . ] [ ]
@cite_1 @cite_19 @cite_10
1575647584 2136333450 1530375435
We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is, a while loop with linear assignments. We relate the termination of such a simple loop, on all initial values, to the eigenvectors corresponding to only the positive real eigenvalues of the matrix defining the loop assignments. This characterization of termination is reminiscent of the famous stability theorems in control theory that characterize stability in terms of eigenvalues. In order to verify semialgebraic programs, we automatize the Floyd Naur Hoare proof method. The main task is to automatically infer valid invariants and rank functions. First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd Naur Hoare verification conditions is handled by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using semidefinite programming solvers. This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal dual interior point methods generalizing those well-known in linear programming to convex optimization. The framework is applied to invariance and termination proof of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties. We present an automated method for proving the termination of an unnested program loop by synthesizing linear ranking functions. The method is complete. Namely, if a linear ranking function exists then it will be discovered by our method. The method relies on the fact that we can obtain the linear ranking functions of the program loop as the solutions of a system of linear inequalities that we derive from the program loop. The method is used as a subroutine in a method for proving termination and other liveness properties of more general programs via transition invariants; see [PR03].