Geometric nontermination arguments

DOI10.1007/978-3-319-89963-3_16MaRDI QIDQ2324233zbMATH OpenOpenAlexFDO

Authors Jan Leike, Matthias Heizmann

Publication date 16 September 2019

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1609.05207

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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 $exists$-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.

Recommendations

• scientific article; zbMATH DE number 1746669
• A geometrical argument for a theorem of G. E. Welters
• Geometric non-vanishing
• The geometry of non-distributive logics
• scientific article; zbMATH DE number 1745036
• Nonrealizability proofs in computational geometry
• Geometric finiteness and rationality
• scientific article; zbMATH DE number 500964
• A parametrized geometric finitness theorem

Cited in

(10)

• Synthesizing ranking functions for loop programs via SVM
• \textsc{LTL} falsification in infinite-state systems
• Automatic discovery of fair paths in infinite-state transition systems
• Termination of polynomial loops
• Proving the existence of fair paths in infinite-state systems
• Geometric degree of nonconservativity
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries
• Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
• Multiphase-linear ranking functions and their relation to recurrent sets
• The 2-dimensional constraint loop problem is decidable

This page was built for publication: Geometric nontermination arguments

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2324233)