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 the 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. © Springer-Verlag Berlin Heidelberg 2004.
CITATION STYLE
Esparza, J., & Etessami, K. (2004). Verifying probabilistic procedural programs. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3328, 16–31. https://doi.org/10.1007/978-3-540-30538-5_2
Mendeley helps you to discover research relevant for your work.