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

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

Namespace Prefixes

PrefixIRI
n22http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n19http://localhost/temp/predkladatel/
n7http://purl.org/net/nknouf/ns/bibtex#
n23http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n12http://linked.opendata.cz/resource/domain/vavai/projekt/
n6http://linked.opendata.cz/resource/domain/vavai/subjekt/
n5http://linked.opendata.cz/ontology/domain/vavai/
n9https://schema.org/
shttp://schema.org/
n13http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F13%3A00072717%21RIV14-MSM-14330___/
skoshttp://www.w3.org/2004/02/skos/core#
n4http://linked.opendata.cz/ontology/domain/vavai/riv/
n8http://bibframe.org/vocab/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n10http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n21http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n18http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n14http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F13%3A00072717%21RIV14-MSM-14330___
rdf:type
n5:Vysledek skos:Concept
dcterms:description
We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”. We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”.
dcterms:title
Local Model Checking of Weighted CTL with Upper-Bound Constraints Local Model Checking of Weighted CTL with Upper-Bound Constraints
skos:prefLabel
Local Model Checking of Weighted CTL with Upper-Bound Constraints Local Model Checking of Weighted CTL with Upper-Bound Constraints
skos:notation
RIV/00216224:14330/13:00072717!RIV14-MSM-14330___
n5:predkladatel
n6:orjk%3A14330
n4:aktivita
n18:I n18:P
n4:aktivity
I, P(LG13010)
n4:dodaniDat
n14:2014
n4:domaciTvurceVysledku
n23:2753057
n4:druhVysledku
n11:D
n4:duvernostUdaju
n21:S
n4:entitaPredkladatele
n13:predkladatel
n4:idSjednocenehoVysledku
85248
n4:idVysledku
RIV/00216224:14330/13:00072717
n4:jazykVysledku
n16:eng
n4:klicovaSlova
weigted CTL; model checking; Kripke structure; on-the-fly technique
n4:klicoveSlovo
n10:on-the-fly%20technique n10:model%20checking n10:Kripke%20structure n10:weigted%20CTL
n4:kontrolniKodProRIV
[6BEEB2A06A7D]
n4:mistoKonaniAkce
New York, USA
n4:mistoVydani
Netherlands
n4:nazevZdroje
Proceedings of International SPIN Symposium on Model Checking of Software (SPIN'13)
n4:obor
n17:IN
n4:pocetDomacichTvurcuVysledku
1
n4:pocetTvurcuVysledku
4
n4:projekt
n12:LG13010
n4:rokUplatneniVysledku
n14:2013
n4:tvurceVysledku
Larsen, Kim G. Jensen, Jonas F. Oestergaard, Lars K. Srba, Jiří
n4:typAkce
n22:WRD
n4:zahajeniAkce
2013-01-01+01:00
s:issn
0302-9743
s:numberOfPages
18
n8:doi
10.1007/978-3-642-39176-7_12
n7:hasPublisher
Springer-Verlag
n9:isbn
9783642391750
n19:organizacniJednotka
14330