Detail publikace

A Logic of Singly Indexed Arrays

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

Originální název

A Logic of Singly Indexed Arrays

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

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.

Klíčová slova

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

Autoři

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

Rok RIV

2008

Vydáno

3. 12. 2008

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-540-89438-4

Kniha

Logic for Programming, Artificial Intelligence and Reasoning

Edice

Lecture Notes in Computer Science

Strany od

558

Strany do

573

Strany počet

16

BibTex

@inproceedings{BUT34278,
  author="Iosif {Radu} and Tomáš {Vojnar} and Peter {Habermehl}",
  title="A Logic of Singly Indexed Arrays",
  booktitle="Logic for Programming, Artificial Intelligence and Reasoning",
  year="2008",
  series="Lecture Notes in Computer Science",
  volume="5330",
  pages="558--573",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-89438-4"
}