What else is decidable about integer arrays?

Kód výsledku v IS VaVaI

RIV/00216305:26230/08:PU76681 - isvavai.cz

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

What else is decidable about integer arrays?

Popis výsledku v původním jazyce

We introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the $exists^* forall^*$ first-order fragment and allows (1) Presburger constraints on existentially quantified variables, (2) difference constraints aswell as periodicity constraints on universally quantified indices, and (3) difference constraints on values. In particular, using our logic, one can express constraints on consecutive elements of arrays (e.g., $forall i ~.~ 0 leq i < n rightarrow a[i+1]=a[i]-1$) as well as periodic facts (e.g., $forall i ~.~ i equiv_2 0 rightarrow a[i] = 0$). The decision procedure follows the automata-theoretic approach: we translate formulae into a special class of B"uchi counter automata such that anymodel of a formula corresponds to an accepting run of an automaton, and vice versa. The emptiness problem for this class of counter automata is shown to be
decidable as a consequence of earlier results on counter automata with a flat c

Název v anglickém jazyce

What else is decidable about integer arrays?

Popis výsledku anglicky

We introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the $exists^* forall^*$ first-order fragment and allows (1) Presburger constraints on existentially quantified variables, (2) difference constraints aswell as periodicity constraints on universally quantified indices, and (3) difference constraints on values. In particular, using our logic, one can express constraints on consecutive elements of arrays (e.g., $forall i ~.~ 0 leq i < n rightarrow a[i+1]=a[i]-1$) as well as periodic facts (e.g., $forall i ~.~ i equiv_2 0 rightarrow a[i] = 0$). The decision procedure follows the automata-theoretic approach: we translate formulae into a special class of B"uchi counter automata such that anymodel of a formula corresponds to an accepting run of an automaton, and vice versa. The emptiness problem for this class of counter automata is shown to be
decidable as a consequence of earlier results on counter automata with a flat c

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

GA102/07/0322: Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů

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ů

Název statě ve sborníku

Foundations of Software Science and Computation Structures

ISBN

978-3-540-78497-5

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

—

Název nakladatele

Springer Verlag

Místo vydání

Berlin

Místo konání akce

Budapešť

Datum konání akce

29. 3. 2008

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—