Abstract / Description of output
Monolithic finite-state probabilistic programs have been abstractly modeled by finite Markov chains, and the algorithmic verification problems for them have been investigated very extensively. In this paper we survey recent work conducted by the authors together with colleagues on he algorithmic verification of probabilistic procedural programs ([BKS,EKM04,EY04]). Probabilistic procedural programs can more naturally be modeled by recursive Markov chains ([EY04)], or equivalently, probabilistic pushdown automata ([EKM04)]. A very rich theory emerges for these models. While our recent work solves a number of verification problems for these models, many intriguing questions remain open.
| Original language | English |
|---|---|
| Title of host publication | FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, |
| Subtitle of host publication | 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings |
| Publisher | Springer |
| Pages | 16-31 |
| Number of pages | 16 |
| Volume | 3328 |
| ISBN (Electronic) | 978-3-540-30538-5 |
| ISBN (Print) | 978-3-540-24058-7 |
| DOIs | |
| Publication status | Published - 2004 |