Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twentieth Annual IEEE Symposium on

Logic in Computer Science (LICS 2005)

Paper: Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances (at LICS 2005)

Authors: Javier Esparza Antonín Kučera Richard Mayr

Abstract

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.

BibTeX

  @InProceedings{KueraMayr-QuantitativeAnalysi,
    author = 	 {Javier Esparza and Antonín Kučera and Richard Mayr},
    title = 	 {Quantitative Analysis of Probabilistic Pushdown Automata:  Expectations and Variances},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {117--126},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski