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

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.

Anglický 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.

BibTex

``````
@misc{BUT63914,
author="Peter {Habermehl} and Iosif {Radu} and Tomáš {Vojnar}",
title="A Logic of Singly Indexed Arrays",
annote="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.",