Publication detail

A Logic of Singly Indexed Arrays

IOSIF, R. VOJNAR, T. HABERMEHL, P.

Original Title

A Logic of Singly Indexed Arrays

English Title

A Logic of Singly Indexed Arrays

Type

conference paper

Language

en

Original Abstract

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.

English abstract

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.

Keywords

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

RIV year

2008

Released

03.12.2008

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-540-89438-4

Book

Logic for Programming, Artificial Intelligence and Reasoning

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

558

Pages to

573

Pages count

16

Documents

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"
}