Skip navigation
Skip navigation

Geometric Nontermination Arguments

Leike, Jan; Heizmann, Matthias

Description

We present a new kind of nontermination argument, called geometric nontermination argument. The geometric nontermination argument is a finite representation of an infinite execution that has the form of a sum of several geometric series. For so-called linear lasso programs we can decide the existence of a geometric nontermination argument using a nonlinear algebraic ∃-constraint. We show that a deterministic conjunctive loop program with nonnegative eigenvalues is nonterminating if an only if...[Show more]

CollectionsANU Research Publications
Date published: 2018
Type: Conference paper
URI: http://hdl.handle.net/1885/307613
Source: Tools and Algorithms for the Construction and Analysis of Systems, conference proceedings
DOI: 10.1007/978-3-319-89963-3_16
Access Rights: Open Access

Download

File Description SizeFormat Image
Geometric Nontermination Arguments.pdf349.22 kBAdobe PDFThumbnail


This item is licensed under a Creative Commons License Creative Commons

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator