A Logic of Singly Indexed Arrays

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F08%3APU78077" target="_blank" >RIV/00216305:26230/08:PU78077 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
A Logic of Singly Indexed Arrays
Original language description
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 <br>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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA102%2F07%2F0322" target="_blank" >GA102/07/0322: Advanced Formal Approaches in the Design and Verification of Computer-Based Systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2008
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Logic for Programming, Artificial Intelligence and Reasoning
ISBN
978-3-540-89438-4
ISSN
—
e-ISSN
—
Number of pages
16
Pages from-to
—
Publisher name
Springer Verlag
Place of publication
Berlin
Event location
Doha
Event date
Nov 22, 2008
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)