Publication Details
A Logic of Singly Indexed Arrays
mathematical logic, arrays, decidability, decision procedure, formal verification, automata
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.
@techreport{BUT63914,
author="Peter {Habermehl} and Iosif {Radu} and Tomáš {Vojnar}",
title="A Logic of Singly Indexed Arrays",
year="2008",
publisher="VERIMAG",
address="TR-2008-9, Grenoble",
pages="19",
url="http://www-verimag.imag.fr/TR/TR-2008-9.ps"
}