A Logic of Singly Indexed Arrays

This report is the full version of an LPAR'08 paper, in which we present a logic interpreted over integer arrays, which allowsdifference bound  comparisons between array elements situated within aconstant sized window. We show that the satisfiability problem for thelogic is undecidable for formulae  with a quantifier prefix$\{\exists,\forall\}^*\forall^*\exists^*\forall^*$. For formulae  withquantifier prefixes in the $\exists^*\forall^*$ fragment, decidabilityis established  by an automata-theoretic argument. For each formula inthe $\exists^*\forall^*$ fragment, we  can build a~flat counterautomaton with difference bound transition rules (FCADBM) whose traces
correspondto the models of the formula. The construction is modular, followingthe syntax of  the formula. Decidability of the $\exists^*\forall^*$fragment of the logic is a consequence  of the fact that reachabilityof a control state is decidable for FCADBM.