All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

A Logic of Singly Indexed Arrays

The result's identifiers

  • 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

Alternative languages

  • 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&nbsp; comparisons between array elements situated within a constant sized window. We show that the satisfiability problem for the logic is undecidable for formulae&nbsp; with a quantifier prefix ${exists,forall}^*forall^*exists^*forall^*$. For formulae&nbsp; with quantifier prefixes in the $exists^*forall^*$ fragment, decidability is established&nbsp; by an automata-theoretic argument. For each formula in the $exists^*forall^*$ fragment, we&nbsp; 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&nbsp; the formula. Decidability of the $exists^*forall^*$ fragment of the logic is a consequence&nbsp; of the fact that reachability of a control state is decidable for FCADBM.

  • Czech name

  • Czech description

Classification

  • Type

    D - Article in proceedings

  • CEP classification

    JC - Computer hardware and software

  • OECD FORD branch

Result continuities

  • 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)

Others

  • Publication year

    2008

  • Confidentiality

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

Data specific for result type

  • 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