This HTML5 document contains 46 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
n17	http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dcterms	http://purl.org/dc/terms/
n22	http://localhost/temp/predkladatel/
n21	http://purl.org/net/nknouf/ns/bibtex#
n13	http://linked.opendata.cz/resource/domain/vavai/projekt/
n12	http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n19	http://linked.opendata.cz/ontology/domain/vavai/
n15	https://schema.org/
n8	http://linked.opendata.cz/resource/domain/vavai/zamer/
s	http://schema.org/
skos	http://www.w3.org/2004/02/skos/core#
n3	http://linked.opendata.cz/ontology/domain/vavai/riv/
n2	http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
n6	http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n7	http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdh	http://www.w3.org/2001/XMLSchema#
n14	http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n11	http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n10	http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n16	http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n4	http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F08%3APU76681%21RIV10-MSM-26230___/
n18	http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item

n2:RIV%2F00216305%3A26230%2F08%3APU76681%21RIV10-MSM-26230___

rdf:type

skos:Concept n19:Vysledek

dcterms:description

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 as well 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 &lt; 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\&quot;uchi counter automata such that any model 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<br>decidable as a consequence of earlier results on counter automata with a flat control structure 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 as well 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 &lt; 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\&quot;uchi counter automata such that any model 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<br>decidable as a consequence of earlier results on counter automata with a flat control structure

dcterms:title

What else is decidable about integer arrays? What else is decidable about integer arrays?

skos:prefLabel

What else is decidable about integer arrays? What else is decidable about integer arrays?

skos:notation

RIV/00216305:26230/08:PU76681!RIV10-MSM-26230___

n3:aktivita

n11:Z n11:P

n3:aktivity

P(GA102/07/0322), Z(MSM0021630528)

n3:dodaniDat

n18:2010

n3:domaciTvurceVysledku

n12:9761985

n3:druhVysledku

n16:D

n3:duvernostUdaju

n7:S

n3:entitaPredkladatele

n4:predkladatel

n3:idSjednocenehoVysledku

405691

n3:idVysledku

RIV/00216305:26230/08:PU76681

n3:jazykVysledku

n14:eng

n3:klicovaSlova

mathematical logic, arrays, decidability, decision procedure, formal verification, automata<br>

n3:klicoveSlovo

n6:automata%3Cbr%3E n6:formal%20verification n6:arrays n6:mathematical%20logic n6:decidability n6:decision%20procedure

n3:kontrolniKodProRIV

[BB16B5692C95]

n3:mistoKonaniAkce

Budapešť

n3:mistoVydani

Berlin

n3:nazevZdroje

Foundations of Software Science and Computation Structures

n3:obor

n10:JC

n3:pocetDomacichTvurcuVysledku

1

n3:pocetTvurcuVysledku

3

n3:projekt

n13:GA102%2F07%2F0322

n3:rokUplatneniVysledku

n18:2008

n3:tvurceVysledku

Vojnar, Tomáš Radu, Iosif Habermehl, Peter

n3:typAkce

n17:WRD

n3:zahajeniAkce

2008-03-29+01:00

n3:zamer

n8:MSM0021630528

s:numberOfPages

16

n21:hasPublisher

Springer-Verlag

n15:isbn

978-3-540-78497-5

n22:organizacniJednotka

26230