Quantitative analysis of probabilistic pushdown automata: Expectations and variances - (Extended abstract)

被引：0

作者：

Esparza, J ^{[1
]}

Kucera, A ^{[1
]}

Mayr, R ^{[1
]}

机构：

[1] Univ Stuttgart, Inst Formal Methods Comp Sci, D-70569 Stuttgart, Germany

来源：

LICS 2005: 20TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE - PROCEEDINGS | 2005年

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：117 / 126

页数：10

共 15 条

[1] Alur R, 2004, LECT NOTES COMPUT SC, V2988, P467
[2] Alur R, 2001, LECT NOTES COMPUT SC, V2102, P207
[3] Alur R., 2004, STOC, P202, DOI [10.1145/1007352.1007390, DOI 10.1145/1007352.1007390]
[4] Benedikt M, 2001, LECT NOTES COMPUT SC, V2076, P652
[5] Bouajjani A, 1997, LECT NOTES COMPUT SC, V1243, P135
[6] Brázdil T, 2005, LECT NOTES COMPUT SC, V3404, P145
[7] Canny J., 1988, Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, P460, DOI 10.1145/62212.62257
[8] CHAUDHURI S, 2005, LNCS, V3440
[9] de Alfaro L, 1998, THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, P454
[10] Model checking probabilistic pushdown automata
Esparza, J
Kucera, A
Mayr, R
[J]. 19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 12 - 21

← 1 2 →