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

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

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n19http://localhost/temp/predkladatel/
n16http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n8http://linked.opendata.cz/resource/domain/vavai/projekt/
n14http://linked.opendata.cz/resource/domain/vavai/subjekt/
n12http://linked.opendata.cz/ontology/domain/vavai/
n20http://linked.opendata.cz/resource/domain/vavai/zamer/
n11http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F12%3APU98200%21RIV13-GA0-26230___/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
rdfshttp://www.w3.org/2000/01/rdf-schema#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n17http://bibframe.org/vocab/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n5http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n18http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n22http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n21http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n10http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F12%3APU98200%21RIV13-GA0-26230___
rdf:type
n12:Vysledek skos:Concept
rdfs:seeAlso
http://www.springerlink.com/content/137uu7118p2054j2/
dcterms:description
Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations in regular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verification o Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations in regular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verification o
dcterms:title
Abstract Regular (Tree) Model Checking Abstract Regular (Tree) Model Checking
skos:prefLabel
Abstract Regular (Tree) Model Checking Abstract Regular (Tree) Model Checking
skos:notation
RIV/00216305:26230/12:PU98200!RIV13-GA0-26230___
n12:predkladatel
n14:orjk%3A26230
n3:aktivita
n4:P n4:Z n4:S
n3:aktivity
P(GAP103/10/0306), P(GP201/09/P531), P(MEB021023), P(OC10009), S, Z(MSM0021630528)
n3:cisloPeriodika
2
n3:dodaniDat
n10:2013
n3:domaciTvurceVysledku
n16:9761985 n16:4978536
n3:druhVysledku
n21:J
n3:duvernostUdaju
n13:S
n3:entitaPredkladatele
n11:predkladatel
n3:idSjednocenehoVysledku
120805
n3:idVysledku
RIV/00216305:26230/12:PU98200
n3:jazykVysledku
n18:eng
n3:klicovaSlova
Formal verification, Infinite-state and parameterised systems, Programs with dynamic linked data structures, Regular model checking, Abstraction, Finite word and tree automata
n3:klicoveSlovo
n5:Programs%20with%20dynamic%20linked%20data%20structures n5:Regular%20model%20checking n5:Finite%20word%20and%20tree%20automata n5:Infinite-state%20and%20parameterised%20systems n5:Formal%20verification n5:Abstraction
n3:kodStatuVydavatele
DE - Spolková republika Německo
n3:kontrolniKodProRIV
[4475F77B56FE]
n3:nazevZdroje
International Journal on Software Tools for Technology Transfer
n3:obor
n22:IN
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
4
n3:projekt
n8:MEB021023 n8:OC10009 n8:GP201%2F09%2FP531 n8:GAP103%2F10%2F0306
n3:rokUplatneniVysledku
n10:2012
n3:svazekPeriodika
14
n3:tvurceVysledku
Habermehl, Peter Vojnar, Tomáš Bouajjani, Ahmed Rogalewicz, Adam
n3:zamer
n20:MSM0021630528
s:issn
1433-2779
s:numberOfPages
25
n17:doi
10.1007/s10009-011-0205-y
n19:organizacniJednotka
26230