Verifying Probabilistic Procedural Programs

Javier Esparza, Kousha Etessami

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationFSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science,
Subtitle of host publication24th International Conference, Chennai, India, December 16-18, 2004, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-30538-5
ISBN (Print) 978-3-540-24058-7
Publication statusPublished - 2004


Dive into the research topics of 'Verifying Probabilistic Procedural Programs'. Together they form a unique fingerprint.

Cite this