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

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

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F13%3A00072856%21RIV14-MSM-14330___
rdf:type
n8:Vysledek skos:Concept
dcterms:description
We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We give an algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, as an extension of the PRISM tool. We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We give an algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, as an extension of the PRISM tool.
dcterms:title
Automatic Verification of Competitive Stochastic Systems Automatic Verification of Competitive Stochastic Systems
skos:prefLabel
Automatic Verification of Competitive Stochastic Systems Automatic Verification of Competitive Stochastic Systems
skos:notation
RIV/00216224:14330/13:00072856!RIV14-MSM-14330___
n8:predkladatel
n11:orjk%3A14330
n3:aktivita
n16:I n16:P
n3:aktivity
I, P(LG13010)
n3:cisloPeriodika
1
n3:dodaniDat
n4:2014
n3:domaciTvurceVysledku
n17:2477912
n3:druhVysledku
n20:J
n3:duvernostUdaju
n6:S
n3:entitaPredkladatele
n12:predkladatel
n3:idSjednocenehoVysledku
62626
n3:idVysledku
RIV/00216224:14330/13:00072856
n3:jazykVysledku
n10:eng
n3:klicovaSlova
Quantitative verification; Probabilistic model checking; Stochastic multi-player games; Probabilistic temporal logic
n3:klicoveSlovo
n13:Probabilistic%20model%20checking n13:Stochastic%20multi-player%20games n13:Probabilistic%20temporal%20logic n13:Quantitative%20verification
n3:kodStatuVydavatele
US - Spojené státy americké
n3:kontrolniKodProRIV
[10957ACD49B5]
n3:nazevZdroje
Formal Methods in System Design
n3:obor
n19:IN
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
5
n3:projekt
n14:LG13010
n3:rokUplatneniVysledku
n4:2013
n3:svazekPeriodika
43
n3:tvurceVysledku
Simaitis, Aistis Chen, Taolue Kwiatkowska, Marta Parker, David Forejt, Vojtěch
n3:wos
000321223500003
s:issn
0925-9856
s:numberOfPages
32
n18:doi
10.1007/s10703-013-0183-7
n15:organizacniJednotka
14330