What’s Decidable about Sequences

Abstract. We present a first-order theory of (finite) sequences with integer el-ements, Presburger arithmetic, and regularity constraints, which can model sig-nificant properties of data structures such as lists and queues. We give a deci-sion procedure for the quantifier-free fragment, based on an encoding into the first-order theory of concatenation; the procedure has PSPACE complexity. The quantifier-free fragment of the theory of sequences can express properties such as sortedness and injectivity, as well as Boolean combinations of periodic and arithmetic facts relating the elements of the sequence and their positions (e.g., “for all even i’s, the element at position i has value i + 3 or 2i”). The result-ing expressive power is orthogonal to that of the most expressive decidable log-ics for arrays. Some examples demonstrate that the fragment is also suitable to reason about sequence-manipulating programs within the standard framework of axiomatic semantics.