A Forward Analysis for Recurrent Sets

8 years 10 days ago

Download www.cs.le.ac.uk

Non-termination of structured imperative programs is primarily due to inﬁnite loops. An important class of non-terminating loop behaviors can be characterized using the notion of recurrent sets. A recurrent set is a set of states from which execution of the loop cannot or might not escape. Existing analyses that infer recurrent sets to our knowledge rely on one of: the combination of forward and backward analyses, quantiﬁer elimination, or SMT-solvers. We propose forward abstract interpretation–based analysis that can be used together ossibly complicated abstract domain where none of the above is readily available. The analysis searches for a recurrent set of every individual loop in a by building a graph of abstract states and analyzing it in a novel way. The graph is searched for a witness of a recurrent set that takes the form of what we call a recurrent component which is somewhat similar to the notion of an end component in a Markov decision process.

Alexey Bakhirkin, Josh Berdine, Nir Piterman

Real-time Traffic