Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HABERMEHL, P., RADU, I., VOJNAR, T.
Originální název
A Logic of Singly Indexed Arrays
Typ
audiovizuální tvorba
Jazyk
angličtina
Originální abstrakt
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 automata-theoretic 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.
Klíčová slova
mathematical logic, arrays, decidability, decision procedure, formal verification, automata
Autoři
Vydáno
3. 12. 2008
Nakladatel
VERIMAG
Místo
TR-2008-9, Grenoble
Strany počet
19
URL
http://www-verimag.imag.fr/TR/TR-2008-9.ps
BibTex
@misc{BUT63914, author="Peter {Habermehl} and Iosif {Radu} and Tomáš {Vojnar}", title="A Logic of Singly Indexed Arrays", year="2008", pages="19", publisher="VERIMAG", address="TR-2008-9, Grenoble", url="http://www-verimag.imag.fr/TR/TR-2008-9.ps", note="presentation" }