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
n21http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n22http://localhost/temp/predkladatel/
n11http://purl.org/net/nknouf/ns/bibtex#
n18http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n13http://linked.opendata.cz/resource/domain/vavai/projekt/
n19http://linked.opendata.cz/ontology/domain/vavai/
n14http://linked.opendata.cz/resource/domain/vavai/zamer/
n8https://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#
n4http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F04%3A00010191%21RIV08-MSM-14330___/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n10http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n16http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F04%3A00010191%21RIV08-MSM-14330___
rdf:type
skos:Concept n19:Vysledek
dcterms:description
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable. We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable. V práci je rozebrána problematika automatického ověřování platnosti formulí temporálních logik pro procesy pravděpodobnostních zásobníkových automatů. Nejprve je uvažována třída vlastností, která je formulovatelná jako zobecněný problém náhodné procházky. Je dokázáno, že kvalitativní i kvantitativní varianta tohoto problému je rozhodnutelná. Pak je dokázána rozhodnutelnost problému platnosti dané formule kvalitativního fragmentu logiky PCTL pro daný zásobníkový proces. Jsou také uvažovány vlastnosti popsatelné pomocí deterministických Buchiho automatů a ukázána rozhodnutelnost příslušných problémů.
dcterms:title
Ověřování platnosti formulí temporálních logik pro procesy zásobníkových automatů Model Checking Probabilistic Pushdown Automata Model Checking Probabilistic Pushdown Automata
skos:prefLabel
Model Checking Probabilistic Pushdown Automata Model Checking Probabilistic Pushdown Automata Ověřování platnosti formulí temporálních logik pro procesy zásobníkových automatů
skos:notation
RIV/00216224:14330/04:00010191!RIV08-MSM-14330___
n3:strany
12-21
n3:aktivita
n10:P n10:Z
n3:aktivity
P(GA201/03/1161), Z(MSM 143300001)
n3:dodaniDat
n16:2008
n3:domaciTvurceVysledku
n18:9872655
n3:druhVysledku
n20:D
n3:duvernostUdaju
n15:S
n3:entitaPredkladatele
n4:predkladatel
n3:idSjednocenehoVysledku
573885
n3:idVysledku
RIV/00216224:14330/04:00010191
n3:jazykVysledku
n6:eng
n3:klicovaSlova
Probabilistic Pushdown Automata; Model Checking
n3:klicoveSlovo
n7:Model%20Checking n7:Probabilistic%20Pushdown%20Automata
n3:kontrolniKodProRIV
[0DBBB39EEB48]
n3:mistoKonaniAkce
Turku, Finland
n3:mistoVydani
Los Alamitos (California)
n3:nazevZdroje
Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004)
n3:obor
n17:IN
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
3
n3:projekt
n13:GA201%2F03%2F1161
n3:rokUplatneniVysledku
n16:2004
n3:tvurceVysledku
Mayr, Richard Esparza, Javier Kučera, Antonín
n3:typAkce
n21:WRD
n3:zahajeniAkce
2004-07-13+02:00
n3:zamer
n14:MSM%20143300001
s:numberOfPages
10
n11:hasPublisher
IEEE Computer Society
n8:isbn
0-7695-2192-4
n22:organizacniJednotka
14330