Geometric Series as Nontermination Arguments for Linear Lasso Programs

We present a new kind of nontermination argument for linear lasso programs, called geometric nontermination argument. A geometric nontermination argument is a finite representation of an infinite execution of the form \((\vec{x} + \sum_{i=0}^t \lambda^i \vec{y})_{t \geq 0}\). The existence of this n...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2014-05
Main Authors: Leike, Jan, Heizmann, Matthias
Format: Article
Language:English
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a new kind of nontermination argument for linear lasso programs, called geometric nontermination argument. A geometric nontermination argument is a finite representation of an infinite execution of the form \((\vec{x} + \sum_{i=0}^t \lambda^i \vec{y})_{t \geq 0}\). The existence of this nontermination argument can be stated as a set of nonlinear algebraic constraints. We show that every linear loop program that has a bounded infinite execution also has a geometric nontermination argument. Furthermore, we discuss nonterminating programs that do not have a geometric nontermination argument.
ISSN:2331-8422