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%3APU78078" target="_blank" >RIV/00216305:26230/08:PU78078 - 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

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.

Czech name

Jednoindexová logika nad poli

Czech description

Jedná se úplnou verzi článku publikovaného na LPAR'08. Článek zavádí specializovanou logiku pro specifikaci vlastností programů pracujících s poli neomezené velikosti obsahující celočíselné údaje o rovněž neomezené velikosti. Tato logika se vyznačuje tím, že umožňuje v jedné, univerzálně kvantifikované formuli porovnávat obsah různých buněk polí pouze s využitím jediného sdíleného indexu. Pro tuto logiku je v článku ukázána obecná nerozhodnutelnost splnitelnosti formulí. Na druhou stranu pro $exists^*forall^*$ fragment této logiky je navržena rozhodovací procedura založená na určitém speciálním typu automatů s čítači. Oproti dřívějším výsledkům v této oblasti je navržená rozhodovací procedura výrazně jednodušší.

Type

A - Audiovisual production

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

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ů

ISBN

—

Place of publication

—

Publisher/client name

—

Version

—

Carrier ID

—