. "Ov\u011B\u0159ov\u00E1n\u00ED platnosti formul\u00ED tempor\u00E1ln\u00EDch logik pro procesy z\u00E1sobn\u00EDkov\u00FDch automat\u016F"@cs . "[0DBBB39EEB48]" . . "12-21" . . "0-7695-2192-4" . "Probabilistic Pushdown Automata; Model Checking"@en . "1"^^ . "2004-07-13+02:00"^^ . "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." . . . "Model Checking Probabilistic Pushdown Automata" . "Model Checking Probabilistic Pushdown Automata"@en . "IEEE Computer Society" . "573885" . "3"^^ . "10"^^ . "Model Checking Probabilistic Pushdown Automata" . "Los Alamitos (California)" . "Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004)" . "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."@en . . . . . . "Mayr, Richard" . "Esparza, Javier" . "RIV/00216224:14330/04:00010191!RIV08-MSM-14330___" . . . . . . "Model Checking Probabilistic Pushdown Automata"@en . "Ku\u010Dera, Anton\u00EDn" . "P(GA201/03/1161), Z(MSM 143300001)" . . . "V pr\u00E1ci je rozebr\u00E1na problematika automatick\u00E9ho ov\u011B\u0159ov\u00E1n\u00ED platnosti formul\u00ED tempor\u00E1ln\u00EDch logik pro procesy pravd\u011Bpodobnostn\u00EDch z\u00E1sobn\u00EDkov\u00FDch automat\u016F. Nejprve je uva\u017Eov\u00E1na t\u0159\u00EDda vlastnost\u00ED, kter\u00E1 je formulovateln\u00E1 jako zobecn\u011Bn\u00FD probl\u00E9m n\u00E1hodn\u00E9 proch\u00E1zky. Je dok\u00E1z\u00E1no, \u017Ee kvalitativn\u00ED i kvantitativn\u00ED varianta tohoto probl\u00E9mu je rozhodnuteln\u00E1. Pak je dok\u00E1z\u00E1na rozhodnutelnost probl\u00E9mu platnosti dan\u00E9 formule kvalitativn\u00EDho fragmentu logiky PCTL pro dan\u00FD z\u00E1sobn\u00EDkov\u00FD proces. Jsou tak\u00E9 uva\u017Eov\u00E1ny vlastnosti popsateln\u00E9 pomoc\u00ED deterministick\u00FDch Buchiho automat\u016F a uk\u00E1z\u00E1na rozhodnutelnost p\u0159\u00EDslu\u0161n\u00FDch probl\u00E9m\u016F."@cs . "14330" . "RIV/00216224:14330/04:00010191" . "Turku, Finland" . "Ov\u011B\u0159ov\u00E1n\u00ED platnosti formul\u00ED tempor\u00E1ln\u00EDch logik pro procesy z\u00E1sobn\u00EDkov\u00FDch automat\u016F"@cs .