Other formats:
BibTeX
LaTeX
RIS
@inproceedings{572993,
author = {Esparza, Javier and Kučera, Antonín and Mayr, Richard},
address = {Los Alamitos, California},
booktitle = {Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
keywords = {Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis},
language = {eng},
location = {Los Alamitos, California},
isbn = {0-7695-2266-1},
pages = {117-126},
publisher = {IEEE Computer Society},
title = {Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances},
year = {2005}
}
TY - JOUR
ID - 572993
AU - Esparza, Javier - Kučera, Antonín - Mayr, Richard
PY - 2005
TI - Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances
PB - IEEE Computer Society
CY - Los Alamitos, California
SN - 0769522661
KW - Probabilistic Pushdown Automata
KW - Infinite Markov Chains
KW - Quantitative Analysis
N2 - 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.
ER -
ESPARZA, Javier, Antonín KUČERA and Richard MAYR. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. In \textit{Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005)}. Los Alamitos, California: IEEE Computer Society, 2005, p.~117-126. ISBN~0-7695-2266-1.
|
