Technical reportHABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. TR20089, Grenoble: VERIMAG, 2008.  Publication language:  english 

Original title:  A Logic of Singly Indexed Arrays 

Title (cs):  Jednoindexová logika nad poli 

Pages:  19 

Place:  TR20089, Grenoble, FR 

Year:  2008 

Publisher:  VERIMAG 

URL:  http://wwwverimag.imag.fr/TR/TR20089.ps [PS] 

Keywords 

mathematical logic, arrays, decidability, decision procedure, formal verification, automata 
Annotation 

This report is the full version of an LPAR'08 paper, in which we present a logic interpreted over integer arrays, which allows
difference bound comparisons between array elements situated within a
constant sized window. We show that the satisfiability problem for the
logic is undecidable for formulae with a quantifier prefix
$\{\exists,\forall\}^*\forall^*\exists^*\forall^*$. For formulae with
quantifier prefixes in the $\exists^*\forall^*$ fragment, decidability
is established by an automatatheoretic argument. For each formula in
the $\exists^*\forall^*$ fragment, we can build a~flat counter
automaton with difference bound transition rules (FCADBM) whose traces correspond
to the models of the formula. The construction is modular, following
the syntax of the formula. Decidability of the $\exists^*\forall^*$
fragment of the logic is a consequence of the fact that reachability
of a control state is decidable for FCADBM. 
BibTeX: 

@TECHREPORT{
author = {Peter Habermehl and Radu Iosif and Tom{\'{a}}{\v{s}} Vojnar},
title = {A Logic of Singly Indexed Arrays},
pages = {19},
year = {2008},
location = {TR20089, Grenoble, FR},
publisher = {VERIMAG},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso88592?id=8817}
} 
