Jednoindexová logika nad poli

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F08%3APU78078" target="_blank" >RIV/00216305:26230/08:PU78078 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

A Logic of Singly Indexed Arrays

Popis výsledku v původním jazyce

This report is the full version of an LPAR'08 paper, in which 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.

Název v anglickém jazyce

A Logic of Singly Indexed Arrays

Popis výsledku anglicky

This report is the full version of an LPAR'08 paper, in which 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.

Druh

A - Audiovizuální tvorba

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GA102%2F07%2F0322" target="_blank" >GA102/07/0322: Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2008

Kód důvěrnosti údajů

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

ISBN

—

Místo vydání

—

Název nakladatele resp. objednatele

—

Verze

—

Identifikační číslo nosiče

—