Faculty of Information Technology, BUT

Publication Details

A Logic of Singly Indexed Arrays

HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. In: Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, vol. 5330. Berlin: Springer Verlag, 2008, pp. 558-573. ISBN 978-3-540-89438-4.
Czech title
Jednoindexová logika nad poli
Type
conference paper
Language
english
Authors
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords
mathematical logic, arrays, decidability, decision procedure, formal verification, automata
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.
Published
2008
Pages
558-573
Proceedings
Logic for Programming, Artificial Intelligence and Reasoning
Series
Lecture Notes in Computer Science
Volume
5330
Conference
15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning -- LPAR'08, Doha, QA
ISBN
978-3-540-89438-4
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB8816,
   author = "Peter Habermehl and Radu Iosif and Tom\'{a}\v{s} Vojnar",
   title = "A Logic of Singly Indexed Arrays",
   pages = "558--573",
   booktitle = "Logic for Programming, Artificial Intelligence and Reasoning",
   series = "Lecture Notes in Computer Science",
   volume = 5330,
   year = 2008,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-89438-4",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8816"
}
Back to top