Detail publikace
A Logic of Singly Indexed Arrays
Originální název
A Logic of Singly Indexed Arrays
Anglický název
A Logic of Singly Indexed Arrays
Jazyk
en
Originální abstrakt
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.
Anglický abstrakt
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.
BibTex
@inproceedings{BUT34278,
author="Iosif {Radu} and Tomáš {Vojnar} and Peter {Habermehl}",
title="A Logic of Singly Indexed Arrays",
annote="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.",
address="Springer Verlag",
booktitle="Logic for Programming, Artificial Intelligence and Reasoning",
chapter="34278",
edition="Lecture Notes in Computer Science",
howpublished="print",
institution="Springer Verlag",
journal="Lecture Notes in Computer Science (IF 0,513)",
year="2008",
month="december",
pages="558--573",
publisher="Springer Verlag",
type="conference paper"
}