@inproceedings{83e8822bf1334897b5ece046201d6374,
title = "Geometric nontermination arguments",
abstract = "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 there exists a geometric nontermination argument. Furthermore, we present an evaluation that demonstrates that our method is feasible in practice.",
author = "Jan Leike and Matthias Heizmann",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2018.; 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 ; Conference date: 14-04-2018 Through 20-04-2018",
year = "2018",
doi = "10.1007/978-3-319-89963-3_16",
language = "English",
isbn = "9783319899626",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "266--283",
editor = "Dirk Beyer and Marieke Huisman",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings",
address = "Germany",
}