ESPARZA, Javier, Antonín KUČERA a Richard MAYR. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005). Los Alamitos, California: IEEE Computer Society, 2005, s. 117-126. ISBN 0-7695-2266-1.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances
Název česky Kvantitativní analýza pravděpodobnostních zásobníkových automatů: střední hodnoty a rozptyl
Autoři ESPARZA, Javier (724 Španělsko), Antonín KUČERA (203 Česká republika, garant) a Richard MAYR (276 Německo).
Vydání Los Alamitos, California, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), od s. 117-126, 10 s. 2005.
Nakladatel IEEE Computer Society
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/05:00012515
Organizační jednotka Fakulta informatiky
ISBN 0-7695-2266-1
UT WoS 000230786500013
Klíčová slova anglicky Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis
Štítky Infinite Markov Chains, Probabilistic Pushdown Automata, Quantitative Analysis
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 22. 11. 2006 17:28.
Anotace
Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking problem for pPDA and various probabilistic temporal logics. In this paper we concentrate on computing the expected values and variances of various random variables defined over runs of a given probabilistic pushdown automaton. In particular, we show how to compute the expected accumulated reward and the expected gain for certain classes of reward functions. Using these results, we show how to analyze various quantitative properties of pPDA that are not expressible in conventional probabilistic temporal logics.
Anotace česky
Pravděpodobnostní zásobníkové automaty jsou přirozeným modelem pro pravděpodobnostní programy obsahující rekurzivní procedury. V článku se soustředíme na výpočet středních hodnot a rozptylu jistých náhodných proměnných definovaných na bězích daného zásbníkového automatu. Pomocí těchto výsledků lze dále vypočítat různé kvantitativní charakteristiky pravděpodobnostních zásobníkových automatů, které nelze vyjádřit v běžných temporálních logikách.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 13. 5. 2024 19:10