TY - JOUR
T1 - Verifying probabilistic procedural programs
AU - Esparza, Javier
AU - Etessami, Kousha
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=35048813444&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-30538-5_2
DO - 10.1007/978-3-540-30538-5_2
M3 - Article
AN - SCOPUS:35048813444
SN - 0302-9743
VL - 3328
SP - 16
EP - 31
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -