Non-termination Sets of Simple Linear Loops

DOI10.1007/978-3-642-32943-2_5MaRDI QIDQ2915099zbMATH OpenOpenAlexFDO

Authors Liyun Dai, Bican Xia

Publication date 21 September 2012

Published in Theoretical Aspects of Computing – ICTAC 2012 (Search for Journal in Brave)

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

zbMATH Keywords

eigenvalueterminationnon-termination setsimple linear loopTarski formula

Mathematics Subject Classification ID

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

Abstract: A simple linear loop is a simple while loop with linear assignments and linear loop guards. If a simple linear loop has only two program variables, we give a complete algorithm for computing the set of all the inputs on which the loop does not terminate. For the case of more program variables, we show that the non-termination set cannot be described by Tarski formulae in general

Recommendations

• On termination of integer linear loops
• Termination of linear loops over the integers
• scientific article; zbMATH DE number 3887949
• Reflections on termination of linear loops
• Termination of linear loops under commutative updates
• TERMINATION ANALYSIS OF LINEAR LOOPS
• On the termination of integer loops
• scientific article; zbMATH DE number 759546
• CONCUR 2005 – Concurrency Theory

Cited in

(2)

• A second-order formulation of non-termination
• Proving termination of nonlinear command sequences

This page was built for publication: Non-termination Sets of Simple Linear Loops

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