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/
n10http://localhost/temp/predkladatel/
n6http://purl.org/net/nknouf/ns/bibtex#
n15http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F08%3A00026224%21RIV10-MSM-14330___/
n21http://linked.opendata.cz/resource/domain/vavai/projekt/
n7http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n9http://linked.opendata.cz/ontology/domain/vavai/
n16http://linked.opendata.cz/resource/domain/vavai/zamer/
n13https://schema.org/
shttp://schema.org/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/
skoshttp://www.w3.org/2004/02/skos/core#
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/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n18http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n11http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F08%3A00026224%21RIV10-MSM-14330___
rdf:type
n9:Vysledek skos:Concept
dcterms:description
We study the satisfiability problem for qualitative PCTL (Probabilistic Computation Tree Logic), which is obtained from %22ordinary%22 CTL by replacing the EX, AX, EU, and AU operators with their qualitative counterparts X>0, X=1, U>0, and U=1, respectively. As opposed to CTL, qualitative PCTL does not have a small model property, and there are even qualitative PCTL formulae which have only infinite-state models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is EXPTIME-complete and we give an exponential-time algorithm which for a given formula computes a finite description of a model (if it exists), or answers %22not satisfiable%22 (otherwise). We also consider the finite satisfiability problem and provide analogous results. That is, we show that the finite satisfiability problem for qualitative PCTL is EXPTIME-complete, and every finite satisfiable formula has a model of an exponential size which can effectively be constructed in exponential time. We study the satisfiability problem for qualitative PCTL (Probabilistic Computation Tree Logic), which is obtained from %22ordinary%22 CTL by replacing the EX, AX, EU, and AU operators with their qualitative counterparts X>0, X=1, U>0, and U=1, respectively. As opposed to CTL, qualitative PCTL does not have a small model property, and there are even qualitative PCTL formulae which have only infinite-state models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is EXPTIME-complete and we give an exponential-time algorithm which for a given formula computes a finite description of a model (if it exists), or answers %22not satisfiable%22 (otherwise). We also consider the finite satisfiability problem and provide analogous results. That is, we show that the finite satisfiability problem for qualitative PCTL is EXPTIME-complete, and every finite satisfiable formula has a model of an exponential size which can effectively be constructed in exponential time.
dcterms:title
The Satisfiability Problem for Probabilistic CTL The Satisfiability Problem for Probabilistic CTL
skos:prefLabel
The Satisfiability Problem for Probabilistic CTL The Satisfiability Problem for Probabilistic CTL
skos:notation
RIV/00216224:14330/08:00026224!RIV10-MSM-14330___
n4:aktivita
n12:Z n12:P
n4:aktivity
P(1M0545), Z(MSM0021622419)
n4:dodaniDat
n11:2010
n4:domaciTvurceVysledku
n7:2477912 n7:3503054 n7:1762834 n7:9872655
n4:druhVysledku
n17:D
n4:duvernostUdaju
n5:S
n4:entitaPredkladatele
n15:predkladatel
n4:idSjednocenehoVysledku
393788
n4:idVysledku
RIV/00216224:14330/08:00026224
n4:jazykVysledku
n18:eng
n4:klicovaSlova
Stochastic systems; branching-time temporal logics
n4:klicoveSlovo
n19:branching-time%20temporal%20logics n19:Stochastic%20systems
n4:kontrolniKodProRIV
[C11FB54C4747]
n4:mistoKonaniAkce
Pittsburgh, USA
n4:mistoVydani
Los Alamitos, California
n4:nazevZdroje
23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings
n4:obor
n14:IN
n4:pocetDomacichTvurcuVysledku
4
n4:pocetTvurcuVysledku
4
n4:projekt
n21:1M0545
n4:rokUplatneniVysledku
n11:2008
n4:tvurceVysledku
Křetínský, Jan Forejt, Vojtěch Kučera, Antonín Brázdil, Tomáš
n4:typAkce
n22:WRD
n4:wos
000258728700033
n4:zahajeniAkce
2008-06-24+02:00
n4:zamer
n16:MSM0021622419
s:numberOfPages
10
n6:hasPublisher
IEEE Computer Society
n13:isbn
978-0-7695-3183-0
n10:organizacniJednotka
14330