On the Complexity of Word-Level Model Checking with Arrays

Abstract

We study the computational complexity of deciding reachability in symbolic transition systems represented in quantifier-free first-order logic with bit-vectors and arrays. It is known that without arrays, the problem is PSPACE-complete (resp. EXPSPACE-complete) if the bit-widths are encoded in unary (resp. binary). We show that the problem becomes EXPSPACE-complete (resp. 2-EXPSPACE-complete in the binary case) when arrays indexed by bit-vectors are present, even if array values are limited to bit-vector sorts. Further, we show that the problem is NONELEMENTARY if we allow arrays indexed by other arrays.