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
n5http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n22http://localhost/temp/predkladatel/
n21http://purl.org/net/nknouf/ns/bibtex#
n14http://linked.opendata.cz/resource/domain/vavai/projekt/
n7http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n20http://linked.opendata.cz/ontology/domain/vavai/
n15http://linked.opendata.cz/resource/domain/vavai/zamer/
n10https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n19http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n11http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F08%3A00024825%21RIV10-GA0-14330___/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n18http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n17http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F08%3A00024825%21RIV10-GA0-14330___
rdf:type
skos:Concept n20:Vysledek
dcterms:description
We show that the controller synthesis and verification problems for Markov decision processes with qualitative PECTL* objectives are 2-EXPTIME complete. More precisely, the algorithms are polynomial in the size of a given Markov decision process and doubly exponential in the size of a given qualitative PECTL* formula. Moreover, we show that if a given qualitative PECTL* objective is achievable by some strategy, then it is also achievable by an effectively constructible one-counter strategy, where the associated complexity bounds are essentially the same as above. For the fragment of qualitative PCTL objectives, we obtain EXPTIME completeness and the algorithms are only singly exponential in the size of the formula. We show that the controller synthesis and verification problems for Markov decision processes with qualitative PECTL* objectives are 2-EXPTIME complete. More precisely, the algorithms are polynomial in the size of a given Markov decision process and doubly exponential in the size of a given qualitative PECTL* formula. Moreover, we show that if a given qualitative PECTL* objective is achievable by some strategy, then it is also achievable by an effectively constructible one-counter strategy, where the associated complexity bounds are essentially the same as above. For the fragment of qualitative PCTL objectives, we obtain EXPTIME completeness and the algorithms are only singly exponential in the size of the formula.
dcterms:title
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
skos:prefLabel
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
skos:notation
RIV/00216224:14330/08:00024825!RIV10-GA0-14330___
n3:aktivita
n12:P n12:Z
n3:aktivity
P(1M0545), P(GD102/05/H050), Z(MSM0021622419)
n3:dodaniDat
n17:2010
n3:domaciTvurceVysledku
n7:2477912 n7:9872655 n7:1762834
n3:druhVysledku
n4:D
n3:duvernostUdaju
n16:S
n3:entitaPredkladatele
n11:predkladatel
n3:idSjednocenehoVysledku
361276
n3:idVysledku
RIV/00216224:14330/08:00024825
n3:jazykVysledku
n6:eng
n3:klicovaSlova
Markov decision processes; Probabilistic Temporal Logics
n3:klicoveSlovo
n19:Probabilistic%20Temporal%20Logics n19:Markov%20decision%20processes
n3:kontrolniKodProRIV
[15D0F2DC0BCD]
n3:mistoKonaniAkce
Reykjavik, Iceland
n3:mistoVydani
Berlin, Heidelberg, New York
n3:nazevZdroje
Automata, Languages and Programming. 35th International Colloquium, ICALP 2008. Reykjavik, Iceland, July 2008. Proceedings, Part II.
n3:obor
n18:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:projekt
n14:GD102%2F05%2FH050 n14:1M0545
n3:rokUplatneniVysledku
n17:2008
n3:tvurceVysledku
Brázdil, Tomáš Kučera, Antonín Forejt, Vojtěch
n3:typAkce
n5:WRD
n3:wos
00025766310
n3:zahajeniAkce
2008-07-07+02:00
n3:zamer
n15:MSM0021622419
s:numberOfPages
12
n21:hasPublisher
Springer-Verlag
n10:isbn
3-540-70582-1
n22:organizacniJednotka
14330